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