操作系统形式化验证实践教程(11) - 结构化证明语言Isar（转载）
操作系统形式化验证实践教程(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
操作系统形式化验证实践教程(11) - 结构化证明语言Isar（转载）相关推荐
- 操作系统形式化验证实践教程(11) - 结构化证明语言Isar
操作系统形式化验证实践教程(11) - 结构化证明语言Isar 结构化证明语言Isar基本语法 apply方法和by方法虽然可以完成功能,但是看起来更像是命令式语言.使用Isar语言,还可以写得更加形 ...
- 操作系统形式化验证实践教程(10) - 一阶直觉逻辑
操作系统形式化验证实践教程(10) - 一阶直觉逻辑 前面我们用了九讲的篇幅把seL4验证操作系统的地图给大家迅速过了一遍,基础好的同学已经可以基于前面的知识开始自己的工作了. 对于只学过离散数学,而 ...
- 操作系统形式化验证实践教程(7) - C代码的自动验证
操作系统形式化验证实践教程(7) - C代码的自动验证 上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
- 操作系统形式化验证实践教程(7) - C代码的自动验证（转载）
操作系统形式化验证实践教程(7) - C代码的自动验证 上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
- linux内核形式化验证,聪明人的笨功夫 -- MesaTEE安全形式化验证实践
各类TEE(例如TPM和Intel SGX)提供了强大的可信计算硬件基础,但他们并不直接保证软件的安全性.诸如缓冲区溢出等内存安全问题为攻击者提供了侵入TEE的可乘之机.因此,软件内存安全保护极其重要 ...
- 数据科学 IPython 笔记本 9.11 结构化数据：NumPy 的结构化数组
9.11 结构化数据:NumPy 的结构化数组 本节是<Python 数据科学手册>(Python Data Science Handbook)的摘录. 译者:飞龙 协议:CC BY-NC ...
- Rockwell 罗克韦尔AB Logix 5000控制器 结构化文本语言（ST） 梯形图（LD）顺序功能图（SFC）功能块图（FBD） IEC 61131-3 手册
Logix 5000 Controllers IEC 61131-3 Compliance 1756 ControlLogix, 1756 GuardLogix, 1769 CompactLogix, ...
- st计算机编程语言,ST（结构化文本语言(ST)）_百度百科
ST (结构化文本语言(ST)) 语音 编辑 锁定 讨论 上传视频 本词条缺少概述图,补充相关内容使词条更完整,还能快速升级,赶紧来编辑吧! 结构化文本/结构式文件编程语言(英语:Structured ...
- 1-1 结构化数据建模流程范例
一.准备数据 titanic数据集(下载链接:https://www.kaggle.com/c/titanic/data)的目标是根据乘客信息预测他们在Titanic号撞击冰山沉没后能否生存. 结构化 ...
最新文章
- Matlab与线性代数 -- 寻找矩阵的非零元素
- 八皇后问题（回溯法）
- 学习曾国藩，学做人做事学技术
- 贪心——区间选点问题(用最少数量的箭引爆气球 Leetcode 452)
- DataTable 转换 DataSet
- [转载] Python连接MySQL、Mongodb、SQLite
- js 终止 for 循环
- win10切换桌面_探秘Win10系统中的不可错过的实用功能
- 【STM32】STM32F103C8T6+L298N通过PWM控制直流电机转速
- JS递归算法经典案例与分析
- perl 5.10.0安装包下载
- Pr 视频效果：变换
- （JavaScript）Mixin 模式
- 面试官都会问些什么问题？
- 【HGE】使用C++从加密压缩包中读取图像文件并显示
- 学术规范与论文写作（期末考试答案）（方便检索版）
- Python基本环境配置
- python mitmproxy +雷电模拟器 安装
- libopencv_viz.so未定义使用
- 关于JPEG2000软件