0

1 
(* Title: ZF/nat.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
For nat.thy. Natural numbers in ZermeloFraenkel Set Theory


7 
*)


8 


9 
open Nat;


10 


11 
goal Nat.thy "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})";


12 
by (rtac bnd_monoI 1);


13 
by (REPEAT (ares_tac [subset_refl, RepFun_mono, Un_mono] 2));


14 
by (cut_facts_tac [infinity] 1);


15 
by (fast_tac ZF_cs 1);


16 
val nat_bnd_mono = result();


17 


18 
(* nat = {0} Un {succ(x). x:nat} *)


19 
val nat_unfold = nat_bnd_mono RS (nat_def RS def_lfp_Tarski);


20 


21 
(** Type checking of 0 and successor **)


22 


23 
goal Nat.thy "0 : nat";


24 
by (rtac (nat_unfold RS ssubst) 1);


25 
by (rtac (singletonI RS UnI1) 1);


26 
val nat_0I = result();


27 


28 
val prems = goal Nat.thy "n : nat ==> succ(n) : nat";


29 
by (rtac (nat_unfold RS ssubst) 1);


30 
by (rtac (RepFunI RS UnI2) 1);


31 
by (resolve_tac prems 1);


32 
val nat_succI = result();


33 


34 
goalw Nat.thy [one_def] "1 : nat";


35 
by (rtac (nat_0I RS nat_succI) 1);


36 
val nat_1I = result();


37 


38 
goal Nat.thy "bool <= nat";


39 
by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1 ORELSE etac boolE 1));


40 
val bool_subset_nat = result();


41 


42 
val bool_into_nat = bool_subset_nat RS subsetD;


43 


44 


45 
(** Injectivity properties and induction **)


46 


47 
(*Mathematical induction*)


48 
val major::prems = goal Nat.thy


49 
"[ n: nat; P(0); !!x. [ x: nat; P(x) ] ==> P(succ(x)) ] ==> P(n)";


50 
by (rtac ([nat_def, nat_bnd_mono, major] MRS def_induct) 1);


51 
by (fast_tac (ZF_cs addIs prems) 1);


52 
val nat_induct = result();


53 


54 
(*Perform induction on n, then prove the n:nat subgoal using prems. *)


55 
fun nat_ind_tac a prems i =


56 
EVERY [res_inst_tac [("n",a)] nat_induct i,


57 
rename_last_tac a ["1"] (i+2),


58 
ares_tac prems i];


59 


60 
val major::prems = goal Nat.thy


61 
"[ n: nat; n=0 ==> P; !!x. [ x: nat; n=succ(x) ] ==> P ] ==> P";


62 
br (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1;


63 
by (DEPTH_SOLVE (eresolve_tac [singletonE,RepFunE] 1


64 
ORELSE ares_tac prems 1));


65 
val natE = result();


66 


67 
val prems = goal Nat.thy "n: nat ==> Ord(n)";


68 
by (nat_ind_tac "n" prems 1);


69 
by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));


70 
val naturals_are_ordinals = result();


71 


72 
goal Nat.thy "!!n. n: nat ==> n=0  0:n";


73 
by (etac nat_induct 1);


74 
by (fast_tac ZF_cs 1);


75 
by (fast_tac (ZF_cs addIs [naturals_are_ordinals RS Ord_0_mem_succ]) 1);


76 
val natE0 = result();


77 


78 
goal Nat.thy "Ord(nat)";


79 
by (rtac OrdI 1);


80 
by (etac (naturals_are_ordinals RS Ord_is_Transset) 2);


81 
by (rewtac Transset_def);


82 
by (rtac ballI 1);


83 
by (etac nat_induct 1);


84 
by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1));


85 
val Ord_nat = result();


86 


87 
(** Variations on mathematical induction **)


88 


89 
(*complete induction*)


90 
val complete_induct = Ord_nat RSN (2, Ord_induct);


91 


92 
val prems = goal Nat.thy


93 
"[ m: nat; n: nat; \


94 
\ !!x. [ x: nat; m<=x; P(x) ] ==> P(succ(x)) \


95 
\ ] ==> m <= n > P(m) > P(n)";


96 
by (nat_ind_tac "n" prems 1);


97 
by (ALLGOALS


98 
(ASM_SIMP_TAC


99 
(ZF_ss addrews (prems@distrib_rews@[subset_empty_iff, subset_succ_iff,


100 
Ord_nat RS Ord_in_Ord]))));


101 
val nat_induct_from_lemma = result();


102 


103 
(*Induction starting from m rather than 0*)


104 
val prems = goal Nat.thy


105 
"[ m <= n; m: nat; n: nat; \


106 
\ P(m); \


107 
\ !!x. [ x: nat; m<=x; P(x) ] ==> P(succ(x)) \


108 
\ ] ==> P(n)";


109 
by (rtac (nat_induct_from_lemma RS mp RS mp) 1);


110 
by (REPEAT (ares_tac prems 1));


111 
val nat_induct_from = result();


112 


113 
(*Induction suitable for subtraction and lessthan*)


114 
val prems = goal Nat.thy


115 
"[ m: nat; n: nat; \


116 
\ !!x. [ x: nat ] ==> P(x,0); \


117 
\ !!y. [ y: nat ] ==> P(0,succ(y)); \


118 
\ !!x y. [ x: nat; y: nat; P(x,y) ] ==> P(succ(x),succ(y)) \


119 
\ ] ==> P(m,n)";


120 
by (res_inst_tac [("x","m")] bspec 1);


121 
by (resolve_tac prems 2);


122 
by (nat_ind_tac "n" prems 1);


123 
by (rtac ballI 2);


124 
by (nat_ind_tac "x" [] 2);


125 
by (REPEAT (ares_tac (prems@[ballI]) 1 ORELSE etac bspec 1));


126 
val diff_induct = result();


127 


128 
(** nat_case **)


129 


130 
goalw Nat.thy [nat_case_def] "nat_case(0,a,b) = a";


131 
by (fast_tac (ZF_cs addIs [the_equality]) 1);


132 
val nat_case_0 = result();


133 


134 
goalw Nat.thy [nat_case_def] "nat_case(succ(m),a,b) = b(m)";


135 
by (fast_tac (ZF_cs addIs [the_equality]) 1);


136 
val nat_case_succ = result();


137 


138 
val major::prems = goal Nat.thy


139 
"[ n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) \


140 
\ ] ==> nat_case(n,a,b) : C(n)";


141 
by (rtac (major RS nat_induct) 1);


142 
by (REPEAT (resolve_tac [nat_case_0 RS ssubst,


143 
nat_case_succ RS ssubst] 1


144 
THEN resolve_tac prems 1));


145 
by (assume_tac 1);


146 
val nat_case_type = result();


147 


148 
val prems = goalw Nat.thy [nat_case_def]


149 
"[ n=n'; a=a'; !!m z. b(m)=b'(m) \


150 
\ ] ==> nat_case(n,a,b)=nat_case(n',a',b')";


151 
by (REPEAT (resolve_tac [the_cong,disj_cong,ex_cong] 1


152 
ORELSE EVERY1 (map rtac ((prems RL [ssubst]) @ [iff_refl]))));


153 
val nat_case_cong = result();


154 


155 


156 
(** nat_rec  used to define eclose and transrec, then obsolete **)


157 


158 
val nat_rec_trans = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans);


159 


160 
goal Nat.thy "nat_rec(0,a,b) = a";


161 
by (rtac nat_rec_trans 1);


162 
by (rtac nat_case_0 1);


163 
val nat_rec_0 = result();


164 


165 
val [prem] = goal Nat.thy


166 
"m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";


167 
val nat_rec_ss = ZF_ss


168 
addcongs (mk_typed_congs Nat.thy [("b", "[i,i]=>i")])


169 
addrews [prem, nat_case_succ, nat_succI, Memrel_iff,


170 
vimage_singleton_iff];


171 
by (rtac nat_rec_trans 1);


172 
by (SIMP_TAC nat_rec_ss 1);


173 
val nat_rec_succ = result();


174 


175 
(** The union of two natural numbers is a natural number  their maximum **)


176 


177 
(* [ ?i : nat; ?j : nat ] ==> ?i Un ?j : nat *)


178 
val Un_nat_type = standard (Ord_nat RSN (3,Ord_member_UnI));


179 


180 
(* [ ?i : nat; ?j : nat ] ==> ?i Int ?j : nat *)


181 
val Int_nat_type = standard (Ord_nat RSN (3,Ord_member_IntI));


182 
