操作系统形式化验证实践教程(11) - 结构化证明语言Isar 结构化证明语言Isar基本语法 apply方法和by方法虽然可以完成功能，但是看起来更像是命令式语言。使用Isar语言，还可以写得更加形式化一点。
Isar的格式看起来像这样:
proof assume “公式1” from “公式1" have “公式2” by 方法 … from “公式n” show “结论” by 方法 qed
虽然换了种写法，但是其实核心内容并没有变。
直接proof指定方法 最简单的写法，就是把by的内容放到proof语句之后，然后就直接qed了。 我们看7个例子：
lemma A1: “A ⟹ (B⟹A)” proof(erule thin_rl,Pure.assumption) qed
lemma A2 : “(A ⟹ (B⟹C)) ⟹ ((A⟹B) ⟹ (A⟹C))” proof(erule meta_impE,assumption,assumption) qed
lemma A3: “(A∧B) ⟹ A” proof(erule conjunct1) qed
lemma A4: “(A∧B) ⟹ B” proof(erule conjunct2) qed
lemma A5: “A ⟹ (B ⟹ (A∧B))” proof(erule conjI,assumption) qed
lemma A6: “A ⟹ (A ∨ B)” proof(erule disjI1) qed
lemma A7: “B ⟹ (A ∨ B)” proof(erule disjI2) qed
assume have show 下面我们尝试用assume…have…show的方法改写一下。proof语句的参数我们给个"-"，表示空值：
lemma “(A ⟹ (B⟹C)) ⟹ ((A⟹B) ⟹ (A⟹C))” proof - assume Fact0: “(A ⟹ (B⟹C))” from Fact0 show “((A⟹B) ⟹ (A⟹C))” by (rule meta_impE) qed
this 上一节我们在assume和show中使用了标签，但是Isar认为使用标签是不好的，容易给词法分析造成困扰。 如果使用上一条中的公式，我们就直接使用this来指代，上一节的例子就变成这样：
lemma “(A ⟹ (B⟹C)) ⟹ ((A⟹B) ⟹ (A⟹C))” proof - assume “(A ⟹ (B⟹C))” from this show “((A⟹B) ⟹ (A⟹C))” by (rule meta_impE) qed
then 尽可能使用this之后，我们发现from this用的很广泛，于是我们可以给from this起一个别名叫then。于是上节的例子可以写成下面这样：
lemma “(A ⟹ (B⟹C)) ⟹ ((A⟹B) ⟹ (A⟹C))” proof - assume “(A ⟹ (B⟹C))” then show “((A⟹B) ⟹ (A⟹C))” by (rule meta_impE) qed
thus和hence 换成then之后，我们发现from this终于被隐藏起来了。但是，大量的then have和then show又出来了。于是我们可以再简化一下，给then have起个别名hence，给then show起个别名thus。 于是上节的例子可以写成这样：
lemma “(A ⟹ (B⟹C)) ⟹ ((A⟹B) ⟹ (A⟹C))” proof - assume “(A ⟹ (B⟹C))” thus “((A⟹B) ⟹ (A⟹C))” by (rule meta_impE) qed
假设拆分 当lemma比较长时，可以将其拆分成几个独立的假设，然后在proof中使用。 我们来看个例子：
lemma impE_2: assumes 1:‹P⟶Q› and 2: ‹Q⟹R› and 3: ‹P⟶Q ⟹ P› shows ‹R› proof - from 3 and 1 have ‹P› by simp with 1 have ‹Q› by (rule impE) with 2 show ‹R› by simp qed
这里我们又使用了一个新的缩写with，with xxx等于from xxx this，是from的一个语法糖。 其中的"‹",写作。同样“›”写作. 也可以通过"来输入，然后IDE中会提示。
我们来看ASCII源码：
lemma impE_2: assumes 1:<open>P<longrightarrow>Q<close> and 2: <open>Q<Longrightarrow>R<close> and 3: <open>P<longrightarrow>Q <Longrightarrow> P<close> shows <open>R<close> proof - from 3 and 1 have <open>P<close> by simp with 1 have <open>Q<close> by (rule impE) with 2 show <open>R<close> by simp qed
对了，针对这样分立条件的，不使用Isar的情况下该如何写呢？我们可以使用using来使用假设们然后再用by来引用证明方法，来看个例子：
lemma impE_3: assumes 1:‹P⟶Q› and 2: ‹Q⟹R› and 3: ‹P⟶Q ⟹ P› shows ‹R› using “1” “2” “3” by blast
巩固下，再来个例子：
lemma notE_2: assumes 1: ‹¬P› and 2:‹¬P ⟹ P› shows ‹R› using “1” “2” by auto
小结 Isar语言的出现，是希望能够能通过一些语法糖，让证明看起来更像是用自然语言书写，提升可读性。 但是其基本原理跟没有Isar语言框架是一致的。数理逻辑知识目前仍然是主要要攻克的点，而非语言和框架。
原文链接：https://blog.csdn.net/lusing/article/details/108328674?utm_medium=distribute.pc_feed.none-task-blog-personrec_tag-19.nonecase&depth_1-utm_source=distribute.pc_feed.none-task-blog-personrec_tag-19.nonecase&request_id=5f4d91c86fbae3485ef553ec
