src/HOL/Basic_BNFs.thy
 author paulson Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) changeset 62379 340738057c8c parent 62335 e85c42f4f30a child 67091 1393c2340eec permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
```     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 \<open>Registration of Basic Types as Bounded Natural Functors\<close>
```
```    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 inductive
```
```    34    pred_sum :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool" for P1 P2
```
```    35 where
```
```    36   "P1 a \<Longrightarrow> pred_sum P1 P2 (Inl a)"
```
```    37 | "P2 b \<Longrightarrow> pred_sum P1 P2 (Inr b)"
```
```    38
```
```    39 lemma pred_sum_inject[code, simp]:
```
```    40   "pred_sum P1 P2 (Inl a) \<longleftrightarrow> P1 a"
```
```    41   "pred_sum P1 P2 (Inr b) \<longleftrightarrow> P2 b"
```
```    42   by (simp add: pred_sum.simps)+
```
```    43
```
```    44 bnf "'a + 'b"
```
```    45   map: map_sum
```
```    46   sets: setl setr
```
```    47   bd: natLeq
```
```    48   wits: Inl Inr
```
```    49   rel: rel_sum
```
```    50   pred: pred_sum
```
```    51 proof -
```
```    52   show "map_sum id id = id" by (rule map_sum.id)
```
```    53 next
```
```    54   fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
```
```    55   show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2"
```
```    56     by (rule map_sum.comp[symmetric])
```
```    57 next
```
```    58   fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
```
```    59   assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
```
```    60          a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
```
```    61   thus "map_sum f1 f2 x = map_sum g1 g2 x"
```
```    62   proof (cases x)
```
```    63     case Inl thus ?thesis using a1 by (clarsimp simp: sum_set_defs(1))
```
```    64   next
```
```    65     case Inr thus ?thesis using a2 by (clarsimp simp: sum_set_defs(2))
```
```    66   qed
```
```    67 next
```
```    68   fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
```
```    69   show "setl o map_sum f1 f2 = image f1 o setl"
```
```    70     by (rule ext, unfold o_apply) (simp add: sum_set_defs(1) split: sum.split)
```
```    71 next
```
```    72   fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
```
```    73   show "setr o map_sum f1 f2 = image f2 o setr"
```
```    74     by (rule ext, unfold o_apply) (simp add: sum_set_defs(2) split: sum.split)
```
```    75 next
```
```    76   show "card_order natLeq" by (rule natLeq_card_order)
```
```    77 next
```
```    78   show "cinfinite natLeq" by (rule natLeq_cinfinite)
```
```    79 next
```
```    80   fix x :: "'o + 'p"
```
```    81   show "|setl x| \<le>o natLeq"
```
```    82     apply (rule ordLess_imp_ordLeq)
```
```    83     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
```
```    84     by (simp add: sum_set_defs(1) split: sum.split)
```
```    85 next
```
```    86   fix x :: "'o + 'p"
```
```    87   show "|setr x| \<le>o natLeq"
```
```    88     apply (rule ordLess_imp_ordLeq)
```
```    89     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
```
```    90     by (simp add: sum_set_defs(2) split: sum.split)
```
```    91 next
```
```    92   fix R1 R2 S1 S2
```
```    93   show "rel_sum R1 R2 OO rel_sum S1 S2 \<le> rel_sum (R1 OO S1) (R2 OO S2)"
```
```    94     by (force elim: rel_sum.cases)
```
```    95 next
```
```    96   fix R S
```
```    97   show "rel_sum R S = (\<lambda>x y.
```
```    98     \<exists>z. (setl z \<subseteq> {(x, y). R x y} \<and> setr z \<subseteq> {(x, y). S x y}) \<and>
```
```    99     map_sum fst fst z = x \<and> map_sum snd snd z = y)"
```
```   100   unfolding sum_set_defs relcompp.simps conversep.simps fun_eq_iff
```
```   101   by (fastforce elim: rel_sum.cases split: sum.splits)
```
```   102 qed (auto simp: sum_set_defs fun_eq_iff pred_sum.simps split: sum.splits)
```
```   103
```
```   104 inductive_set fsts :: "'a \<times> 'b \<Rightarrow> 'a set" for p :: "'a \<times> 'b" where
```
```   105   "fst p \<in> fsts p"
```
```   106 inductive_set snds :: "'a \<times> 'b \<Rightarrow> 'b set" for p :: "'a \<times> 'b" where
```
```   107   "snd p \<in> snds p"
```
```   108
```
```   109 lemma prod_set_defs[code]: "fsts = (\<lambda>p. {fst p})" "snds = (\<lambda>p. {snd p})"
```
```   110   by (auto intro: fsts.intros snds.intros elim: fsts.cases snds.cases)
```
```   111
```
```   112 inductive
```
```   113   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
```
```   114 where
```
```   115   "\<lbrakk>R1 a b; R2 c d\<rbrakk> \<Longrightarrow> rel_prod R1 R2 (a, c) (b, d)"
```
```   116
```
```   117 inductive
```
```   118   pred_prod :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" for P1 P2
```
```   119 where
```
```   120   "\<lbrakk>P1 a; P2 b\<rbrakk> \<Longrightarrow> pred_prod P1 P2 (a, b)"
```
```   121
```
```   122 lemma rel_prod_inject [code, simp]:
```
```   123   "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
```
```   124   by (auto intro: rel_prod.intros elim: rel_prod.cases)
```
```   125
```
```   126 lemma pred_prod_inject [code, simp]:
```
```   127   "pred_prod P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
```
```   128   by (auto intro: pred_prod.intros elim: pred_prod.cases)
```
```   129
```
```   130 lemma rel_prod_conv:
```
```   131   "rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
```
```   132   by (rule ext, rule ext) auto
```
```   133
```
```   134 definition
```
```   135   pred_fun :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
```
```   136 where
```
```   137   "pred_fun A B = (\<lambda>f. \<forall>x. A x \<longrightarrow> B (f x))"
```
```   138
```
```   139 lemma pred_funI: "(\<And>x. A x \<Longrightarrow> B (f x)) \<Longrightarrow> pred_fun A B f"
```
```   140   unfolding pred_fun_def by simp
```
```   141
```
```   142 bnf "'a \<times> 'b"
```
```   143   map: map_prod
```
```   144   sets: fsts snds
```
```   145   bd: natLeq
```
```   146   rel: rel_prod
```
```   147   pred: pred_prod
```
```   148 proof (unfold prod_set_defs)
```
```   149   show "map_prod id id = id" by (rule map_prod.id)
```
```   150 next
```
```   151   fix f1 f2 g1 g2
```
```   152   show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2"
```
```   153     by (rule map_prod.comp[symmetric])
```
```   154 next
```
```   155   fix x f1 f2 g1 g2
```
```   156   assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
```
```   157   thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp
```
```   158 next
```
```   159   fix f1 f2
```
```   160   show "(\<lambda>x. {fst x}) o map_prod f1 f2 = image f1 o (\<lambda>x. {fst x})"
```
```   161     by (rule ext, unfold o_apply) simp
```
```   162 next
```
```   163   fix f1 f2
```
```   164   show "(\<lambda>x. {snd x}) o map_prod f1 f2 = image f2 o (\<lambda>x. {snd x})"
```
```   165     by (rule ext, unfold o_apply) simp
```
```   166 next
```
```   167   show "card_order natLeq" by (rule natLeq_card_order)
```
```   168 next
```
```   169   show "cinfinite natLeq" by (rule natLeq_cinfinite)
```
```   170 next
```
```   171   fix x
```
```   172   show "|{fst x}| \<le>o natLeq"
```
```   173     by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
```
```   174 next
```
```   175   fix x
```
```   176   show "|{snd x}| \<le>o natLeq"
```
```   177     by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
```
```   178 next
```
```   179   fix R1 R2 S1 S2
```
```   180   show "rel_prod R1 R2 OO rel_prod S1 S2 \<le> rel_prod (R1 OO S1) (R2 OO S2)" by auto
```
```   181 next
```
```   182   fix R S
```
```   183   show "rel_prod R S = (\<lambda>x y.
```
```   184     \<exists>z. ({fst z} \<subseteq> {(x, y). R x y} \<and> {snd z} \<subseteq> {(x, y). S x y}) \<and>
```
```   185       map_prod fst fst z = x \<and> map_prod snd snd z = y)"
```
```   186   unfolding prod_set_defs rel_prod_inject relcompp.simps conversep.simps fun_eq_iff
```
```   187   by auto
```
```   188 qed auto
```
```   189
```
```   190 bnf "'a \<Rightarrow> 'b"
```
```   191   map: "op \<circ>"
```
```   192   sets: range
```
```   193   bd: "natLeq +c |UNIV :: 'a set|"
```
```   194   rel: "rel_fun op ="
```
```   195   pred: "pred_fun (\<lambda>_. True)"
```
```   196 proof
```
```   197   fix f show "id \<circ> f = id f" by simp
```
```   198 next
```
```   199   fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
```
```   200   unfolding comp_def[abs_def] ..
```
```   201 next
```
```   202   fix x f g
```
```   203   assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
```
```   204   thus "f \<circ> x = g \<circ> x" by auto
```
```   205 next
```
```   206   fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
```
```   207     by (auto simp add: fun_eq_iff)
```
```   208 next
```
```   209   show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
```
```   210   apply (rule card_order_csum)
```
```   211   apply (rule natLeq_card_order)
```
```   212   by (rule card_of_card_order_on)
```
```   213 (*  *)
```
```   214   show "cinfinite (natLeq +c ?U)"
```
```   215     apply (rule cinfinite_csum)
```
```   216     apply (rule disjI1)
```
```   217     by (rule natLeq_cinfinite)
```
```   218 next
```
```   219   fix f :: "'d => 'a"
```
```   220   have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
```
```   221   also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
```
```   222   finally show "|range f| \<le>o natLeq +c ?U" .
```
```   223 next
```
```   224   fix R S
```
```   225   show "rel_fun op = R OO rel_fun op = S \<le> rel_fun op = (R OO S)" by (auto simp: rel_fun_def)
```
```   226 next
```
```   227   fix R
```
```   228   show "rel_fun op = R = (\<lambda>x y.
```
```   229     \<exists>z. range z \<subseteq> {(x, y). R x y} \<and> fst \<circ> z = x \<and> snd \<circ> z = y)"
```
```   230   unfolding rel_fun_def subset_iff by (force simp: fun_eq_iff[symmetric])
```
```   231 qed (auto simp: pred_fun_def)
```
```   232
```
```   233 end
```