If you use structured evidence (starting with the proof keyword), you can use the case keyboard to select the case you want to prove and give names to the variables created by the case analysis / induction:
lemma "length (rev xs) = length xs" proof (induct xs) case Nil then show ?case ... next case (Cons x xs) then show ?case ... qed
Here, case (Cons x xs) tells Isabelle that you want to prove the case where the list consists of the starting element and the remaining list (i.e., the induction step) and name the variables x and xs .
In the proof block, you can see the list of cases using the print_cases .
If, on the other hand, you use the apply style, there is no direct way to name these variables (also in this case you may need case_tac instead of cases , because you will have to process the associated variables instead of free variables). There is a rename_tac method that can be used to rename external meta-quantized variables.
For most projects (with the exception of program verification, for example, in the L4.verified project), the general style of evidence is to use mostly structured evidence. Unstructured evidence is used for intelligence and becomes so complex that variables need to be renamed.
Lars noschinski
source share