是否可以给我自己的名字使用案例分析或感应时产生的变量？
Answer 1:
如果使用的是结构化的证明（与初始proof关键字），您可以使用case keywoard选择你想证明，并给予名称由案例分析/感应创建的变量的情况：
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)告诉伊莎贝尔要证明的情况下列表包含一个开始元素和剩余的列表（即感应步骤），并命名变量x和xs 。
在证据块，你可以看到的案件清单print_cases命令。
如果您使用的是另一方面apply风格的，有来命名这些变量（也，在这种情况下，你很可能需要没有直接的方法case_tac代替cases ，你将不得不面对绑定变量，而不是自由变量）。 有该方法rename_tac可用于重命名最外面的元定量变量。
对于大多数项目（程序验证，就像在L4.verified项目显着的例外），共同证明的风格是大部分使用结构化证明。 非结构化证明用于勘探和变得很少如此复杂，以至于有必要重新命名您的变量。
文章来源: Can I name the variables generated by case analysis?
