23 |
23 |
24 lemma natLeq_cinfinite: "cinfinite natLeq" |
24 lemma natLeq_cinfinite: "cinfinite natLeq" |
25 unfolding cinfinite_def Field_natLeq by (rule nat_infinite) |
25 unfolding cinfinite_def Field_natLeq by (rule nat_infinite) |
26 |
26 |
27 bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"] |
27 bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"] |
|
28 "\<lambda>x :: ('a \<times> 'b) set. x" |
28 apply auto |
29 apply auto |
29 apply (rule natLeq_card_order) |
30 apply (rule natLeq_card_order) |
30 apply (rule natLeq_cinfinite) |
31 apply (rule natLeq_cinfinite) |
31 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) |
32 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) |
32 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on) |
33 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] |
33 apply (rule ordLeq_transitive) |
34 apply (rule ordLeq_transitive) |
34 apply (rule ordLeq_cexp1[of natLeq]) |
35 apply (rule ordLeq_cexp1[of natLeq]) |
35 apply (rule Cinfinite_Cnotzero) |
36 apply (rule Cinfinite_Cnotzero) |
36 apply (rule conjI) |
37 apply (rule conjI) |
37 apply (rule natLeq_cinfinite) |
38 apply (rule natLeq_cinfinite) |
45 apply (rule ordLeq_transitive) |
46 apply (rule ordLeq_transitive) |
46 apply (rule cone_ordLeq_ctwo) |
47 apply (rule cone_ordLeq_ctwo) |
47 apply (rule ordLeq_csum2) |
48 apply (rule ordLeq_csum2) |
48 apply (rule Card_order_ctwo) |
49 apply (rule Card_order_ctwo) |
49 apply (rule natLeq_Card_order) |
50 apply (rule natLeq_Card_order) |
|
51 apply (auto simp: Gr_def fun_eq_iff) |
50 done |
52 done |
51 |
53 |
52 lemma ID_pred[simp]: "ID_pred \<phi> = \<phi>" |
54 bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] Id |
53 unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto |
|
54 |
|
55 bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] |
|
56 apply (auto simp add: wpull_id) |
55 apply (auto simp add: wpull_id) |
57 apply (rule card_order_csum) |
56 apply (rule card_order_csum) |
58 apply (rule natLeq_card_order) |
57 apply (rule natLeq_card_order) |
59 apply (rule card_of_card_order_on) |
58 apply (rule card_of_card_order_on) |
60 apply (rule cinfinite_csum) |
59 apply (rule cinfinite_csum) |
66 apply (rule card_of_Card_order) |
65 apply (rule card_of_Card_order) |
67 apply (rule cexp_mono2'') |
66 apply (rule cexp_mono2'') |
68 apply (rule ordLeq_csum2) |
67 apply (rule ordLeq_csum2) |
69 apply (rule card_of_Card_order) |
68 apply (rule card_of_Card_order) |
70 apply (rule ctwo_Cnotzero) |
69 apply (rule ctwo_Cnotzero) |
71 by (rule card_of_Card_order) |
70 apply (rule card_of_Card_order) |
72 |
71 apply (auto simp: Id_def Gr_def fun_eq_iff) |
73 lemma DEADID_pred[simp]: "DEADID_pred = (op =)" |
72 done |
74 unfolding DEADID_pred_def DEADID.rel_Id by simp |
|
75 |
73 |
76 definition setl :: "'a + 'b \<Rightarrow> 'a set" where |
74 definition setl :: "'a + 'b \<Rightarrow> 'a set" where |
77 "setl x = (case x of Inl z => {z} | _ => {})" |
75 "setl x = (case x of Inl z => {z} | _ => {})" |
78 |
76 |
79 definition setr :: "'a + 'b \<Rightarrow> 'b set" where |
77 definition setr :: "'a + 'b \<Rightarrow> 'b set" where |
80 "setr x = (case x of Inr z => {z} | _ => {})" |
78 "setr x = (case x of Inr z => {z} | _ => {})" |
81 |
79 |
82 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def] |
80 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def] |
83 |
81 |
84 bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] |
82 (*### RENAME TODO *) |
|
83 definition sum_rel0 :: "('a \<times> 'b) set \<Rightarrow> ('c \<times> 'd) set \<Rightarrow> (('a + 'c) \<times> ('b + 'd)) set" where |
|
84 "sum_rel0 R S = |
|
85 {x. case x of (Inl a, Inl c) \<Rightarrow> (a, c) \<in> R |
|
86 | (Inr b, Inr d) \<Rightarrow> (b, d) \<in> S |
|
87 | _ \<Rightarrow> False}" |
|
88 |
|
89 bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel0 |
85 proof - |
90 proof - |
86 show "sum_map id id = id" by (rule sum_map.id) |
91 show "sum_map id id = id" by (rule sum_map.id) |
87 next |
92 next |
88 fix f1 f2 g1 g2 |
93 fix f1 f2 g1 g2 |
89 show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2" |
94 show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2" |
188 qed |
193 qed |
189 } |
194 } |
190 thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow> |
195 thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow> |
191 (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce |
196 (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce |
192 qed |
197 qed |
|
198 next |
|
199 fix R S |
|
200 show "sum_rel0 R S = |
|
201 (Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map fst fst))\<inverse> O |
|
202 Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map snd snd)" |
|
203 unfolding setl_def setr_def sum_rel0_def Gr_def relcomp_unfold converse_unfold |
|
204 by (fastforce split: sum.splits) |
193 qed (auto simp: sum_set_defs) |
205 qed (auto simp: sum_set_defs) |
194 |
|
195 lemma sum_pred[simp]: |
|
196 "sum_pred \<phi> \<psi> x y = |
|
197 (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False) |
|
198 | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))" |
|
199 unfolding setl_def setr_def sum_pred_def sum_rel_def Gr_def relcomp_unfold converse_unfold |
|
200 by (fastforce split: sum.splits)+ |
|
201 |
206 |
202 lemma singleton_ordLeq_ctwo_natLeq: "|{x}| \<le>o ctwo *c natLeq" |
207 lemma singleton_ordLeq_ctwo_natLeq: "|{x}| \<le>o ctwo *c natLeq" |
203 apply (rule ordLeq_transitive) |
208 apply (rule ordLeq_transitive) |
204 apply (rule ordLeq_cprod2) |
209 apply (rule ordLeq_cprod2) |
205 apply (rule ctwo_Cnotzero) |
210 apply (rule ctwo_Cnotzero) |
215 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where |
220 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where |
216 "snds x = {snd x}" |
221 "snds x = {snd x}" |
217 |
222 |
218 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] |
223 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] |
219 |
224 |
220 bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] |
225 definition prod_rel0 :: "('a \<times> 'b) set \<Rightarrow> ('c \<times> 'd) set \<Rightarrow> (('a \<times> 'c) \<times> 'b \<times> 'd) set" where |
|
226 "prod_rel0 R S = {((a, c), b, d) | a b c d. (a, b) \<in> R \<and> (c, d) \<in> S}" |
|
227 |
|
228 bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel0 |
221 proof (unfold prod_set_defs) |
229 proof (unfold prod_set_defs) |
222 show "map_pair id id = id" by (rule map_pair.id) |
230 show "map_pair id id = id" by (rule map_pair.id) |
223 next |
231 next |
224 fix f1 f2 g1 g2 |
232 fix f1 f2 g1 g2 |
225 show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2" |
233 show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2" |
290 assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22" |
298 assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22" |
291 thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} |
299 thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} |
292 {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22} |
300 {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22} |
293 (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)" |
301 (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)" |
294 unfolding wpull_def by simp fast |
302 unfolding wpull_def by simp fast |
|
303 next |
|
304 fix R S |
|
305 show "prod_rel0 R S = |
|
306 (Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair fst fst))\<inverse> O |
|
307 Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair snd snd)" |
|
308 unfolding prod_set_defs prod_rel0_def Gr_def relcomp_unfold converse_unfold |
|
309 by auto |
295 qed simp+ |
310 qed simp+ |
296 |
|
297 lemma prod_pred[simp]: |
|
298 "prod_pred \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> (\<phi> a1 a2 \<and> \<psi> b1 b2))" |
|
299 unfolding prod_set_defs prod_pred_def prod_rel_def Gr_def relcomp_unfold converse_unfold by auto |
|
300 |
311 |
301 (* Categorical version of pullback: *) |
312 (* Categorical version of pullback: *) |
302 lemma wpull_cat: |
313 lemma wpull_cat: |
303 assumes p: "wpull A B1 B2 f1 f2 p1 p2" |
314 assumes p: "wpull A B1 B2 f1 f2 p1 p2" |
304 and c: "f1 o q1 = f2 o q2" |
315 and c: "f1 o q1 = f2 o q2" |
332 qed |
343 qed |
333 moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce |
344 moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce |
334 ultimately show ?thesis using card_of_ordLeq by fast |
345 ultimately show ?thesis using card_of_ordLeq by fast |
335 qed |
346 qed |
336 |
347 |
337 bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" |
348 definition fun_rel0 :: "('a \<times> 'b) set \<Rightarrow> (('c \<Rightarrow> 'a) \<times> ('c \<Rightarrow> 'b)) set" where |
338 ["%c x::'b::type. c::'a::type"] |
349 "fun_rel0 R = {(f, g) | f g. \<forall>x. (f x, g x) \<in> R}" |
|
350 |
|
351 bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"] |
|
352 fun_rel0 |
339 proof |
353 proof |
340 fix f show "id \<circ> f = id f" by simp |
354 fix f show "id \<circ> f = id f" by simp |
341 next |
355 next |
342 fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f" |
356 fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f" |
343 unfolding comp_def[abs_def] .. |
357 unfolding comp_def[abs_def] .. |
391 fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2" |
405 fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2" |
392 and c: "f1 \<circ> g1 = f2 \<circ> g2" |
406 and c: "f1 \<circ> g1 = f2 \<circ> g2" |
393 show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2" |
407 show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2" |
394 using wpull_cat[OF p c r] by simp metis |
408 using wpull_cat[OF p c r] by simp metis |
395 qed |
409 qed |
|
410 next |
|
411 fix R |
|
412 show "fun_rel0 R = (Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)" |
|
413 unfolding fun_rel0_def Gr_def relcomp_unfold converse_unfold |
|
414 by (auto intro!: exI dest!: in_mono) |
396 qed auto |
415 qed auto |
397 |
416 |
398 lemma fun_pred[simp]: "fun_pred \<phi> f g = (\<forall>x. \<phi> (f x) (g x))" |
|
399 unfolding fun_rel_def fun_pred_def Gr_def relcomp_unfold converse_unfold |
|
400 by (auto intro!: exI dest!: in_mono) |
|
401 |
|
402 end |
417 end |