src/HOL/ZF/Zet.thy
 author krauss Tue Mar 02 12:26:50 2010 +0100 (2010-03-02) changeset 35440 bdf8ad377877 parent 35416 d8d7d1b785af child 35502 3d105282262e permissions -rw-r--r--
killed more recdefs
 obua@19203 ` 1` ```(* Title: HOL/ZF/Zet.thy ``` obua@19203 ` 2` ``` Author: Steven Obua ``` obua@19203 ` 3` obua@19203 ` 4` ``` Introduces a type 'a zet of ZF representable sets. ``` obua@19203 ` 5` ``` See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan ``` obua@19203 ` 6` ```*) ``` obua@19203 ` 7` obua@19203 ` 8` ```theory Zet ``` obua@19203 ` 9` ```imports HOLZF ``` obua@19203 ` 10` ```begin ``` obua@19203 ` 11` obua@19203 ` 12` ```typedef 'a zet = "{A :: 'a set | A f z. inj_on f A \ f ` A \ explode z}" ``` obua@19203 ` 13` ``` by blast ``` obua@19203 ` 14` haftmann@35416 ` 15` ```definition zin :: "'a \ 'a zet \ bool" where ``` obua@19203 ` 16` ``` "zin x A == x \ (Rep_zet A)" ``` obua@19203 ` 17` obua@19203 ` 18` ```lemma zet_ext_eq: "(A = B) = (! x. zin x A = zin x B)" ``` obua@19203 ` 19` ``` by (auto simp add: Rep_zet_inject[symmetric] zin_def) ``` obua@19203 ` 20` haftmann@35416 ` 21` ```definition zimage :: "('a \ 'b) \ 'a zet \ 'b zet" where ``` obua@19203 ` 22` ``` "zimage f A == Abs_zet (image f (Rep_zet A))" ``` obua@19203 ` 23` obua@19203 ` 24` ```lemma zet_def': "zet = {A :: 'a set | A f z. inj_on f A \ f ` A = explode z}" ``` obua@19203 ` 25` ``` apply (rule set_ext) ``` obua@19203 ` 26` ``` apply (auto simp add: zet_def) ``` obua@19203 ` 27` ``` apply (rule_tac x=f in exI) ``` obua@19203 ` 28` ``` apply auto ``` obua@19203 ` 29` ``` apply (rule_tac x="Sep z (\ y. y \ (f ` x))" in exI) ``` obua@19203 ` 30` ``` apply (auto simp add: explode_def Sep) ``` obua@19203 ` 31` ``` done ``` obua@19203 ` 32` obua@19203 ` 33` ```lemma image_zet_rep: "A \ zet \ ? z . g ` A = explode z" ``` obua@19203 ` 34` ``` apply (auto simp add: zet_def') ``` nipkow@33057 ` 35` ``` apply (rule_tac x="Repl z (g o (inv_into A f))" in exI) ``` obua@19203 ` 36` ``` apply (simp add: explode_Repl_eq) ``` obua@19203 ` 37` ``` apply (subgoal_tac "explode z = f ` A") ``` nipkow@32988 ` 38` ``` apply (simp_all add: comp_image_eq) ``` obua@19203 ` 39` ``` done ``` obua@19203 ` 40` obua@19203 ` 41` ```lemma zet_image_mem: ``` obua@19203 ` 42` ``` assumes Azet: "A \ zet" ``` obua@19203 ` 43` ``` shows "g ` A \ zet" ``` obua@19203 ` 44` ```proof - ``` obua@19203 ` 45` ``` from Azet have "? (f :: _ \ ZF). inj_on f A" ``` obua@19203 ` 46` ``` by (auto simp add: zet_def') ``` obua@19203 ` 47` ``` then obtain f where injf: "inj_on (f :: _ \ ZF) A" ``` obua@19203 ` 48` ``` by auto ``` nipkow@33057 ` 49` ``` let ?w = "f o (inv_into A g)" ``` nipkow@33057 ` 50` ``` have subset: "(inv_into A g) ` (g ` A) \ A" ``` nipkow@33057 ` 51` ``` by (auto simp add: inv_into_into) ``` nipkow@33057 ` 52` ``` have "inj_on (inv_into A g) (g ` A)" by (simp add: inj_on_inv_into) ``` obua@19203 ` 53` ``` then have injw: "inj_on ?w (g ` A)" ``` obua@19203 ` 54` ``` apply (rule comp_inj_on) ``` obua@19203 ` 55` ``` apply (rule subset_inj_on[where B=A]) ``` obua@19203 ` 56` ``` apply (auto simp add: subset injf) ``` obua@19203 ` 57` ``` done ``` obua@19203 ` 58` ``` show ?thesis ``` obua@19203 ` 59` ``` apply (simp add: zet_def' comp_image_eq[symmetric]) ``` obua@19203 ` 60` ``` apply (rule exI[where x="?w"]) ``` obua@19203 ` 61` ``` apply (simp add: injw image_zet_rep Azet) ``` obua@19203 ` 62` ``` done ``` obua@19203 ` 63` ```qed ``` obua@19203 ` 64` obua@19203 ` 65` ```lemma Rep_zimage_eq: "Rep_zet (zimage f A) = image f (Rep_zet A)" ``` obua@19203 ` 66` ``` apply (simp add: zimage_def) ``` obua@19203 ` 67` ``` apply (subst Abs_zet_inverse) ``` obua@19203 ` 68` ``` apply (simp_all add: Rep_zet zet_image_mem) ``` obua@19203 ` 69` ``` done ``` obua@19203 ` 70` obua@19203 ` 71` ```lemma zimage_iff: "zin y (zimage f A) = (? x. zin x A & y = f x)" ``` obua@19203 ` 72` ``` by (auto simp add: zin_def Rep_zimage_eq) ``` obua@19203 ` 73` haftmann@35416 ` 74` ```definition zimplode :: "ZF zet \ ZF" where ``` obua@19203 ` 75` ``` "zimplode A == implode (Rep_zet A)" ``` haftmann@35416 ` 76` haftmann@35416 ` 77` ```definition zexplode :: "ZF \ ZF zet" where ``` obua@19203 ` 78` ``` "zexplode z == Abs_zet (explode z)" ``` obua@19203 ` 79` obua@19203 ` 80` ```lemma Rep_zet_eq_explode: "? z. Rep_zet A = explode z" ``` obua@19203 ` 81` ``` by (rule image_zet_rep[where g="\ x. x",OF Rep_zet, simplified]) ``` obua@19203 ` 82` obua@19203 ` 83` ```lemma zexplode_zimplode: "zexplode (zimplode A) = A" ``` obua@19203 ` 84` ``` apply (simp add: zimplode_def zexplode_def) ``` obua@19203 ` 85` ``` apply (simp add: implode_def) ``` nipkow@33057 ` 86` ``` apply (subst f_inv_into_f[where y="Rep_zet A"]) ``` obua@19203 ` 87` ``` apply (auto simp add: Rep_zet_inverse Rep_zet_eq_explode image_def) ``` obua@19203 ` 88` ``` done ``` obua@19203 ` 89` obua@19203 ` 90` ```lemma explode_mem_zet: "explode z \ zet" ``` obua@19203 ` 91` ``` apply (simp add: zet_def') ``` obua@19203 ` 92` ``` apply (rule_tac x="% x. x" in exI) ``` obua@19203 ` 93` ``` apply (auto simp add: inj_on_def) ``` obua@19203 ` 94` ``` done ``` obua@19203 ` 95` obua@19203 ` 96` ```lemma zimplode_zexplode: "zimplode (zexplode z) = z" ``` obua@19203 ` 97` ``` apply (simp add: zimplode_def zexplode_def) ``` obua@19203 ` 98` ``` apply (subst Abs_zet_inverse) ``` obua@19203 ` 99` ``` apply (auto simp add: explode_mem_zet implode_explode) ``` obua@19203 ` 100` ``` done ``` obua@19203 ` 101` obua@19203 ` 102` ```lemma zin_zexplode_eq: "zin x (zexplode A) = Elem x A" ``` obua@19203 ` 103` ``` apply (simp add: zin_def zexplode_def) ``` obua@19203 ` 104` ``` apply (subst Abs_zet_inverse) ``` obua@19203 ` 105` ``` apply (simp_all add: explode_Elem explode_mem_zet) ``` obua@19203 ` 106` ``` done ``` obua@19203 ` 107` obua@19203 ` 108` ```lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A" ``` obua@19203 ` 109` ``` apply (simp add: zimage_def) ``` obua@19203 ` 110` ``` apply (subst Abs_zet_inverse) ``` obua@19203 ` 111` ``` apply (simp_all add: comp_image_eq zet_image_mem Rep_zet) ``` obua@19203 ` 112` ``` done ``` obua@19203 ` 113` ``` ``` haftmann@35416 ` 114` ```definition zunion :: "'a zet \ 'a zet \ 'a zet" where ``` obua@19203 ` 115` ``` "zunion a b \ Abs_zet ((Rep_zet a) \ (Rep_zet b))" ``` haftmann@35416 ` 116` haftmann@35416 ` 117` ```definition zsubset :: "'a zet \ 'a zet \ bool" where ``` obua@19203 ` 118` ``` "zsubset a b \ ! x. zin x a \ zin x b" ``` obua@19203 ` 119` obua@19203 ` 120` ```lemma explode_union: "explode (union a b) = (explode a) \ (explode b)" ``` obua@19203 ` 121` ``` apply (rule set_ext) ``` obua@19203 ` 122` ``` apply (simp add: explode_def union) ``` obua@19203 ` 123` ``` done ``` obua@19203 ` 124` obua@19203 ` 125` ```lemma Rep_zet_zunion: "Rep_zet (zunion a b) = (Rep_zet a) \ (Rep_zet b)" ``` obua@19203 ` 126` ```proof - ``` obua@19203 ` 127` ``` from Rep_zet[of a] have "? f z. inj_on f (Rep_zet a) \ f ` (Rep_zet a) = explode z" ``` obua@19203 ` 128` ``` by (auto simp add: zet_def') ``` obua@19203 ` 129` ``` then obtain fa za where a:"inj_on fa (Rep_zet a) \ fa ` (Rep_zet a) = explode za" ``` obua@19203 ` 130` ``` by blast ``` obua@19203 ` 131` ``` from a have fa: "inj_on fa (Rep_zet a)" by blast ``` obua@19203 ` 132` ``` from a have za: "fa ` (Rep_zet a) = explode za" by blast ``` obua@19203 ` 133` ``` from Rep_zet[of b] have "? f z. inj_on f (Rep_zet b) \ f ` (Rep_zet b) = explode z" ``` obua@19203 ` 134` ``` by (auto simp add: zet_def') ``` obua@19203 ` 135` ``` then obtain fb zb where b:"inj_on fb (Rep_zet b) \ fb ` (Rep_zet b) = explode zb" ``` obua@19203 ` 136` ``` by blast ``` obua@19203 ` 137` ``` from b have fb: "inj_on fb (Rep_zet b)" by blast ``` obua@19203 ` 138` ``` from b have zb: "fb ` (Rep_zet b) = explode zb" by blast ``` obua@19203 ` 139` ``` let ?f = "(\ x. if x \ (Rep_zet a) then Opair (fa x) (Empty) else Opair (fb x) (Singleton Empty))" ``` obua@19203 ` 140` ``` let ?z = "CartProd (union za zb) (Upair Empty (Singleton Empty))" ``` obua@19203 ` 141` ``` have se: "Singleton Empty \ Empty" ``` obua@19203 ` 142` ``` apply (auto simp add: Ext Singleton) ``` obua@19203 ` 143` ``` apply (rule exI[where x=Empty]) ``` obua@19203 ` 144` ``` apply (simp add: Empty) ``` obua@19203 ` 145` ``` done ``` obua@19203 ` 146` ``` show ?thesis ``` obua@19203 ` 147` ``` apply (simp add: zunion_def) ``` obua@19203 ` 148` ``` apply (subst Abs_zet_inverse) ``` obua@19203 ` 149` ``` apply (auto simp add: zet_def) ``` obua@19203 ` 150` ``` apply (rule exI[where x = ?f]) ``` obua@19203 ` 151` ``` apply (rule conjI) ``` obua@19203 ` 152` ``` apply (auto simp add: inj_on_def Opair inj_onD[OF fa] inj_onD[OF fb] se se[symmetric]) ``` obua@19203 ` 153` ``` apply (rule exI[where x = ?z]) ``` obua@19203 ` 154` ``` apply (insert za zb) ``` obua@19203 ` 155` ``` apply (auto simp add: explode_def CartProd union Upair Opair) ``` obua@19203 ` 156` ``` done ``` obua@19203 ` 157` ```qed ``` obua@19203 ` 158` obua@19203 ` 159` ```lemma zunion: "zin x (zunion a b) = ((zin x a) \ (zin x b))" ``` obua@19203 ` 160` ``` by (auto simp add: zin_def Rep_zet_zunion) ``` obua@19203 ` 161` obua@19203 ` 162` ```lemma zimage_zexplode_eq: "zimage f (zexplode z) = zexplode (Repl z f)" ``` obua@19203 ` 163` ``` by (simp add: zet_ext_eq zin_zexplode_eq Repl zimage_iff) ``` obua@19203 ` 164` obua@19203 ` 165` ```lemma range_explode_eq_zet: "range explode = zet" ``` obua@19203 ` 166` ``` apply (rule set_ext) ``` obua@19203 ` 167` ``` apply (auto simp add: explode_mem_zet) ``` obua@19203 ` 168` ``` apply (drule image_zet_rep) ``` obua@19203 ` 169` ``` apply (simp add: image_def) ``` obua@19203 ` 170` ``` apply auto ``` obua@19203 ` 171` ``` apply (rule_tac x=z in exI) ``` obua@19203 ` 172` ``` apply auto ``` obua@19203 ` 173` ``` done ``` obua@19203 ` 174` obua@19203 ` 175` ```lemma Elem_zimplode: "(Elem x (zimplode z)) = (zin x z)" ``` obua@19203 ` 176` ``` apply (simp add: zimplode_def) ``` obua@19203 ` 177` ``` apply (subst Elem_implode) ``` obua@19203 ` 178` ``` apply (simp_all add: zin_def Rep_zet range_explode_eq_zet) ``` obua@19203 ` 179` ``` done ``` obua@19203 ` 180` haftmann@35416 ` 181` ```definition zempty :: "'a zet" where ``` obua@19203 ` 182` ``` "zempty \ Abs_zet {}" ``` obua@19203 ` 183` obua@19203 ` 184` ```lemma zempty[simp]: "\ (zin x zempty)" ``` obua@19203 ` 185` ``` by (auto simp add: zin_def zempty_def Abs_zet_inverse zet_def) ``` obua@19203 ` 186` obua@19203 ` 187` ```lemma zimage_zempty[simp]: "zimage f zempty = zempty" ``` obua@19203 ` 188` ``` by (auto simp add: zet_ext_eq zimage_iff) ``` obua@19203 ` 189` obua@19203 ` 190` ```lemma zunion_zempty_left[simp]: "zunion zempty a = a" ``` obua@19203 ` 191` ``` by (simp add: zet_ext_eq zunion) ``` obua@19203 ` 192` obua@19203 ` 193` ```lemma zunion_zempty_right[simp]: "zunion a zempty = a" ``` obua@19203 ` 194` ``` by (simp add: zet_ext_eq zunion) ``` obua@19203 ` 195` obua@19203 ` 196` ```lemma zimage_id[simp]: "zimage id A = A" ``` obua@19203 ` 197` ``` by (simp add: zet_ext_eq zimage_iff) ``` obua@19203 ` 198` krauss@35440 ` 199` ```lemma zimage_cong[recdef_cong, fundef_cong]: "\ M = N; !! x. zin x N \ f x = g x \ \ zimage f M = zimage g N" ``` obua@19203 ` 200` ``` by (auto simp add: zet_ext_eq zimage_iff) ``` obua@19203 ` 201` obua@19203 ` 202` ```end ```