CODEWITHSUNDEEP
isabelle
Denis
Denis

Reputation: 1271

Named function cases in proof by induction

Is it possible to use names pred_Zero and pred_Suc instead of 1 and 2 in the following proof by induction?

fun pred where
  pred_Zero:
  "pred 0 = 0"
| pred_Suc:
  "pred (Suc n) = n"

lemma pred_le:
  "pred n ≤ n"
proof (induct rule: pred.induct)
  case 1
  thus ?case by simp
next
  case (2 n)
  thus ?case by simp
qed

Upvotes: 1

Views: 106

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8278

You can assign names to the cases of an induction or cases rule using the case_names attribute:

proof (induct rule: pred.induct [case_names pred_Zero pred_Suc])

More canonical names for the cases would be 0 and Suc, and in this particular case you might as well just use the default induction rule nat.induct anyway since the induction rule generated forpred is identical to nat.induct.

Upvotes: 2

Related Questions