4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Towards ordinal arithmetic. Also useful with wfrec. |
6 Towards ordinal arithmetic. Also useful with wfrec. |
7 *) |
7 *) |
8 |
8 |
9 OrderArith = Order + Sum + Ordinal + |
9 theory OrderArith = Order + Sum + Ordinal: |
10 consts |
10 constdefs |
11 radd, rmult :: [i,i,i,i]=>i |
11 |
12 rvimage :: [i,i,i]=>i |
|
13 |
|
14 defs |
|
15 (*disjoint sum of two relations; underlies ordinal addition*) |
12 (*disjoint sum of two relations; underlies ordinal addition*) |
16 radd_def "radd(A,r,B,s) == |
13 radd :: "[i,i,i,i]=>i" |
|
14 "radd(A,r,B,s) == |
17 {z: (A+B) * (A+B). |
15 {z: (A+B) * (A+B). |
18 (EX x y. z = <Inl(x), Inr(y)>) | |
16 (EX x y. z = <Inl(x), Inr(y)>) | |
19 (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) | |
17 (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) | |
20 (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}" |
18 (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}" |
21 |
19 |
22 (*lexicographic product of two relations; underlies ordinal multiplication*) |
20 (*lexicographic product of two relations; underlies ordinal multiplication*) |
23 rmult_def "rmult(A,r,B,s) == |
21 rmult :: "[i,i,i,i]=>i" |
|
22 "rmult(A,r,B,s) == |
24 {z: (A*B) * (A*B). |
23 {z: (A*B) * (A*B). |
25 EX x' y' x y. z = <<x',y'>, <x,y>> & |
24 EX x' y' x y. z = <<x',y'>, <x,y>> & |
26 (<x',x>: r | (x'=x & <y',y>: s))}" |
25 (<x',x>: r | (x'=x & <y',y>: s))}" |
27 |
26 |
28 (*inverse image of a relation*) |
27 (*inverse image of a relation*) |
29 rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}" |
28 rvimage :: "[i,i,i]=>i" |
30 |
29 "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}" |
31 constdefs |
30 |
32 measure :: "[i, i\\<Rightarrow>i] \\<Rightarrow> i" |
31 measure :: "[i, i\<Rightarrow>i] \<Rightarrow> i" |
33 "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}" |
32 "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}" |
34 |
33 |
|
34 |
|
35 (**** Addition of relations -- disjoint sum ****) |
|
36 |
|
37 (** Rewrite rules. Can be used to obtain introduction rules **) |
|
38 |
|
39 lemma radd_Inl_Inr_iff [iff]: |
|
40 "<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B" |
|
41 apply (unfold radd_def) |
|
42 apply blast |
|
43 done |
|
44 |
|
45 lemma radd_Inl_iff [iff]: |
|
46 "<Inl(a'), Inl(a)> : radd(A,r,B,s) <-> a':A & a:A & <a',a>:r" |
|
47 apply (unfold radd_def) |
|
48 apply blast |
|
49 done |
|
50 |
|
51 lemma radd_Inr_iff [iff]: |
|
52 "<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s" |
|
53 apply (unfold radd_def) |
|
54 apply blast |
|
55 done |
|
56 |
|
57 lemma radd_Inr_Inl_iff [iff]: |
|
58 "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False" |
|
59 apply (unfold radd_def) |
|
60 apply blast |
|
61 done |
|
62 |
|
63 (** Elimination Rule **) |
|
64 |
|
65 lemma raddE: |
|
66 "[| <p',p> : radd(A,r,B,s); |
|
67 !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q; |
|
68 !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q; |
|
69 !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q |
|
70 |] ==> Q" |
|
71 apply (unfold radd_def) |
|
72 apply (blast intro: elim:); |
|
73 done |
|
74 |
|
75 (** Type checking **) |
|
76 |
|
77 lemma radd_type: "radd(A,r,B,s) <= (A+B) * (A+B)" |
|
78 apply (unfold radd_def) |
|
79 apply (rule Collect_subset) |
|
80 done |
|
81 |
|
82 lemmas field_radd = radd_type [THEN field_rel_subset] |
|
83 |
|
84 (** Linearity **) |
|
85 |
|
86 lemma linear_radd: |
|
87 "[| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))" |
|
88 apply (unfold linear_def) |
|
89 apply (blast intro: elim:); |
|
90 done |
|
91 |
|
92 |
|
93 (** Well-foundedness **) |
|
94 |
|
95 lemma wf_on_radd: "[| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))" |
|
96 apply (rule wf_onI2) |
|
97 apply (subgoal_tac "ALL x:A. Inl (x) : Ba") |
|
98 (*Proving the lemma, which is needed twice!*) |
|
99 prefer 2 |
|
100 apply (erule_tac V = "y : A + B" in thin_rl) |
|
101 apply (rule_tac ballI) |
|
102 apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption) |
|
103 apply (blast intro: elim:); |
|
104 (*Returning to main part of proof*) |
|
105 apply safe |
|
106 apply blast |
|
107 apply (erule_tac r = "s" and a = "ya" in wf_on_induct , assumption) |
|
108 apply (blast intro: elim:); |
|
109 done |
|
110 |
|
111 lemma wf_radd: "[| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))" |
|
112 apply (simp add: wf_iff_wf_on_field) |
|
113 apply (rule wf_on_subset_A [OF _ field_radd]) |
|
114 apply (blast intro: wf_on_radd) |
|
115 done |
|
116 |
|
117 lemma well_ord_radd: |
|
118 "[| well_ord(A,r); well_ord(B,s) |] ==> well_ord(A+B, radd(A,r,B,s))" |
|
119 apply (rule well_ordI) |
|
120 apply (simp add: well_ord_def wf_on_radd) |
|
121 apply (simp add: well_ord_def tot_ord_def linear_radd) |
|
122 done |
|
123 |
|
124 (** An ord_iso congruence law **) |
|
125 |
|
126 lemma sum_bij: |
|
127 "[| f: bij(A,C); g: bij(B,D) |] |
|
128 ==> (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)" |
|
129 apply (rule_tac d = "case (%x. Inl (converse (f) `x) , %y. Inr (converse (g) `y))" in lam_bijective) |
|
130 apply (typecheck add: bij_is_inj inj_is_fun) |
|
131 apply (auto simp add: left_inverse_bij right_inverse_bij) |
|
132 done |
|
133 |
|
134 lemma sum_ord_iso_cong: |
|
135 "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ==> |
|
136 (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) |
|
137 : ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))" |
|
138 apply (unfold ord_iso_def) |
|
139 apply (safe intro!: sum_bij) |
|
140 (*Do the beta-reductions now*) |
|
141 apply (auto cong add: conj_cong simp add: bij_is_fun [THEN apply_type]) |
|
142 done |
|
143 |
|
144 (*Could we prove an ord_iso result? Perhaps |
|
145 ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *) |
|
146 lemma sum_disjoint_bij: "A Int B = 0 ==> |
|
147 (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)" |
|
148 apply (rule_tac d = "%z. if z:A then Inl (z) else Inr (z) " in lam_bijective) |
|
149 apply auto |
|
150 done |
|
151 |
|
152 (** Associativity **) |
|
153 |
|
154 lemma sum_assoc_bij: |
|
155 "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) |
|
156 : bij((A+B)+C, A+(B+C))" |
|
157 apply (rule_tac d = "case (%x. Inl (Inl (x)), case (%x. Inl (Inr (x)), Inr))" |
|
158 in lam_bijective) |
|
159 apply auto |
|
160 done |
|
161 |
|
162 lemma sum_assoc_ord_iso: |
|
163 "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) |
|
164 : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), |
|
165 A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))" |
|
166 apply (rule sum_assoc_bij [THEN ord_isoI]) |
|
167 apply auto |
|
168 done |
|
169 |
|
170 |
|
171 (**** Multiplication of relations -- lexicographic product ****) |
|
172 |
|
173 (** Rewrite rule. Can be used to obtain introduction rules **) |
|
174 |
|
175 lemma rmult_iff [iff]: |
|
176 "<<a',b'>, <a,b>> : rmult(A,r,B,s) <-> |
|
177 (<a',a>: r & a':A & a:A & b': B & b: B) | |
|
178 (<b',b>: s & a'=a & a:A & b': B & b: B)" |
|
179 |
|
180 apply (unfold rmult_def) |
|
181 apply blast |
|
182 done |
|
183 |
|
184 lemma rmultE: |
|
185 "[| <<a',b'>, <a,b>> : rmult(A,r,B,s); |
|
186 [| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q; |
|
187 [| <b',b>: s; a:A; a'=a; b':B; b:B |] ==> Q |
|
188 |] ==> Q" |
|
189 apply (blast intro: elim:); |
|
190 done |
|
191 |
|
192 (** Type checking **) |
|
193 |
|
194 lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)" |
|
195 apply (unfold rmult_def) |
|
196 apply (rule Collect_subset) |
|
197 done |
|
198 |
|
199 lemmas field_rmult = rmult_type [THEN field_rel_subset] |
|
200 |
|
201 (** Linearity **) |
|
202 |
|
203 lemma linear_rmult: |
|
204 "[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))" |
|
205 apply (simp add: linear_def); |
|
206 apply (blast intro: elim:); |
|
207 done |
|
208 |
|
209 (** Well-foundedness **) |
|
210 |
|
211 lemma wf_on_rmult: "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))" |
|
212 apply (rule wf_onI2) |
|
213 apply (erule SigmaE) |
|
214 apply (erule ssubst) |
|
215 apply (subgoal_tac "ALL b:B. <x,b>: Ba") |
|
216 apply blast |
|
217 apply (erule_tac a = "x" in wf_on_induct , assumption) |
|
218 apply (rule ballI) |
|
219 apply (erule_tac a = "b" in wf_on_induct , assumption) |
|
220 apply (best elim!: rmultE bspec [THEN mp]) |
|
221 done |
|
222 |
|
223 |
|
224 lemma wf_rmult: "[| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))" |
|
225 apply (simp add: wf_iff_wf_on_field) |
|
226 apply (rule wf_on_subset_A [OF _ field_rmult]) |
|
227 apply (blast intro: wf_on_rmult) |
|
228 done |
|
229 |
|
230 lemma well_ord_rmult: |
|
231 "[| well_ord(A,r); well_ord(B,s) |] ==> well_ord(A*B, rmult(A,r,B,s))" |
|
232 apply (rule well_ordI) |
|
233 apply (simp add: well_ord_def wf_on_rmult) |
|
234 apply (simp add: well_ord_def tot_ord_def linear_rmult) |
|
235 done |
|
236 |
|
237 |
|
238 (** An ord_iso congruence law **) |
|
239 |
|
240 lemma prod_bij: |
|
241 "[| f: bij(A,C); g: bij(B,D) |] |
|
242 ==> (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)" |
|
243 apply (rule_tac d = "%<x,y>. <converse (f) `x, converse (g) `y>" |
|
244 in lam_bijective) |
|
245 apply (typecheck add: bij_is_inj inj_is_fun) |
|
246 apply (auto simp add: left_inverse_bij right_inverse_bij) |
|
247 done |
|
248 |
|
249 lemma prod_ord_iso_cong: |
|
250 "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] |
|
251 ==> (lam <x,y>:A*B. <f`x, g`y>) |
|
252 : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))" |
|
253 apply (unfold ord_iso_def) |
|
254 apply (safe intro!: prod_bij) |
|
255 apply (simp_all add: bij_is_fun [THEN apply_type]) |
|
256 apply (blast intro: bij_is_inj [THEN inj_apply_equality]) |
|
257 done |
|
258 |
|
259 lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)" |
|
260 apply (rule_tac d = "snd" in lam_bijective) |
|
261 apply auto |
|
262 done |
|
263 |
|
264 (*Used??*) |
|
265 lemma singleton_prod_ord_iso: |
|
266 "well_ord({x},xr) ==> |
|
267 (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))" |
|
268 apply (rule singleton_prod_bij [THEN ord_isoI]) |
|
269 apply (simp (no_asm_simp)) |
|
270 apply (blast dest: well_ord_is_wf [THEN wf_on_not_refl]) |
|
271 done |
|
272 |
|
273 (*Here we build a complicated function term, then simplify it using |
|
274 case_cong, id_conv, comp_lam, case_case.*) |
|
275 lemma prod_sum_singleton_bij: |
|
276 "a~:C ==> |
|
277 (lam x:C*B + D. case(%x. x, %y.<a,y>, x)) |
|
278 : bij(C*B + D, C*B Un {a}*D)" |
|
279 apply (rule subst_elem) |
|
280 apply (rule id_bij [THEN sum_bij, THEN comp_bij]) |
|
281 apply (rule singleton_prod_bij) |
|
282 apply (rule sum_disjoint_bij) |
|
283 apply blast |
|
284 apply (simp (no_asm_simp) cong add: case_cong) |
|
285 apply (rule comp_lam [THEN trans, symmetric]) |
|
286 apply (fast elim!: case_type) |
|
287 apply (simp (no_asm_simp) add: case_case) |
|
288 done |
|
289 |
|
290 lemma prod_sum_singleton_ord_iso: |
|
291 "[| a:A; well_ord(A,r) |] ==> |
|
292 (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x)) |
|
293 : ord_iso(pred(A,a,r)*B + pred(B,b,s), |
|
294 radd(A*B, rmult(A,r,B,s), B, s), |
|
295 pred(A,a,r)*B Un {a}*pred(B,b,s), rmult(A,r,B,s))" |
|
296 apply (rule prod_sum_singleton_bij [THEN ord_isoI]) |
|
297 apply (simp (no_asm_simp) add: pred_iff well_ord_is_wf [THEN wf_on_not_refl]) |
|
298 apply (auto elim!: well_ord_is_wf [THEN wf_on_asym] predE) |
|
299 done |
|
300 |
|
301 (** Distributive law **) |
|
302 |
|
303 lemma sum_prod_distrib_bij: |
|
304 "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) |
|
305 : bij((A+B)*C, (A*C)+(B*C))" |
|
306 apply (rule_tac d = "case (%<x,y>.<Inl (x) ,y>, %<x,y>.<Inr (x) ,y>) " |
|
307 in lam_bijective) |
|
308 apply auto |
|
309 done |
|
310 |
|
311 lemma sum_prod_distrib_ord_iso: |
|
312 "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) |
|
313 : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), |
|
314 (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))" |
|
315 apply (rule sum_prod_distrib_bij [THEN ord_isoI]) |
|
316 apply auto |
|
317 done |
|
318 |
|
319 (** Associativity **) |
|
320 |
|
321 lemma prod_assoc_bij: |
|
322 "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))" |
|
323 apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective) |
|
324 apply auto |
|
325 done |
|
326 |
|
327 lemma prod_assoc_ord_iso: |
|
328 "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) |
|
329 : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), |
|
330 A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))" |
|
331 apply (rule prod_assoc_bij [THEN ord_isoI]) |
|
332 apply auto |
|
333 done |
|
334 |
|
335 (**** Inverse image of a relation ****) |
|
336 |
|
337 (** Rewrite rule **) |
|
338 |
|
339 lemma rvimage_iff: "<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A" |
|
340 apply (unfold rvimage_def) |
|
341 apply blast |
|
342 done |
|
343 |
|
344 (** Type checking **) |
|
345 |
|
346 lemma rvimage_type: "rvimage(A,f,r) <= A*A" |
|
347 apply (unfold rvimage_def) |
|
348 apply (rule Collect_subset) |
|
349 done |
|
350 |
|
351 lemmas field_rvimage = rvimage_type [THEN field_rel_subset] |
|
352 |
|
353 lemma rvimage_converse: "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))" |
|
354 apply (unfold rvimage_def) |
|
355 apply blast |
|
356 done |
|
357 |
|
358 |
|
359 (** Partial Ordering Properties **) |
|
360 |
|
361 lemma irrefl_rvimage: |
|
362 "[| f: inj(A,B); irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))" |
|
363 apply (unfold irrefl_def rvimage_def) |
|
364 apply (blast intro: inj_is_fun [THEN apply_type]) |
|
365 done |
|
366 |
|
367 lemma trans_on_rvimage: |
|
368 "[| f: inj(A,B); trans[B](r) |] ==> trans[A](rvimage(A,f,r))" |
|
369 apply (unfold trans_on_def rvimage_def) |
|
370 apply (blast intro: inj_is_fun [THEN apply_type]) |
|
371 done |
|
372 |
|
373 lemma part_ord_rvimage: |
|
374 "[| f: inj(A,B); part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))" |
|
375 apply (unfold part_ord_def) |
|
376 apply (blast intro!: irrefl_rvimage trans_on_rvimage) |
|
377 done |
|
378 |
|
379 (** Linearity **) |
|
380 |
|
381 lemma linear_rvimage: |
|
382 "[| f: inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))" |
|
383 apply (simp add: inj_def linear_def rvimage_iff) |
|
384 apply (blast intro: apply_funtype); |
|
385 done |
|
386 |
|
387 lemma tot_ord_rvimage: |
|
388 "[| f: inj(A,B); tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))" |
|
389 apply (unfold tot_ord_def) |
|
390 apply (blast intro!: part_ord_rvimage linear_rvimage) |
|
391 done |
|
392 |
|
393 |
|
394 (** Well-foundedness **) |
|
395 |
|
396 (*Not sure if wf_on_rvimage could be proved from this!*) |
|
397 lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))" |
|
398 apply (simp (no_asm_use) add: rvimage_def wf_eq_minimal) |
|
399 apply clarify |
|
400 apply (subgoal_tac "EX w. w : {w: {f`x. x:Q}. EX x. x: Q & (f`x = w) }") |
|
401 apply (erule allE) |
|
402 apply (erule impE) |
|
403 apply assumption; |
|
404 apply blast |
|
405 apply (blast intro: elim:); |
|
406 done |
|
407 |
|
408 lemma wf_on_rvimage: "[| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))" |
|
409 apply (rule wf_onI2) |
|
410 apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba") |
|
411 apply blast |
|
412 apply (erule_tac a = "f`y" in wf_on_induct) |
|
413 apply (blast intro!: apply_funtype) |
|
414 apply (blast intro!: apply_funtype dest!: rvimage_iff [THEN iffD1]) |
|
415 done |
|
416 |
|
417 (*Note that we need only wf[A](...) and linear(A,...) to get the result!*) |
|
418 lemma well_ord_rvimage: |
|
419 "[| f: inj(A,B); well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))" |
|
420 apply (rule well_ordI) |
|
421 apply (unfold well_ord_def tot_ord_def) |
|
422 apply (blast intro!: wf_on_rvimage inj_is_fun) |
|
423 apply (blast intro!: linear_rvimage) |
|
424 done |
|
425 |
|
426 lemma ord_iso_rvimage: |
|
427 "f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)" |
|
428 apply (unfold ord_iso_def) |
|
429 apply (simp add: rvimage_iff) |
|
430 done |
|
431 |
|
432 lemma ord_iso_rvimage_eq: |
|
433 "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A" |
|
434 apply (unfold ord_iso_def rvimage_def) |
|
435 apply blast |
|
436 done |
|
437 |
|
438 |
|
439 (** The "measure" relation is useful with wfrec **) |
|
440 |
|
441 lemma measure_eq_rvimage_Memrel: |
|
442 "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))" |
|
443 apply (simp (no_asm) add: measure_def rvimage_def Memrel_iff) |
|
444 apply (rule equalityI) |
|
445 apply auto |
|
446 apply (auto intro: Ord_in_Ord simp add: lt_def) |
|
447 done |
|
448 |
|
449 lemma wf_measure [iff]: "wf(measure(A,f))" |
|
450 apply (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage) |
|
451 done |
|
452 |
|
453 lemma measure_iff [iff]: "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)" |
|
454 apply (simp (no_asm) add: measure_def) |
|
455 done |
|
456 |
|
457 ML {* |
|
458 val measure_def = thm "measure_def"; |
|
459 val radd_Inl_Inr_iff = thm "radd_Inl_Inr_iff"; |
|
460 val radd_Inl_iff = thm "radd_Inl_iff"; |
|
461 val radd_Inr_iff = thm "radd_Inr_iff"; |
|
462 val radd_Inr_Inl_iff = thm "radd_Inr_Inl_iff"; |
|
463 val raddE = thm "raddE"; |
|
464 val radd_type = thm "radd_type"; |
|
465 val field_radd = thm "field_radd"; |
|
466 val linear_radd = thm "linear_radd"; |
|
467 val wf_on_radd = thm "wf_on_radd"; |
|
468 val wf_radd = thm "wf_radd"; |
|
469 val well_ord_radd = thm "well_ord_radd"; |
|
470 val sum_bij = thm "sum_bij"; |
|
471 val sum_ord_iso_cong = thm "sum_ord_iso_cong"; |
|
472 val sum_disjoint_bij = thm "sum_disjoint_bij"; |
|
473 val sum_assoc_bij = thm "sum_assoc_bij"; |
|
474 val sum_assoc_ord_iso = thm "sum_assoc_ord_iso"; |
|
475 val rmult_iff = thm "rmult_iff"; |
|
476 val rmultE = thm "rmultE"; |
|
477 val rmult_type = thm "rmult_type"; |
|
478 val field_rmult = thm "field_rmult"; |
|
479 val linear_rmult = thm "linear_rmult"; |
|
480 val wf_on_rmult = thm "wf_on_rmult"; |
|
481 val wf_rmult = thm "wf_rmult"; |
|
482 val well_ord_rmult = thm "well_ord_rmult"; |
|
483 val prod_bij = thm "prod_bij"; |
|
484 val prod_ord_iso_cong = thm "prod_ord_iso_cong"; |
|
485 val singleton_prod_bij = thm "singleton_prod_bij"; |
|
486 val singleton_prod_ord_iso = thm "singleton_prod_ord_iso"; |
|
487 val prod_sum_singleton_bij = thm "prod_sum_singleton_bij"; |
|
488 val prod_sum_singleton_ord_iso = thm "prod_sum_singleton_ord_iso"; |
|
489 val sum_prod_distrib_bij = thm "sum_prod_distrib_bij"; |
|
490 val sum_prod_distrib_ord_iso = thm "sum_prod_distrib_ord_iso"; |
|
491 val prod_assoc_bij = thm "prod_assoc_bij"; |
|
492 val prod_assoc_ord_iso = thm "prod_assoc_ord_iso"; |
|
493 val rvimage_iff = thm "rvimage_iff"; |
|
494 val rvimage_type = thm "rvimage_type"; |
|
495 val field_rvimage = thm "field_rvimage"; |
|
496 val rvimage_converse = thm "rvimage_converse"; |
|
497 val irrefl_rvimage = thm "irrefl_rvimage"; |
|
498 val trans_on_rvimage = thm "trans_on_rvimage"; |
|
499 val part_ord_rvimage = thm "part_ord_rvimage"; |
|
500 val linear_rvimage = thm "linear_rvimage"; |
|
501 val tot_ord_rvimage = thm "tot_ord_rvimage"; |
|
502 val wf_rvimage = thm "wf_rvimage"; |
|
503 val wf_on_rvimage = thm "wf_on_rvimage"; |
|
504 val well_ord_rvimage = thm "well_ord_rvimage"; |
|
505 val ord_iso_rvimage = thm "ord_iso_rvimage"; |
|
506 val ord_iso_rvimage_eq = thm "ord_iso_rvimage_eq"; |
|
507 val measure_eq_rvimage_Memrel = thm "measure_eq_rvimage_Memrel"; |
|
508 val wf_measure = thm "wf_measure"; |
|
509 val measure_iff = thm "measure_iff"; |
|
510 *} |
35 |
511 |
36 end |
512 end |