|
1 (* Title: HOL/Codatatype/BNF_Util.thy |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 Copyright 2012 |
|
5 |
|
6 Library for bounded natural functors. |
|
7 *) |
|
8 |
|
9 header {* Library for Bounded Natural Functors *} |
|
10 |
|
11 theory BNF_Util |
|
12 imports |
|
13 "../Ordinals_and_Cardinals/Cardinal_Arithmetic" |
|
14 "~~/src/HOL/Library/Prefix_Order" |
|
15 Equiv_Relations_More |
|
16 begin |
|
17 |
|
18 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y" |
|
19 by (erule iffI) (erule contrapos_pn) |
|
20 |
|
21 lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp |
|
22 |
|
23 lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by clarsimp |
|
24 |
|
25 lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True" |
|
26 by presburger |
|
27 |
|
28 lemma case_unit: "(case u of () => f) = f" |
|
29 by (cases u) (hypsubst, rule unit.cases) |
|
30 |
|
31 lemma All_point_1: "(\<And>z. z = b \<Longrightarrow> phi z) \<equiv> Trueprop (phi b)" |
|
32 by presburger |
|
33 |
|
34 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)" |
|
35 by blast |
|
36 |
|
37 lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})" |
|
38 by blast |
|
39 |
|
40 lemma mem_Collect_eq_split: "{(x, y). (x, y) \<in> X} = X" |
|
41 by simp |
|
42 |
|
43 lemma image_comp: "image (f o g) = image f o image g" |
|
44 by (rule ext) (auto simp only: o_apply image_def) |
|
45 |
|
46 lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})" |
|
47 by (rule ext) simp |
|
48 |
|
49 lemma Union_natural: "Union o image (image f) = image f o Union" |
|
50 by (rule ext) (auto simp only: o_apply) |
|
51 |
|
52 lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A" |
|
53 by (unfold o_assoc) |
|
54 |
|
55 lemma comp_single_set_bd: |
|
56 assumes fbd_Card_order: "Card_order fbd" and |
|
57 fset_bd: "\<And>x. |fset x| \<le>o fbd" and |
|
58 gset_bd: "\<And>x. |gset x| \<le>o gbd" |
|
59 shows "|\<Union>fset ` gset x| \<le>o gbd *c fbd" |
|
60 apply (subst sym[OF SUP_def]) |
|
61 apply (rule ordLeq_transitive) |
|
62 apply (rule card_of_UNION_Sigma) |
|
63 apply (subst SIGMA_CSUM) |
|
64 apply (rule ordLeq_transitive) |
|
65 apply (rule card_of_Csum_Times') |
|
66 apply (rule fbd_Card_order) |
|
67 apply (rule ballI) |
|
68 apply (rule fset_bd) |
|
69 apply (rule ordLeq_transitive) |
|
70 apply (rule cprod_mono1) |
|
71 apply (rule gset_bd) |
|
72 apply (rule ordIso_imp_ordLeq) |
|
73 apply (rule ordIso_refl) |
|
74 apply (rule Card_order_cprod) |
|
75 done |
|
76 |
|
77 lemma Union_image_insert: "\<Union>f ` insert a B = f a \<union> \<Union>f ` B" |
|
78 by simp |
|
79 |
|
80 lemma Union_image_empty: "A \<union> \<Union>f ` {} = A" |
|
81 by simp |
|
82 |
|
83 definition collect where |
|
84 "collect F x = (\<Union>f \<in> F. f x)" |
|
85 |
|
86 lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)" |
|
87 by (rule ext) (auto simp only: o_apply collect_def) |
|
88 |
|
89 lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F" |
|
90 by (rule ext) (auto simp add: collect_def) |
|
91 |
|
92 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})" |
|
93 by blast |
|
94 |
|
95 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |
|
96 by blast |
|
97 |
|
98 lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a" |
|
99 by simp |
|
100 |
|
101 lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D" |
|
102 by simp |
|
103 |
|
104 lemma UN_image_subset: "\<Union>f ` g x \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})" |
|
105 by blast |
|
106 |
|
107 lemma image_Collect_subsetI: |
|
108 "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B" |
|
109 by blast |
|
110 |
|
111 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>(\<lambda>f. f x) ` X| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd" |
|
112 by (unfold o_apply collect_def SUP_def) |
|
113 |
|
114 lemma sum_case_comp_Inl: |
|
115 "sum_case f g \<circ> Inl = f" |
|
116 unfolding comp_def by simp |
|
117 |
|
118 lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x" |
|
119 by (auto split: sum.splits) |
|
120 |
|
121 lemma converse_mono: |
|
122 "R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2" |
|
123 unfolding converse_def by auto |
|
124 |
|
125 lemma converse_shift: |
|
126 "R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2" |
|
127 unfolding converse_def by auto |
|
128 |
|
129 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A" |
|
130 by auto |
|
131 |
|
132 lemma equiv_triv1: |
|
133 assumes "equiv A R" and "(a, b) \<in> R" and "(a, c) \<in> R" |
|
134 shows "(b, c) \<in> R" |
|
135 using assms unfolding equiv_def sym_def trans_def by blast |
|
136 |
|
137 lemma equiv_triv2: |
|
138 assumes "equiv A R" and "(a, b) \<in> R" and "(b, c) \<in> R" |
|
139 shows "(a, c) \<in> R" |
|
140 using assms unfolding equiv_def trans_def by blast |
|
141 |
|
142 lemma equiv_proj: |
|
143 assumes e: "equiv A R" and "z \<in> R" |
|
144 shows "(proj R o fst) z = (proj R o snd) z" |
|
145 proof - |
|
146 from assms(2) have z: "(fst z, snd z) \<in> R" by auto |
|
147 have P: "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" by (erule equiv_triv1[OF e z]) |
|
148 have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z]) |
|
149 with P show ?thesis unfolding proj_def[abs_def] by auto |
|
150 qed |
|
151 |
|
152 |
|
153 section{* Weak pullbacks: *} |
|
154 |
|
155 definition csquare where |
|
156 "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))" |
|
157 |
|
158 definition wpull where |
|
159 "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> |
|
160 (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> (\<exists> a \<in> A. p1 a = b1 \<and> p2 a = b2))" |
|
161 |
|
162 lemma wpull_cong: |
|
163 "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2" |
|
164 by simp |
|
165 |
|
166 lemma wpull_id: "wpull UNIV B1 B2 id id id id" |
|
167 unfolding wpull_def by simp |
|
168 |
|
169 |
|
170 (* Weak pseudo-pullbacks *) |
|
171 |
|
172 definition wppull where |
|
173 "wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow> |
|
174 (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> |
|
175 (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))" |
|
176 |
|
177 |
|
178 (* The pullback of sets *) |
|
179 definition thePull where |
|
180 "thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}" |
|
181 |
|
182 lemma wpull_thePull: |
|
183 "wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd" |
|
184 unfolding wpull_def thePull_def by auto |
|
185 |
|
186 lemma wppull_thePull: |
|
187 assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" |
|
188 shows |
|
189 "\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2. |
|
190 j a' \<in> A \<and> |
|
191 e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')" |
|
192 (is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')") |
|
193 proof(rule bchoice[of ?A' ?phi], default) |
|
194 fix a' assume a': "a' \<in> ?A'" |
|
195 hence "fst a' \<in> B1" unfolding thePull_def by auto |
|
196 moreover |
|
197 from a' have "snd a' \<in> B2" unfolding thePull_def by auto |
|
198 moreover have "f1 (fst a') = f2 (snd a')" |
|
199 using a' unfolding csquare_def thePull_def by auto |
|
200 ultimately show "\<exists> ja'. ?phi a' ja'" |
|
201 using assms unfolding wppull_def by auto |
|
202 qed |
|
203 |
|
204 lemma wpull_wppull: |
|
205 assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and |
|
206 1: "\<forall> a' \<in> A'. j a' \<in> A \<and> e1 (p1 (j a')) = e1 (p1' a') \<and> e2 (p2 (j a')) = e2 (p2' a')" |
|
207 shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2" |
|
208 unfolding wppull_def proof safe |
|
209 fix b1 b2 |
|
210 assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2" |
|
211 then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'" |
|
212 using wp unfolding wpull_def by blast |
|
213 show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2" |
|
214 apply(rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto |
|
215 qed |
|
216 |
|
217 lemma wppull_id: "\<lbrakk>wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\<rbrakk> \<Longrightarrow> |
|
218 wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2" |
|
219 by (erule wpull_wppull) auto |
|
220 |
|
221 |
|
222 (* Operators: *) |
|
223 definition diag where "diag A \<equiv> {(a,a) | a. a \<in> A}" |
|
224 definition "Gr A f = {(a,f a) | a. a \<in> A}" |
|
225 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}" |
|
226 |
|
227 lemma diagI: "x \<in> A \<Longrightarrow> (x, x) \<in> diag A" |
|
228 unfolding diag_def by simp |
|
229 |
|
230 lemma diagE: "(a, b) \<in> diag A \<Longrightarrow> a = b" |
|
231 unfolding diag_def by simp |
|
232 |
|
233 lemma diagE': "x \<in> diag A \<Longrightarrow> fst x = snd x" |
|
234 unfolding diag_def by auto |
|
235 |
|
236 lemma diag_fst: "x \<in> diag A \<Longrightarrow> fst x \<in> A" |
|
237 unfolding diag_def by auto |
|
238 |
|
239 lemma diag_UNIV: "diag UNIV = Id" |
|
240 unfolding diag_def by auto |
|
241 |
|
242 lemma diag_converse: "diag A = (diag A) ^-1" |
|
243 unfolding diag_def by auto |
|
244 |
|
245 lemma diag_Comp: "diag A = diag A O diag A" |
|
246 unfolding diag_def by auto |
|
247 |
|
248 lemma diag_Gr: "diag A = Gr A id" |
|
249 unfolding diag_def Gr_def by simp |
|
250 |
|
251 lemma diag_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> diag UNIV" |
|
252 unfolding diag_def by auto |
|
253 |
|
254 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g" |
|
255 unfolding image2_def by auto |
|
256 |
|
257 lemma Id_def': "Id = {(a,b). a = b}" |
|
258 by auto |
|
259 |
|
260 lemma Id_alt: "Id = Gr UNIV id" |
|
261 unfolding Gr_def by auto |
|
262 |
|
263 lemma Id_subset: "Id \<subseteq> {(a, b). P a b \<or> a = b}" |
|
264 by auto |
|
265 |
|
266 lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b" |
|
267 by auto |
|
268 |
|
269 lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)" |
|
270 unfolding image2_def Gr_def by auto |
|
271 |
|
272 lemma GrI: "\<lbrakk>x \<in> A; f x = fx\<rbrakk> \<Longrightarrow> (x, fx) \<in> Gr A f" |
|
273 unfolding Gr_def by simp |
|
274 |
|
275 lemma GrE: "(x, fx) \<in> Gr A f \<Longrightarrow> (x \<in> A \<Longrightarrow> f x = fx \<Longrightarrow> P) \<Longrightarrow> P" |
|
276 unfolding Gr_def by simp |
|
277 |
|
278 lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A" |
|
279 unfolding Gr_def by simp |
|
280 |
|
281 lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx" |
|
282 unfolding Gr_def by simp |
|
283 |
|
284 lemma Gr_UNIV_id: "f = id \<Longrightarrow> (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f" |
|
285 unfolding Gr_def by auto |
|
286 |
|
287 lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R" |
|
288 unfolding Gr_def by auto |
|
289 |
|
290 lemma Gr_mono: "A \<subseteq> B \<Longrightarrow> Gr A f \<subseteq> Gr B f" |
|
291 unfolding Gr_def by auto |
|
292 |
|
293 lemma subst_rel_def: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g" |
|
294 by simp |
|
295 |
|
296 lemma abs_pred_def: "\<lbrakk>\<And>x y. (x, y) \<in> rel = pred x y\<rbrakk> \<Longrightarrow> rel = Collect (split pred)" |
|
297 by auto |
|
298 |
|
299 lemma Collect_split_cong: "Collect (split pred) = Collect (split pred') \<Longrightarrow> pred = pred'" |
|
300 by blast |
|
301 |
|
302 lemma pred_def_abs: "rel = Collect (split pred) \<Longrightarrow> pred = (\<lambda>x y. (x, y) \<in> rel)" |
|
303 by auto |
|
304 |
|
305 lemma wpull_Gr: |
|
306 "wpull (Gr A f) A (f ` A) f id fst snd" |
|
307 unfolding wpull_def Gr_def by auto |
|
308 |
|
309 lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B" |
|
310 unfolding Gr_def by auto |
|
311 |
|
312 lemma equiv_Image: "equiv A R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> a \<in> A \<and> b \<in> A \<and> R `` {a} = R `` {b})" |
|
313 unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD) |
|
314 |
|
315 definition relImage where |
|
316 "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}" |
|
317 |
|
318 definition relInvImage where |
|
319 "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}" |
|
320 |
|
321 lemma relImage_Gr: |
|
322 "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f" |
|
323 unfolding relImage_def Gr_def relcomp_def by auto |
|
324 |
|
325 lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1" |
|
326 unfolding Gr_def relcomp_def image_def relInvImage_def by auto |
|
327 |
|
328 lemma relImage_mono: |
|
329 "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f" |
|
330 unfolding relImage_def by auto |
|
331 |
|
332 lemma relInvImage_mono: |
|
333 "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f" |
|
334 unfolding relInvImage_def by auto |
|
335 |
|
336 lemma relInvImage_diag: |
|
337 "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (diag B) f \<subseteq> Id" |
|
338 unfolding relInvImage_def diag_def by auto |
|
339 |
|
340 lemma relInvImage_UNIV_relImage: |
|
341 "R \<subseteq> relInvImage UNIV (relImage R f) f" |
|
342 unfolding relInvImage_def relImage_def by auto |
|
343 |
|
344 lemma relImage_proj: |
|
345 assumes "equiv A R" |
|
346 shows "relImage R (proj R) \<subseteq> diag (A//R)" |
|
347 unfolding relImage_def diag_def apply safe |
|
348 using proj_iff[OF assms] |
|
349 by (metis assms equiv_Image proj_def proj_preserves) |
|
350 |
|
351 lemma relImage_relInvImage: |
|
352 assumes "R \<subseteq> f ` A <*> f ` A" |
|
353 shows "relImage (relInvImage A R f) f = R" |
|
354 using assms unfolding relImage_def relInvImage_def by fastforce |
|
355 |
|
356 |
|
357 (* Relation composition as a weak pseudo-pullback *) |
|
358 |
|
359 (* pick middle *) |
|
360 definition "pickM P Q a c = (SOME b. (a,b) \<in> P \<and> (b,c) \<in> Q)" |
|
361 |
|
362 lemma pickM: |
|
363 assumes "(a,c) \<in> P O Q" |
|
364 shows "(a, pickM P Q a c) \<in> P \<and> (pickM P Q a c, c) \<in> Q" |
|
365 unfolding pickM_def apply(rule someI_ex) |
|
366 using assms unfolding relcomp_def by auto |
|
367 |
|
368 definition fstO where "fstO P Q ac = (fst ac, pickM P Q (fst ac) (snd ac))" |
|
369 definition sndO where "sndO P Q ac = (pickM P Q (fst ac) (snd ac), snd ac)" |
|
370 |
|
371 lemma fstO_in: "ac \<in> P O Q \<Longrightarrow> fstO P Q ac \<in> P" |
|
372 by (metis assms fstO_def pickM surjective_pairing) |
|
373 |
|
374 lemma fst_fstO: "fst bc = (fst \<circ> fstO P Q) bc" |
|
375 unfolding comp_def fstO_def by simp |
|
376 |
|
377 lemma snd_sndO: "snd bc = (snd \<circ> sndO P Q) bc" |
|
378 unfolding comp_def sndO_def by simp |
|
379 |
|
380 lemma sndO_in: "ac \<in> P O Q \<Longrightarrow> sndO P Q ac \<in> Q" |
|
381 by (metis assms sndO_def pickM surjective_pairing) |
|
382 |
|
383 lemma csquare_fstO_sndO: |
|
384 "csquare (P O Q) snd fst (fstO P Q) (sndO P Q)" |
|
385 unfolding csquare_def fstO_def sndO_def using pickM by auto |
|
386 |
|
387 lemma wppull_fstO_sndO: |
|
388 shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)" |
|
389 using pickM unfolding wppull_def fstO_def sndO_def relcomp_def by auto |
|
390 |
|
391 lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)" |
|
392 by simp |
|
393 |
|
394 lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy" |
|
395 by (simp split: prod.split) |
|
396 |
|
397 lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy" |
|
398 by (simp split: prod.split) |
|
399 |
|
400 lemma flip_rel: "A \<subseteq> (R ^-1) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> R" |
|
401 by auto |
|
402 |
|
403 lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" |
|
404 by simp |
|
405 |
|
406 lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" |
|
407 by simp |
|
408 |
|
409 lemma fst_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> fst (snd x) = y" |
|
410 by simp |
|
411 |
|
412 lemma snd_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> snd (snd x) = z" |
|
413 by simp |
|
414 |
|
415 lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y" |
|
416 by simp |
|
417 |
|
418 lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z" |
|
419 by simp |
|
420 |
|
421 lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X" |
|
422 by auto |
|
423 |
|
424 lemma Collect_restrict': "{(x, y) | x y. phi x y \<and> P x y} \<subseteq> {(x, y) | x y. phi x y}" |
|
425 by auto |
|
426 |
|
427 lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x" |
|
428 by auto |
|
429 |
|
430 lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> rel.underS R j" |
|
431 unfolding rel.underS_def by simp |
|
432 |
|
433 lemma underS_E: "i \<in> rel.underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R" |
|
434 unfolding rel.underS_def by simp |
|
435 |
|
436 lemma underS_Field: "i \<in> rel.underS R j \<Longrightarrow> i \<in> Field R" |
|
437 unfolding rel.underS_def Field_def by auto |
|
438 |
|
439 lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R" |
|
440 unfolding Field_def by auto |
|
441 |
|
442 |
|
443 subsection {* Convolution product *} |
|
444 |
|
445 definition convol ("<_ , _>") where |
|
446 "<f , g> \<equiv> %a. (f a, g a)" |
|
447 |
|
448 lemma fst_convol: |
|
449 "fst o <f , g> = f" |
|
450 apply(rule ext) |
|
451 unfolding convol_def by simp |
|
452 |
|
453 lemma snd_convol: |
|
454 "snd o <f , g> = g" |
|
455 apply(rule ext) |
|
456 unfolding convol_def by simp |
|
457 |
|
458 lemma fst_convol': "fst (<f, g> x) = f x" |
|
459 using fst_convol unfolding convol_def by simp |
|
460 |
|
461 lemma snd_convol': "snd (<f, g> x) = g x" |
|
462 using snd_convol unfolding convol_def by simp |
|
463 |
|
464 lemma image_convolD: "\<lbrakk>(a, b) \<in> <f, g> ` X\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> X \<and> a = f x \<and> b = g x" |
|
465 unfolding convol_def by auto |
|
466 |
|
467 lemma convol_expand_snd: "fst o f = g \<Longrightarrow> <g, snd o f> = f" |
|
468 unfolding convol_def by auto |
|
469 |
|
470 subsection{* Facts about functions *} |
|
471 |
|
472 lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)" |
|
473 unfolding o_def fun_eq_iff by simp |
|
474 |
|
475 lemma pointfree_idE: "f o g = id \<Longrightarrow> f (g x) = x" |
|
476 unfolding o_def fun_eq_iff by simp |
|
477 |
|
478 definition inver where |
|
479 "inver g f A = (ALL a : A. g (f a) = a)" |
|
480 |
|
481 lemma bij_betw_iff_ex: |
|
482 "bij_betw f A B = (EX g. g ` B = A \<and> inver g f A \<and> inver f g B)" (is "?L = ?R") |
|
483 proof (rule iffI) |
|
484 assume ?L |
|
485 hence f: "f ` A = B" and inj_f: "inj_on f A" unfolding bij_betw_def by auto |
|
486 let ?phi = "% b a. a : A \<and> f a = b" |
|
487 have "ALL b : B. EX a. ?phi b a" using f by blast |
|
488 then obtain g where g: "ALL b : B. g b : A \<and> f (g b) = b" |
|
489 using bchoice[of B ?phi] by blast |
|
490 hence gg: "ALL b : f ` A. g b : A \<and> f (g b) = b" using f by blast |
|
491 have gf: "inver g f A" unfolding inver_def by (metis gg imageI inj_f the_inv_into_f_f) |
|
492 moreover have "g ` B \<le> A \<and> inver f g B" using g unfolding inver_def by blast |
|
493 moreover have "A \<le> g ` B" |
|
494 proof safe |
|
495 fix a assume a: "a : A" |
|
496 hence "f a : B" using f by auto |
|
497 moreover have "a = g (f a)" using a gf unfolding inver_def by auto |
|
498 ultimately show "a : g ` B" by blast |
|
499 qed |
|
500 ultimately show ?R by blast |
|
501 next |
|
502 assume ?R |
|
503 then obtain g where g: "g ` B = A \<and> inver g f A \<and> inver f g B" by blast |
|
504 show ?L unfolding bij_betw_def |
|
505 proof safe |
|
506 show "inj_on f A" unfolding inj_on_def |
|
507 proof safe |
|
508 fix a1 a2 assume a: "a1 : A" "a2 : A" and "f a1 = f a2" |
|
509 hence "g (f a1) = g (f a2)" by simp |
|
510 thus "a1 = a2" using a g unfolding inver_def by simp |
|
511 qed |
|
512 next |
|
513 fix a assume "a : A" |
|
514 then obtain b where b: "b : B" and a: "a = g b" using g by blast |
|
515 hence "b = f (g b)" using g unfolding inver_def by auto |
|
516 thus "f a : B" unfolding a using b by simp |
|
517 next |
|
518 fix b assume "b : B" |
|
519 hence "g b : A \<and> b = f (g b)" using g unfolding inver_def by auto |
|
520 thus "b : f ` A" by auto |
|
521 qed |
|
522 qed |
|
523 |
|
524 lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f" |
|
525 unfolding bij_def inj_on_def by auto blast |
|
526 |
|
527 lemma bij_betw_ex_weakE: |
|
528 "\<lbrakk>bij_betw f A B\<rbrakk> \<Longrightarrow> \<exists>g. g ` B \<subseteq> A \<and> inver g f A \<and> inver f g B" |
|
529 by (auto simp only: bij_betw_iff_ex) |
|
530 |
|
531 lemma inver_surj: "\<lbrakk>g ` B \<subseteq> A; f ` A \<subseteq> B; inver g f A\<rbrakk> \<Longrightarrow> g ` B = A" |
|
532 unfolding inver_def by auto (rule rev_image_eqI, auto) |
|
533 |
|
534 lemma inver_mono: "\<lbrakk>A \<subseteq> B; inver f g B\<rbrakk> \<Longrightarrow> inver f g A" |
|
535 unfolding inver_def by auto |
|
536 |
|
537 lemma inver_pointfree: "inver f g A = (\<forall>a \<in> A. (f o g) a = a)" |
|
538 unfolding inver_def by simp |
|
539 |
|
540 lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B" |
|
541 unfolding bij_betw_def by auto |
|
542 |
|
543 lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B" |
|
544 unfolding bij_betw_def by auto |
|
545 |
|
546 lemma inverE: "\<lbrakk>inver f f' A; x \<in> A\<rbrakk> \<Longrightarrow> f (f' x) = x" |
|
547 unfolding inver_def by auto |
|
548 |
|
549 lemma bij_betw_inver1: "bij_betw f A B \<Longrightarrow> inver (inv_into A f) f A" |
|
550 unfolding bij_betw_def inver_def by auto |
|
551 |
|
552 lemma bij_betw_inver2: "bij_betw f A B \<Longrightarrow> inver f (inv_into A f) B" |
|
553 unfolding bij_betw_def inver_def by auto |
|
554 |
|
555 lemma bij_betwI: "\<lbrakk>bij_betw g B A; inver g f A; inver f g B\<rbrakk> \<Longrightarrow> bij_betw f A B" |
|
556 by (metis bij_betw_iff_ex bij_betw_imageE) |
|
557 |
|
558 lemma bij_betwI': |
|
559 "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y); |
|
560 \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y; |
|
561 \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y" |
|
562 unfolding bij_betw_def inj_on_def by auto (metis rev_image_eqI) |
|
563 |
|
564 lemma o_bij: |
|
565 assumes gf: "g o f = id" and fg: "f o g = id" |
|
566 shows "bij f" |
|
567 unfolding bij_def inj_on_def surj_def proof safe |
|
568 fix a1 a2 assume "f a1 = f a2" |
|
569 hence "g ( f a1) = g (f a2)" by simp |
|
570 thus "a1 = a2" using gf unfolding fun_eq_iff by simp |
|
571 next |
|
572 fix b |
|
573 have "b = f (g b)" |
|
574 using fg unfolding fun_eq_iff by simp |
|
575 thus "EX a. b = f a" by blast |
|
576 qed |
|
577 |
|
578 lemma surj_fun_eq: |
|
579 assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x" |
|
580 shows "g1 = g2" |
|
581 proof (rule ext) |
|
582 fix y |
|
583 from surj_on obtain x where "x \<in> X" and "y = f x" by blast |
|
584 thus "g1 y = g2 y" using eq_on by simp |
|
585 qed |
|
586 |
|
587 lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r" |
|
588 unfolding wo_rel_def card_order_on_def by blast |
|
589 |
|
590 lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow> |
|
591 \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r" |
|
592 unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit) |
|
593 |
|
594 lemma Card_order_trans: |
|
595 "\<lbrakk>Card_order r; x \<noteq> y; (x, y) \<in> r; y \<noteq> z; (y, z) \<in> r\<rbrakk> \<Longrightarrow> x \<noteq> z \<and> (x, z) \<in> r" |
|
596 unfolding card_order_on_def well_order_on_def linear_order_on_def |
|
597 partial_order_on_def preorder_on_def trans_def antisym_def by blast |
|
598 |
|
599 lemma Cinfinite_limit2: |
|
600 assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r" |
|
601 shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)" |
|
602 proof - |
|
603 from r have trans: "trans r" and total: "Total r" and antisym: "antisym r" |
|
604 unfolding card_order_on_def well_order_on_def linear_order_on_def |
|
605 partial_order_on_def preorder_on_def by auto |
|
606 obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r" |
|
607 using Cinfinite_limit[OF x1 r] by blast |
|
608 obtain y2 where y2: "y2 \<in> Field r" "x2 \<noteq> y2" "(x2, y2) \<in> r" |
|
609 using Cinfinite_limit[OF x2 r] by blast |
|
610 show ?thesis |
|
611 proof (cases "y1 = y2") |
|
612 case True with y1 y2 show ?thesis by blast |
|
613 next |
|
614 case False |
|
615 with y1(1) y2(1) total have "(y1, y2) \<in> r \<or> (y2, y1) \<in> r" |
|
616 unfolding total_on_def by auto |
|
617 thus ?thesis |
|
618 proof |
|
619 assume *: "(y1, y2) \<in> r" |
|
620 with trans y1(3) have "(x1, y2) \<in> r" unfolding trans_def by blast |
|
621 with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def) |
|
622 next |
|
623 assume *: "(y2, y1) \<in> r" |
|
624 with trans y2(3) have "(x2, y1) \<in> r" unfolding trans_def by blast |
|
625 with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def) |
|
626 qed |
|
627 qed |
|
628 qed |
|
629 |
|
630 lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk> |
|
631 \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" |
|
632 proof (induct X rule: finite_induct) |
|
633 case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto |
|
634 next |
|
635 case (insert x X) |
|
636 then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast |
|
637 then obtain z where z: "z \<in> Field r" "x \<noteq> z \<and> (x, z) \<in> r" "y \<noteq> z \<and> (y, z) \<in> r" |
|
638 using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast |
|
639 show ?case by (metis Card_order_trans insert(5) insertE y(2) z) |
|
640 qed |
|
641 |
|
642 lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A" |
|
643 by auto |
|
644 |
|
645 (*helps resolution*) |
|
646 lemma well_order_induct_imp: |
|
647 "wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow> |
|
648 x \<in> Field r \<longrightarrow> P x" |
|
649 by (erule wo_rel.well_order_induct) |
|
650 |
|
651 lemma meta_spec2: |
|
652 assumes "(\<And>x y. PROP P x y)" |
|
653 shows "PROP P x y" |
|
654 by (rule `(\<And>x y. PROP P x y)`) |
|
655 |
|
656 (*Extended Sublist*) |
|
657 |
|
658 definition prefCl where |
|
659 "prefCl Kl = (\<forall> kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)" |
|
660 definition PrefCl where |
|
661 "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> kl' \<le> kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))" |
|
662 |
|
663 lemma prefCl_UN: |
|
664 "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)" |
|
665 unfolding prefCl_def PrefCl_def by fastforce |
|
666 |
|
667 definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}" |
|
668 definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}" |
|
669 definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))" |
|
670 |
|
671 lemmas sh_def = Shift_def shift_def |
|
672 |
|
673 lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k" |
|
674 unfolding Shift_def Succ_def by simp |
|
675 |
|
676 lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)" |
|
677 unfolding Shift_def clists_def Field_card_of by auto |
|
678 |
|
679 lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)" |
|
680 unfolding prefCl_def Shift_def |
|
681 proof safe |
|
682 fix kl1 kl2 |
|
683 assume "\<forall>kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl" |
|
684 "kl1 \<le> kl2" "k # kl2 \<in> Kl" |
|
685 thus "k # kl1 \<in> Kl" using Cons_prefix_Cons[of k kl1 k kl2] by blast |
|
686 qed |
|
687 |
|
688 lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl" |
|
689 unfolding Shift_def by simp |
|
690 |
|
691 lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []" |
|
692 unfolding Succ_def proof |
|
693 assume "prefCl Kl" "k # kl \<in> Kl" |
|
694 moreover have "k # [] \<le> k # kl" by auto |
|
695 ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast |
|
696 thus "[] @ [k] \<in> Kl" by simp |
|
697 qed |
|
698 |
|
699 lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl" |
|
700 unfolding Succ_def by simp |
|
701 |
|
702 lemmas SuccE = SuccD[elim_format] |
|
703 |
|
704 lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl" |
|
705 unfolding Succ_def by simp |
|
706 |
|
707 lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl" |
|
708 unfolding Shift_def by simp |
|
709 |
|
710 lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)" |
|
711 unfolding Succ_def Shift_def by auto |
|
712 |
|
713 lemma ShiftI: "k # kl \<in> Kl \<Longrightarrow> kl \<in> Shift Kl k" |
|
714 unfolding Shift_def by simp |
|
715 |
|
716 lemma Func_cexp: "|Func A B| =o |B| ^c |A|" |
|
717 unfolding cexp_def Field_card_of by (simp only: card_of_refl) |
|
718 |
|
719 lemma clists_bound: "A \<in> Field (cpow (clists r)) - {{}} \<Longrightarrow> |A| \<le>o clists r" |
|
720 unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1) |
|
721 |
|
722 lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False" |
|
723 unfolding cpow_def clists_def |
|
724 by (auto simp add: card_of_ordIso_czero_iff_empty[symmetric]) |
|
725 (erule notE, erule ordIso_transitive, rule czero_ordIso) |
|
726 |
|
727 lemma incl_UNION_I: |
|
728 assumes "i \<in> I" and "A \<subseteq> F i" |
|
729 shows "A \<subseteq> UNION I F" |
|
730 using assms by auto |
|
731 |
|
732 lemma Nil_clists: "{[]} \<subseteq> Field (clists r)" |
|
733 unfolding clists_def Field_card_of by auto |
|
734 |
|
735 lemma Cons_clists: |
|
736 "\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)" |
|
737 unfolding clists_def Field_card_of by auto |
|
738 |
|
739 lemma length_Cons: "length (x#xs) = Suc (length xs)" |
|
740 by simp |
|
741 |
|
742 lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)" |
|
743 by simp |
|
744 |
|
745 (*injection into the field of a cardinal*) |
|
746 definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r" |
|
747 definition "toCard A r \<equiv> SOME f. toCard_pred A r f" |
|
748 |
|
749 lemma ex_toCard_pred: |
|
750 "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f" |
|
751 unfolding toCard_pred_def |
|
752 using card_of_ordLeq[of A "Field r"] |
|
753 ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"] |
|
754 by blast |
|
755 |
|
756 lemma toCard_pred_toCard: |
|
757 "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)" |
|
758 unfolding toCard_def using someI_ex[OF ex_toCard_pred] . |
|
759 |
|
760 lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> |
|
761 toCard A r x = toCard A r y \<longleftrightarrow> x = y" |
|
762 using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast |
|
763 |
|
764 lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r" |
|
765 using toCard_pred_toCard unfolding toCard_pred_def by blast |
|
766 |
|
767 definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k" |
|
768 |
|
769 lemma fromCard_toCard: |
|
770 "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b" |
|
771 unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj) |
|
772 |
|
773 (* pick according to the weak pullback *) |
|
774 definition pickWP_pred where |
|
775 "pickWP_pred A p1 p2 b1 b2 a \<equiv> |
|
776 a \<in> A \<and> p1 a = b1 \<and> p2 a = b2" |
|
777 |
|
778 definition pickWP where |
|
779 "pickWP A p1 p2 b1 b2 \<equiv> |
|
780 SOME a. pickWP_pred A p1 p2 b1 b2 a" |
|
781 |
|
782 lemma pickWP_pred: |
|
783 assumes "wpull A B1 B2 f1 f2 p1 p2" and |
|
784 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2" |
|
785 shows "\<exists> a. pickWP_pred A p1 p2 b1 b2 a" |
|
786 using assms unfolding wpull_def pickWP_pred_def by blast |
|
787 |
|
788 lemma pickWP_pred_pickWP: |
|
789 assumes "wpull A B1 B2 f1 f2 p1 p2" and |
|
790 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2" |
|
791 shows "pickWP_pred A p1 p2 b1 b2 (pickWP A p1 p2 b1 b2)" |
|
792 unfolding pickWP_def using assms by(rule someI_ex[OF pickWP_pred]) |
|
793 |
|
794 lemma pickWP: |
|
795 assumes "wpull A B1 B2 f1 f2 p1 p2" and |
|
796 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2" |
|
797 shows "pickWP A p1 p2 b1 b2 \<in> A" |
|
798 "p1 (pickWP A p1 p2 b1 b2) = b1" |
|
799 "p2 (pickWP A p1 p2 b1 b2) = b2" |
|
800 using assms pickWP_pred_pickWP unfolding pickWP_pred_def by fastforce+ |
|
801 |
|
802 lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp |
|
803 |
|
804 lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)" |
|
805 unfolding Field_card_of csum_def by auto |
|
806 |
|
807 lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)" |
|
808 unfolding Field_card_of csum_def by auto |
|
809 |
|
810 lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1" |
|
811 by auto |
|
812 |
|
813 lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)" |
|
814 by auto |
|
815 |
|
816 lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1" |
|
817 by auto |
|
818 |
|
819 lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)" |
|
820 by auto |
|
821 |
|
822 lemma sum_case_cong: "p = q \<Longrightarrow> sum_case f g p = sum_case f g q" |
|
823 by simp |
|
824 |
|
825 lemma sum_case_step: |
|
826 "sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p" |
|
827 "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p" |
|
828 by auto |
|
829 |
|
830 lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
|
831 by simp |
|
832 |
|
833 lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P" |
|
834 by blast |
|
835 |
|
836 lemma obj_sumE_f: |
|
837 "\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P" |
|
838 by (metis sum.exhaust) |
|
839 |
|
840 lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
|
841 by (cases s) auto |
|
842 |
|
843 lemma obj_sum_step: |
|
844 "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P" |
|
845 by (metis obj_sumE) |
|
846 |
|
847 lemma sum_case_if: |
|
848 "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" |
|
849 by simp |
|
850 |
|
851 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y" |
|
852 by simp |
|
853 |
|
854 end |