author | paulson |
Fri, 18 Sep 1998 15:15:40 +0200 | |
changeset 5507 | 2fd99b2d41e1 |
parent 5268 | 59ef39008514 |
child 5525 | 896f8234b864 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/integ.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
1614 | 6 |
The integers as equivalence classes over nat*nat. |
0 | 7 |
|
8 |
Could also prove... |
|
9 |
"znegative(z) ==> $# zmagnitude(z) = $~ z" |
|
10 |
"~ znegative(z) ==> $# zmagnitude(z) = z" |
|
11 |
$< is a linear ordering |
|
12 |
$+ and $* are monotonic wrt $< |
|
13 |
*) |
|
14 |
||
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
15 |
AddSEs [quotientE]; |
0 | 16 |
|
17 |
(*** Proving that intrel is an equivalence relation ***) |
|
18 |
||
19 |
(*By luck, requires no typing premises for y1, y2,y3*) |
|
20 |
val eqa::eqb::prems = goal Arith.thy |
|
21 |
"[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2; \ |
|
22 |
\ x1: nat; x2: nat; x3: nat |] ==> x1 #+ y3 = x3 #+ y1"; |
|
23 |
by (res_inst_tac [("k","x2")] add_left_cancel 1); |
|
438 | 24 |
by (resolve_tac prems 2); |
25 |
by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems); |
|
2034 | 26 |
by (stac eqb 1); |
438 | 27 |
by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems); |
2034 | 28 |
by (stac eqa 1); |
438 | 29 |
by (rtac (add_left_commute) 1 THEN typechk_tac prems); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
30 |
qed "integ_trans_lemma"; |
0 | 31 |
|
32 |
(** Natural deduction for intrel **) |
|
33 |
||
5068 | 34 |
Goalw [intrel_def] |
438 | 35 |
"<<x1,y1>,<x2,y2>>: intrel <-> \ |
36 |
\ x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1"; |
|
2469 | 37 |
by (Fast_tac 1); |
760 | 38 |
qed "intrel_iff"; |
438 | 39 |
|
5068 | 40 |
Goalw [intrel_def] |
5137 | 41 |
"[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ |
438 | 42 |
\ <<x1,y1>,<x2,y2>>: intrel"; |
4091 | 43 |
by (fast_tac (claset() addIs prems) 1); |
760 | 44 |
qed "intrelI"; |
0 | 45 |
|
46 |
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*) |
|
5068 | 47 |
Goalw [intrel_def] |
0 | 48 |
"p: intrel --> (EX x1 y1 x2 y2. \ |
49 |
\ p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \ |
|
50 |
\ x1: nat & y1: nat & x2: nat & y2: nat)"; |
|
2469 | 51 |
by (Fast_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
52 |
qed "intrelE_lemma"; |
0 | 53 |
|
54 |
val [major,minor] = goal Integ.thy |
|
55 |
"[| p: intrel; \ |
|
56 |
\ !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>; x1#+y2 = x2#+y1; \ |
|
57 |
\ x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \ |
|
58 |
\ ==> Q"; |
|
59 |
by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1); |
|
60 |
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); |
|
760 | 61 |
qed "intrelE"; |
0 | 62 |
|
2469 | 63 |
AddSIs [intrelI]; |
64 |
AddSEs [intrelE]; |
|
0 | 65 |
|
5068 | 66 |
Goalw [equiv_def, refl_def, sym_def, trans_def] |
438 | 67 |
"equiv(nat*nat, intrel)"; |
4091 | 68 |
by (fast_tac (claset() addSEs [sym, integ_trans_lemma]) 1); |
760 | 69 |
qed "equiv_intrel"; |
0 | 70 |
|
71 |
||
2469 | 72 |
Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff, |
73 |
add_0_right, add_succ_right]; |
|
74 |
Addcongs [conj_cong]; |
|
0 | 75 |
|
438 | 76 |
val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class); |
0 | 77 |
|
78 |
(** znat: the injection from nat to integ **) |
|
79 |
||
5068 | 80 |
Goalw [integ_def,quotient_def,znat_def] |
5137 | 81 |
"m : nat ==> $#m : integ"; |
4091 | 82 |
by (fast_tac (claset() addSIs [nat_0I]) 1); |
760 | 83 |
qed "znat_type"; |
0 | 84 |
|
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
85 |
Addsimps [znat_type]; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
86 |
|
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
87 |
Goalw [znat_def] "[| $#m = $#n; m: nat |] ==> m=n"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
88 |
by (dtac (sym RS eq_intrelD) 1); |
438 | 89 |
by (typechk_tac [nat_0I, SigmaI]); |
2469 | 90 |
by (Asm_full_simp_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
91 |
qed "znat_inject"; |
0 | 92 |
|
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
93 |
AddSDs [znat_inject]; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
94 |
|
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
95 |
Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
96 |
by (Blast_tac 1); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
97 |
qed "znat_znat_eq"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
98 |
Addsimps [znat_znat_eq]; |
0 | 99 |
|
100 |
(**** zminus: unary negation on integ ****) |
|
101 |
||
5137 | 102 |
Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})"; |
4152 | 103 |
by Safe_tac; |
4091 | 104 |
by (asm_full_simp_tac (simpset() addsimps add_ac) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
105 |
qed "zminus_congruent"; |
0 | 106 |
|
107 |
(*Resolve th against the corresponding facts for zminus*) |
|
108 |
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent]; |
|
109 |
||
5137 | 110 |
Goalw [integ_def,zminus_def] "z : integ ==> $~z : integ"; |
438 | 111 |
by (typechk_tac [split_type, SigmaI, zminus_ize UN_equiv_class_type, |
1461 | 112 |
quotientI]); |
760 | 113 |
qed "zminus_type"; |
0 | 114 |
|
5137 | 115 |
Goalw [integ_def,zminus_def] "[| $~z = $~w; z: integ; w: integ |] ==> z=w"; |
438 | 116 |
by (etac (zminus_ize UN_equiv_class_inject) 1); |
4152 | 117 |
by Safe_tac; |
438 | 118 |
(*The setloop is only needed because assumptions are in the wrong order!*) |
4091 | 119 |
by (asm_full_simp_tac (simpset() addsimps add_ac |
1461 | 120 |
setloop dtac eq_intrelD) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
121 |
qed "zminus_inject"; |
0 | 122 |
|
5068 | 123 |
Goalw [zminus_def] |
5137 | 124 |
"[| x: nat; y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}"; |
4091 | 125 |
by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1); |
760 | 126 |
qed "zminus"; |
0 | 127 |
|
5137 | 128 |
Goalw [integ_def] "z : integ ==> $~ ($~ z) = z"; |
0 | 129 |
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
4091 | 130 |
by (asm_simp_tac (simpset() addsimps [zminus]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
131 |
qed "zminus_zminus"; |
0 | 132 |
|
5068 | 133 |
Goalw [integ_def, znat_def] "$~ ($#0) = $#0"; |
4091 | 134 |
by (simp_tac (simpset() addsimps [zminus]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
135 |
qed "zminus_0"; |
0 | 136 |
|
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
137 |
Addsimps [zminus_zminus, zminus_0]; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
138 |
|
0 | 139 |
|
140 |
(**** znegative: the test for negative integers ****) |
|
141 |
||
1021 | 142 |
(*No natural number is negative!*) |
5068 | 143 |
Goalw [znegative_def, znat_def] "~ znegative($# n)"; |
4152 | 144 |
by Safe_tac; |
1021 | 145 |
by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1); |
146 |
by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1); |
|
4091 | 147 |
by (fast_tac (claset() addss |
148 |
(simpset() addsimps [add_le_self2 RS le_imp_not_lt])) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
149 |
qed "not_znegative_znat"; |
0 | 150 |
|
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
151 |
Addsimps [not_znegative_znat]; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
152 |
AddSEs [not_znegative_znat RS notE]; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
153 |
|
5137 | 154 |
Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))"; |
4091 | 155 |
by (asm_simp_tac (simpset() addsimps [zminus]) 1); |
5168 | 156 |
by (blast_tac (claset() addIs [nat_0_le]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
157 |
qed "znegative_zminus_znat"; |
0 | 158 |
|
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
159 |
Addsimps [znegative_zminus_znat]; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
160 |
|
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
161 |
Goalw [znegative_def, znat_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
162 |
by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
163 |
be natE 1; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
164 |
by (dres_inst_tac [("x","0")] spec 2); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
165 |
by Auto_tac; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
166 |
qed "not_znegative_imp_zero"; |
0 | 167 |
|
168 |
(**** zmagnitude: magnitide of an integer, as a natural number ****) |
|
169 |
||
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
170 |
Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
171 |
by Auto_tac; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
172 |
qed "zmagnitude_znat"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
173 |
|
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
174 |
Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
175 |
by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset())); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
176 |
qed "zmagnitude_zminus_znat"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
177 |
|
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
178 |
Addsimps [zmagnitude_znat, zmagnitude_zminus_znat]; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
179 |
|
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
180 |
Goalw [zmagnitude_def] "zmagnitude(z) : nat"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
181 |
br theI2 1; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
182 |
by Auto_tac; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
183 |
qed "zmagnitude_type"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
184 |
|
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
185 |
Goalw [integ_def, znegative_def, znat_def] |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
186 |
"[| z: integ; ~ znegative(z) |] ==> EX n:nat. z = $# n"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
187 |
by (auto_tac(claset() , simpset() addsimps [image_singleton_iff])); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
188 |
by (rename_tac "i j" 1); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
189 |
by (dres_inst_tac [("x", "i")] spec 1); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
190 |
by (dres_inst_tac [("x", "j")] spec 1); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
191 |
br bexI 1; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
192 |
br (add_diff_inverse2 RS sym) 1; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
193 |
by Auto_tac; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
194 |
by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
195 |
qed "not_zneg_znat"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
196 |
|
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
197 |
Goal "[| z: integ; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
198 |
bd not_zneg_znat 1; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
199 |
by Auto_tac; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
200 |
qed "not_zneg_mag"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
201 |
|
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
202 |
Addsimps [not_zneg_mag]; |
0 | 203 |
|
438 | 204 |
|
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
205 |
Goalw [integ_def, znegative_def, znat_def] |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
206 |
"[| z: integ; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
207 |
by (auto_tac(claset() addSDs [less_imp_Suc_add], |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
208 |
simpset() addsimps [zminus, image_singleton_iff])); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
209 |
by (rename_tac "m n j k" 1); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
210 |
by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
211 |
by (rotate_tac ~2 2); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
212 |
by (asm_full_simp_tac (simpset() addsimps add_ac) 2); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
213 |
by (blast_tac (claset() addSDs [add_left_cancel]) 1); |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
214 |
qed "zneg_znat"; |
0 | 215 |
|
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
216 |
Goal "[| z: integ; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
217 |
bd zneg_znat 1; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
218 |
by Auto_tac; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
219 |
qed "zneg_mag"; |
0 | 220 |
|
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
221 |
Addsimps [zneg_mag]; |
0 | 222 |
|
223 |
||
224 |
(**** zadd: addition on integ ****) |
|
225 |
||
226 |
(** Congruence property for addition **) |
|
227 |
||
5068 | 228 |
Goalw [congruent2_def] |
1461 | 229 |
"congruent2(intrel, %z1 z2. \ |
1110
756aa2e81f6e
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
1021
diff
changeset
|
230 |
\ let <x1,y1>=z1; <x2,y2>=z2 \ |
756aa2e81f6e
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
1021
diff
changeset
|
231 |
\ in intrel``{<x1#+x2, y1#+y2>})"; |
0 | 232 |
(*Proof via congruent2_commuteI seems longer*) |
4152 | 233 |
by Safe_tac; |
4091 | 234 |
by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1); |
438 | 235 |
(*The rest should be trivial, but rearranging terms is hard; |
236 |
add_ac does not help rewriting with the assumptions.*) |
|
237 |
by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1); |
|
238 |
by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3); |
|
0 | 239 |
by (typechk_tac [add_type]); |
4091 | 240 |
by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
241 |
qed "zadd_congruent2"; |
0 | 242 |
|
243 |
(*Resolve th against the corresponding facts for zadd*) |
|
244 |
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; |
|
245 |
||
5137 | 246 |
Goalw [integ_def,zadd_def] "[| z: integ; w: integ |] ==> z $+ w : integ"; |
1110
756aa2e81f6e
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
1021
diff
changeset
|
247 |
by (rtac (zadd_ize UN_equiv_class_type2) 1); |
4091 | 248 |
by (simp_tac (simpset() addsimps [Let_def]) 3); |
1110
756aa2e81f6e
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
1021
diff
changeset
|
249 |
by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
250 |
qed "zadd_type"; |
0 | 251 |
|
5068 | 252 |
Goalw [zadd_def] |
5137 | 253 |
"[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ |
1461 | 254 |
\ (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = \ |
255 |
\ intrel `` {<x1#+x2, y1#+y2>}"; |
|
4091 | 256 |
by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1); |
257 |
by (simp_tac (simpset() addsimps [Let_def]) 1); |
|
760 | 258 |
qed "zadd"; |
0 | 259 |
|
5137 | 260 |
Goalw [integ_def,znat_def] "z : integ ==> $#0 $+ z = z"; |
438 | 261 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
4091 | 262 |
by (asm_simp_tac (simpset() addsimps [zadd]) 1); |
760 | 263 |
qed "zadd_0"; |
0 | 264 |
|
5137 | 265 |
Goalw [integ_def] "[| z: integ; w: integ |] ==> $~ (z $+ w) = $~ z $+ $~ w"; |
438 | 266 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
4091 | 267 |
by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
268 |
qed "zminus_zadd_distrib"; |
0 | 269 |
|
5137 | 270 |
Goalw [integ_def] "[| z: integ; w: integ |] ==> z $+ w = w $+ z"; |
438 | 271 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
4091 | 272 |
by (asm_simp_tac (simpset() addsimps (add_ac @ [zadd])) 1); |
760 | 273 |
qed "zadd_commute"; |
0 | 274 |
|
5068 | 275 |
Goalw [integ_def] |
5137 | 276 |
"[| z1: integ; z2: integ; z3: integ |] \ |
277 |
\ ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)"; |
|
438 | 278 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
0 | 279 |
(*rewriting is much faster without intrel_iff, etc.*) |
4091 | 280 |
by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1); |
760 | 281 |
qed "zadd_assoc"; |
0 | 282 |
|
904
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
283 |
(*For AC rewriting*) |
5137 | 284 |
Goal "[| z1:integ; z2:integ; z3: integ |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)"; |
285 |
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_commute]) 1); |
|
286 |
qed "zadd_left_commute"; |
|
904
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
287 |
|
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
288 |
(*Integer addition is an AC operator*) |
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
289 |
val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute]; |
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
290 |
|
5068 | 291 |
Goalw [znat_def] |
5137 | 292 |
"[| m: nat; n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)"; |
4091 | 293 |
by (asm_simp_tac (simpset() addsimps [zadd]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
294 |
qed "znat_add"; |
0 | 295 |
|
5137 | 296 |
Goalw [integ_def,znat_def] "z : integ ==> z $+ ($~ z) = $#0"; |
438 | 297 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
4091 | 298 |
by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1); |
760 | 299 |
qed "zadd_zminus_inverse"; |
0 | 300 |
|
5137 | 301 |
Goal "z : integ ==> ($~ z) $+ z = $#0"; |
438 | 302 |
by (asm_simp_tac |
4091 | 303 |
(simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
304 |
qed "zadd_zminus_inverse2"; |
0 | 305 |
|
5137 | 306 |
Goal "z:integ ==> z $+ $#0 = z"; |
0 | 307 |
by (rtac (zadd_commute RS trans) 1); |
438 | 308 |
by (REPEAT (ares_tac [znat_type, nat_0I, zadd_0] 1)); |
760 | 309 |
qed "zadd_0_right"; |
0 | 310 |
|
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
311 |
Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2]; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
312 |
|
0 | 313 |
|
314 |
(*Need properties of $- ??? Or use $- just as an abbreviation? |
|
315 |
[| m: nat; n: nat; m>=n |] ==> $# (m #- n) = ($#m) $- ($#n) |
|
316 |
*) |
|
317 |
||
318 |
(**** zmult: multiplication on integ ****) |
|
319 |
||
320 |
(** Congruence property for multiplication **) |
|
321 |
||
5268 | 322 |
Goal "congruent2(intrel, %p1 p2. \ |
1461 | 323 |
\ split(%x1 y1. split(%x2 y2. \ |
0 | 324 |
\ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))"; |
325 |
by (rtac (equiv_intrel RS congruent2_commuteI) 1); |
|
4152 | 326 |
by Safe_tac; |
2469 | 327 |
by (ALLGOALS Asm_simp_tac); |
0 | 328 |
(*Proof that zmult is congruent in one argument*) |
438 | 329 |
by (asm_simp_tac |
4091 | 330 |
(simpset() addsimps (add_ac @ [add_mult_distrib_left RS sym])) 2); |
438 | 331 |
by (asm_simp_tac |
4091 | 332 |
(simpset() addsimps ([add_assoc RS sym, add_mult_distrib_left RS sym])) 2); |
0 | 333 |
(*Proof that zmult is commutative on representatives*) |
4091 | 334 |
by (asm_simp_tac (simpset() addsimps (mult_ac@add_ac)) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
335 |
qed "zmult_congruent2"; |
0 | 336 |
|
438 | 337 |
|
0 | 338 |
(*Resolve th against the corresponding facts for zmult*) |
339 |
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2]; |
|
340 |
||
5137 | 341 |
Goalw [integ_def,zmult_def] "[| z: integ; w: integ |] ==> z $* w : integ"; |
438 | 342 |
by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2, |
1461 | 343 |
split_type, add_type, mult_type, |
344 |
quotientI, SigmaI] 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
345 |
qed "zmult_type"; |
0 | 346 |
|
5068 | 347 |
Goalw [zmult_def] |
5137 | 348 |
"[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ |
1461 | 349 |
\ (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = \ |
438 | 350 |
\ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"; |
4091 | 351 |
by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1); |
760 | 352 |
qed "zmult"; |
0 | 353 |
|
5137 | 354 |
Goalw [integ_def,znat_def] "z : integ ==> $#0 $* z = $#0"; |
438 | 355 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
4091 | 356 |
by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
357 |
qed "zmult_0"; |
0 | 358 |
|
5137 | 359 |
Goalw [integ_def,znat_def] "z : integ ==> $#1 $* z = z"; |
438 | 360 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
4091 | 361 |
by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1); |
760 | 362 |
qed "zmult_1"; |
0 | 363 |
|
5137 | 364 |
Goalw [integ_def] "[| z: integ; w: integ |] ==> ($~ z) $* w = $~ (z $* w)"; |
438 | 365 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
4091 | 366 |
by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
367 |
qed "zmult_zminus"; |
0 | 368 |
|
5507
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
369 |
Addsimps [zmult_0, zmult_1, zmult_zminus]; |
2fd99b2d41e1
simpler definition of zmagnitude, and new thms for it
paulson
parents:
5268
diff
changeset
|
370 |
|
5137 | 371 |
Goalw [integ_def] "[| z: integ; w: integ |] ==> ($~ z) $* ($~ w) = (z $* w)"; |
438 | 372 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
4091 | 373 |
by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
374 |
qed "zmult_zminus_zminus"; |
0 | 375 |
|
5137 | 376 |
Goalw [integ_def] "[| z: integ; w: integ |] ==> z $* w = w $* z"; |
438 | 377 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
4091 | 378 |
by (asm_simp_tac (simpset() addsimps ([zmult] @ add_ac @ mult_ac)) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
379 |
qed "zmult_commute"; |
0 | 380 |
|
5068 | 381 |
Goalw [integ_def] |
5137 | 382 |
"[| z1: integ; z2: integ; z3: integ |] \ |
383 |
\ ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)"; |
|
438 | 384 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
385 |
by (asm_simp_tac |
|
4091 | 386 |
(simpset() addsimps ([zmult, add_mult_distrib_left, |
1461 | 387 |
add_mult_distrib] @ add_ac @ mult_ac)) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
388 |
qed "zmult_assoc"; |
0 | 389 |
|
904
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
390 |
(*For AC rewriting*) |
5137 | 391 |
Goal "[| z1:integ; z2:integ; z3: integ |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)"; |
392 |
by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym, zmult_commute]) 1); |
|
393 |
qed "zmult_left_commute"; |
|
904
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
394 |
|
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
395 |
(*Integer multiplication is an AC operator*) |
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
396 |
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute]; |
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
397 |
|
5068 | 398 |
Goalw [integ_def] |
5137 | 399 |
"[| z1: integ; z2: integ; w: integ |] ==> \ |
0 | 400 |
\ (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)"; |
438 | 401 |
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1)); |
4091 | 402 |
by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1); |
403 |
by (asm_simp_tac (simpset() addsimps (add_ac @ mult_ac)) 1); |
|
760 | 404 |
qed "zadd_zmult_distrib"; |
0 | 405 |
|
406 |
val integ_typechecks = |
|
407 |
[znat_type, zminus_type, zmagnitude_type, zadd_type, zmult_type]; |
|
408 |
||
2469 | 409 |
Addsimps integ_typechecks; |
904
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
410 |
|
5240dcd12adb
Proved zadd_left_commute and zmult_left_commute to define
lcp
parents:
804
diff
changeset
|
411 |
|
2469 | 412 |