src/HOL/ZF/Zet.thy
changeset 19203 778507520684
child 22931 11cc1ccad58e
equal deleted 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