Isabelle/Isarに複数の変数を使って存在命題を効率的に証明するにはどうすればよいですか？

Question

Isabelle/Isarに補題∃ n m k . [n, m, k] = [2, 3, 5]を証明したいとします。 45ページのイザベル/ HOLチュートリアルで提案されているように、私は先に行く場合は、次のように、私の証明はなります

もちろん

lemma "∃ n m k . [n, m, k] = [2, 3, 5]" 
proof 
    show "∃ m k . [2, m, k] = [2, 3, 5]" 
    proof 
    show "∃ k . [2, 3, k] = [2, 3, 5]" 
    proof 
     show "[2, 3, 5] = [2, 3, 5]" by simp 
    qed 
    qed 
qed 

、これはあまりにも冗長です。どのように私は証明書が簡潔で読みやすいように上記のような命題を証明することができますか？

Answer 1

複数の存在量限定子は、単一量子導入ルールを複数回適用することによって、単一ステップで導入することができます。たとえば、証明方法(rule exI)+は、最も外側に存在するすべての量限定子を導入します。

lemma "∃n m k. [n, m, k] = [2, 3, 5]" 
proof(rule exI)+ 
    show "[2, 3, 5] = [2, 3, 5]" by simp 
qed 

また、あなたが最初にインスタンスプロパティを述べ、その後、インスタンス化を行うために自動証明方法を使用することができます。通常blastはここではうまくいきます。あなたの例では、数値がオーバーロードされているため、型名を追加する必要があります。

lemma "∃n m k :: nat. [n, m, k] = [2, 3, 5]" 
proof - 
    have "[2, 3, 5 :: nat] = [2, 3, 5]" by simp 
    then show ?thesis by blast 
qed