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