--- a/src/ZF/Nat.thy Wed Jun 05 12:24:14 2002 +0200
+++ b/src/ZF/Nat.thy Wed Jun 05 15:34:55 2002 +0200
@@ -83,13 +83,14 @@
(*Mathematical induction*)
lemma nat_induct:
"[| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)"
-apply (erule def_induct [OF nat_def nat_bnd_mono], blast)
-done
+by (erule def_induct [OF nat_def nat_bnd_mono], blast)
+
+(*fixed up for induct method*)
+lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat]
lemma natE:
"[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
-apply (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto)
-done
+by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto)
lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
by (erule nat_induct, auto)
@@ -145,7 +146,12 @@
(** Variations on mathematical induction **)
(*complete induction*)
-lemmas complete_induct = Ord_induct [OF _ Ord_nat]
+
+lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1]
+
+lemmas complete_induct_rule =
+ complete_induct [rule_format, case_names less, consumes 1]
+
lemma nat_induct_from_lemma [rule_format]:
"[| n: nat; m: nat;
@@ -178,6 +184,9 @@
apply (erule_tac n=j in nat_induct, auto)
done
+(*fixed up for induct method*)
+lemmas diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2]
+
(** Induction principle analogous to trancl_induct **)
lemma succ_lt_induct_lemma [rule_format]:
@@ -268,6 +277,7 @@
lemma nat_nonempty [simp]: "nat ~= 0"
by blast
+
ML
{*
val Le_def = thm "Le_def";