author  lcp 
Fri, 23 Dec 1994 16:30:35 +0100  
changeset 829  ba28811c3496 
parent 760  f0200e91b272 
child 1461  6bcb44e4d6e5 
permissions  rwrr 
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); 

760  16 
qed "nat_bnd_mono"; 
0  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); 

760  26 
qed "nat_0I"; 
0  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); 

760  32 
qed "nat_succI"; 
0  33 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

34 
goal Nat.thy "1 : nat"; 
0  35 
by (rtac (nat_0I RS nat_succI) 1); 
760  36 
qed "nat_1I"; 
0  37 

829  38 
goal Nat.thy "2 : nat"; 
39 
by (rtac (nat_1I RS nat_succI) 1); 

40 
qed "nat_2I"; 

41 

0  42 
goal Nat.thy "bool <= nat"; 
120  43 
by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1 
44 
ORELSE eresolve_tac [boolE,ssubst] 1)); 

760  45 
qed "bool_subset_nat"; 
0  46 

47 
val bool_into_nat = bool_subset_nat RS subsetD; 

48 

49 

50 
(** Injectivity properties and induction **) 

51 

52 
(*Mathematical induction*) 

53 
val major::prems = goal Nat.thy 

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

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

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

760  57 
qed "nat_induct"; 
0  58 

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

60 
fun nat_ind_tac a prems i = 

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

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

63 
ares_tac prems i]; 

64 

65 
val major::prems = goal Nat.thy 

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

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

67 
by (rtac (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1); 
0  68 
by (DEPTH_SOLVE (eresolve_tac [singletonE,RepFunE] 1 
69 
ORELSE ares_tac prems 1)); 

760  70 
qed "natE"; 
0  71 

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

73 
by (nat_ind_tac "n" prems 1); 

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

760  75 
qed "nat_into_Ord"; 
0  76 

30  77 
(* i: nat ==> 0 le i *) 
435  78 
val nat_0_le = nat_into_Ord RS Ord_0_le; 
79 

80 
val nat_le_refl = nat_into_Ord RS le_refl; 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

81 

0  82 
goal Nat.thy "Ord(nat)"; 
83 
by (rtac OrdI 1); 

435  84 
by (etac (nat_into_Ord RS Ord_is_Transset) 2); 
0  85 
by (rewtac Transset_def); 
86 
by (rtac ballI 1); 

87 
by (etac nat_induct 1); 

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

760  89 
qed "Ord_nat"; 
0  90 

435  91 
goalw Nat.thy [Limit_def] "Limit(nat)"; 
92 
by (safe_tac (ZF_cs addSIs [ltI, nat_0I, nat_1I, nat_succI, Ord_nat])); 

93 
by (etac ltD 1); 

760  94 
qed "Limit_nat"; 
435  95 

484  96 
goal Nat.thy "!!i. Limit(i) ==> nat le i"; 
97 
by (resolve_tac [subset_imp_le] 1); 

98 
by (rtac subsetI 1); 

99 
by (eresolve_tac [nat_induct] 1); 

100 
by (fast_tac (ZF_cs addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2); 

101 
by (REPEAT (ares_tac [Limit_has_0 RS ltD, 

102 
Ord_nat, Limit_is_Ord] 1)); 

760  103 
qed "nat_le_Limit"; 
484  104 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

105 
(* succ(i): nat ==> i: nat *) 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

106 
val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans; 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

107 

6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

108 
(* [ succ(i): k; k: nat ] ==> i: k *) 
435  109 
val succ_in_naturalD = [succI1, asm_rl, nat_into_Ord] MRS Ord_trans; 
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

110 

30  111 
goal Nat.thy "!!m n. [ m<n; n: nat ] ==> m: nat"; 
112 
by (etac ltE 1); 

113 
by (etac (Ord_nat RSN (3,Ord_trans)) 1); 

114 
by (assume_tac 1); 

760  115 
qed "lt_nat_in_nat"; 
30  116 

117 

0  118 
(** Variations on mathematical induction **) 
119 

120 
(*complete induction*) 

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

122 

123 
val prems = goal Nat.thy 

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

30  125 
\ !!x. [ x: nat; m le x; P(x) ] ==> P(succ(x)) \ 
126 
\ ] ==> m le n > P(m) > P(n)"; 

0  127 
by (nat_ind_tac "n" prems 1); 
128 
by (ALLGOALS 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

129 
(asm_simp_tac 
30  130 
(ZF_ss addsimps (prems@distrib_rews@[le0_iff, le_succ_iff])))); 
760  131 
qed "nat_induct_from_lemma"; 
0  132 

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

134 
val prems = goal Nat.thy 

30  135 
"[ m le n; m: nat; n: nat; \ 
0  136 
\ P(m); \ 
30  137 
\ !!x. [ x: nat; m le x; P(x) ] ==> P(succ(x)) \ 
0  138 
\ ] ==> P(n)"; 
139 
by (rtac (nat_induct_from_lemma RS mp RS mp) 1); 

140 
by (REPEAT (ares_tac prems 1)); 

760  141 
qed "nat_induct_from"; 
0  142 

143 
(*Induction suitable for subtraction and lessthan*) 

144 
val prems = goal Nat.thy 

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

30  146 
\ !!x. x: nat ==> P(x,0); \ 
147 
\ !!y. y: nat ==> P(0,succ(y)); \ 

0  148 
\ !!x y. [ x: nat; y: nat; P(x,y) ] ==> P(succ(x),succ(y)) \ 
149 
\ ] ==> P(m,n)"; 

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

151 
by (resolve_tac prems 2); 

152 
by (nat_ind_tac "n" prems 1); 

153 
by (rtac ballI 2); 

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

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

760  156 
qed "diff_induct"; 
0  157 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

158 
(** Induction principle analogous to trancl_induct **) 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

159 

6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

160 
goal Nat.thy 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

161 
"!!m. m: nat ==> P(m,succ(m)) > (ALL x: nat. P(m,x) > P(m,succ(x))) > \ 
30  162 
\ (ALL n:nat. m<n > P(m,n))"; 
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

163 
by (etac nat_induct 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

164 
by (ALLGOALS 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

165 
(EVERY' [rtac (impI RS impI), rtac (nat_induct RS ballI), assume_tac, 
30  166 
fast_tac lt_cs, fast_tac lt_cs])); 
760  167 
qed "succ_lt_induct_lemma"; 
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

168 

6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

169 
val prems = goal Nat.thy 
30  170 
"[ m<n; n: nat; \ 
171 
\ P(m,succ(m)); \ 

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

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

173 
\ ] ==> P(m,n)"; 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

174 
by (res_inst_tac [("P4","P")] 
30  175 
(succ_lt_induct_lemma RS mp RS mp RS bspec RS mp) 1); 
176 
by (REPEAT (ares_tac (prems @ [ballI, impI, lt_nat_in_nat]) 1)); 

760  177 
qed "succ_lt_induct"; 
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

178 

0  179 
(** nat_case **) 
180 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

181 
goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a"; 
0  182 
by (fast_tac (ZF_cs addIs [the_equality]) 1); 
760  183 
qed "nat_case_0"; 
0  184 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

185 
goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)"; 
0  186 
by (fast_tac (ZF_cs addIs [the_equality]) 1); 
760  187 
qed "nat_case_succ"; 
0  188 

189 
val major::prems = goal Nat.thy 

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

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

191 
\ ] ==> nat_case(a,b,n) : C(n)"; 
0  192 
by (rtac (major RS nat_induct) 1); 
30  193 
by (ALLGOALS 
194 
(asm_simp_tac (ZF_ss addsimps (prems @ [nat_case_0, nat_case_succ])))); 

760  195 
qed "nat_case_type"; 
0  196 

197 

30  198 
(** nat_rec  used to define eclose and transrec, then obsolete; 
199 
rec, from arith.ML, has fewer typing conditions **) 

0  200 

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

202 

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

204 
by (rtac nat_rec_trans 1); 

205 
by (rtac nat_case_0 1); 

760  206 
qed "nat_rec_0"; 
0  207 

208 
val [prem] = goal Nat.thy 

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

210 
by (rtac nat_rec_trans 1); 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

211 
by (simp_tac (ZF_ss addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

212 
vimage_singleton_iff]) 1); 
760  213 
qed "nat_rec_succ"; 
0  214 

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

216 

30  217 
goal Nat.thy "!!i j. [ i: nat; j: nat ] ==> i Un j: nat"; 
218 
by (rtac (Un_least_lt RS ltD) 1); 

219 
by (REPEAT (ares_tac [ltI, Ord_nat] 1)); 

760  220 
qed "Un_nat_type"; 
0  221 

30  222 
goal Nat.thy "!!i j. [ i: nat; j: nat ] ==> i Int j: nat"; 
223 
by (rtac (Int_greatest_lt RS ltD) 1); 

224 
by (REPEAT (ares_tac [ltI, Ord_nat] 1)); 

760  225 
qed "Int_nat_type"; 