2

嗨，我是一个新手，试图学习如何在伊莎贝尔中使用共归纳法。我一直在查看 HOL/Datatype_Examples/Process.thy (Andrei Popescu) 2012。随着 2019 年 Isabelle 的进步很大（而不是因为任何个人技能），我已经简化了证明，但仍然不明白他们为什么决定做第一个步。

工作简化证明是

lemma solution_PROC[simp]: "solution sys (PROC p) = p"
proof-
  {fix q assume "q = solution sys (PROC p)" (* How did they know to do this! *)
   hence "p = q"
   proof (coinduct rule: process.coinduct)
     case (Eq_process process process')
     then show ?case
       by simp 
   qed
 }
  thus ?thesis by metis
qed

我失败的天真方法是：

lemma solution_PROCFail: " p  = solution sys (PROC p)"
proof (coinduct rule: process.coinduct) (* look up  process.coinduct and 
            you can see the extra goal forced by the misalignment*)  
  case Eq_process
  then show ?thesis  (* cannot solve*)
qed

两个问题：

  1. 语法 {fix q 假设 "q = solution sys (PROC p)" .....} 是本地引理的旧语法吗？

更重要的是 2. 我怎么知道什么时候尝试这种技术？

非常感谢大卫

4

1 回答 1

1

  1. 语法等价于

    have ‹p = q› if ‹q = solution sys (PROC p)› for q
  using that by (coinduct rule: process.coinduct) simp

在

{fix q assume "q = solution sys (PROC p)" (* How did they know to do this! *)
   hence "p = q"
   proof (coinduct rule: process.coinduct)
     case (Eq_process process process')
     then show ?case
       by simp 
   qed
 }

{}打开一个新块（带有语言环境变量和语言环境假设），并假设引入了一个本地假设。块导出形式的定理?q2 = solution sys (PROC p) ⟹ p = ?q2。

您可能应该阅读 Isar 教程（如具体语义，而不是 isar-ref）以了解这些非常有用的构造。

  1. 这个想法是你需要一个涉及协推谓词的假设。我会将该技术描述为 Isabelle 中的标准解决方法，因为（共）归纳有时会失去变量之间的联系。

  2. lemma solution_PROCFail: " p  = solution sys (PROC p)"
proof (coinduct rule: process.coinduct) (* look up  process.coinduct and 
        you can see the extra goal forced by the misalignment*)  
  case Eq_process
  then show ?thesis  (* cannot solve*)
qed

失败，因为生成的案例/节目是垃圾（发生这种情况，请查看状态面板）。

于 2020-02-06T06:12:56.387 回答