author | clasohm |
Wed, 14 Dec 1994 11:41:49 +0100 | |
changeset 782 | 200a16083201 |
parent 770 | 216ec1299bf0 |
child 815 | de2d8a63256d |
permissions | -rw-r--r-- |
437 | 1 |
(* Title: ZF/OrderArith.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
6 |
Towards ordinal arithmetic |
|
7 |
*) |
|
8 |
||
9 |
open OrderArith; |
|
10 |
||
11 |
||
12 |
(**** Addition of relations -- disjoint sum ****) |
|
13 |
||
14 |
(** Rewrite rules. Can be used to obtain introduction rules **) |
|
15 |
||
16 |
goalw OrderArith.thy [radd_def] |
|
17 |
"<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B"; |
|
18 |
by (fast_tac sum_cs 1); |
|
760 | 19 |
qed "radd_Inl_Inr_iff"; |
437 | 20 |
|
21 |
goalw OrderArith.thy [radd_def] |
|
22 |
"<Inl(a'), Inl(a)> : radd(A,r,B,s) <-> <a',a>:r & a':A & a:A"; |
|
23 |
by (fast_tac sum_cs 1); |
|
760 | 24 |
qed "radd_Inl_iff"; |
437 | 25 |
|
26 |
goalw OrderArith.thy [radd_def] |
|
27 |
"<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> <b',b>:s & b':B & b:B"; |
|
28 |
by (fast_tac sum_cs 1); |
|
760 | 29 |
qed "radd_Inr_iff"; |
437 | 30 |
|
31 |
goalw OrderArith.thy [radd_def] |
|
32 |
"<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False"; |
|
33 |
by (fast_tac sum_cs 1); |
|
760 | 34 |
qed "radd_Inr_Inl_iff"; |
437 | 35 |
|
36 |
(** Elimination Rule **) |
|
37 |
||
38 |
val major::prems = goalw OrderArith.thy [radd_def] |
|
39 |
"[| <p',p> : radd(A,r,B,s); \ |
|
40 |
\ !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q; \ |
|
41 |
\ !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q; \ |
|
42 |
\ !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q \ |
|
43 |
\ |] ==> Q"; |
|
44 |
by (cut_facts_tac [major] 1); |
|
45 |
(*Split into the three cases*) |
|
46 |
by (REPEAT_FIRST |
|
47 |
(eresolve_tac [CollectE, Pair_inject, conjE, exE, SigmaE, disjE])); |
|
48 |
(*Apply each premise to correct subgoal; can't just use fast_tac |
|
49 |
because hyp_subst_tac would delete equalities too quickly*) |
|
50 |
by (EVERY (map (fn prem => |
|
51 |
EVERY1 [rtac prem, assume_tac, REPEAT o fast_tac sum_cs]) |
|
52 |
prems)); |
|
760 | 53 |
qed "raddE"; |
437 | 54 |
|
55 |
(** Type checking **) |
|
56 |
||
57 |
goalw OrderArith.thy [radd_def] "radd(A,r,B,s) <= (A+B) * (A+B)"; |
|
58 |
by (rtac Collect_subset 1); |
|
760 | 59 |
qed "radd_type"; |
437 | 60 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
770
diff
changeset
|
61 |
bind_thm ("field_radd", (radd_type RS field_rel_subset)); |
437 | 62 |
|
63 |
(** Linearity **) |
|
64 |
||
65 |
val radd_ss = sum_ss addsimps [radd_Inl_iff, radd_Inr_iff, |
|
66 |
radd_Inl_Inr_iff, radd_Inr_Inl_iff]; |
|
67 |
||
68 |
goalw OrderArith.thy [linear_def] |
|
69 |
"!!r s. [| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"; |
|
70 |
by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac sumE)); |
|
71 |
by (ALLGOALS (asm_simp_tac radd_ss)); |
|
760 | 72 |
qed "linear_radd"; |
437 | 73 |
|
74 |
||
75 |
(** Well-foundedness **) |
|
76 |
||
77 |
goal OrderArith.thy |
|
78 |
"!!r s. [| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"; |
|
79 |
by (rtac wf_onI2 1); |
|
80 |
by (subgoal_tac "ALL x:A. Inl(x): Ba" 1); |
|
81 |
(*Proving the lemma, which is needed twice!*) |
|
662 | 82 |
by (eres_inst_tac [("V", "y : A + B")] thin_rl 2); |
437 | 83 |
by (rtac ballI 2); |
84 |
by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2); |
|
85 |
by (etac (bspec RS mp) 2); |
|
86 |
by (fast_tac sum_cs 2); |
|
87 |
by (best_tac (sum_cs addSEs [raddE]) 2); |
|
88 |
(*Returning to main part of proof*) |
|
89 |
by (REPEAT_FIRST (eresolve_tac [sumE, ssubst])); |
|
90 |
by (best_tac sum_cs 1); |
|
91 |
by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1); |
|
92 |
by (etac (bspec RS mp) 1); |
|
93 |
by (fast_tac sum_cs 1); |
|
94 |
by (best_tac (sum_cs addSEs [raddE]) 1); |
|
760 | 95 |
qed "wf_on_radd"; |
437 | 96 |
|
97 |
goal OrderArith.thy |
|
98 |
"!!r s. [| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))"; |
|
99 |
by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1); |
|
100 |
by (rtac (field_radd RSN (2, wf_on_subset_A)) 1); |
|
101 |
by (REPEAT (ares_tac [wf_on_radd] 1)); |
|
760 | 102 |
qed "wf_radd"; |
437 | 103 |
|
104 |
goal OrderArith.thy |
|
105 |
"!!r s. [| well_ord(A,r); well_ord(B,s) |] ==> \ |
|
106 |
\ well_ord(A+B, radd(A,r,B,s))"; |
|
107 |
by (rtac well_ordI 1); |
|
108 |
by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, wf_on_radd]) 1); |
|
109 |
by (asm_full_simp_tac |
|
110 |
(ZF_ss addsimps [well_ord_def, tot_ord_def, linear_radd]) 1); |
|
760 | 111 |
qed "well_ord_radd"; |
437 | 112 |
|
113 |
||
114 |
(**** Multiplication of relations -- lexicographic product ****) |
|
115 |
||
116 |
(** Rewrite rule. Can be used to obtain introduction rules **) |
|
117 |
||
118 |
goalw OrderArith.thy [rmult_def] |
|
119 |
"!!r s. <<a',b'>, <a,b>> : rmult(A,r,B,s) <-> \ |
|
120 |
\ (<a',a>: r & a':A & a:A & b': B & b: B) | \ |
|
121 |
\ (<b',b>: s & a'=a & a:A & b': B & b: B)"; |
|
122 |
by (fast_tac ZF_cs 1); |
|
760 | 123 |
qed "rmult_iff"; |
437 | 124 |
|
125 |
val major::prems = goal OrderArith.thy |
|
126 |
"[| <<a',b'>, <a,b>> : rmult(A,r,B,s); \ |
|
127 |
\ [| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q; \ |
|
128 |
\ [| <b',b>: s; a:A; a'=a; b':B; b:B |] ==> Q \ |
|
129 |
\ |] ==> Q"; |
|
130 |
by (rtac (major RS (rmult_iff RS iffD1) RS disjE) 1); |
|
131 |
by (DEPTH_SOLVE (eresolve_tac ([asm_rl, conjE] @ prems) 1)); |
|
760 | 132 |
qed "rmultE"; |
437 | 133 |
|
134 |
(** Type checking **) |
|
135 |
||
136 |
goalw OrderArith.thy [rmult_def] "rmult(A,r,B,s) <= (A*B) * (A*B)"; |
|
137 |
by (rtac Collect_subset 1); |
|
760 | 138 |
qed "rmult_type"; |
437 | 139 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
770
diff
changeset
|
140 |
bind_thm ("field_rmult", (rmult_type RS field_rel_subset)); |
437 | 141 |
|
142 |
(** Linearity **) |
|
143 |
||
144 |
val [lina,linb] = goal OrderArith.thy |
|
145 |
"[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"; |
|
146 |
by (rewtac linear_def); (*Note! the premises are NOT rewritten*) |
|
147 |
by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac SigmaE)); |
|
148 |
by (asm_simp_tac (ZF_ss addsimps [rmult_iff]) 1); |
|
149 |
by (res_inst_tac [("x","xa"), ("y","xb")] (lina RS linearE) 1); |
|
150 |
by (res_inst_tac [("x","ya"), ("y","yb")] (linb RS linearE) 4); |
|
151 |
by (REPEAT_SOME (fast_tac ZF_cs)); |
|
760 | 152 |
qed "linear_rmult"; |
437 | 153 |
|
154 |
||
155 |
(** Well-foundedness **) |
|
156 |
||
157 |
goal OrderArith.thy |
|
158 |
"!!r s. [| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))"; |
|
159 |
by (rtac wf_onI2 1); |
|
160 |
by (etac SigmaE 1); |
|
161 |
by (etac ssubst 1); |
|
162 |
by (subgoal_tac "ALL b:B. <x,b>: Ba" 1); |
|
163 |
by (fast_tac ZF_cs 1); |
|
164 |
by (eres_inst_tac [("a","x")] wf_on_induct 1 THEN assume_tac 1); |
|
165 |
by (rtac ballI 1); |
|
166 |
by (eres_inst_tac [("a","b")] wf_on_induct 1 THEN assume_tac 1); |
|
167 |
by (etac (bspec RS mp) 1); |
|
168 |
by (fast_tac ZF_cs 1); |
|
169 |
by (best_tac (ZF_cs addSEs [rmultE]) 1); |
|
760 | 170 |
qed "wf_on_rmult"; |
437 | 171 |
|
172 |
||
173 |
goal OrderArith.thy |
|
174 |
"!!r s. [| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))"; |
|
175 |
by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1); |
|
176 |
by (rtac (field_rmult RSN (2, wf_on_subset_A)) 1); |
|
177 |
by (REPEAT (ares_tac [wf_on_rmult] 1)); |
|
760 | 178 |
qed "wf_rmult"; |
437 | 179 |
|
180 |
goal OrderArith.thy |
|
181 |
"!!r s. [| well_ord(A,r); well_ord(B,s) |] ==> \ |
|
182 |
\ well_ord(A*B, rmult(A,r,B,s))"; |
|
183 |
by (rtac well_ordI 1); |
|
184 |
by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, wf_on_rmult]) 1); |
|
185 |
by (asm_full_simp_tac |
|
186 |
(ZF_ss addsimps [well_ord_def, tot_ord_def, linear_rmult]) 1); |
|
760 | 187 |
qed "well_ord_rmult"; |
437 | 188 |
|
189 |
||
190 |
(**** Inverse image of a relation ****) |
|
191 |
||
192 |
(** Rewrite rule **) |
|
193 |
||
194 |
goalw OrderArith.thy [rvimage_def] |
|
195 |
"<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A"; |
|
196 |
by (fast_tac ZF_cs 1); |
|
760 | 197 |
qed "rvimage_iff"; |
437 | 198 |
|
199 |
(** Type checking **) |
|
200 |
||
201 |
goalw OrderArith.thy [rvimage_def] "rvimage(A,f,r) <= A*A"; |
|
202 |
by (rtac Collect_subset 1); |
|
760 | 203 |
qed "rvimage_type"; |
437 | 204 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
770
diff
changeset
|
205 |
bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset)); |
437 | 206 |
|
207 |
||
208 |
(** Linearity **) |
|
209 |
||
210 |
val [finj,lin] = goalw OrderArith.thy [inj_def] |
|
211 |
"[| f: inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))"; |
|
212 |
by (rewtac linear_def); (*Note! the premises are NOT rewritten*) |
|
213 |
by (REPEAT_FIRST (ares_tac [ballI])); |
|
214 |
by (asm_simp_tac (ZF_ss addsimps [rvimage_iff]) 1); |
|
215 |
by (cut_facts_tac [finj] 1); |
|
216 |
by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1); |
|
217 |
by (REPEAT_SOME (fast_tac (ZF_cs addSIs [apply_type]))); |
|
760 | 218 |
qed "linear_rvimage"; |
437 | 219 |
|
220 |
||
221 |
(** Well-foundedness **) |
|
222 |
||
223 |
goal OrderArith.thy |
|
224 |
"!!r. [| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))"; |
|
225 |
by (rtac wf_onI2 1); |
|
226 |
by (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba" 1); |
|
227 |
by (fast_tac ZF_cs 1); |
|
228 |
by (eres_inst_tac [("a","f`y")] wf_on_induct 1); |
|
229 |
by (fast_tac (ZF_cs addSIs [apply_type]) 1); |
|
230 |
by (best_tac (ZF_cs addSIs [apply_type] addSDs [rvimage_iff RS iffD1]) 1); |
|
760 | 231 |
qed "wf_on_rvimage"; |
437 | 232 |
|
233 |
goal OrderArith.thy |
|
234 |
"!!r. [| f: inj(A,B); well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))"; |
|
235 |
by (rtac well_ordI 1); |
|
236 |
by (rewrite_goals_tac [well_ord_def, tot_ord_def]); |
|
237 |
by (fast_tac (ZF_cs addSIs [wf_on_rvimage, inj_is_fun]) 1); |
|
238 |
by (fast_tac (ZF_cs addSIs [linear_rvimage]) 1); |
|
760 | 239 |
qed "well_ord_rvimage"; |