conversion of Nat to Isar
authorpaulson
Wed May 22 17:26:34 2002 +0200 (2002-05-22)
changeset 131713208b614dc71
parent 13170 9e23faed6c97
child 13172 03a5afa7b888
conversion of Nat to Isar
src/ZF/Cardinal.ML
src/ZF/IsaMakefile
src/ZF/Nat.ML
src/ZF/Nat.thy
     1.1 --- a/src/ZF/Cardinal.ML	Wed May 22 17:25:40 2002 +0200
     1.2 +++ b/src/ZF/Cardinal.ML	Wed May 22 17:26:34 2002 +0200
     1.3 @@ -472,7 +472,7 @@
     1.4  qed "succ_lepoll_succD";
     1.5  
     1.6  Goal "m:nat ==> ALL n: nat. m lepoll n --> m le n";
     1.7 -by (nat_ind_tac "m" [] 1);  (*induct_tac isn't available yet*)
     1.8 +by (etac nat_induct 1);  (*induct_tac isn't available yet*)
     1.9  by (blast_tac (claset() addSIs [nat_0_le]) 1);
    1.10  by (rtac ballI 1);
    1.11  by (eres_inst_tac [("n","n")] natE 1);
     2.1 --- a/src/ZF/IsaMakefile	Wed May 22 17:25:40 2002 +0200
     2.2 +++ b/src/ZF/IsaMakefile	Wed May 22 17:26:34 2002 +0200
     2.3 @@ -37,8 +37,7 @@
     2.4    Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy	\
     2.5    Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML			\
     2.6    Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
     2.7 -  Main_ZFC.ML Main_ZFC.thy	\
     2.8 -  Nat.ML Nat.thy Order.thy OrderArith.thy	\
     2.9 +  Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy	\
    2.10    OrderType.thy Ordinal.thy OrdQuant.thy Perm.ML Perm.thy	\
    2.11    QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML	\
    2.12    Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
     3.1 --- a/src/ZF/Nat.ML	Wed May 22 17:25:40 2002 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,253 +0,0 @@
     3.4 -(*  Title:      ZF/Nat.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1992  University of Cambridge
     3.8 -
     3.9 -Natural numbers in Zermelo-Fraenkel Set Theory 
    3.10 -*)
    3.11 -
    3.12 -Goal "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})";
    3.13 -by (rtac bnd_monoI 1);
    3.14 -by (REPEAT (ares_tac [subset_refl, RepFun_mono, Un_mono] 2)); 
    3.15 -by (cut_facts_tac [infinity] 1);
    3.16 -by (Blast_tac 1);
    3.17 -qed "nat_bnd_mono";
    3.18 -
    3.19 -(* nat = {0} Un {succ(x). x:nat} *)
    3.20 -bind_thm ("nat_unfold", nat_bnd_mono RS (nat_def RS def_lfp_unfold));
    3.21 -
    3.22 -(** Type checking of 0 and successor **)
    3.23 -
    3.24 -Goal "0 : nat";
    3.25 -by (stac nat_unfold 1);
    3.26 -by (rtac (singletonI RS UnI1) 1);
    3.27 -qed "nat_0I";
    3.28 -
    3.29 -Goal "n : nat ==> succ(n) : nat";
    3.30 -by (stac nat_unfold 1);
    3.31 -by (etac (RepFunI RS UnI2) 1);
    3.32 -qed "nat_succI";
    3.33 -
    3.34 -Goal "1 : nat";
    3.35 -by (rtac (nat_0I RS nat_succI) 1);
    3.36 -qed "nat_1I";
    3.37 -
    3.38 -Goal "2 : nat";
    3.39 -by (rtac (nat_1I RS nat_succI) 1);
    3.40 -qed "nat_2I";
    3.41 -
    3.42 -AddIffs [nat_0I, nat_1I, nat_2I];
    3.43 -AddSIs  [nat_succI];
    3.44 -AddTCs  [nat_0I, nat_1I, nat_2I, nat_succI];
    3.45 -
    3.46 -Goal "bool <= nat";
    3.47 -by (blast_tac (claset() addSEs [boolE]) 1);
    3.48 -qed "bool_subset_nat";
    3.49 -
    3.50 -bind_thm ("bool_into_nat", bool_subset_nat RS subsetD);
    3.51 -
    3.52 -
    3.53 -(** Injectivity properties and induction **)
    3.54 -
    3.55 -(*Mathematical induction*)
    3.56 -val major::prems = Goal
    3.57 -    "[| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)";
    3.58 -by (rtac ([nat_def, nat_bnd_mono, major] MRS def_induct) 1);
    3.59 -by (blast_tac (claset() addIs prems) 1);
    3.60 -qed "nat_induct";
    3.61 -
    3.62 -(*Perform induction on n, then prove the n:nat subgoal using prems. *)
    3.63 -fun nat_ind_tac a prems i = 
    3.64 -    EVERY [res_inst_tac [("n",a)] nat_induct i,
    3.65 -           rename_last_tac a ["1"] (i+2),
    3.66 -           ares_tac prems i];
    3.67 -
    3.68 -val major::prems = Goal
    3.69 -    "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P";
    3.70 -by (rtac (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1);
    3.71 -by (DEPTH_SOLVE (eresolve_tac [singletonE,RepFunE] 1
    3.72 -          ORELSE ares_tac prems 1));
    3.73 -qed "natE";
    3.74 -
    3.75 -Goal "n: nat ==> Ord(n)";
    3.76 -by (nat_ind_tac "n" [] 1);
    3.77 -by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
    3.78 -qed "nat_into_Ord";
    3.79 -
    3.80 -Addsimps [nat_into_Ord];
    3.81 -
    3.82 -(* i: nat ==> 0 le i; same thing as 0<succ(i)  *)
    3.83 -bind_thm ("nat_0_le", nat_into_Ord RS Ord_0_le);
    3.84 -
    3.85 -(* i: nat ==> i le i; same thing as i<succ(i)  *)
    3.86 -bind_thm ("nat_le_refl", nat_into_Ord RS le_refl);
    3.87 -
    3.88 -Goal "Ord(nat)";
    3.89 -by (rtac OrdI 1);
    3.90 -by (etac (nat_into_Ord RS Ord_is_Transset) 2);
    3.91 -by (rewtac Transset_def);
    3.92 -by (rtac ballI 1);
    3.93 -by (etac nat_induct 1);
    3.94 -by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1));
    3.95 -qed "Ord_nat";
    3.96 -
    3.97 -Goalw [Limit_def] "Limit(nat)";
    3.98 -by (safe_tac (claset() addSIs [ltI, Ord_nat]));
    3.99 -by (etac ltD 1);
   3.100 -qed "Limit_nat";
   3.101 -
   3.102 -(* succ(i): nat ==> i: nat *)
   3.103 -bind_thm ("succ_natD", [succI1, asm_rl, Ord_nat] MRS Ord_trans);
   3.104 -AddSDs   [succ_natD];
   3.105 -
   3.106 -Goal "succ(n): nat <-> n: nat";
   3.107 -by (Blast_tac 1);
   3.108 -qed "nat_succ_iff";
   3.109 -
   3.110 -AddIffs [Ord_nat, Limit_nat, nat_succ_iff];
   3.111 -
   3.112 -Goal "Limit(i) ==> nat le i";
   3.113 -by (rtac subset_imp_le 1);
   3.114 -by (rtac subsetI 1);
   3.115 -by (etac nat_induct 1);
   3.116 -by (blast_tac (claset() addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2);
   3.117 -by (REPEAT (ares_tac [Limit_has_0 RS ltD, Ord_nat, Limit_is_Ord] 1));
   3.118 -qed "nat_le_Limit";
   3.119 -
   3.120 -(* [| succ(i): k;  k: nat |] ==> i: k *)
   3.121 -bind_thm ("succ_in_naturalD", [succI1, asm_rl, nat_into_Ord] MRS Ord_trans);
   3.122 -
   3.123 -Goal "[| m<n;  n: nat |] ==> m: nat";
   3.124 -by (etac ltE 1);
   3.125 -by (etac (Ord_nat RSN (3,Ord_trans)) 1);
   3.126 -by (assume_tac 1);
   3.127 -qed "lt_nat_in_nat";
   3.128 -
   3.129 -Goal "[| m le n; n:nat |] ==> m:nat";
   3.130 -by (blast_tac (claset() addSDs [lt_nat_in_nat]) 1);
   3.131 -qed "le_in_nat";
   3.132 -
   3.133 -
   3.134 -(** Variations on mathematical induction **)
   3.135 -
   3.136 -(*complete induction*)
   3.137 -bind_thm ("complete_induct", Ord_nat RSN (2, Ord_induct));
   3.138 -
   3.139 -val prems = Goal
   3.140 -    "[| m: nat;  n: nat;  \
   3.141 -\       !!x. [| x: nat;  m le x;  P(x) |] ==> P(succ(x)) \
   3.142 -\    |] ==> m le n --> P(m) --> P(n)";
   3.143 -by (nat_ind_tac "n" prems 1);
   3.144 -by (ALLGOALS
   3.145 -    (asm_simp_tac
   3.146 -     (simpset() addsimps prems @ distrib_simps @ [le0_iff, le_succ_iff])));
   3.147 -qed "nat_induct_from_lemma";
   3.148 -
   3.149 -(*Induction starting from m rather than 0*)
   3.150 -val prems = Goal
   3.151 -    "[| m le n;  m: nat;  n: nat;  \
   3.152 -\       P(m);  \
   3.153 -\       !!x. [| x: nat;  m le x;  P(x) |] ==> P(succ(x)) \
   3.154 -\    |] ==> P(n)";
   3.155 -by (rtac (nat_induct_from_lemma RS mp RS mp) 1);
   3.156 -by (REPEAT (ares_tac prems 1));
   3.157 -qed "nat_induct_from";
   3.158 -
   3.159 -(*Induction suitable for subtraction and less-than*)
   3.160 -val prems = Goal
   3.161 -    "[| m: nat;  n: nat;  \
   3.162 -\       !!x. x: nat ==> P(x,0);  \
   3.163 -\       !!y. y: nat ==> P(0,succ(y));  \
   3.164 -\       !!x y. [| x: nat;  y: nat;  P(x,y) |] ==> P(succ(x),succ(y))  \
   3.165 -\    |] ==> P(m,n)";
   3.166 -by (res_inst_tac [("x","m")] bspec 1);
   3.167 -by (resolve_tac prems 2);
   3.168 -by (nat_ind_tac "n" prems 1);
   3.169 -by (rtac ballI 2);
   3.170 -by (nat_ind_tac "x" [] 2);
   3.171 -by (REPEAT (ares_tac (prems@[ballI]) 1 ORELSE etac bspec 1));
   3.172 -qed "diff_induct";
   3.173 -
   3.174 -(** Induction principle analogous to trancl_induct **)
   3.175 -
   3.176 -val le_cs = claset() addSIs [leCI] addSEs [leE] addEs [lt_asym];
   3.177 -
   3.178 -Goal "m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \
   3.179 -\                 (ALL n:nat. m<n --> P(m,n))";
   3.180 -by (etac nat_induct 1);
   3.181 -by (rtac (impI RS impI) 1);
   3.182 -by (rtac (nat_induct RS ballI) 1);
   3.183 -by (assume_tac 1);
   3.184 -by (Blast_tac 1);
   3.185 -by (asm_simp_tac (simpset() addsimps [le_iff]) 1);
   3.186 -by (Blast_tac 1);
   3.187 -(*and again*)
   3.188 -by (rtac (impI RS impI) 1);
   3.189 -by (rtac (nat_induct RS ballI) 1);
   3.190 -by (assume_tac 1);
   3.191 -by (Blast_tac 1);
   3.192 -by (asm_simp_tac (simpset() addsimps [le_iff]) 1);
   3.193 -by (Blast_tac 1);
   3.194 -qed "succ_lt_induct_lemma";
   3.195 -
   3.196 -val prems = Goal
   3.197 -    "[| m<n;  n: nat;                                   \
   3.198 -\       P(m,succ(m));                                   \
   3.199 -\       !!x. [| x: nat;  P(m,x) |] ==> P(m,succ(x))     \
   3.200 -\    |] ==> P(m,n)";
   3.201 -by (res_inst_tac [("P4","P")] 
   3.202 -     (succ_lt_induct_lemma RS mp RS mp RS bspec RS mp) 1);
   3.203 -by (REPEAT (ares_tac (prems @ [ballI, impI, lt_nat_in_nat]) 1));
   3.204 -qed "succ_lt_induct";
   3.205 -
   3.206 -(** nat_case **)
   3.207 -
   3.208 -Goalw [nat_case_def] "nat_case(a,b,0) = a";
   3.209 -by (Blast_tac 1);
   3.210 -qed "nat_case_0";
   3.211 -
   3.212 -Goalw [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
   3.213 -by (Blast_tac 1);
   3.214 -qed "nat_case_succ";
   3.215 -
   3.216 -Addsimps [nat_case_0, nat_case_succ];
   3.217 -
   3.218 -val major::prems = Goal
   3.219 -    "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m))  \
   3.220 -\    |] ==> nat_case(a,b,n) : C(n)";
   3.221 -by (rtac (major RS nat_induct) 1);
   3.222 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   3.223 -qed "nat_case_type";
   3.224 -
   3.225 -
   3.226 -(** nat_rec -- used to define eclose and transrec, then obsolete;
   3.227 -    rec, from arith.ML, has fewer typing conditions **)
   3.228 -
   3.229 -val lemma = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans);
   3.230 -
   3.231 -Goal "nat_rec(0,a,b) = a";
   3.232 -by (rtac lemma 1);
   3.233 -by (rtac nat_case_0 1);
   3.234 -qed "nat_rec_0";
   3.235 -
   3.236 -Goal "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
   3.237 -by (rtac lemma 1);
   3.238 -by (asm_simp_tac (simpset() addsimps [vimage_singleton_iff]) 1);
   3.239 -qed "nat_rec_succ";
   3.240 -
   3.241 -(** The union of two natural numbers is a natural number -- their maximum **)
   3.242 -
   3.243 -Goal "[| i: nat; j: nat |] ==> i Un j: nat";
   3.244 -by (rtac (Un_least_lt RS ltD) 1);
   3.245 -by (REPEAT (ares_tac [ltI, Ord_nat] 1));
   3.246 -qed "Un_nat_type";
   3.247 -
   3.248 -Goal "[| i: nat; j: nat |] ==> i Int j: nat";
   3.249 -by (rtac (Int_greatest_lt RS ltD) 1);
   3.250 -by (REPEAT (ares_tac [ltI, Ord_nat] 1));
   3.251 -qed "Int_nat_type";
   3.252 -
   3.253 -Goal "nat ~= 0";
   3.254 -by (Blast_tac 1);
   3.255 -qed "nat_nonempty";
   3.256 -Addsimps [nat_nonempty];  (*needed to simplify unions over nat*)
     4.1 --- a/src/ZF/Nat.thy	Wed May 22 17:25:40 2002 +0200
     4.2 +++ b/src/ZF/Nat.thy	Wed May 22 17:26:34 2002 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  Natural numbers in Zermelo-Fraenkel Set Theory 
     4.5  *)
     4.6  
     4.7 -Nat = OrdQuant + Bool + mono +
     4.8 +theory Nat = OrdQuant + Bool + mono:
     4.9  
    4.10  constdefs
    4.11    nat :: i
    4.12 @@ -33,10 +33,253 @@
    4.13    Gt :: i
    4.14      "Gt == {<x,y>:nat*nat. y < x}"
    4.15  
    4.16 -  less_than :: i=>i
    4.17 +  less_than :: "i=>i"
    4.18      "less_than(n) == {i:nat.  i<n}"
    4.19  
    4.20 -  greater_than :: i=>i
    4.21 +  greater_than :: "i=>i"
    4.22      "greater_than(n) == {i:nat. n < i}"
    4.23  
    4.24 +lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})"
    4.25 +apply (rule bnd_monoI)
    4.26 +apply (cut_tac infinity, blast)
    4.27 +apply blast 
    4.28 +done
    4.29 +
    4.30 +(* nat = {0} Un {succ(x). x:nat} *)
    4.31 +lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold], standard]
    4.32 +
    4.33 +(** Type checking of 0 and successor **)
    4.34 +
    4.35 +lemma nat_0I [iff,TC]: "0 : nat"
    4.36 +apply (subst nat_unfold)
    4.37 +apply (rule singletonI [THEN UnI1])
    4.38 +done
    4.39 +
    4.40 +lemma nat_succI [intro!,TC]: "n : nat ==> succ(n) : nat"
    4.41 +apply (subst nat_unfold)
    4.42 +apply (erule RepFunI [THEN UnI2])
    4.43 +done
    4.44 +
    4.45 +lemma nat_1I [iff,TC]: "1 : nat"
    4.46 +by (rule nat_0I [THEN nat_succI])
    4.47 +
    4.48 +lemma nat_2I [iff,TC]: "2 : nat"
    4.49 +by (rule nat_1I [THEN nat_succI])
    4.50 +
    4.51 +lemma bool_subset_nat: "bool <= nat"
    4.52 +by (blast elim!: boolE)
    4.53 +
    4.54 +lemmas bool_into_nat = bool_subset_nat [THEN subsetD, standard]
    4.55 +
    4.56 +
    4.57 +(** Injectivity properties and induction **)
    4.58 +
    4.59 +(*Mathematical induction*)
    4.60 +lemma nat_induct:
    4.61 +    "[| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)"
    4.62 +apply (erule def_induct [OF nat_def nat_bnd_mono], blast)
    4.63 +done
    4.64 +
    4.65 +lemma natE:
    4.66 +    "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
    4.67 +apply (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) 
    4.68 +done
    4.69 +
    4.70 +lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
    4.71 +by (erule nat_induct, auto)
    4.72 +
    4.73 +(* i: nat ==> 0 le i; same thing as 0<succ(i)  *)
    4.74 +lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le, standard]
    4.75 +
    4.76 +(* i: nat ==> i le i; same thing as i<succ(i)  *)
    4.77 +lemmas nat_le_refl = nat_into_Ord [THEN le_refl, standard]
    4.78 +
    4.79 +lemma Ord_nat [iff]: "Ord(nat)"
    4.80 +apply (rule OrdI)
    4.81 +apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset])
    4.82 +apply (unfold Transset_def)
    4.83 +apply (rule ballI)
    4.84 +apply (erule nat_induct, auto) 
    4.85 +done
    4.86 +
    4.87 +lemma Limit_nat [iff]: "Limit(nat)"
    4.88 +apply (unfold Limit_def)
    4.89 +apply (safe intro!: ltI Ord_nat)
    4.90 +apply (erule ltD)
    4.91 +done
    4.92 +
    4.93 +lemma succ_natD [dest!]: "succ(i): nat ==> i: nat"
    4.94 +by (rule Ord_trans [OF succI1], auto)
    4.95 +
    4.96 +lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
    4.97 +by blast
    4.98 +
    4.99 +lemma nat_le_Limit: "Limit(i) ==> nat le i"
   4.100 +apply (rule subset_imp_le)
   4.101 +apply (simp_all add: Limit_is_Ord) 
   4.102 +apply (rule subsetI)
   4.103 +apply (erule nat_induct)
   4.104 + apply (erule Limit_has_0 [THEN ltD]) 
   4.105 +apply (blast intro: Limit_has_succ [THEN ltD] ltI Limit_is_Ord)
   4.106 +done
   4.107 +
   4.108 +(* [| succ(i): k;  k: nat |] ==> i: k *)
   4.109 +lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord]
   4.110 +
   4.111 +lemma lt_nat_in_nat: "[| m<n;  n: nat |] ==> m: nat"
   4.112 +apply (erule ltE)
   4.113 +apply (erule Ord_trans, assumption)
   4.114 +apply simp 
   4.115 +done
   4.116 +
   4.117 +lemma le_in_nat: "[| m le n; n:nat |] ==> m:nat"
   4.118 +by (blast dest!: lt_nat_in_nat)
   4.119 +
   4.120 +
   4.121 +(** Variations on mathematical induction **)
   4.122 +
   4.123 +(*complete induction*)
   4.124 +lemmas complete_induct = Ord_induct [OF _ Ord_nat]
   4.125 +
   4.126 +lemma nat_induct_from_lemma [rule_format]: 
   4.127 +    "[| n: nat;  m: nat;   
   4.128 +        !!x. [| x: nat;  m le x;  P(x) |] ==> P(succ(x)) |] 
   4.129 +     ==> m le n --> P(m) --> P(n)"
   4.130 +apply (erule nat_induct) 
   4.131 +apply (simp_all add: distrib_simps le0_iff le_succ_iff)
   4.132 +done
   4.133 +
   4.134 +(*Induction starting from m rather than 0*)
   4.135 +lemma nat_induct_from: 
   4.136 +    "[| m le n;  m: nat;  n: nat;   
   4.137 +        P(m);   
   4.138 +        !!x. [| x: nat;  m le x;  P(x) |] ==> P(succ(x)) |]
   4.139 +     ==> P(n)"
   4.140 +apply (blast intro: nat_induct_from_lemma)
   4.141 +done
   4.142 +
   4.143 +(*Induction suitable for subtraction and less-than*)
   4.144 +lemma diff_induct: 
   4.145 +    "[| m: nat;  n: nat;   
   4.146 +        !!x. x: nat ==> P(x,0);   
   4.147 +        !!y. y: nat ==> P(0,succ(y));   
   4.148 +        !!x y. [| x: nat;  y: nat;  P(x,y) |] ==> P(succ(x),succ(y)) |]
   4.149 +     ==> P(m,n)"
   4.150 +apply (erule_tac x = "m" in rev_bspec)
   4.151 +apply (erule nat_induct, simp) 
   4.152 +apply (rule ballI)
   4.153 +apply (rename_tac i j)
   4.154 +apply (erule_tac n=j in nat_induct, auto)  
   4.155 +done
   4.156 +
   4.157 +(** Induction principle analogous to trancl_induct **)
   4.158 +
   4.159 +lemma succ_lt_induct_lemma [rule_format]:
   4.160 +     "m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) -->  
   4.161 +                 (ALL n:nat. m<n --> P(m,n))"
   4.162 +apply (erule nat_induct)
   4.163 + apply (intro impI, rule nat_induct [THEN ballI])
   4.164 +   prefer 4 apply (intro impI, rule nat_induct [THEN ballI])
   4.165 +apply (auto simp add: le_iff) 
   4.166 +done
   4.167 +
   4.168 +lemma succ_lt_induct:
   4.169 +    "[| m<n;  n: nat;                                    
   4.170 +        P(m,succ(m));                                    
   4.171 +        !!x. [| x: nat;  P(m,x) |] ==> P(m,succ(x)) |]
   4.172 +     ==> P(m,n)"
   4.173 +by (blast intro: succ_lt_induct_lemma lt_nat_in_nat) 
   4.174 +
   4.175 +(** nat_case **)
   4.176 +
   4.177 +lemma nat_case_0 [simp]: "nat_case(a,b,0) = a"
   4.178 +by (unfold nat_case_def, blast)
   4.179 +
   4.180 +lemma nat_case_succ [simp]: "nat_case(a,b,succ(m)) = b(m)"
   4.181 +by (unfold nat_case_def, blast)
   4.182 +
   4.183 +lemma nat_case_type: 
   4.184 +    "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m)) |]
   4.185 +     ==> nat_case(a,b,n) : C(n)"
   4.186 +apply (erule nat_induct, auto) 
   4.187 +done
   4.188 +
   4.189 +
   4.190 +(** nat_rec -- used to define eclose and transrec, then obsolete
   4.191 +    rec, from arith.ML, has fewer typing conditions **)
   4.192 +
   4.193 +lemma nat_rec_0: "nat_rec(0,a,b) = a"
   4.194 +apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
   4.195 + apply (rule wf_Memrel) 
   4.196 +apply (rule nat_case_0)
   4.197 +done
   4.198 +
   4.199 +lemma nat_rec_succ: "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))"
   4.200 +apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
   4.201 + apply (rule wf_Memrel) 
   4.202 +apply (simp add: vimage_singleton_iff)
   4.203 +done
   4.204 +
   4.205 +(** The union of two natural numbers is a natural number -- their maximum **)
   4.206 +
   4.207 +lemma Un_nat_type: "[| i: nat; j: nat |] ==> i Un j: nat"
   4.208 +apply (rule Un_least_lt [THEN ltD])
   4.209 +apply (simp_all add: lt_def) 
   4.210 +done
   4.211 +
   4.212 +lemma Int_nat_type: "[| i: nat; j: nat |] ==> i Int j: nat"
   4.213 +apply (rule Int_greatest_lt [THEN ltD])
   4.214 +apply (simp_all add: lt_def) 
   4.215 +done
   4.216 +
   4.217 +(*needed to simplify unions over nat*)
   4.218 +lemma nat_nonempty [simp]: "nat ~= 0"
   4.219 +by blast
   4.220 +
   4.221 +ML
   4.222 +{*
   4.223 +val Le_def = thm "Le_def";
   4.224 +val Lt_def = thm "Lt_def";
   4.225 +val Ge_def = thm "Ge_def";
   4.226 +val Gt_def = thm "Gt_def";
   4.227 +val less_than_def = thm "less_than_def";
   4.228 +val greater_than_def = thm "greater_than_def";
   4.229 +
   4.230 +val nat_bnd_mono = thm "nat_bnd_mono";
   4.231 +val nat_unfold = thm "nat_unfold";
   4.232 +val nat_0I = thm "nat_0I";
   4.233 +val nat_succI = thm "nat_succI";
   4.234 +val nat_1I = thm "nat_1I";
   4.235 +val nat_2I = thm "nat_2I";
   4.236 +val bool_subset_nat = thm "bool_subset_nat";
   4.237 +val bool_into_nat = thm "bool_into_nat";
   4.238 +val nat_induct = thm "nat_induct";
   4.239 +val natE = thm "natE";
   4.240 +val nat_into_Ord = thm "nat_into_Ord";
   4.241 +val nat_0_le = thm "nat_0_le";
   4.242 +val nat_le_refl = thm "nat_le_refl";
   4.243 +val Ord_nat = thm "Ord_nat";
   4.244 +val Limit_nat = thm "Limit_nat";
   4.245 +val succ_natD = thm "succ_natD";
   4.246 +val nat_succ_iff = thm "nat_succ_iff";
   4.247 +val nat_le_Limit = thm "nat_le_Limit";
   4.248 +val succ_in_naturalD = thm "succ_in_naturalD";
   4.249 +val lt_nat_in_nat = thm "lt_nat_in_nat";
   4.250 +val le_in_nat = thm "le_in_nat";
   4.251 +val complete_induct = thm "complete_induct";
   4.252 +val nat_induct_from_lemma = thm "nat_induct_from_lemma";
   4.253 +val nat_induct_from = thm "nat_induct_from";
   4.254 +val diff_induct = thm "diff_induct";
   4.255 +val succ_lt_induct_lemma = thm "succ_lt_induct_lemma";
   4.256 +val succ_lt_induct = thm "succ_lt_induct";
   4.257 +val nat_case_0 = thm "nat_case_0";
   4.258 +val nat_case_succ = thm "nat_case_succ";
   4.259 +val nat_case_type = thm "nat_case_type";
   4.260 +val nat_rec_0 = thm "nat_rec_0";
   4.261 +val nat_rec_succ = thm "nat_rec_succ";
   4.262 +val Un_nat_type = thm "Un_nat_type";
   4.263 +val Int_nat_type = thm "Int_nat_type";
   4.264 +val nat_nonempty = thm "nat_nonempty";
   4.265 +*}
   4.266 +
   4.267  end