# HG changeset patch # User paulson # Date 1022081194 -7200 # Node ID 3208b614dc716ea09f63ac42906659775abf2c81 # Parent 9e23faed6c97c927086eccd96f28af1fa9061caa conversion of Nat to Isar diff -r 9e23faed6c97 -r 3208b614dc71 src/ZF/Cardinal.ML --- 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); diff -r 9e23faed6c97 -r 3208b614dc71 src/ZF/IsaMakefile --- 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 \ diff -r 9e23faed6c97 -r 3208b614dc71 src/ZF/Nat.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 i le i; same thing as i 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 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 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 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*) diff -r 9e23faed6c97 -r 3208b614dc71 src/ZF/Nat.thy --- 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 == {:nat*nat. y < x}" - less_than :: i=>i + less_than :: "i=>i" "less_than(n) == {i:nat. ii + 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 i le i; same thing as i 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 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 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 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