src/HOL/Basic_BNFs.thy
 author blanchet Thu Mar 06 15:29:18 2014 +0100 (2014-03-06) changeset 55944 7ab8f003fe41 parent 55943 5c2df04e97d1 child 55945 e96383acecf9 permissions -rw-r--r--
renamed 'prod_rel' to 'rel_prod'
1 (*  Title:      HOL/Basic_BNFs.thy
2     Author:     Dmitriy Traytel, TU Muenchen
3     Author:     Andrei Popescu, TU Muenchen
4     Author:     Jasmin Blanchette, TU Muenchen
5     Copyright   2012
7 Registration of basic types as bounded natural functors.
8 *)
10 header {* Registration of Basic Types as Bounded Natural Functors *}
12 theory Basic_BNFs
13 imports BNF_Def
14 begin
16 definition setl :: "'a + 'b \<Rightarrow> 'a set" where
17 "setl x = (case x of Inl z => {z} | _ => {})"
19 definition setr :: "'a + 'b \<Rightarrow> 'b set" where
20 "setr x = (case x of Inr z => {z} | _ => {})"
22 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
24 definition
25    rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
26 where
27    "rel_sum R1 R2 x y =
28      (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
29      | (Inr x, Inr y) \<Rightarrow> R2 x y
30      | _ \<Rightarrow> False)"
32 lemma rel_sum_simps[simp]:
33   "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
34   "rel_sum R1 R2 (Inl a1) (Inr b2) = False"
35   "rel_sum R1 R2 (Inr a2) (Inl b1) = False"
36   "rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
37   unfolding rel_sum_def by simp_all
39 bnf "'a + 'b"
40   map: map_sum
41   sets: setl setr
42   bd: natLeq
43   wits: Inl Inr
44   rel: rel_sum
45 proof -
46   show "map_sum id id = id" by (rule map_sum.id)
47 next
48   fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
49   show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2"
50     by (rule map_sum.comp[symmetric])
51 next
52   fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
53   assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
54          a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
55   thus "map_sum f1 f2 x = map_sum g1 g2 x"
56   proof (cases x)
57     case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
58   next
59     case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
60   qed
61 next
62   fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
63   show "setl o map_sum f1 f2 = image f1 o setl"
64     by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
65 next
66   fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
67   show "setr o map_sum f1 f2 = image f2 o setr"
68     by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
69 next
70   show "card_order natLeq" by (rule natLeq_card_order)
71 next
72   show "cinfinite natLeq" by (rule natLeq_cinfinite)
73 next
74   fix x :: "'o + 'p"
75   show "|setl x| \<le>o natLeq"
76     apply (rule ordLess_imp_ordLeq)
77     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
78     by (simp add: setl_def split: sum.split)
79 next
80   fix x :: "'o + 'p"
81   show "|setr x| \<le>o natLeq"
82     apply (rule ordLess_imp_ordLeq)
83     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
84     by (simp add: setr_def split: sum.split)
85 next
86   fix R1 R2 S1 S2
87   show "rel_sum R1 R2 OO rel_sum S1 S2 \<le> rel_sum (R1 OO S1) (R2 OO S2)"
88     by (auto simp: rel_sum_def split: sum.splits)
89 next
90   fix R S
91   show "rel_sum R S =
92         (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
93         Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
94   unfolding setl_def setr_def rel_sum_def Grp_def relcompp.simps conversep.simps fun_eq_iff
95   by (fastforce split: sum.splits)
96 qed (auto simp: sum_set_defs)
98 definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
99 "fsts x = {fst x}"
101 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
102 "snds x = {snd x}"
104 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
106 definition
107   rel_prod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
108 where
109   "rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
111 lemma rel_prod_apply [simp]:
112   "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
113   by (simp add: rel_prod_def)
115 bnf "'a \<times> 'b"
116   map: map_prod
117   sets: fsts snds
118   bd: natLeq
119   rel: rel_prod
120 proof (unfold prod_set_defs)
121   show "map_prod id id = id" by (rule map_prod.id)
122 next
123   fix f1 f2 g1 g2
124   show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2"
125     by (rule map_prod.comp[symmetric])
126 next
127   fix x f1 f2 g1 g2
128   assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
129   thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp
130 next
131   fix f1 f2
132   show "(\<lambda>x. {fst x}) o map_prod f1 f2 = image f1 o (\<lambda>x. {fst x})"
133     by (rule ext, unfold o_apply) simp
134 next
135   fix f1 f2
136   show "(\<lambda>x. {snd x}) o map_prod f1 f2 = image f2 o (\<lambda>x. {snd x})"
137     by (rule ext, unfold o_apply) simp
138 next
139   show "card_order natLeq" by (rule natLeq_card_order)
140 next
141   show "cinfinite natLeq" by (rule natLeq_cinfinite)
142 next
143   fix x
144   show "|{fst x}| \<le>o natLeq"
145     by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
146 next
147   fix x
148   show "|{snd x}| \<le>o natLeq"
149     by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
150 next
151   fix R1 R2 S1 S2
152   show "rel_prod R1 R2 OO rel_prod S1 S2 \<le> rel_prod (R1 OO S1) (R2 OO S2)" by auto
153 next
154   fix R S
155   show "rel_prod R S =
156         (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
157         Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
158   unfolding prod_set_defs rel_prod_def Grp_def relcompp.simps conversep.simps fun_eq_iff
159   by auto
160 qed
162 bnf "'a \<Rightarrow> 'b"
163   map: "op \<circ>"
164   sets: range
165   bd: "natLeq +c |UNIV :: 'a set|"
166   rel: "fun_rel op ="
167 proof
168   fix f show "id \<circ> f = id f" by simp
169 next
170   fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
171   unfolding comp_def[abs_def] ..
172 next
173   fix x f g
174   assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
175   thus "f \<circ> x = g \<circ> x" by auto
176 next
177   fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
178   unfolding image_def comp_def[abs_def] by auto
179 next
180   show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
181   apply (rule card_order_csum)
182   apply (rule natLeq_card_order)
183   by (rule card_of_card_order_on)
184 (*  *)
185   show "cinfinite (natLeq +c ?U)"
186     apply (rule cinfinite_csum)
187     apply (rule disjI1)
188     by (rule natLeq_cinfinite)
189 next
190   fix f :: "'d => 'a"
191   have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
192   also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
193   finally show "|range f| \<le>o natLeq +c ?U" .
194 next
195   fix R S
196   show "fun_rel op = R OO fun_rel op = S \<le> fun_rel op = (R OO S)" by (auto simp: fun_rel_def)
197 next
198   fix R
199   show "fun_rel op = R =
200         (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
201          Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
202   unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
203     comp_apply mem_Collect_eq split_beta bex_UNIV
204   proof (safe, unfold fun_eq_iff[symmetric])
205     fix x xa a b c xb y aa ba
206     assume *: "x = a" "xa = c" "a = ba" "b = aa" "c = (\<lambda>x. snd (b x))" "ba = (\<lambda>x. fst (aa x))" and
207        **: "\<forall>t. (\<exists>x. t = aa x) \<longrightarrow> R (fst t) (snd t)"
208     show "R (x y) (xa y)" unfolding * by (rule mp[OF spec[OF **]]) blast
209   qed force
210 qed
212 end