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