src/HOL/Basic_BNFs.thy
author blanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55058 4e700eb471d4
parent 54841 src/HOL/BNF/Basic_BNFs.thy@af71b753c459
child 55062 6d3fad6f01c9
permissions -rw-r--r--
moved BNF files to 'HOL'
     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    (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
    15   Lifting_Sum
    16   Lifting_Product
    17   Main
    18 begin
    19 
    20 bnf ID: 'a
    21   map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    22   sets: "\<lambda>x. {x}"
    23   bd: natLeq
    24   rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    25 apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
    26 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    27 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
    28 done
    29 
    30 bnf DEADID: 'a
    31   map: "id :: 'a \<Rightarrow> 'a"
    32   bd: "natLeq +c |UNIV :: 'a set|"
    33   rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
    34 by (auto simp add: Grp_def
    35   card_order_csum natLeq_card_order card_of_card_order_on
    36   cinfinite_csum natLeq_cinfinite)
    37 
    38 definition setl :: "'a + 'b \<Rightarrow> 'a set" where
    39 "setl x = (case x of Inl z => {z} | _ => {})"
    40 
    41 definition setr :: "'a + 'b \<Rightarrow> 'b set" where
    42 "setr x = (case x of Inr z => {z} | _ => {})"
    43 
    44 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
    45 
    46 bnf "'a + 'b"
    47   map: sum_map
    48   sets: setl setr
    49   bd: natLeq
    50   wits: Inl Inr
    51   rel: sum_rel
    52 proof -
    53   show "sum_map id id = id" by (rule sum_map.id)
    54 next
    55   fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
    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 and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and 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 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    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 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    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 :: "'o + 'p"
    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 :: "'o + 'p"
    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 R1 R2 S1 S2
    94   show "sum_rel R1 R2 OO sum_rel S1 S2 \<le> sum_rel (R1 OO S1) (R2 OO S2)"
    95     by (auto simp: sum_rel_def split: sum.splits)
    96 next
    97   fix R S
    98   show "sum_rel R S =
    99         (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
   100         Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
   101   unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
   102   by (fastforce split: sum.splits)
   103 qed (auto simp: sum_set_defs)
   104 
   105 definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
   106 "fsts x = {fst x}"
   107 
   108 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
   109 "snds x = {snd x}"
   110 
   111 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
   112 
   113 bnf "'a \<times> 'b"
   114   map: map_pair
   115   sets: fsts snds
   116   bd: natLeq
   117   rel: prod_rel
   118 proof (unfold prod_set_defs)
   119   show "map_pair id id = id" by (rule map_pair.id)
   120 next
   121   fix f1 f2 g1 g2
   122   show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
   123     by (rule map_pair.comp[symmetric])
   124 next
   125   fix x f1 f2 g1 g2
   126   assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
   127   thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
   128 next
   129   fix f1 f2
   130   show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
   131     by (rule ext, unfold o_apply) simp
   132 next
   133   fix f1 f2
   134   show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
   135     by (rule ext, unfold o_apply) simp
   136 next
   137   show "card_order natLeq" by (rule natLeq_card_order)
   138 next
   139   show "cinfinite natLeq" by (rule natLeq_cinfinite)
   140 next
   141   fix x
   142   show "|{fst x}| \<le>o natLeq"
   143     by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
   144 next
   145   fix x
   146   show "|{snd x}| \<le>o natLeq"
   147     by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
   148 next
   149   fix R1 R2 S1 S2
   150   show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
   151 next
   152   fix R S
   153   show "prod_rel R S =
   154         (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
   155         Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
   156   unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
   157   by auto
   158 qed
   159 
   160 bnf "'a \<Rightarrow> 'b"
   161   map: "op \<circ>"
   162   sets: range
   163   bd: "natLeq +c |UNIV :: 'a set|"
   164   rel: "fun_rel op ="
   165 proof
   166   fix f show "id \<circ> f = id f" by simp
   167 next
   168   fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
   169   unfolding comp_def[abs_def] ..
   170 next
   171   fix x f g
   172   assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
   173   thus "f \<circ> x = g \<circ> x" by auto
   174 next
   175   fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
   176   unfolding image_def comp_def[abs_def] by auto
   177 next
   178   show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
   179   apply (rule card_order_csum)
   180   apply (rule natLeq_card_order)
   181   by (rule card_of_card_order_on)
   182 (*  *)
   183   show "cinfinite (natLeq +c ?U)"
   184     apply (rule cinfinite_csum)
   185     apply (rule disjI1)
   186     by (rule natLeq_cinfinite)
   187 next
   188   fix f :: "'d => 'a"
   189   have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
   190   also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
   191   finally show "|range f| \<le>o natLeq +c ?U" .
   192 next
   193   fix R S
   194   show "fun_rel op = R OO fun_rel op = S \<le> fun_rel op = (R OO S)" by (auto simp: fun_rel_def)
   195 next
   196   fix R
   197   show "fun_rel op = R =
   198         (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
   199          Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
   200   unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps  subset_iff image_iff
   201   by auto (force, metis (no_types) pair_collapse)
   202 qed
   203 
   204 end