Isabelle前提案例分析：如何对instr类型的i执行分情况证明？

证明状态与类型定义回顾 #

当前证明状态：

1. ⋀i is s stk stack.
       (⋀stack.
           length (exec is s stack) = n' ⟹
           length stack = n ⟹ ok n is n') ⟹
       length (exec (i # is) s stack) = n' ⟹
       length stack = n ⟹ ok n (i # is) n'

instr类型定义：

datatype instr = LOADI val | LOAD vname | ADD

分情况拆分的战术操作 #

在Isabelle的证明脚本中，直接使用case_tac i战术即可对变量i按其datatype的构造器进行分情况拆分：

• 执行该战术会生成三个子目标，分别对应i = LOADI val、i = LOAD vname、i = ADD三种情况
• 若需明确指定拆分类型以避免歧义，可写成case_tac i :: instr

拆分完成后，你可以针对每种指令类型，结合exec函数定义与ok谓词的性质分别完成证明。

内容的提问来源于stack exchange，提问作者cxandru