Can I name the variables generated by case analysi

问题:

Is it possible to give my own names to the variables generated when using case analysis or induction?

回答1:

If you are using structured proofs (starting with the proof keyword), you can use the case keywoard to select the case you want to prove and give names to the variables created by 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 a list consists of a start element and a 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 with the print_cases command.

If on the other hand you are using apply-style, there is no direct way to name these variables (also, in this case you are likely to need case_tac instead of cases, as you will have to deal with bound variables instead of free variables). There is the method rename_tac which can be used to rename the outermost meta-quantified variables.

For most projects (with the notable exception of program verification, like in the L4.verified project), the common proof style is to use mostly structured proofs. Unstructured proofs are used for exploration and become seldom so complex that it is necessary to rename your variables.