author  lcp 
Fri, 17 Sep 1993 16:16:38 +0200  
changeset 6  8ce8c4d13d4d 
parent 0  a5a9c433f639 
child 15  6c6d2f6e3185 
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); 

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 

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

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

99 
(ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff, 
0  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 

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

130 
goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a"; 
0  131 
by (fast_tac (ZF_cs addIs [the_equality]) 1); 
132 
val nat_case_0 = result(); 

133 

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

134 
goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)"; 
0  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)) \ 

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

140 
\ ] ==> nat_case(a,b,n) : C(n)"; 
0  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 

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

150 

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

152 

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

154 
by (rtac nat_rec_trans 1); 

155 
by (rtac nat_case_0 1); 

156 
val nat_rec_0 = result(); 

157 

158 
val [prem] = goal Nat.thy 

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

160 
val nat_rec_ss = ZF_ss 

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

161 
addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

162 
vimage_singleton_iff]; 
0  163 
by (rtac nat_rec_trans 1); 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

164 
by (simp_tac nat_rec_ss 1); 
0  165 
val nat_rec_succ = result(); 
166 

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

168 

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

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

171 

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

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

174 