80 Goalw [integ_def,quotient_def,znat_def] |
80 Goalw [integ_def,quotient_def,znat_def] |
81 "m : nat ==> $#m : integ"; |
81 "m : nat ==> $#m : integ"; |
82 by (fast_tac (claset() addSIs [nat_0I]) 1); |
82 by (fast_tac (claset() addSIs [nat_0I]) 1); |
83 qed "znat_type"; |
83 qed "znat_type"; |
84 |
84 |
85 Goalw [znat_def] "[| $#m = $#n; n: nat |] ==> m=n"; |
85 Addsimps [znat_type]; |
86 by (dtac eq_intrelD 1); |
86 |
|
87 Goalw [znat_def] "[| $#m = $#n; m: nat |] ==> m=n"; |
|
88 by (dtac (sym RS eq_intrelD) 1); |
87 by (typechk_tac [nat_0I, SigmaI]); |
89 by (typechk_tac [nat_0I, SigmaI]); |
88 by (Asm_full_simp_tac 1); |
90 by (Asm_full_simp_tac 1); |
89 qed "znat_inject"; |
91 qed "znat_inject"; |
90 |
92 |
|
93 AddSDs [znat_inject]; |
|
94 |
|
95 Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; |
|
96 by (Blast_tac 1); |
|
97 qed "znat_znat_eq"; |
|
98 Addsimps [znat_znat_eq]; |
91 |
99 |
92 (**** zminus: unary negation on integ ****) |
100 (**** zminus: unary negation on integ ****) |
93 |
101 |
94 Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})"; |
102 Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})"; |
95 by Safe_tac; |
103 by Safe_tac; |
136 by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1); |
146 by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1); |
137 by (fast_tac (claset() addss |
147 by (fast_tac (claset() addss |
138 (simpset() addsimps [add_le_self2 RS le_imp_not_lt])) 1); |
148 (simpset() addsimps [add_le_self2 RS le_imp_not_lt])) 1); |
139 qed "not_znegative_znat"; |
149 qed "not_znegative_znat"; |
140 |
150 |
|
151 Addsimps [not_znegative_znat]; |
|
152 AddSEs [not_znegative_znat RS notE]; |
|
153 |
141 Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))"; |
154 Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))"; |
142 by (asm_simp_tac (simpset() addsimps [zminus]) 1); |
155 by (asm_simp_tac (simpset() addsimps [zminus]) 1); |
143 by (blast_tac (claset() addIs [nat_0_le]) 1); |
156 by (blast_tac (claset() addIs [nat_0_le]) 1); |
144 qed "znegative_zminus_znat"; |
157 qed "znegative_zminus_znat"; |
145 |
158 |
|
159 Addsimps [znegative_zminus_znat]; |
|
160 |
|
161 Goalw [znegative_def, znat_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0"; |
|
162 by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1); |
|
163 be natE 1; |
|
164 by (dres_inst_tac [("x","0")] spec 2); |
|
165 by Auto_tac; |
|
166 qed "not_znegative_imp_zero"; |
146 |
167 |
147 (**** zmagnitude: magnitide of an integer, as a natural number ****) |
168 (**** zmagnitude: magnitide of an integer, as a natural number ****) |
148 |
169 |
149 Goalw [congruent_def] "congruent(intrel, %<x,y>. (y#-x) #+ (x#-y))"; |
170 Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n"; |
150 by Safe_tac; |
171 by Auto_tac; |
151 by (ALLGOALS Asm_simp_tac); |
172 qed "zmagnitude_znat"; |
152 by (etac rev_mp 1); |
173 |
153 by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1 THEN |
174 Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n"; |
154 REPEAT (assume_tac 1)); |
175 by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset())); |
155 by (Asm_simp_tac 3); |
176 qed "zmagnitude_zminus_znat"; |
156 by (asm_simp_tac (*this one's very sensitive to order of rewrites*) |
177 |
157 (simpset() delsimps [add_succ_right] |
178 Addsimps [zmagnitude_znat, zmagnitude_zminus_znat]; |
158 addsimps [diff_add_inverse,diff_add_0]) 2); |
179 |
159 by (Asm_simp_tac 1); |
180 Goalw [zmagnitude_def] "zmagnitude(z) : nat"; |
160 by (rtac impI 1); |
181 br theI2 1; |
161 by (etac subst 1); |
182 by Auto_tac; |
162 by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1 THEN |
|
163 REPEAT (assume_tac 1)); |
|
164 by (asm_simp_tac (simpset() addsimps [diff_add_inverse, diff_add_0]) 1); |
|
165 qed "zmagnitude_congruent"; |
|
166 |
|
167 |
|
168 (*Resolve th against the corresponding facts for zmagnitude*) |
|
169 val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent]; |
|
170 |
|
171 Goalw [integ_def,zmagnitude_def] |
|
172 "z : integ ==> zmagnitude(z) : nat"; |
|
173 by (typechk_tac [split_type, zmagnitude_ize UN_equiv_class_type, |
|
174 add_type, diff_type]); |
|
175 qed "zmagnitude_type"; |
183 qed "zmagnitude_type"; |
176 |
184 |
177 Goalw [zmagnitude_def] |
185 Goalw [integ_def, znegative_def, znat_def] |
178 "[| x: nat; y: nat |] \ |
186 "[| z: integ; ~ znegative(z) |] ==> EX n:nat. z = $# n"; |
179 \ ==> zmagnitude (intrel``{<x,y>}) = (y #- x) #+ (x #- y)"; |
187 by (auto_tac(claset() , simpset() addsimps [image_singleton_iff])); |
180 by (asm_simp_tac |
188 by (rename_tac "i j" 1); |
181 (simpset() addsimps [zmagnitude_ize UN_equiv_class, SigmaI]) 1); |
189 by (dres_inst_tac [("x", "i")] spec 1); |
182 qed "zmagnitude"; |
190 by (dres_inst_tac [("x", "j")] spec 1); |
183 |
191 br bexI 1; |
184 Goalw [znat_def] "n: nat ==> zmagnitude($# n) = n"; |
192 br (add_diff_inverse2 RS sym) 1; |
185 by (asm_simp_tac (simpset() addsimps [zmagnitude]) 1); |
193 by Auto_tac; |
186 qed "zmagnitude_znat"; |
194 by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1); |
187 |
195 qed "not_zneg_znat"; |
188 Goalw [znat_def] "n: nat ==> zmagnitude($~ $# n) = n"; |
196 |
189 by (asm_simp_tac (simpset() addsimps [zmagnitude, zminus]) 1); |
197 Goal "[| z: integ; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; |
190 qed "zmagnitude_zminus_znat"; |
198 bd not_zneg_znat 1; |
|
199 by Auto_tac; |
|
200 qed "not_zneg_mag"; |
|
201 |
|
202 Addsimps [not_zneg_mag]; |
|
203 |
|
204 |
|
205 Goalw [integ_def, znegative_def, znat_def] |
|
206 "[| z: integ; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; |
|
207 by (auto_tac(claset() addSDs [less_imp_Suc_add], |
|
208 simpset() addsimps [zminus, image_singleton_iff])); |
|
209 by (rename_tac "m n j k" 1); |
|
210 by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1); |
|
211 by (rotate_tac ~2 2); |
|
212 by (asm_full_simp_tac (simpset() addsimps add_ac) 2); |
|
213 by (blast_tac (claset() addSDs [add_left_cancel]) 1); |
|
214 qed "zneg_znat"; |
|
215 |
|
216 Goal "[| z: integ; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; |
|
217 bd zneg_znat 1; |
|
218 by Auto_tac; |
|
219 qed "zneg_mag"; |
|
220 |
|
221 Addsimps [zneg_mag]; |
191 |
222 |
192 |
223 |
193 (**** zadd: addition on integ ****) |
224 (**** zadd: addition on integ ****) |
194 |
225 |
195 (** Congruence property for addition **) |
226 (** Congruence property for addition **) |
331 Goalw [integ_def] "[| z: integ; w: integ |] ==> ($~ z) $* w = $~ (z $* w)"; |
364 Goalw [integ_def] "[| z: integ; w: integ |] ==> ($~ z) $* w = $~ (z $* w)"; |
332 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
365 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
333 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
366 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
334 qed "zmult_zminus"; |
367 qed "zmult_zminus"; |
335 |
368 |
|
369 Addsimps [zmult_0, zmult_1, zmult_zminus]; |
|
370 |
336 Goalw [integ_def] "[| z: integ; w: integ |] ==> ($~ z) $* ($~ w) = (z $* w)"; |
371 Goalw [integ_def] "[| z: integ; w: integ |] ==> ($~ z) $* ($~ w) = (z $* w)"; |
337 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
372 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
338 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
373 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
339 qed "zmult_zminus_zminus"; |
374 qed "zmult_zminus_zminus"; |
340 |
375 |