如果您使用结构化校样(从proof关键字开始),您可以使用casekeywoard选择要证明的案例,并为案例分析/归纳创建的变量命名:
lemma "length (rev xs) = length xs"
proof (induct xs)
case Nil
then show ?case ...
next
case (Cons x xs)
then show ?case ...
qed
这里case (Cons x xs)告诉Isabelle你要证明列表由一个开始元素和一个剩余列表(即归纳步骤)组成的情况,并命名变量x和xs.
在校样块中,您可以使用该print_cases命令查看案例列表.
另一方面,如果您使用的是apply-style,则没有直接的方法来命名这些变量(在这种情况下,您可能需要case_tac代替cases,因为您将不得不处理绑定变量而不是自由变量).有一种方法rename_tac可用于重命名最外层的元量化变量.
对于大多数项目(除了程序验证之外,例如在L4.verified项目中),常见的证明样式是使用大多数结构化证明.非结构化样张用于探索,很少变得如此复杂,以至于必须重命名变量.