src/HOL/Basic_BNFs.thy
author blanchet
Thu Mar 06 13:36:15 2014 +0100 (2014-03-06)
changeset 55931 62156e694f3d
parent 55811 aa1acc25126b
child 55932 68c5104d2204
permissions -rw-r--r--
renamed 'map_sum' to 'sum_map'
     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
     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 bnf ID: 'a
    17   map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    18   sets: "\<lambda>x. {x}"
    19   bd: natLeq
    20   rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    21 apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
    22 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    23 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
    24 done
    25 
    26 bnf DEADID: 'a
    27   map: "id :: 'a \<Rightarrow> 'a"
    28   bd: natLeq
    29   rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
    30 by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
    31 
    32 definition setl :: "'a + 'b \<Rightarrow> 'a set" where
    33 "setl x = (case x of Inl z => {z} | _ => {})"
    34 
    35 definition setr :: "'a + 'b \<Rightarrow> 'b set" where
    36 "setr x = (case x of Inr z => {z} | _ => {})"
    37 
    38 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
    39 
    40 definition
    41    sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
    42 where
    43    "sum_rel R1 R2 x y =
    44      (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    45      | (Inr x, Inr y) \<Rightarrow> R2 x y
    46      | _ \<Rightarrow> False)"
    47 
    48 lemma sum_rel_simps[simp]:
    49   "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    50   "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
    51   "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    52   "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    53   unfolding sum_rel_def by simp_all
    54 
    55 bnf "'a + 'b"
    56   map: map_sum
    57   sets: setl setr
    58   bd: natLeq
    59   wits: Inl Inr
    60   rel: sum_rel
    61 proof -
    62   show "map_sum id id = id" by (rule map_sum.id)
    63 next
    64   fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
    65   show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2"
    66     by (rule map_sum.comp[symmetric])
    67 next
    68   fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
    69   assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
    70          a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
    71   thus "map_sum f1 f2 x = map_sum g1 g2 x"
    72   proof (cases x)
    73     case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
    74   next
    75     case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
    76   qed
    77 next
    78   fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    79   show "setl o map_sum f1 f2 = image f1 o setl"
    80     by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
    81 next
    82   fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    83   show "setr o map_sum f1 f2 = image f2 o setr"
    84     by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
    85 next
    86   show "card_order natLeq" by (rule natLeq_card_order)
    87 next
    88   show "cinfinite natLeq" by (rule natLeq_cinfinite)
    89 next
    90   fix x :: "'o + 'p"
    91   show "|setl x| \<le>o natLeq"
    92     apply (rule ordLess_imp_ordLeq)
    93     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
    94     by (simp add: setl_def split: sum.split)
    95 next
    96   fix x :: "'o + 'p"
    97   show "|setr x| \<le>o natLeq"
    98     apply (rule ordLess_imp_ordLeq)
    99     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
   100     by (simp add: setr_def split: sum.split)
   101 next
   102   fix R1 R2 S1 S2
   103   show "sum_rel R1 R2 OO sum_rel S1 S2 \<le> sum_rel (R1 OO S1) (R2 OO S2)"
   104     by (auto simp: sum_rel_def split: sum.splits)
   105 next
   106   fix R S
   107   show "sum_rel R S =
   108         (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
   109         Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
   110   unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
   111   by (fastforce split: sum.splits)
   112 qed (auto simp: sum_set_defs)
   113 
   114 definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
   115 "fsts x = {fst x}"
   116 
   117 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
   118 "snds x = {snd x}"
   119 
   120 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
   121 
   122 definition
   123   prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
   124 where
   125   "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
   126 
   127 lemma prod_rel_apply [simp]:
   128   "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
   129   by (simp add: prod_rel_def)
   130 
   131 bnf "'a \<times> 'b"
   132   map: map_pair
   133   sets: fsts snds
   134   bd: natLeq
   135   rel: prod_rel
   136 proof (unfold prod_set_defs)
   137   show "map_pair id id = id" by (rule map_pair.id)
   138 next
   139   fix f1 f2 g1 g2
   140   show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
   141     by (rule map_pair.comp[symmetric])
   142 next
   143   fix x f1 f2 g1 g2
   144   assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
   145   thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
   146 next
   147   fix f1 f2
   148   show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
   149     by (rule ext, unfold o_apply) simp
   150 next
   151   fix f1 f2
   152   show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
   153     by (rule ext, unfold o_apply) simp
   154 next
   155   show "card_order natLeq" by (rule natLeq_card_order)
   156 next
   157   show "cinfinite natLeq" by (rule natLeq_cinfinite)
   158 next
   159   fix x
   160   show "|{fst x}| \<le>o natLeq"
   161     by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
   162 next
   163   fix x
   164   show "|{snd x}| \<le>o natLeq"
   165     by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
   166 next
   167   fix R1 R2 S1 S2
   168   show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
   169 next
   170   fix R S
   171   show "prod_rel R S =
   172         (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
   173         Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
   174   unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
   175   by auto
   176 qed
   177 
   178 bnf "'a \<Rightarrow> 'b"
   179   map: "op \<circ>"
   180   sets: range
   181   bd: "natLeq +c |UNIV :: 'a set|"
   182   rel: "fun_rel op ="
   183 proof
   184   fix f show "id \<circ> f = id f" by simp
   185 next
   186   fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
   187   unfolding comp_def[abs_def] ..
   188 next
   189   fix x f g
   190   assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
   191   thus "f \<circ> x = g \<circ> x" by auto
   192 next
   193   fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
   194   unfolding image_def comp_def[abs_def] by auto
   195 next
   196   show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
   197   apply (rule card_order_csum)
   198   apply (rule natLeq_card_order)
   199   by (rule card_of_card_order_on)
   200 (*  *)
   201   show "cinfinite (natLeq +c ?U)"
   202     apply (rule cinfinite_csum)
   203     apply (rule disjI1)
   204     by (rule natLeq_cinfinite)
   205 next
   206   fix f :: "'d => 'a"
   207   have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
   208   also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
   209   finally show "|range f| \<le>o natLeq +c ?U" .
   210 next
   211   fix R S
   212   show "fun_rel op = R OO fun_rel op = S \<le> fun_rel op = (R OO S)" by (auto simp: fun_rel_def)
   213 next
   214   fix R
   215   show "fun_rel op = R =
   216         (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
   217          Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
   218   unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
   219     comp_apply mem_Collect_eq split_beta bex_UNIV
   220   proof (safe, unfold fun_eq_iff[symmetric])
   221     fix x xa a b c xb y aa ba
   222     assume *: "x = a" "xa = c" "a = ba" "b = aa" "c = (\<lambda>x. snd (b x))" "ba = (\<lambda>x. fst (aa x))" and
   223        **: "\<forall>t. (\<exists>x. t = aa x) \<longrightarrow> R (fst t) (snd t)"
   224     show "R (x y) (xa y)" unfolding * by (rule mp[OF spec[OF **]]) blast
   225   qed force
   226 qed
   227 
   228 end