src/HOL/BNF/Basic_BNFs.thy
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 54191 7fba375a7e7d
child 54421 632be352a5a3
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
     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
     5     Copyright   2012
     6 
     7 Registration of basic types as bounded natural functors.
     8 *)
     9 
    10 header {* Registration of Basic Types as Bounded Natural Functors *}
    11 
    12 theory Basic_BNFs
    13 imports BNF_Def
    14 begin
    15 
    16 lemma wpull_id: "wpull UNIV B1 B2 id id id id"
    17 unfolding wpull_def by simp
    18 
    19 lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
    20 
    21 lemma ctwo_card_order: "card_order ctwo"
    22 using Card_order_ctwo by (unfold ctwo_def Field_card_of)
    23 
    24 lemma natLeq_cinfinite: "cinfinite natLeq"
    25 unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
    26 
    27 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"
    28   unfolding wpull_def Grp_def by auto
    29 
    30 bnf ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq"
    31   "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    32 apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
    33 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    34 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
    35 done
    36 
    37 bnf DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
    38 by (auto simp add: wpull_Grp_def Grp_def
    39   card_order_csum natLeq_card_order card_of_card_order_on
    40   cinfinite_csum natLeq_cinfinite)
    41 
    42 definition setl :: "'a + 'b \<Rightarrow> 'a set" where
    43 "setl x = (case x of Inl z => {z} | _ => {})"
    44 
    45 definition setr :: "'a + 'b \<Rightarrow> 'b set" where
    46 "setr x = (case x of Inr z => {z} | _ => {})"
    47 
    48 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
    49 
    50 bnf sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
    51 proof -
    52   show "sum_map id id = id" by (rule sum_map.id)
    53 next
    54   fix f1 f2 g1 g2
    55   show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
    56     by (rule sum_map.comp[symmetric])
    57 next
    58   fix x f1 f2 g1 g2
    59   assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
    60          a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
    61   thus "sum_map f1 f2 x = sum_map g1 g2 x"
    62   proof (cases x)
    63     case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
    64   next
    65     case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
    66   qed
    67 next
    68   fix f1 f2
    69   show "setl o sum_map f1 f2 = image f1 o setl"
    70     by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
    71 next
    72   fix f1 f2
    73   show "setr o sum_map f1 f2 = image f2 o setr"
    74     by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
    75 next
    76   show "card_order natLeq" by (rule natLeq_card_order)
    77 next
    78   show "cinfinite natLeq" by (rule natLeq_cinfinite)
    79 next
    80   fix x
    81   show "|setl x| \<le>o natLeq"
    82     apply (rule ordLess_imp_ordLeq)
    83     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
    84     by (simp add: setl_def split: sum.split)
    85 next
    86   fix x
    87   show "|setr x| \<le>o natLeq"
    88     apply (rule ordLess_imp_ordLeq)
    89     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
    90     by (simp add: setr_def split: sum.split)
    91 next
    92   fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
    93   assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
    94   hence
    95     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"
    96     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"
    97     unfolding wpull_def by blast+
    98   show "wpull {x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2}
    99   {x. setl x \<subseteq> B11 \<and> setr x \<subseteq> B12} {x. setl x \<subseteq> B21 \<and> setr x \<subseteq> B22}
   100   (sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)"
   101     (is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2")
   102   proof (unfold wpull_def)
   103     { fix B1 B2
   104       assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2"
   105       have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2"
   106       proof (cases B1)
   107         case (Inl b1)
   108         { fix b2 assume "B2 = Inr b2"
   109           with Inl *(3) have False by simp
   110         } then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast)
   111         with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2"
   112         by (simp add: setl_def)+
   113         with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+
   114         with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2"
   115         by (simp add: sum_set_defs)+
   116         thus ?thesis by blast
   117       next
   118         case (Inr b1)
   119         { fix b2 assume "B2 = Inl b2"
   120           with Inr *(3) have False by simp
   121         } then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast)
   122         with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2"
   123         by (simp add: sum_set_defs)+
   124         with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+
   125         with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2"
   126         by (simp add: sum_set_defs)+
   127         thus ?thesis by blast
   128       qed
   129     }
   130     thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow>
   131       (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce
   132   qed
   133 next
   134   fix R S
   135   show "sum_rel R S =
   136         (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
   137         Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
   138   unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
   139   by (fastforce split: sum.splits)
   140 qed (auto simp: sum_set_defs)
   141 
   142 definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
   143 "fsts x = {fst x}"
   144 
   145 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
   146 "snds x = {snd x}"
   147 
   148 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
   149 
   150 bnf map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. natLeq" prod_rel
   151 proof (unfold prod_set_defs)
   152   show "map_pair id id = id" by (rule map_pair.id)
   153 next
   154   fix f1 f2 g1 g2
   155   show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
   156     by (rule map_pair.comp[symmetric])
   157 next
   158   fix x f1 f2 g1 g2
   159   assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
   160   thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
   161 next
   162   fix f1 f2
   163   show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
   164     by (rule ext, unfold o_apply) simp
   165 next
   166   fix f1 f2
   167   show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
   168     by (rule ext, unfold o_apply) simp
   169 next
   170   show "card_order natLeq" by (rule natLeq_card_order)
   171 next
   172   show "cinfinite natLeq" by (rule natLeq_cinfinite)
   173 next
   174   fix x
   175   show "|{fst x}| \<le>o natLeq"
   176     by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
   177 next
   178   fix x
   179   show "|{snd x}| \<le>o natLeq"
   180     by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
   181 next
   182   fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
   183   assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
   184   thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}
   185     {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22}
   186    (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)"
   187     unfolding wpull_def by simp fast
   188 next
   189   fix R S
   190   show "prod_rel R S =
   191         (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
   192         Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
   193   unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
   194   by auto
   195 qed
   196 
   197 (* Categorical version of pullback: *)
   198 lemma wpull_cat:
   199 assumes p: "wpull A B1 B2 f1 f2 p1 p2"
   200 and c: "f1 o q1 = f2 o q2"
   201 and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2"
   202 obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h"
   203 proof-
   204   have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d"
   205   proof safe
   206     fix d
   207     have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong)
   208     moreover
   209     have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto
   210     ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d"
   211       using p unfolding wpull_def by auto
   212   qed
   213   then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis
   214   thus ?thesis using that by fastforce
   215 qed
   216 
   217 lemma card_of_bounded_range:
   218   "|{f :: 'd \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|")
   219 proof -
   220   let ?f = "\<lambda>f. %x. if f x \<in> B then f x else undefined"
   221   have "inj_on ?f ?LHS" unfolding inj_on_def
   222   proof (unfold fun_eq_iff, safe)
   223     fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x
   224     assume "range f \<subseteq> B" "range g \<subseteq> B" and eq: "\<forall>x. ?f f x = ?f g x"
   225     hence "f x \<in> B" "g x \<in> B" by auto
   226     with eq have "Some (f x) = Some (g x)" by metis
   227     thus "f x = g x" by simp
   228   qed
   229   moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce
   230   ultimately show ?thesis using card_of_ordLeq by fast
   231 qed
   232 
   233 bnf "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
   234   "fun_rel op ="
   235 proof
   236   fix f show "id \<circ> f = id f" by simp
   237 next
   238   fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
   239   unfolding comp_def[abs_def] ..
   240 next
   241   fix x f g
   242   assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
   243   thus "f \<circ> x = g \<circ> x" by auto
   244 next
   245   fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
   246   unfolding image_def comp_def[abs_def] by auto
   247 next
   248   show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
   249   apply (rule card_order_csum)
   250   apply (rule natLeq_card_order)
   251   by (rule card_of_card_order_on)
   252 (*  *)
   253   show "cinfinite (natLeq +c ?U)"
   254     apply (rule cinfinite_csum)
   255     apply (rule disjI1)
   256     by (rule natLeq_cinfinite)
   257 next
   258   fix f :: "'d => 'a"
   259   have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
   260   also have "?U \<le>o natLeq +c ?U"  by (rule ordLeq_csum2) (rule card_of_Card_order)
   261   finally show "|range f| \<le>o natLeq +c ?U" .
   262 next
   263   fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2"
   264   show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2}
   265     (op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)"
   266   unfolding wpull_def
   267   proof safe
   268     fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2"
   269     and c: "f1 \<circ> g1 = f2 \<circ> g2"
   270     show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2"
   271     using wpull_cat[OF p c r] by simp metis
   272   qed
   273 next
   274   fix R
   275   show "fun_rel op = R =
   276         (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
   277          Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
   278   unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps  subset_iff image_iff
   279   by auto (force, metis pair_collapse)
   280 qed
   281 
   282 end