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 7Registration of basic types as bounded natural functors. 8*) 9 10section \<open>Registration of Basic Types as Bounded Natural Functors\<close> 11 12theory Basic_BNFs 13imports BNF_Def 14begin 15 16inductive_set setl :: "'a + 'b \<Rightarrow> 'a set" for s :: "'a + 'b" where 17 "s = Inl x \<Longrightarrow> x \<in> setl s" 18inductive_set setr :: "'a + 'b \<Rightarrow> 'b set" for s :: "'a + 'b" where 19 "s = Inr x \<Longrightarrow> x \<in> setr s" 20 21lemma sum_set_defs[code]: 22 "setl = (\<lambda>x. case x of Inl z \<Rightarrow> {z} | _ \<Rightarrow> {})" 23 "setr = (\<lambda>x. case x of Inr z \<Rightarrow> {z} | _ \<Rightarrow> {})" 24 by (auto simp: fun_eq_iff intro: setl.intros setr.intros elim: setl.cases setr.cases split: sum.splits) 25 26lemma 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 33inductive 34 pred_sum :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool" for P1 P2 35where 36 "P1 a \<Longrightarrow> pred_sum P1 P2 (Inl a)" 37| "P2 b \<Longrightarrow> pred_sum P1 P2 (Inr b)" 38 39lemma 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 44bnf "'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 51proof - 52 show "map_sum id id = id" by (rule map_sum.id) 53next 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 \<circ> f1) (g2 \<circ> f2) = map_sum g1 g2 \<circ> map_sum f1 f2" 56 by (rule map_sum.comp[symmetric]) 57next 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 67next 68 fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" 69 show "setl \<circ> map_sum f1 f2 = image f1 \<circ> setl" 70 by (rule ext, unfold o_apply) (simp add: sum_set_defs(1) split: sum.split) 71next 72 fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" 73 show "setr \<circ> map_sum f1 f2 = image f2 \<circ> setr" 74 by (rule ext, unfold o_apply) (simp add: sum_set_defs(2) split: sum.split) 75next 76 show "card_order natLeq" by (rule natLeq_card_order) 77next 78 show "cinfinite natLeq" by (rule natLeq_cinfinite) 79next 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) 85next 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) 91next 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) 95next 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) 102qed (auto simp: sum_set_defs fun_eq_iff pred_sum.simps split: sum.splits) 103 104inductive_set fsts :: "'a \<times> 'b \<Rightarrow> 'a set" for p :: "'a \<times> 'b" where 105 "fst p \<in> fsts p" 106inductive_set snds :: "'a \<times> 'b \<Rightarrow> 'b set" for p :: "'a \<times> 'b" where 107 "snd p \<in> snds p" 108 109lemma 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 112inductive 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 114where 115 "\<lbrakk>R1 a b; R2 c d\<rbrakk> \<Longrightarrow> rel_prod R1 R2 (a, c) (b, d)" 116 117inductive 118 pred_prod :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" for P1 P2 119where 120 "\<lbrakk>P1 a; P2 b\<rbrakk> \<Longrightarrow> pred_prod P1 P2 (a, b)" 121 122lemma 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 126lemma 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 130lemma 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 134definition 135 pred_fun :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" 136where 137 "pred_fun A B = (\<lambda>f. \<forall>x. A x \<longrightarrow> B (f x))" 138 139lemma pred_funI: "(\<And>x. A x \<Longrightarrow> B (f x)) \<Longrightarrow> pred_fun A B f" 140 unfolding pred_fun_def by simp 141 142bnf "'a \<times> 'b" 143 map: map_prod 144 sets: fsts snds 145 bd: natLeq 146 rel: rel_prod 147 pred: pred_prod 148proof (unfold prod_set_defs) 149 show "map_prod id id = id" by (rule map_prod.id) 150next 151 fix f1 f2 g1 g2 152 show "map_prod (g1 \<circ> f1) (g2 \<circ> f2) = map_prod g1 g2 \<circ> map_prod f1 f2" 153 by (rule map_prod.comp[symmetric]) 154next 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 158next 159 fix f1 f2 160 show "(\<lambda>x. {fst x}) \<circ> map_prod f1 f2 = image f1 \<circ> (\<lambda>x. {fst x})" 161 by (rule ext, unfold o_apply) simp 162next 163 fix f1 f2 164 show "(\<lambda>x. {snd x}) \<circ> map_prod f1 f2 = image f2 \<circ> (\<lambda>x. {snd x})" 165 by (rule ext, unfold o_apply) simp 166next 167 show "card_order natLeq" by (rule natLeq_card_order) 168next 169 show "cinfinite natLeq" by (rule natLeq_cinfinite) 170next 171 fix x 172 show "|{fst x}| \<le>o natLeq" 173 by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric]) 174next 175 fix x 176 show "|{snd x}| \<le>o natLeq" 177 by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric]) 178next 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 181next 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 188qed auto 189 190bnf "'a \<Rightarrow> 'b" 191 map: "(\<circ>)" 192 sets: range 193 bd: "natLeq +c |UNIV :: 'a set|" 194 rel: "rel_fun (=)" 195 pred: "pred_fun (\<lambda>_. True)" 196proof 197 fix f show "id \<circ> f = id f" by simp 198next 199 fix f g show "(\<circ>) (g \<circ> f) = (\<circ>) g \<circ> (\<circ>) f" 200 unfolding comp_def[abs_def] .. 201next 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 205next 206 fix f show "range \<circ> (\<circ>) f = (`) f \<circ> range" 207 by (auto simp add: fun_eq_iff) 208next 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) 218next 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" . 223next 224 fix R S 225 show "rel_fun (=) R OO rel_fun (=) S \<le> rel_fun (=) (R OO S)" by (auto simp: rel_fun_def) 226next 227 fix R 228 show "rel_fun (=) 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]) 231qed (auto simp: pred_fun_def) 232 233end 234