第一部分 基本技巧 3
第一章 基础 3
1.1 引言 3
1.2 theory（理论） 4
1.3 类型，项和公式 5
1.4 变元 8
1.5 交互与界面 8
1.6 启动 9
第二章 HOL中的函数编程 10
2.1 theory简介 10
2.2 求值 13
2.3 证明简介 13
小结 18
2.4 一些有用的命令 19
2.5 数据类型 19
2.5.1 表（1ist） 20
2.5.2 一般格式 20
2.5.3 原始递归 21
2.5.4 case表达式 22
2.5.5 结构归纳和case分支 22
2.5.6 实例学习：布尔表达式 23
2.6 一些基本类型 27
2.6.1 自然数 27
2.6.2 有序对 29
2.6.3 option类型 29
2.7 定义 30
2.7.1 类型同名 30
2.7.2 常量定义 30
2.8 定义方法 31
第三章 高级函数式编程 32
3.1 化简 32
3.1.1 什么是化简？ 32
3.1.2 化简规则 33
3.1.3 simp方法 34
3.1.4 添加或删除化简规则 34
3.1.5 假设 34
3.1.6 用定义重写 35
3.1.7 let－表达式化简 36
3.1.8 条件化简规则 37
3.1.9 自动Case分解 37
3.1.1 0追踪 39
3.1.1 1寻找定理 41
3.2 启发式归纳 42
3.3 案例学习：编译表达式 45
3.4 高级数据类型 48
3.4.1 互递归 48
3.4.2 嵌套递归 51
3.4.3 嵌套递归的限制 53
3.4.4 案例学习：Tries（特里树） 55
3.5 完全递归函数 59
3.5.1 定义 59
3.5.2 终止性 60
3.5.3 化简 61
3.5.4 归纳 63
第四章 theory的表示 65
4.1 具体语法 65
4.1.1 中缀记号 65
4.1.2 数学符号 66
4.1.3 前缀记号 68
4.1.4 简写 69
4.2 文档编制 70
4.2.1 Isabelle会话 71
4.2.2 结构标记 73
4.2.3 形式评注与反引式 75
4.2.4 符号的释义 78
4.2.5 抑制输出 78
第二部分 逻辑与集合 83
第五章 游戏规则 83
5.1 自然演绎推理 83
5.2 引入规则 84
5.3 消去规则 85
5.4 破坏性规则：一些例子 88
5.5 蕴含 89
5.6 否定 91
5.7 中间处理：规则处理的基本方法 93
5.8 合一与替换 95
5.8.1 替换与subst方法 96
5.8.2 合一及其陷阱 98
5.9 量词 100
5.9.1 全称引入规则 100
5.9.2 全称消去规则 101
5.9.3 存在量词 103
5.9.4 绑定变元改名：rename tac 103
5.9.5 重用假设：frule 104
5.9.6 量词的显式实例化 105
5.10 描述算子 107
5.10.1 确定描述 107
5.10.2 不确定描述 108
5.11 一些失败的证明 110
5.12 使用blast方法证明定理 112
5.13 其他经典推理方法 114
5.14 找到更多的定理 116
5.15 前推证明：转换定理 117
5.15.1 使用of,where和THEN修改定理 117
5.15.2 使用OF修正定理 120
5.16 向后证明中的前向推理 121
5.16.1 insert方法 122
5.16.2 subgoal tac方法 123
5.17 大型证明的管理 125
5.17.1 策略或控制结构 125
5.17.2 子目标编号 126
5.18 证明欧几里德算法的正确性 128
第六章 集合、函数和关系 133
6.1 集合 133
6.1.1 有限集的记号 135
6.1.2 集合描述方法（set comprehension） 136
6.1.3 绑定算子 136
6.1.4 有限性和基数 138
6.2 函数 138
6.2.1 函数基础知识 138
6.2.2 单射，满射，双射 139
6.2.3 函数的像 140
6.3 关系 141
6.3.1 关系基础 141
6.3.2 自反与传递闭包 142
6.3.3 一个证明样本 143
6.4 良基关系和归纳法 144
6.5 不动点算子 146
6.6 案例学习：模型检验的验证 147
6.6.1 命题动态逻辑——PDL 149
6.6.2 计算树逻辑——CTL 152
第七章 集合递归定义 160
7.1 偶数集合 160
7.1.1 构造递归定义 160
7.1.2 使用引入规则 161
7.1.3 规则归纳法 162
7.1.4 规则归纳法与推广 163
7.1.5 规则反演 164
7.1.6 交叉归纳定义 166
7.1.7 归纳定义谓词 167
7.2 自反传递闭包 167
7.3 高级归纳定义 171
7.3.1 引入规则中的全称量词 171
7.3.2 使用单调函数的另一种定义 173
7.3.3 等价性证明 175
7.3.4 规则反演的另一例 176
7.4 案例学习：上下文无关文法 178
第三部分 高级材料 187
第八章 高级types 187
8.1 对和元组 187
8.1.1 带元组的模式匹配 187
8.1.2 定理证明 188
8.2 记录 191
8.2.1 记录基础知识 191
8.2.2 可扩展记录和通用操作 192
8.2.3 记录相等 194
8.2.4 扩展和截断记录 196
8.3 类型类（typeclasses） 198
8.3.1 重载 199
8.3.2 公理 200
8.4 数 205
8.4.1 数字文字 206
8.4.2 自然数类型nat 207
8.4.3 整数类型 209
8.4.4 有理数、实数和复数 211
8.4.5 数值类型类 212
8.5 引入新类型 215
8.5.1 声明新类型 215
8.5.2 定义新类型 216
第九章 高级化简与归纳 220
9.1 化简 220
9.1.1 高级特色 220
9.1.2 化简器如何工作 222
9.2 高级归纳技巧 224
9.2.1 改造命题 224
9.2.2 超结构归纳和超递归归纳 226
9.2.3 新归纳格式的推导 228
9.2.4 再访CTL 229
第十章 案例学习：验证安全协议 234
10.1 Needham-Schroeder公钥协议 235
10.2 代理与消息 237
10.3 敌方建模 238
10.4 事件追踪 240
10.5 协议建模 241
10.6 证明基本性质 243
10.7 证明安全性定理 245
附录 248
参考文献 250
译后记 254