Isabelle/HOLではどのように誘導をIsar/Isarと併用しますか？

Question

以下の例のそれぞれがうまく動作しないのか、より抽象的な誘導が戦術対Isarと相互作用するのかを理解するのは苦労しています。私は最新のIsabelle/HOL（2016-1）で最新のIsabelle/HOL（2016年12月）のプログラミングと検証で4.3に取り組んでいます。

8つのケースがあります：補題は長い（矢印を使用）、証明は構造化（Isar）または非構造化（戦術的）のいずれかです。

theory Confusing_Induction 
    imports Main 
begin 

(* 4.3 *) 
inductive ev :: " nat ⇒ bool " where 
    ev0: " ev 0 " | 
    evSS: " ev n ⟹ ev (n + 2) " 

fun evn :: " nat ⇒ bool " where 
    " evn 0 = True " | 
    " evn (Suc 0) = False " | 
    " evn (Suc (Suc n)) = evn n " 

1.構造ショート補題&構造化された証明

(* Hangs/gets stuck/loops on the following *) 
(* 
lemma assumes a: " ev (Suc(Suc m)) " shows" ev m " 
proof(induction "Suc (Suc m)" arbitrary: " m " rule: ev.induct) 
*) 

2.構造化されていない短い補題&構造化された証明

(* And this one ends up having issues with 
    "Illegal application of proof command in state mode" *) 
(* 
lemma " ev (Suc (Suc m)) ⟹ ev m " 
proof(induction " Suc (Suc m) " arbitrary: " m " rule: ev.induct) 
    case ev0 
    then show ?case sorry 
next 
    case (evSS n) 
    then show ?case sorry 
qed 
*) 

3.構造化された長い補題&構造化された証明

(* And neither of these can apply the induction *) 
(* 
lemma assumes a1: " ev n " and a2: " n = (Suc (Suc m)) " shows " ev m " 
proof (induction " n " arbitrary: " m " rule: ev.induct) 

lemma assumes a1: " n = (Suc (Suc m)) " and a2: "ev n " shows " ev m " 
proof (induction " n " arbitrary: " m " rule: ev.induct) 
*) 

(* But this one can ?! *) 
(* 
lemma assumes a1: " ev n " and a2: " n = (Suc (Suc m)) " shows " ev m " 
proof - 
    from a1 and a2 show " ev m " 
    proof (induction " n " arbitrary: " m " rule: ev.induct) 
    case ev0 
    then show ?case by simp 
    next 
    case (evSS n) thus ?case by simp 
    qed 
qed 
*) 

4.構造化されていない長い補題&構造化された証明

(* And this is the manually expanded form of the Advanced Rule Induciton from 4.4.6 *) 
lemma tmp: " ev n ⟹ n = (Suc (Suc m)) ⟹ ev m " 
proof (induction " n " arbitrary: " m " rule: ev.induct) 
    case ev0 thus ?case by simp 
next 
    case (evSS n) thus ?case by simp 
qed 

lemma " ev (Suc (Suc m)) ⟹ ev m " 
    using tmp by blast 

** 5。構造化された短い補題&構造化されていない証明*

(* Also gets stuck/hangs *) 
(* 
lemma assumes a: " ev (Suc (Suc m)) " shows " ev m " 
    apply(induction "Suc (Suc m)" arbitrary: " m " rule: ev.induct) 
*) 

6.構造化されていない短い補題&構造化されていない証明

(* This goes through no problem (``arbitrary: " m "`` seems to be optional, why?) *) 
lemma " ev (Suc(Suc m)) ⟹ ev m " 
    apply(induction "Suc (Suc m)" arbitrary: " m " rule: ev.induct) 
    apply(auto) 
    done 

7ストラクチャード長い補題&構造化されていない証明

(* But both of these "fail to apply the proof method" *) 
(* 
lemma assumes a1: " n = (Suc (Suc m)) " and a2: " ev n" shows " ev m " 
    apply(induction " n " arbitrary: " m " rule: ev.induct) 

lemma assumes a1: " ev n " and a2: " n = (Suc (Suc m)) " shows " ev m " 
    apply(induction " n " arbitrary: " m " rule: ev.induct) 
*) 

8.構造化されていない長い補題&構造化されていない証明

lemma " ev n ⟹ n = (Suc (Suc m)) ⟹ ev m " 
    apply(induction " n " arbitrary: " m " rule: ev.induct) 
    apply(auto) 
    done 

end 

Answer 1

私はcl-isabelle-users@lists.cam.ac.ukに投稿し、ラリー・ポールソンから次の応答を受信しました。私はそれを下に再現しました。

---

ご質問ありがとうございます。あなたの問題のいくつかは、適切な方法で施設に誘導を供給することと関係していますが、ここには少なくとも2つの大きな問題があります。

(* 1. Structured short lemma & structured proof *) 
(* Hangs/gets stuck/loops on the following *) 

lemma assumes a: "ev (Suc(Suc m))” shows "ev m" 
proof(induction "Suc (Suc m)" rule: ev.induct) 

このようにすると、あなたの前提は見えません。目標は単に「ev m」なので、誘導は適用されません。しかしこのミスによって誘導方法がループすることは絶対に悪いことです。ここで

(* 2. Unstructured short lemma & structured proof *) 
(* And this one ends up having issues with 
    "Illegal application of proof command in state mode" *) 
lemma "ev (Suc (Suc m)) ⟹ ev m" 
proof(induction "Suc (Suc m)" rule: ev.induct) 
    case ev0 
    then show ?case 
    sorry 
next 
    case (evSS n) 
    then show ?case sorry 
qed 

あなたが証拠の残りの部分を壊し、「保留中の目標を絞り込むことができませんでした」というエラーを取得している。あなたは、このエラーメッセージを取得している理由は、何らかの理由で目標との間に不整合があるということですあなたは、誘導方法は、実際には、この証明は素直に書き込むことができます。あなたが持っていると思いますが、その形状はかなり予想外であること。これも非常に悪いです目標は持っている。

lemma "ev (Suc (Suc m)) ⟹ ev m" 
proof(induction "Suc (Suc m)" rule: ev.induct) 
    show "⋀n. ev n ⟹ 
     (n = Suc (Suc m) ⟹ ev m) ⟹ 
     n + 2 = Suc (Suc m) ⟹ ev m" 
    by simp 
qed 

あなたの（3,7,8）明らかに誘導方法が失敗する点を除いて、あなたの（1）と同じ問題です。引数 "Suc（Suc m）"が誘導方法をループさせているのは明らかです何らかの理由で、あなたの（5）のように。

(* 6. Unstructured short lemma & unstructured proof *) 
(* This goes through no problem (``arbitrary: " m "`` seems to be optional, why?) *) 

帰納仮説に一般化される必要のある変数が含まれている場合は、「恣意的な」校正が必要な場合があります。

はあなたの（7）のように書くことができます：（「使用」）に示すようである

lemma assumes "ev n" and " n = (Suc (Suc m)) " shows " ev m " 
    using assms 
proof(induction " n " arbitrary: " m " rule: ev.induct) 
    case ev0 
    then show ?case 
    sorry 
next 
    case (evSS n) 
    then show ?case 
    sorry 
qed 

は、あなたが証拠に仮定を供給することができます。私たちはこのようにして正しいケースを得ることさえできます。

私たちは新しいリリース段階に入っていますが、誘導方法と非原子項に関する問題を直ちに解決できることを願っています。

ラリーポールソン