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