你如何在Isabelle/HOL中使用诱导与战术/ Isar？

Question

我在努力理解为什么下面的每个例子都有效或者不起作用，并且更加抽象地说明诱导如何与战术和Isar进行交互。我在编程工作4.3与最新的伊莎贝尔/ HOL在Windows 10中伊莎贝尔/ HOL（2016年12月）证明（2016-1）

有8例：引理或者是长（包括明确的名称）或简短结构化（使用assumes和shows）或未结构化（使用箭头），并且证明是结构化的（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并得到拉里·保尔森以下响应。我已经在下面转载了它。

---

感谢您的查询。您的一些问题与正确的方式提供前提导入相关，但这里至少有两个大问题。

(* 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米）”是导致感应方法来循环用于由于某些原因，在你的（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 

也就是说，你可以提供的假设来证明如图所示（“使用”）。我们甚至得到正确的情况下，做这种方式。

我们正处在一个新的释放阶段，但我希望涉及感应方法和非原子方面的问题可以及时解决。

Larry Paulson