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

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:
lemma
fixes n :: nat
shows "t4 n ==> ~ t4 (Suc n)"
proof (induction n rule: t4.induct)
case "default_1" then show "?case" by simp
next
case "default_2" then show "?case" by simp
next
case "zero" then show "?case" by simp
next
case "default_3" then show "?case" by simp
next
case "four"
from this show "?case" by simp
qed
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.
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.
Thanks a lot.
-Arthur
Working proof:
lemma
fixes n :: nat
shows "t4 n ==> ~ t4 (Suc n)"
proof (induction n rule: t4.induct)
case "3_1" then show "?case" by simp
next
case "3_2" then show "?case" by simp
next
case "2" then show "?case" by simp
next
case "3_3" then show "?case" by simp
next
case "1"
from this show "?case" by simp
qed

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