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