src/HOL/Basic_BNFs.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 62335 e85c42f4f30a child 67091 1393c2340eec permissions -rw-r--r--
tuned proofs;
 blanchet@55075 1 (* Title: HOL/Basic_BNFs.thy blanchet@48975 2 Author: Dmitriy Traytel, TU Muenchen blanchet@48975 3 Author: Andrei Popescu, TU Muenchen blanchet@48975 4 Author: Jasmin Blanchette, TU Muenchen blanchet@48975 5 Copyright 2012 blanchet@48975 6 blanchet@49309 7 Registration of basic types as bounded natural functors. blanchet@48975 8 *) blanchet@48975 9 wenzelm@60758 10 section \Registration of Basic Types as Bounded Natural Functors\ blanchet@48975 11 blanchet@48975 12 theory Basic_BNFs blanchet@49310 13 imports BNF_Def blanchet@48975 14 begin blanchet@48975 15 traytel@58916 16 inductive_set setl :: "'a + 'b \ 'a set" for s :: "'a + 'b" where traytel@58916 17 "s = Inl x \ x \ setl s" traytel@58916 18 inductive_set setr :: "'a + 'b \ 'b set" for s :: "'a + 'b" where traytel@58916 19 "s = Inr x \ x \ setr s" blanchet@48975 20 traytel@58916 21 lemma sum_set_defs[code]: traytel@58916 22 "setl = (\x. case x of Inl z => {z} | _ => {})" traytel@58916 23 "setr = (\x. case x of Inr z => {z} | _ => {})" traytel@58916 24 by (auto simp: fun_eq_iff intro: setl.intros setr.intros elim: setl.cases setr.cases split: sum.splits) blanchet@48975 25 traytel@58916 26 lemma rel_sum_simps[code, simp]: blanchet@55943 27 "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" blanchet@55943 28 "rel_sum R1 R2 (Inl a1) (Inr b2) = False" blanchet@55943 29 "rel_sum R1 R2 (Inr a2) (Inl b1) = False" blanchet@55943 30 "rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" traytel@58916 31 by (auto intro: rel_sum.intros elim: rel_sum.cases) blanchet@55083 32 traytel@62324 33 inductive traytel@62324 34 pred_sum :: "('a \ bool) \ ('b \ bool) \ 'a + 'b \ bool" for P1 P2 traytel@62324 35 where traytel@62324 36 "P1 a \ pred_sum P1 P2 (Inl a)" traytel@62324 37 | "P2 b \ pred_sum P1 P2 (Inr b)" traytel@62324 38 blanchet@62335 39 lemma pred_sum_inject[code, simp]: blanchet@62335 40 "pred_sum P1 P2 (Inl a) \ P1 a" blanchet@62335 41 "pred_sum P1 P2 (Inr b) \ P2 b" blanchet@62335 42 by (simp add: pred_sum.simps)+ blanchet@62335 43 traytel@54421 44 bnf "'a + 'b" blanchet@55931 45 map: map_sum traytel@54421 46 sets: setl setr traytel@54421 47 bd: natLeq traytel@54421 48 wits: Inl Inr blanchet@55943 49 rel: rel_sum traytel@62324 50 pred: pred_sum blanchet@48975 51 proof - blanchet@55931 52 show "map_sum id id = id" by (rule map_sum.id) blanchet@48975 53 next blanchet@54486 54 fix f1 :: "'o \ 's" and f2 :: "'p \ 't" and g1 :: "'s \ 'q" and g2 :: "'t \ 'r" blanchet@55931 55 show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2" blanchet@55931 56 by (rule map_sum.comp[symmetric]) blanchet@48975 57 next blanchet@54486 58 fix x and f1 :: "'o \ 'q" and f2 :: "'p \ 'r" and g1 g2 blanchet@49451 59 assume a1: "\z. z \ setl x \ f1 z = g1 z" and blanchet@49451 60 a2: "\z. z \ setr x \ f2 z = g2 z" blanchet@55931 61 thus "map_sum f1 f2 x = map_sum g1 g2 x" blanchet@48975 62 proof (cases x) traytel@58916 63 case Inl thus ?thesis using a1 by (clarsimp simp: sum_set_defs(1)) blanchet@48975 64 next traytel@58916 65 case Inr thus ?thesis using a2 by (clarsimp simp: sum_set_defs(2)) blanchet@48975 66 qed blanchet@48975 67 next blanchet@54486 68 fix f1 :: "'o \ 'q" and f2 :: "'p \ 'r" blanchet@55931 69 show "setl o map_sum f1 f2 = image f1 o setl" traytel@58916 70 by (rule ext, unfold o_apply) (simp add: sum_set_defs(1) split: sum.split) blanchet@48975 71 next blanchet@54486 72 fix f1 :: "'o \ 'q" and f2 :: "'p \ 'r" blanchet@55931 73 show "setr o map_sum f1 f2 = image f2 o setr" traytel@58916 74 by (rule ext, unfold o_apply) (simp add: sum_set_defs(2) split: sum.split) blanchet@48975 75 next blanchet@48975 76 show "card_order natLeq" by (rule natLeq_card_order) blanchet@48975 77 next blanchet@48975 78 show "cinfinite natLeq" by (rule natLeq_cinfinite) blanchet@48975 79 next blanchet@54486 80 fix x :: "'o + 'p" blanchet@49451 81 show "|setl x| \o natLeq" blanchet@48975 82 apply (rule ordLess_imp_ordLeq) blanchet@48975 83 apply (rule finite_iff_ordLess_natLeq[THEN iffD1]) traytel@58916 84 by (simp add: sum_set_defs(1) split: sum.split) blanchet@48975 85 next blanchet@54486 86 fix x :: "'o + 'p" blanchet@49451 87 show "|setr x| \o natLeq" blanchet@48975 88 apply (rule ordLess_imp_ordLeq) blanchet@48975 89 apply (rule finite_iff_ordLess_natLeq[THEN iffD1]) traytel@58916 90 by (simp add: sum_set_defs(2) split: sum.split) blanchet@48975 91 next traytel@54841 92 fix R1 R2 S1 S2 blanchet@55943 93 show "rel_sum R1 R2 OO rel_sum S1 S2 \ rel_sum (R1 OO S1) (R2 OO S2)" traytel@58916 94 by (force elim: rel_sum.cases) blanchet@49453 95 next blanchet@49453 96 fix R S traytel@62324 97 show "rel_sum R S = (\x y. traytel@62324 98 \z. (setl z \ {(x, y). R x y} \ setr z \ {(x, y). S x y}) \ traytel@62324 99 map_sum fst fst z = x \ map_sum snd snd z = y)" traytel@62324 100 unfolding sum_set_defs relcompp.simps conversep.simps fun_eq_iff traytel@58916 101 by (fastforce elim: rel_sum.cases split: sum.splits) traytel@62324 102 qed (auto simp: sum_set_defs fun_eq_iff pred_sum.simps split: sum.splits) blanchet@48975 103 traytel@58916 104 inductive_set fsts :: "'a \ 'b \ 'a set" for p :: "'a \ 'b" where traytel@58916 105 "fst p \ fsts p" traytel@58916 106 inductive_set snds :: "'a \ 'b \ 'b set" for p :: "'a \ 'b" where traytel@58916 107 "snd p \ snds p" blanchet@48975 108 traytel@58916 109 lemma prod_set_defs[code]: "fsts = (\p. {fst p})" "snds = (\p. {snd p})" traytel@58916 110 by (auto intro: fsts.intros snds.intros elim: fsts.cases snds.cases) blanchet@48975 111 traytel@58916 112 inductive traytel@58916 113 rel_prod :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a \ 'c \ 'b \ 'd \ bool" for R1 R2 blanchet@55083 114 where traytel@58916 115 "\R1 a b; R2 c d\ \ rel_prod R1 R2 (a, c) (b, d)" traytel@58916 116 traytel@62324 117 inductive traytel@62324 118 pred_prod :: "('a \ bool) \ ('b \ bool) \ 'a \ 'b \ bool" for P1 P2 traytel@62324 119 where traytel@62324 120 "\P1 a; P2 b\ \ pred_prod P1 P2 (a, b)" traytel@62324 121 blanchet@62335 122 lemma rel_prod_inject [code, simp]: traytel@58916 123 "rel_prod R1 R2 (a, b) (c, d) \ R1 a c \ R2 b d" traytel@58916 124 by (auto intro: rel_prod.intros elim: rel_prod.cases) traytel@58916 125 blanchet@62335 126 lemma pred_prod_inject [code, simp]: traytel@62324 127 "pred_prod P1 P2 (a, b) \ P1 a \ P2 b" traytel@62324 128 by (auto intro: pred_prod.intros elim: pred_prod.cases) traytel@62324 129 traytel@58916 130 lemma rel_prod_conv: blanchet@55944 131 "rel_prod R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)" traytel@58916 132 by (rule ext, rule ext) auto blanchet@55083 133 traytel@62324 134 definition traytel@62324 135 pred_fun :: "('a \ bool) \ ('b \ bool) \ ('a \ 'b) \ bool" traytel@62324 136 where traytel@62324 137 "pred_fun A B = (\f. \x. A x \ B (f x))" traytel@62324 138 traytel@62324 139 lemma pred_funI: "(\x. A x \ B (f x)) \ pred_fun A B f" traytel@62324 140 unfolding pred_fun_def by simp traytel@62324 141 traytel@54421 142 bnf "'a \ 'b" blanchet@55932 143 map: map_prod traytel@54421 144 sets: fsts snds traytel@54421 145 bd: natLeq blanchet@55944 146 rel: rel_prod traytel@62324 147 pred: pred_prod blanchet@48975 148 proof (unfold prod_set_defs) blanchet@55932 149 show "map_prod id id = id" by (rule map_prod.id) blanchet@48975 150 next blanchet@48975 151 fix f1 f2 g1 g2 blanchet@55932 152 show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2" blanchet@55932 153 by (rule map_prod.comp[symmetric]) blanchet@48975 154 next blanchet@48975 155 fix x f1 f2 g1 g2 blanchet@48975 156 assume "\z. z \ {fst x} \ f1 z = g1 z" "\z. z \ {snd x} \ f2 z = g2 z" blanchet@55932 157 thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp blanchet@48975 158 next blanchet@48975 159 fix f1 f2 blanchet@55932 160 show "(\x. {fst x}) o map_prod f1 f2 = image f1 o (\x. {fst x})" blanchet@48975 161 by (rule ext, unfold o_apply) simp blanchet@48975 162 next blanchet@48975 163 fix f1 f2 blanchet@55932 164 show "(\x. {snd x}) o map_prod f1 f2 = image f2 o (\x. {snd x})" blanchet@48975 165 by (rule ext, unfold o_apply) simp blanchet@48975 166 next traytel@52635 167 show "card_order natLeq" by (rule natLeq_card_order) blanchet@48975 168 next traytel@52635 169 show "cinfinite natLeq" by (rule natLeq_cinfinite) blanchet@48975 170 next blanchet@48975 171 fix x traytel@52635 172 show "|{fst x}| \o natLeq" traytel@55811 173 by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric]) blanchet@48975 174 next traytel@52635 175 fix x traytel@52635 176 show "|{snd x}| \o natLeq" traytel@55811 177 by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric]) blanchet@48975 178 next traytel@54841 179 fix R1 R2 S1 S2 blanchet@55944 180 show "rel_prod R1 R2 OO rel_prod S1 S2 \ rel_prod (R1 OO S1) (R2 OO S2)" by auto blanchet@49453 181 next blanchet@49453 182 fix R S traytel@62324 183 show "rel_prod R S = (\x y. traytel@62324 184 \z. ({fst z} \ {(x, y). R x y} \ {snd z} \ {(x, y). S x y}) \ traytel@62324 185 map_prod fst fst z = x \ map_prod snd snd z = y)" blanchet@62335 186 unfolding prod_set_defs rel_prod_inject relcompp.simps conversep.simps fun_eq_iff blanchet@49453 187 by auto traytel@62324 188 qed auto blanchet@48975 189 traytel@54421 190 bnf "'a \ 'b" traytel@54421 191 map: "op \" traytel@54421 192 sets: range traytel@54421 193 bd: "natLeq +c |UNIV :: 'a set|" blanchet@55945 194 rel: "rel_fun op =" traytel@62324 195 pred: "pred_fun (\_. True)" blanchet@48975 196 proof blanchet@48975 197 fix f show "id \ f = id f" by simp blanchet@48975 198 next blanchet@48975 199 fix f g show "op \ (g \ f) = op \ g \ op \ f" blanchet@48975 200 unfolding comp_def[abs_def] .. blanchet@48975 201 next blanchet@48975 202 fix x f g blanchet@48975 203 assume "\z. z \ range x \ f z = g z" blanchet@48975 204 thus "f \ x = g \ x" by auto blanchet@48975 205 next blanchet@48975 206 fix f show "range \ op \ f = op ` f \ range" haftmann@56077 207 by (auto simp add: fun_eq_iff) blanchet@48975 208 next blanchet@48975 209 show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)") blanchet@48975 210 apply (rule card_order_csum) blanchet@48975 211 apply (rule natLeq_card_order) blanchet@48975 212 by (rule card_of_card_order_on) blanchet@48975 213 (* *) blanchet@48975 214 show "cinfinite (natLeq +c ?U)" blanchet@48975 215 apply (rule cinfinite_csum) blanchet@48975 216 apply (rule disjI1) blanchet@48975 217 by (rule natLeq_cinfinite) blanchet@48975 218 next blanchet@48975 219 fix f :: "'d => 'a" blanchet@48975 220 have "|range f| \o | (UNIV::'d set) |" (is "_ \o ?U") by (rule card_of_image) blanchet@54486 221 also have "?U \o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order) blanchet@48975 222 finally show "|range f| \o natLeq +c ?U" . blanchet@48975 223 next traytel@54841 224 fix R S blanchet@55945 225 show "rel_fun op = R OO rel_fun op = S \ rel_fun op = (R OO S)" by (auto simp: rel_fun_def) blanchet@49453 226 next blanchet@49463 227 fix R traytel@62324 228 show "rel_fun op = R = (\x y. traytel@62324 229 \z. range z \ {(x, y). R x y} \ fst \ z = x \ snd \ z = y)" traytel@62324 230 unfolding rel_fun_def subset_iff by (force simp: fun_eq_iff[symmetric]) traytel@62324 231 qed (auto simp: pred_fun_def) traytel@54191 232 blanchet@48975 233 end