1 (* Title: HOL/BNF/Basic_BNFs.thy
2 Author: Dmitriy Traytel, TU Muenchen
3 Author: Andrei Popescu, TU Muenchen
4 Author: Jasmin Blanchette, TU Muenchen
7 Registration of basic types as bounded natural functors.
10 header {* Registration of Basic Types as Bounded Natural Functors *}
14 (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
20 lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Grp B1 f1 OO (Grp B2 f2)\<inverse>\<inverse> \<le> (Grp A p1)\<inverse>\<inverse> OO Grp A p2"
21 unfolding wpull_def Grp_def by auto
24 map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
25 sets: "\<lambda>x. {x}"
27 rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
28 apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
29 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
30 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
34 map: "id :: 'a \<Rightarrow> 'a"
35 bd: "natLeq +c |UNIV :: 'a set|"
36 rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
37 by (auto simp add: wpull_Grp_def Grp_def
38 card_order_csum natLeq_card_order card_of_card_order_on
39 cinfinite_csum natLeq_cinfinite)
41 definition setl :: "'a + 'b \<Rightarrow> 'a set" where
42 "setl x = (case x of Inl z => {z} | _ => {})"
44 definition setr :: "'a + 'b \<Rightarrow> 'b set" where
45 "setr x = (case x of Inr z => {z} | _ => {})"
47 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
56 show "sum_map id id = id" by (rule sum_map.id)
58 fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
59 show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
60 by (rule sum_map.comp[symmetric])
62 fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
63 assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
64 a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
65 thus "sum_map f1 f2 x = sum_map g1 g2 x"
67 case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
69 case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
72 fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
73 show "setl o sum_map f1 f2 = image f1 o setl"
74 by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
76 fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
77 show "setr o sum_map f1 f2 = image f2 o setr"
78 by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
80 show "card_order natLeq" by (rule natLeq_card_order)
82 show "cinfinite natLeq" by (rule natLeq_cinfinite)
85 show "|setl x| \<le>o natLeq"
86 apply (rule ordLess_imp_ordLeq)
87 apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
88 by (simp add: setl_def split: sum.split)
91 show "|setr x| \<le>o natLeq"
92 apply (rule ordLess_imp_ordLeq)
93 apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
94 by (simp add: setr_def split: sum.split)
96 fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
97 assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
99 pull1: "\<And>b1 b2. \<lbrakk>b1 \<in> B11; b2 \<in> B21; f11 b1 = f21 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A1. p11 a = b1 \<and> p21 a = b2"
100 and pull2: "\<And>b1 b2. \<lbrakk>b1 \<in> B12; b2 \<in> B22; f12 b1 = f22 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A2. p12 a = b1 \<and> p22 a = b2"
101 unfolding wpull_def by blast+
102 show "wpull {x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2}
103 {x. setl x \<subseteq> B11 \<and> setr x \<subseteq> B12} {x. setl x \<subseteq> B21 \<and> setr x \<subseteq> B22}
104 (sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)"
105 (is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2")
106 proof (unfold wpull_def)
108 assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2"
109 have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2"
112 { fix b2 assume "B2 = Inr b2"
113 with Inl *(3) have False by simp
114 } then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast)
115 with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2"
116 by (simp add: setl_def)+
117 with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+
118 with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2"
119 by (simp add: sum_set_defs)+
120 thus ?thesis by blast
123 { fix b2 assume "B2 = Inl b2"
124 with Inr *(3) have False by simp
125 } then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast)
126 with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2"
127 by (simp add: sum_set_defs)+
128 with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+
129 with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2"
130 by (simp add: sum_set_defs)+
131 thus ?thesis by blast
134 thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow>
135 (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce
140 (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
141 Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
142 unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
143 by (fastforce split: sum.splits)
144 qed (auto simp: sum_set_defs)
146 definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
149 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
152 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
159 proof (unfold prod_set_defs)
160 show "map_pair id id = id" by (rule map_pair.id)
163 show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
164 by (rule map_pair.comp[symmetric])
167 assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
168 thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
171 show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
172 by (rule ext, unfold o_apply) simp
175 show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
176 by (rule ext, unfold o_apply) simp
178 show "card_order natLeq" by (rule natLeq_card_order)
180 show "cinfinite natLeq" by (rule natLeq_cinfinite)
183 show "|{fst x}| \<le>o natLeq"
184 by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
187 show "|{snd x}| \<le>o natLeq"
188 by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
190 fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
191 assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
192 thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}
193 {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22}
194 (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)"
195 unfolding wpull_def by simp fast
199 (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
200 Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
201 unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
205 (* Categorical version of pullback: *)
207 assumes p: "wpull A B1 B2 f1 f2 p1 p2"
208 and c: "f1 o q1 = f2 o q2"
209 and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2"
210 obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h"
212 have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d"
215 have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong)
217 have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto
218 ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d"
219 using p unfolding wpull_def by auto
221 then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis
222 thus ?thesis using that by fastforce
225 bnf "'a \<Rightarrow> 'b"
228 bd: "natLeq +c |UNIV :: 'a set|"
231 fix f show "id \<circ> f = id f" by simp
233 fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
234 unfolding comp_def[abs_def] ..
237 assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
238 thus "f \<circ> x = g \<circ> x" by auto
240 fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
241 unfolding image_def comp_def[abs_def] by auto
243 show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
244 apply (rule card_order_csum)
245 apply (rule natLeq_card_order)
246 by (rule card_of_card_order_on)
248 show "cinfinite (natLeq +c ?U)"
249 apply (rule cinfinite_csum)
251 by (rule natLeq_cinfinite)
254 have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
255 also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
256 finally show "|range f| \<le>o natLeq +c ?U" .
258 fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2"
259 show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2}
260 (op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)"
263 fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2"
264 and c: "f1 \<circ> g1 = f2 \<circ> g2"
265 show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2"
266 using wpull_cat[OF p c r] by simp metis
270 show "fun_rel op = R =
271 (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
272 Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
273 unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
274 by auto (force, metis (no_types) pair_collapse)