src/HOL/Basic_BNFs.thy
changeset 55058 4e700eb471d4
parent 54841 af71b753c459
child 55062 6d3fad6f01c9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -0,0 +1,204 @@
     1.4 +(*  Title:      HOL/BNF/Basic_BNFs.thy
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Author:     Andrei Popescu, TU Muenchen
     1.7 +    Author:     Jasmin Blanchette, TU Muenchen
     1.8 +    Copyright   2012
     1.9 +
    1.10 +Registration of basic types as bounded natural functors.
    1.11 +*)
    1.12 +
    1.13 +header {* Registration of Basic Types as Bounded Natural Functors *}
    1.14 +
    1.15 +theory Basic_BNFs
    1.16 +imports BNF_Def
    1.17 +   (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
    1.18 +  Lifting_Sum
    1.19 +  Lifting_Product
    1.20 +  Main
    1.21 +begin
    1.22 +
    1.23 +bnf ID: 'a
    1.24 +  map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.25 +  sets: "\<lambda>x. {x}"
    1.26 +  bd: natLeq
    1.27 +  rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    1.28 +apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
    1.29 +apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    1.30 +apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
    1.31 +done
    1.32 +
    1.33 +bnf DEADID: 'a
    1.34 +  map: "id :: 'a \<Rightarrow> 'a"
    1.35 +  bd: "natLeq +c |UNIV :: 'a set|"
    1.36 +  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.37 +by (auto simp add: Grp_def
    1.38 +  card_order_csum natLeq_card_order card_of_card_order_on
    1.39 +  cinfinite_csum natLeq_cinfinite)
    1.40 +
    1.41 +definition setl :: "'a + 'b \<Rightarrow> 'a set" where
    1.42 +"setl x = (case x of Inl z => {z} | _ => {})"
    1.43 +
    1.44 +definition setr :: "'a + 'b \<Rightarrow> 'b set" where
    1.45 +"setr x = (case x of Inr z => {z} | _ => {})"
    1.46 +
    1.47 +lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
    1.48 +
    1.49 +bnf "'a + 'b"
    1.50 +  map: sum_map
    1.51 +  sets: setl setr
    1.52 +  bd: natLeq
    1.53 +  wits: Inl Inr
    1.54 +  rel: sum_rel
    1.55 +proof -
    1.56 +  show "sum_map id id = id" by (rule sum_map.id)
    1.57 +next
    1.58 +  fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
    1.59 +  show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
    1.60 +    by (rule sum_map.comp[symmetric])
    1.61 +next
    1.62 +  fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
    1.63 +  assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
    1.64 +         a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
    1.65 +  thus "sum_map f1 f2 x = sum_map g1 g2 x"
    1.66 +  proof (cases x)
    1.67 +    case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
    1.68 +  next
    1.69 +    case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
    1.70 +  qed
    1.71 +next
    1.72 +  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    1.73 +  show "setl o sum_map f1 f2 = image f1 o setl"
    1.74 +    by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
    1.75 +next
    1.76 +  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    1.77 +  show "setr o sum_map f1 f2 = image f2 o setr"
    1.78 +    by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
    1.79 +next
    1.80 +  show "card_order natLeq" by (rule natLeq_card_order)
    1.81 +next
    1.82 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
    1.83 +next
    1.84 +  fix x :: "'o + 'p"
    1.85 +  show "|setl x| \<le>o natLeq"
    1.86 +    apply (rule ordLess_imp_ordLeq)
    1.87 +    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
    1.88 +    by (simp add: setl_def split: sum.split)
    1.89 +next
    1.90 +  fix x :: "'o + 'p"
    1.91 +  show "|setr x| \<le>o natLeq"
    1.92 +    apply (rule ordLess_imp_ordLeq)
    1.93 +    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
    1.94 +    by (simp add: setr_def split: sum.split)
    1.95 +next
    1.96 +  fix R1 R2 S1 S2
    1.97 +  show "sum_rel R1 R2 OO sum_rel S1 S2 \<le> sum_rel (R1 OO S1) (R2 OO S2)"
    1.98 +    by (auto simp: sum_rel_def split: sum.splits)
    1.99 +next
   1.100 +  fix R S
   1.101 +  show "sum_rel R S =
   1.102 +        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
   1.103 +        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
   1.104 +  unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
   1.105 +  by (fastforce split: sum.splits)
   1.106 +qed (auto simp: sum_set_defs)
   1.107 +
   1.108 +definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
   1.109 +"fsts x = {fst x}"
   1.110 +
   1.111 +definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
   1.112 +"snds x = {snd x}"
   1.113 +
   1.114 +lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
   1.115 +
   1.116 +bnf "'a \<times> 'b"
   1.117 +  map: map_pair
   1.118 +  sets: fsts snds
   1.119 +  bd: natLeq
   1.120 +  rel: prod_rel
   1.121 +proof (unfold prod_set_defs)
   1.122 +  show "map_pair id id = id" by (rule map_pair.id)
   1.123 +next
   1.124 +  fix f1 f2 g1 g2
   1.125 +  show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
   1.126 +    by (rule map_pair.comp[symmetric])
   1.127 +next
   1.128 +  fix x f1 f2 g1 g2
   1.129 +  assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
   1.130 +  thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
   1.131 +next
   1.132 +  fix f1 f2
   1.133 +  show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
   1.134 +    by (rule ext, unfold o_apply) simp
   1.135 +next
   1.136 +  fix f1 f2
   1.137 +  show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
   1.138 +    by (rule ext, unfold o_apply) simp
   1.139 +next
   1.140 +  show "card_order natLeq" by (rule natLeq_card_order)
   1.141 +next
   1.142 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   1.143 +next
   1.144 +  fix x
   1.145 +  show "|{fst x}| \<le>o natLeq"
   1.146 +    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
   1.147 +next
   1.148 +  fix x
   1.149 +  show "|{snd x}| \<le>o natLeq"
   1.150 +    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
   1.151 +next
   1.152 +  fix R1 R2 S1 S2
   1.153 +  show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
   1.154 +next
   1.155 +  fix R S
   1.156 +  show "prod_rel R S =
   1.157 +        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
   1.158 +        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
   1.159 +  unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
   1.160 +  by auto
   1.161 +qed
   1.162 +
   1.163 +bnf "'a \<Rightarrow> 'b"
   1.164 +  map: "op \<circ>"
   1.165 +  sets: range
   1.166 +  bd: "natLeq +c |UNIV :: 'a set|"
   1.167 +  rel: "fun_rel op ="
   1.168 +proof
   1.169 +  fix f show "id \<circ> f = id f" by simp
   1.170 +next
   1.171 +  fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
   1.172 +  unfolding comp_def[abs_def] ..
   1.173 +next
   1.174 +  fix x f g
   1.175 +  assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
   1.176 +  thus "f \<circ> x = g \<circ> x" by auto
   1.177 +next
   1.178 +  fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
   1.179 +  unfolding image_def comp_def[abs_def] by auto
   1.180 +next
   1.181 +  show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
   1.182 +  apply (rule card_order_csum)
   1.183 +  apply (rule natLeq_card_order)
   1.184 +  by (rule card_of_card_order_on)
   1.185 +(*  *)
   1.186 +  show "cinfinite (natLeq +c ?U)"
   1.187 +    apply (rule cinfinite_csum)
   1.188 +    apply (rule disjI1)
   1.189 +    by (rule natLeq_cinfinite)
   1.190 +next
   1.191 +  fix f :: "'d => 'a"
   1.192 +  have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
   1.193 +  also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
   1.194 +  finally show "|range f| \<le>o natLeq +c ?U" .
   1.195 +next
   1.196 +  fix R S
   1.197 +  show "fun_rel op = R OO fun_rel op = S \<le> fun_rel op = (R OO S)" by (auto simp: fun_rel_def)
   1.198 +next
   1.199 +  fix R
   1.200 +  show "fun_rel op = R =
   1.201 +        (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
   1.202 +         Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
   1.203 +  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps  subset_iff image_iff
   1.204 +  by auto (force, metis (no_types) pair_collapse)
   1.205 +qed
   1.206 +
   1.207 +end