Re: [isabelle] Naming cases in the induction scheme of a function



On 26.11.2012 00:07, Arthur Peters wrote:
I would like to provide names for clauses in a function and then have them
used in the induction rule.

For example, I have the following function:

fun t4 :: "nat =>  bool" where
   four:
   "t4 (Suc (Suc (Suc (Suc n)))) = t4 n" |
   zero:
   "t4 0 = True" |
   default:
   "t4 _ = False"

And I can reference the cases as 1, 2, 3_1, 3_2, 3_3. See the bottom for a
working proof in this form. However I would like to be able to do something
like the following with the names I gave used in the case names:
[...
I have read that this is possible for inductively defined sets, but it
found no description of how to do the same thing with functions.

The function package does not support this. However, you can use the case_names attribute to annotate the generated induction lemma with the case names:

lemma t4_induct = t4.induct[case_names four zero default]

gives you the induction rule you want.

As a side note, is it possible to combine all the trivial cases (the
defaults and zero) into one proof? All the proofs are identical so it would
be nice to be able to do more than one case at a time.

If the proof is trivial, you can just omit these cases and solve them in the final step:

proof (induct rule: t4_induct)
  case four ...
qed (auto ...)

If the proof is not trivial, but the same, you can do the following thing:

proof (induct rule: t4_induct)
  have X: ... proof the theorem for the trivial cases ...
  { case default show ?case by (... X ...) }
  { case zero show ?case by (... X ...) }
next
  case four ...
qed

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.