src/HOL/Basic_BNFs.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 58446 e89f57d1e46c child 58916 229765cc3414 permissions -rw-r--r--
modernized header uniformly as section;
```     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 section {* Registration of Basic Types as Bounded Natural Functors *}
```
```    11
```
```    12 theory Basic_BNFs
```
```    13 imports BNF_Def
```
```    14 begin
```
```    15
```
```    16 definition setl :: "'a + 'b \<Rightarrow> 'a set" where
```
```    17 "setl x = (case x of Inl z => {z} | _ => {})"
```
```    18
```
```    19 definition setr :: "'a + 'b \<Rightarrow> 'b set" where
```
```    20 "setr x = (case x of Inr z => {z} | _ => {})"
```
```    21
```
```    22 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
```
```    23
```
```    24 lemma rel_sum_simps[simp]:
```
```    25   "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
```
```    26   "rel_sum R1 R2 (Inl a1) (Inr b2) = False"
```
```    27   "rel_sum R1 R2 (Inr a2) (Inl b1) = False"
```
```    28   "rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
```
```    29   unfolding rel_sum_def by simp_all
```
```    30
```
```    31 bnf "'a + 'b"
```
```    32   map: map_sum
```
```    33   sets: setl setr
```
```    34   bd: natLeq
```
```    35   wits: Inl Inr
```
```    36   rel: rel_sum
```
```    37 proof -
```
```    38   show "map_sum id id = id" by (rule map_sum.id)
```
```    39 next
```
```    40   fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
```
```    41   show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2"
```
```    42     by (rule map_sum.comp[symmetric])
```
```    43 next
```
```    44   fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
```
```    45   assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
```
```    46          a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
```
```    47   thus "map_sum f1 f2 x = map_sum g1 g2 x"
```
```    48   proof (cases x)
```
```    49     case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
```
```    50   next
```
```    51     case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
```
```    52   qed
```
```    53 next
```
```    54   fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
```
```    55   show "setl o map_sum f1 f2 = image f1 o setl"
```
```    56     by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
```
```    57 next
```
```    58   fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
```
```    59   show "setr o map_sum f1 f2 = image f2 o setr"
```
```    60     by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
```
```    61 next
```
```    62   show "card_order natLeq" by (rule natLeq_card_order)
```
```    63 next
```
```    64   show "cinfinite natLeq" by (rule natLeq_cinfinite)
```
```    65 next
```
```    66   fix x :: "'o + 'p"
```
```    67   show "|setl x| \<le>o natLeq"
```
```    68     apply (rule ordLess_imp_ordLeq)
```
```    69     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
```
```    70     by (simp add: setl_def split: sum.split)
```
```    71 next
```
```    72   fix x :: "'o + 'p"
```
```    73   show "|setr x| \<le>o natLeq"
```
```    74     apply (rule ordLess_imp_ordLeq)
```
```    75     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
```
```    76     by (simp add: setr_def split: sum.split)
```
```    77 next
```
```    78   fix R1 R2 S1 S2
```
```    79   show "rel_sum R1 R2 OO rel_sum S1 S2 \<le> rel_sum (R1 OO S1) (R2 OO S2)"
```
```    80     by (auto simp: rel_sum_def split: sum.splits)
```
```    81 next
```
```    82   fix R S
```
```    83   show "rel_sum R S =
```
```    84         (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
```
```    85         Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
```
```    86   unfolding setl_def setr_def rel_sum_def Grp_def relcompp.simps conversep.simps fun_eq_iff
```
```    87   by (fastforce split: sum.splits)
```
```    88 qed (auto simp: sum_set_defs)
```
```    89
```
```    90 definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
```
```    91 "fsts x = {fst x}"
```
```    92
```
```    93 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
```
```    94 "snds x = {snd x}"
```
```    95
```
```    96 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
```
```    97
```
```    98 definition
```
```    99   rel_prod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
```
```   100 where
```
```   101   "rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
```
```   102
```
```   103 lemma rel_prod_apply [simp]:
```
```   104   "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
```
```   105   by (simp add: rel_prod_def)
```
```   106
```
```   107 bnf "'a \<times> 'b"
```
```   108   map: map_prod
```
```   109   sets: fsts snds
```
```   110   bd: natLeq
```
```   111   rel: rel_prod
```
```   112 proof (unfold prod_set_defs)
```
```   113   show "map_prod id id = id" by (rule map_prod.id)
```
```   114 next
```
```   115   fix f1 f2 g1 g2
```
```   116   show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2"
```
```   117     by (rule map_prod.comp[symmetric])
```
```   118 next
```
```   119   fix x f1 f2 g1 g2
```
```   120   assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
```
```   121   thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp
```
```   122 next
```
```   123   fix f1 f2
```
```   124   show "(\<lambda>x. {fst x}) o map_prod f1 f2 = image f1 o (\<lambda>x. {fst x})"
```
```   125     by (rule ext, unfold o_apply) simp
```
```   126 next
```
```   127   fix f1 f2
```
```   128   show "(\<lambda>x. {snd x}) o map_prod f1 f2 = image f2 o (\<lambda>x. {snd x})"
```
```   129     by (rule ext, unfold o_apply) simp
```
```   130 next
```
```   131   show "card_order natLeq" by (rule natLeq_card_order)
```
```   132 next
```
```   133   show "cinfinite natLeq" by (rule natLeq_cinfinite)
```
```   134 next
```
```   135   fix x
```
```   136   show "|{fst x}| \<le>o natLeq"
```
```   137     by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
```
```   138 next
```
```   139   fix x
```
```   140   show "|{snd x}| \<le>o natLeq"
```
```   141     by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
```
```   142 next
```
```   143   fix R1 R2 S1 S2
```
```   144   show "rel_prod R1 R2 OO rel_prod S1 S2 \<le> rel_prod (R1 OO S1) (R2 OO S2)" by auto
```
```   145 next
```
```   146   fix R S
```
```   147   show "rel_prod R S =
```
```   148         (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
```
```   149         Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
```
```   150   unfolding prod_set_defs rel_prod_def Grp_def relcompp.simps conversep.simps fun_eq_iff
```
```   151   by auto
```
```   152 qed
```
```   153
```
```   154 bnf "'a \<Rightarrow> 'b"
```
```   155   map: "op \<circ>"
```
```   156   sets: range
```
```   157   bd: "natLeq +c |UNIV :: 'a set|"
```
```   158   rel: "rel_fun op ="
```
```   159 proof
```
```   160   fix f show "id \<circ> f = id f" by simp
```
```   161 next
```
```   162   fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
```
```   163   unfolding comp_def[abs_def] ..
```
```   164 next
```
```   165   fix x f g
```
```   166   assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
```
```   167   thus "f \<circ> x = g \<circ> x" by auto
```
```   168 next
```
```   169   fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
```
```   170     by (auto simp add: fun_eq_iff)
```
```   171 next
```
```   172   show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
```
```   173   apply (rule card_order_csum)
```
```   174   apply (rule natLeq_card_order)
```
```   175   by (rule card_of_card_order_on)
```
```   176 (*  *)
```
```   177   show "cinfinite (natLeq +c ?U)"
```
```   178     apply (rule cinfinite_csum)
```
```   179     apply (rule disjI1)
```
```   180     by (rule natLeq_cinfinite)
```
```   181 next
```
```   182   fix f :: "'d => 'a"
```
```   183   have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
```
```   184   also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
```
```   185   finally show "|range f| \<le>o natLeq +c ?U" .
```
```   186 next
```
```   187   fix R S
```
```   188   show "rel_fun op = R OO rel_fun op = S \<le> rel_fun op = (R OO S)" by (auto simp: rel_fun_def)
```
```   189 next
```
```   190   fix R
```
```   191   show "rel_fun op = R =
```
```   192         (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
```
```   193          Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
```
```   194   unfolding rel_fun_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
```
```   195     comp_apply mem_Collect_eq split_beta bex_UNIV
```
```   196   proof (safe, unfold fun_eq_iff[symmetric])
```
```   197     fix x xa a b c xb y aa ba
```
```   198     assume *: "x = a" "xa = c" "a = ba" "b = aa" "c = (\<lambda>x. snd (b x))" "ba = (\<lambda>x. fst (aa x))" and
```
```   199        **: "\<forall>t. (\<exists>x. t = aa x) \<longrightarrow> R (fst t) (snd t)"
```
```   200     show "R (x y) (xa y)" unfolding * by (rule mp[OF spec[OF **]]) blast
```
```   201   qed force
```
```   202 qed
```
```   203
```
```   204 end
```