[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.