--- a/src/ZF/Cardinal.ML Wed May 22 17:25:40 2002 +0200
+++ b/src/ZF/Cardinal.ML Wed May 22 17:26:34 2002 +0200
@@ -472,7 +472,7 @@
qed "succ_lepoll_succD";
Goal "m:nat ==> ALL n: nat. m lepoll n --> m le n";
-by (nat_ind_tac "m" [] 1); (*induct_tac isn't available yet*)
+by (etac nat_induct 1); (*induct_tac isn't available yet*)
by (blast_tac (claset() addSIs [nat_0_le]) 1);
by (rtac ballI 1);
by (eres_inst_tac [("n","n")] natE 1);
--- a/src/ZF/IsaMakefile Wed May 22 17:25:40 2002 +0200
+++ b/src/ZF/IsaMakefile Wed May 22 17:26:34 2002 +0200
@@ -37,8 +37,7 @@
Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy \
Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML \
Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy \
- Main_ZFC.ML Main_ZFC.thy \
- Nat.ML Nat.thy Order.thy OrderArith.thy \
+ Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy \
OrderType.thy Ordinal.thy OrdQuant.thy Perm.ML Perm.thy \
QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML \
Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \
--- a/src/ZF/Nat.ML Wed May 22 17:25:40 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,253 +0,0 @@
-(* Title: ZF/Nat.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
-
-Natural numbers in Zermelo-Fraenkel Set Theory
-*)
-
-Goal "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})";
-by (rtac bnd_monoI 1);
-by (REPEAT (ares_tac [subset_refl, RepFun_mono, Un_mono] 2));
-by (cut_facts_tac [infinity] 1);
-by (Blast_tac 1);
-qed "nat_bnd_mono";
-
-(* nat = {0} Un {succ(x). x:nat} *)
-bind_thm ("nat_unfold", nat_bnd_mono RS (nat_def RS def_lfp_unfold));
-
-(** Type checking of 0 and successor **)
-
-Goal "0 : nat";
-by (stac nat_unfold 1);
-by (rtac (singletonI RS UnI1) 1);
-qed "nat_0I";
-
-Goal "n : nat ==> succ(n) : nat";
-by (stac nat_unfold 1);
-by (etac (RepFunI RS UnI2) 1);
-qed "nat_succI";
-
-Goal "1 : nat";
-by (rtac (nat_0I RS nat_succI) 1);
-qed "nat_1I";
-
-Goal "2 : nat";
-by (rtac (nat_1I RS nat_succI) 1);
-qed "nat_2I";
-
-AddIffs [nat_0I, nat_1I, nat_2I];
-AddSIs [nat_succI];
-AddTCs [nat_0I, nat_1I, nat_2I, nat_succI];
-
-Goal "bool <= nat";
-by (blast_tac (claset() addSEs [boolE]) 1);
-qed "bool_subset_nat";
-
-bind_thm ("bool_into_nat", bool_subset_nat RS subsetD);
-
-
-(** Injectivity properties and induction **)
-
-(*Mathematical induction*)
-val major::prems = Goal
- "[| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)";
-by (rtac ([nat_def, nat_bnd_mono, major] MRS def_induct) 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "nat_induct";
-
-(*Perform induction on n, then prove the n:nat subgoal using prems. *)
-fun nat_ind_tac a prems i =
- EVERY [res_inst_tac [("n",a)] nat_induct i,
- rename_last_tac a ["1"] (i+2),
- ares_tac prems i];
-
-val major::prems = Goal
- "[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P";
-by (rtac (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1);
-by (DEPTH_SOLVE (eresolve_tac [singletonE,RepFunE] 1
- ORELSE ares_tac prems 1));
-qed "natE";
-
-Goal "n: nat ==> Ord(n)";
-by (nat_ind_tac "n" [] 1);
-by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
-qed "nat_into_Ord";
-
-Addsimps [nat_into_Ord];
-
-(* i: nat ==> 0 le i; same thing as 0<succ(i) *)
-bind_thm ("nat_0_le", nat_into_Ord RS Ord_0_le);
-
-(* i: nat ==> i le i; same thing as i<succ(i) *)
-bind_thm ("nat_le_refl", nat_into_Ord RS le_refl);
-
-Goal "Ord(nat)";
-by (rtac OrdI 1);
-by (etac (nat_into_Ord RS Ord_is_Transset) 2);
-by (rewtac Transset_def);
-by (rtac ballI 1);
-by (etac nat_induct 1);
-by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1));
-qed "Ord_nat";
-
-Goalw [Limit_def] "Limit(nat)";
-by (safe_tac (claset() addSIs [ltI, Ord_nat]));
-by (etac ltD 1);
-qed "Limit_nat";
-
-(* succ(i): nat ==> i: nat *)
-bind_thm ("succ_natD", [succI1, asm_rl, Ord_nat] MRS Ord_trans);
-AddSDs [succ_natD];
-
-Goal "succ(n): nat <-> n: nat";
-by (Blast_tac 1);
-qed "nat_succ_iff";
-
-AddIffs [Ord_nat, Limit_nat, nat_succ_iff];
-
-Goal "Limit(i) ==> nat le i";
-by (rtac subset_imp_le 1);
-by (rtac subsetI 1);
-by (etac nat_induct 1);
-by (blast_tac (claset() addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2);
-by (REPEAT (ares_tac [Limit_has_0 RS ltD, Ord_nat, Limit_is_Ord] 1));
-qed "nat_le_Limit";
-
-(* [| succ(i): k; k: nat |] ==> i: k *)
-bind_thm ("succ_in_naturalD", [succI1, asm_rl, nat_into_Ord] MRS Ord_trans);
-
-Goal "[| m<n; n: nat |] ==> m: nat";
-by (etac ltE 1);
-by (etac (Ord_nat RSN (3,Ord_trans)) 1);
-by (assume_tac 1);
-qed "lt_nat_in_nat";
-
-Goal "[| m le n; n:nat |] ==> m:nat";
-by (blast_tac (claset() addSDs [lt_nat_in_nat]) 1);
-qed "le_in_nat";
-
-
-(** Variations on mathematical induction **)
-
-(*complete induction*)
-bind_thm ("complete_induct", Ord_nat RSN (2, Ord_induct));
-
-val prems = Goal
- "[| m: nat; n: nat; \
-\ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \
-\ |] ==> m le n --> P(m) --> P(n)";
-by (nat_ind_tac "n" prems 1);
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps prems @ distrib_simps @ [le0_iff, le_succ_iff])));
-qed "nat_induct_from_lemma";
-
-(*Induction starting from m rather than 0*)
-val prems = Goal
- "[| m le n; m: nat; n: nat; \
-\ P(m); \
-\ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \
-\ |] ==> P(n)";
-by (rtac (nat_induct_from_lemma RS mp RS mp) 1);
-by (REPEAT (ares_tac prems 1));
-qed "nat_induct_from";
-
-(*Induction suitable for subtraction and less-than*)
-val prems = Goal
- "[| m: nat; n: nat; \
-\ !!x. x: nat ==> P(x,0); \
-\ !!y. y: nat ==> P(0,succ(y)); \
-\ !!x y. [| x: nat; y: nat; P(x,y) |] ==> P(succ(x),succ(y)) \
-\ |] ==> P(m,n)";
-by (res_inst_tac [("x","m")] bspec 1);
-by (resolve_tac prems 2);
-by (nat_ind_tac "n" prems 1);
-by (rtac ballI 2);
-by (nat_ind_tac "x" [] 2);
-by (REPEAT (ares_tac (prems@[ballI]) 1 ORELSE etac bspec 1));
-qed "diff_induct";
-
-(** Induction principle analogous to trancl_induct **)
-
-val le_cs = claset() addSIs [leCI] addSEs [leE] addEs [lt_asym];
-
-Goal "m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \
-\ (ALL n:nat. m<n --> P(m,n))";
-by (etac nat_induct 1);
-by (rtac (impI RS impI) 1);
-by (rtac (nat_induct RS ballI) 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-by (asm_simp_tac (simpset() addsimps [le_iff]) 1);
-by (Blast_tac 1);
-(*and again*)
-by (rtac (impI RS impI) 1);
-by (rtac (nat_induct RS ballI) 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-by (asm_simp_tac (simpset() addsimps [le_iff]) 1);
-by (Blast_tac 1);
-qed "succ_lt_induct_lemma";
-
-val prems = Goal
- "[| m<n; n: nat; \
-\ P(m,succ(m)); \
-\ !!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) \
-\ |] ==> P(m,n)";
-by (res_inst_tac [("P4","P")]
- (succ_lt_induct_lemma RS mp RS mp RS bspec RS mp) 1);
-by (REPEAT (ares_tac (prems @ [ballI, impI, lt_nat_in_nat]) 1));
-qed "succ_lt_induct";
-
-(** nat_case **)
-
-Goalw [nat_case_def] "nat_case(a,b,0) = a";
-by (Blast_tac 1);
-qed "nat_case_0";
-
-Goalw [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
-by (Blast_tac 1);
-qed "nat_case_succ";
-
-Addsimps [nat_case_0, nat_case_succ];
-
-val major::prems = Goal
- "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) \
-\ |] ==> nat_case(a,b,n) : C(n)";
-by (rtac (major RS nat_induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
-qed "nat_case_type";
-
-
-(** nat_rec -- used to define eclose and transrec, then obsolete;
- rec, from arith.ML, has fewer typing conditions **)
-
-val lemma = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans);
-
-Goal "nat_rec(0,a,b) = a";
-by (rtac lemma 1);
-by (rtac nat_case_0 1);
-qed "nat_rec_0";
-
-Goal "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
-by (rtac lemma 1);
-by (asm_simp_tac (simpset() addsimps [vimage_singleton_iff]) 1);
-qed "nat_rec_succ";
-
-(** The union of two natural numbers is a natural number -- their maximum **)
-
-Goal "[| i: nat; j: nat |] ==> i Un j: nat";
-by (rtac (Un_least_lt RS ltD) 1);
-by (REPEAT (ares_tac [ltI, Ord_nat] 1));
-qed "Un_nat_type";
-
-Goal "[| i: nat; j: nat |] ==> i Int j: nat";
-by (rtac (Int_greatest_lt RS ltD) 1);
-by (REPEAT (ares_tac [ltI, Ord_nat] 1));
-qed "Int_nat_type";
-
-Goal "nat ~= 0";
-by (Blast_tac 1);
-qed "nat_nonempty";
-Addsimps [nat_nonempty]; (*needed to simplify unions over nat*)
--- a/src/ZF/Nat.thy Wed May 22 17:25:40 2002 +0200
+++ b/src/ZF/Nat.thy Wed May 22 17:26:34 2002 +0200
@@ -6,7 +6,7 @@
Natural numbers in Zermelo-Fraenkel Set Theory
*)
-Nat = OrdQuant + Bool + mono +
+theory Nat = OrdQuant + Bool + mono:
constdefs
nat :: i
@@ -33,10 +33,253 @@
Gt :: i
"Gt == {<x,y>:nat*nat. y < x}"
- less_than :: i=>i
+ less_than :: "i=>i"
"less_than(n) == {i:nat. i<n}"
- greater_than :: i=>i
+ greater_than :: "i=>i"
"greater_than(n) == {i:nat. n < i}"
+lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})"
+apply (rule bnd_monoI)
+apply (cut_tac infinity, blast)
+apply blast
+done
+
+(* nat = {0} Un {succ(x). x:nat} *)
+lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold], standard]
+
+(** Type checking of 0 and successor **)
+
+lemma nat_0I [iff,TC]: "0 : nat"
+apply (subst nat_unfold)
+apply (rule singletonI [THEN UnI1])
+done
+
+lemma nat_succI [intro!,TC]: "n : nat ==> succ(n) : nat"
+apply (subst nat_unfold)
+apply (erule RepFunI [THEN UnI2])
+done
+
+lemma nat_1I [iff,TC]: "1 : nat"
+by (rule nat_0I [THEN nat_succI])
+
+lemma nat_2I [iff,TC]: "2 : nat"
+by (rule nat_1I [THEN nat_succI])
+
+lemma bool_subset_nat: "bool <= nat"
+by (blast elim!: boolE)
+
+lemmas bool_into_nat = bool_subset_nat [THEN subsetD, standard]
+
+
+(** Injectivity properties and induction **)
+
+(*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
+
+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
+
+lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
+by (erule nat_induct, auto)
+
+(* i: nat ==> 0 le i; same thing as 0<succ(i) *)
+lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le, standard]
+
+(* i: nat ==> i le i; same thing as i<succ(i) *)
+lemmas nat_le_refl = nat_into_Ord [THEN le_refl, standard]
+
+lemma Ord_nat [iff]: "Ord(nat)"
+apply (rule OrdI)
+apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset])
+apply (unfold Transset_def)
+apply (rule ballI)
+apply (erule nat_induct, auto)
+done
+
+lemma Limit_nat [iff]: "Limit(nat)"
+apply (unfold Limit_def)
+apply (safe intro!: ltI Ord_nat)
+apply (erule ltD)
+done
+
+lemma succ_natD [dest!]: "succ(i): nat ==> i: nat"
+by (rule Ord_trans [OF succI1], auto)
+
+lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
+by blast
+
+lemma nat_le_Limit: "Limit(i) ==> nat le i"
+apply (rule subset_imp_le)
+apply (simp_all add: Limit_is_Ord)
+apply (rule subsetI)
+apply (erule nat_induct)
+ apply (erule Limit_has_0 [THEN ltD])
+apply (blast intro: Limit_has_succ [THEN ltD] ltI Limit_is_Ord)
+done
+
+(* [| succ(i): k; k: nat |] ==> i: k *)
+lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord]
+
+lemma lt_nat_in_nat: "[| m<n; n: nat |] ==> m: nat"
+apply (erule ltE)
+apply (erule Ord_trans, assumption)
+apply simp
+done
+
+lemma le_in_nat: "[| m le n; n:nat |] ==> m:nat"
+by (blast dest!: lt_nat_in_nat)
+
+
+(** Variations on mathematical induction **)
+
+(*complete induction*)
+lemmas complete_induct = Ord_induct [OF _ Ord_nat]
+
+lemma nat_induct_from_lemma [rule_format]:
+ "[| n: nat; m: nat;
+ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) |]
+ ==> m le n --> P(m) --> P(n)"
+apply (erule nat_induct)
+apply (simp_all add: distrib_simps le0_iff le_succ_iff)
+done
+
+(*Induction starting from m rather than 0*)
+lemma nat_induct_from:
+ "[| m le n; m: nat; n: nat;
+ P(m);
+ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) |]
+ ==> P(n)"
+apply (blast intro: nat_induct_from_lemma)
+done
+
+(*Induction suitable for subtraction and less-than*)
+lemma diff_induct:
+ "[| m: nat; n: nat;
+ !!x. x: nat ==> P(x,0);
+ !!y. y: nat ==> P(0,succ(y));
+ !!x y. [| x: nat; y: nat; P(x,y) |] ==> P(succ(x),succ(y)) |]
+ ==> P(m,n)"
+apply (erule_tac x = "m" in rev_bspec)
+apply (erule nat_induct, simp)
+apply (rule ballI)
+apply (rename_tac i j)
+apply (erule_tac n=j in nat_induct, auto)
+done
+
+(** Induction principle analogous to trancl_induct **)
+
+lemma succ_lt_induct_lemma [rule_format]:
+ "m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) -->
+ (ALL n:nat. m<n --> P(m,n))"
+apply (erule nat_induct)
+ apply (intro impI, rule nat_induct [THEN ballI])
+ prefer 4 apply (intro impI, rule nat_induct [THEN ballI])
+apply (auto simp add: le_iff)
+done
+
+lemma succ_lt_induct:
+ "[| m<n; n: nat;
+ P(m,succ(m));
+ !!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) |]
+ ==> P(m,n)"
+by (blast intro: succ_lt_induct_lemma lt_nat_in_nat)
+
+(** nat_case **)
+
+lemma nat_case_0 [simp]: "nat_case(a,b,0) = a"
+by (unfold nat_case_def, blast)
+
+lemma nat_case_succ [simp]: "nat_case(a,b,succ(m)) = b(m)"
+by (unfold nat_case_def, blast)
+
+lemma nat_case_type:
+ "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |]
+ ==> nat_case(a,b,n) : C(n)"
+apply (erule nat_induct, auto)
+done
+
+
+(** nat_rec -- used to define eclose and transrec, then obsolete
+ rec, from arith.ML, has fewer typing conditions **)
+
+lemma nat_rec_0: "nat_rec(0,a,b) = a"
+apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
+ apply (rule wf_Memrel)
+apply (rule nat_case_0)
+done
+
+lemma nat_rec_succ: "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))"
+apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
+ apply (rule wf_Memrel)
+apply (simp add: vimage_singleton_iff)
+done
+
+(** The union of two natural numbers is a natural number -- their maximum **)
+
+lemma Un_nat_type: "[| i: nat; j: nat |] ==> i Un j: nat"
+apply (rule Un_least_lt [THEN ltD])
+apply (simp_all add: lt_def)
+done
+
+lemma Int_nat_type: "[| i: nat; j: nat |] ==> i Int j: nat"
+apply (rule Int_greatest_lt [THEN ltD])
+apply (simp_all add: lt_def)
+done
+
+(*needed to simplify unions over nat*)
+lemma nat_nonempty [simp]: "nat ~= 0"
+by blast
+
+ML
+{*
+val Le_def = thm "Le_def";
+val Lt_def = thm "Lt_def";
+val Ge_def = thm "Ge_def";
+val Gt_def = thm "Gt_def";
+val less_than_def = thm "less_than_def";
+val greater_than_def = thm "greater_than_def";
+
+val nat_bnd_mono = thm "nat_bnd_mono";
+val nat_unfold = thm "nat_unfold";
+val nat_0I = thm "nat_0I";
+val nat_succI = thm "nat_succI";
+val nat_1I = thm "nat_1I";
+val nat_2I = thm "nat_2I";
+val bool_subset_nat = thm "bool_subset_nat";
+val bool_into_nat = thm "bool_into_nat";
+val nat_induct = thm "nat_induct";
+val natE = thm "natE";
+val nat_into_Ord = thm "nat_into_Ord";
+val nat_0_le = thm "nat_0_le";
+val nat_le_refl = thm "nat_le_refl";
+val Ord_nat = thm "Ord_nat";
+val Limit_nat = thm "Limit_nat";
+val succ_natD = thm "succ_natD";
+val nat_succ_iff = thm "nat_succ_iff";
+val nat_le_Limit = thm "nat_le_Limit";
+val succ_in_naturalD = thm "succ_in_naturalD";
+val lt_nat_in_nat = thm "lt_nat_in_nat";
+val le_in_nat = thm "le_in_nat";
+val complete_induct = thm "complete_induct";
+val nat_induct_from_lemma = thm "nat_induct_from_lemma";
+val nat_induct_from = thm "nat_induct_from";
+val diff_induct = thm "diff_induct";
+val succ_lt_induct_lemma = thm "succ_lt_induct_lemma";
+val succ_lt_induct = thm "succ_lt_induct";
+val nat_case_0 = thm "nat_case_0";
+val nat_case_succ = thm "nat_case_succ";
+val nat_case_type = thm "nat_case_type";
+val nat_rec_0 = thm "nat_rec_0";
+val nat_rec_succ = thm "nat_rec_succ";
+val Un_nat_type = thm "Un_nat_type";
+val Int_nat_type = thm "Int_nat_type";
+val nat_nonempty = thm "nat_nonempty";
+*}
+
end