src/HOL/ZF/Zet.thy
author nipkow
Thu Oct 22 09:27:48 2009 +0200 (2009-10-22)
changeset 33057 764547b68538
parent 32988 d1d4d7a08a66
child 35416 d8d7d1b785af
permissions -rw-r--r--
inv_onto -> inv_into
     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_zet_rep: "A \<in> zet \<Longrightarrow> ? z . g ` A = explode z"
    37   apply (auto simp add: zet_def')
    38   apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
    39   apply (simp add: explode_Repl_eq)
    40   apply (subgoal_tac "explode z = f ` A")
    41   apply (simp_all add: comp_image_eq)
    42   done
    43 
    44 lemma zet_image_mem:
    45   assumes Azet: "A \<in> zet"
    46   shows "g ` A \<in> zet"
    47 proof -
    48   from Azet have "? (f :: _ \<Rightarrow> ZF). inj_on f A" 
    49     by (auto simp add: zet_def')
    50   then obtain f where injf: "inj_on (f :: _ \<Rightarrow> ZF) A"  
    51     by auto
    52   let ?w = "f o (inv_into A g)"
    53   have subset: "(inv_into A g) ` (g ` A) \<subseteq> A"
    54     by (auto simp add: inv_into_into)
    55   have "inj_on (inv_into A g) (g ` A)" by (simp add: inj_on_inv_into)
    56   then have injw: "inj_on ?w (g ` A)"
    57     apply (rule comp_inj_on)
    58     apply (rule subset_inj_on[where B=A])
    59     apply (auto simp add: subset injf)
    60     done
    61   show ?thesis
    62     apply (simp add: zet_def' comp_image_eq[symmetric])
    63     apply (rule exI[where x="?w"])
    64     apply (simp add: injw image_zet_rep Azet)
    65     done
    66 qed
    67 
    68 lemma Rep_zimage_eq: "Rep_zet (zimage f A) = image f (Rep_zet A)"
    69   apply (simp add: zimage_def)
    70   apply (subst Abs_zet_inverse)
    71   apply (simp_all add: Rep_zet zet_image_mem)
    72   done
    73 
    74 lemma zimage_iff: "zin y (zimage f A) = (? x. zin x A & y = f x)"
    75   by (auto simp add: zin_def Rep_zimage_eq)
    76 
    77 constdefs
    78   zimplode :: "ZF zet \<Rightarrow> ZF"
    79   "zimplode A == implode (Rep_zet A)"
    80   zexplode :: "ZF \<Rightarrow> ZF zet"
    81   "zexplode z == Abs_zet (explode z)"
    82 
    83 lemma Rep_zet_eq_explode: "? z. Rep_zet A = explode z"
    84   by (rule image_zet_rep[where g="\<lambda> x. x",OF Rep_zet, simplified])
    85 
    86 lemma zexplode_zimplode: "zexplode (zimplode A) = A"
    87   apply (simp add: zimplode_def zexplode_def)
    88   apply (simp add: implode_def)
    89   apply (subst f_inv_into_f[where y="Rep_zet A"])
    90   apply (auto simp add: Rep_zet_inverse Rep_zet_eq_explode image_def)
    91   done
    92 
    93 lemma explode_mem_zet: "explode z \<in> zet"
    94   apply (simp add: zet_def')
    95   apply (rule_tac x="% x. x" in exI)
    96   apply (auto simp add: inj_on_def)
    97   done
    98 
    99 lemma zimplode_zexplode: "zimplode (zexplode z) = z"
   100   apply (simp add: zimplode_def zexplode_def)
   101   apply (subst Abs_zet_inverse)
   102   apply (auto simp add: explode_mem_zet implode_explode)
   103   done  
   104 
   105 lemma zin_zexplode_eq: "zin x (zexplode A) = Elem x A"
   106   apply (simp add: zin_def zexplode_def)
   107   apply (subst Abs_zet_inverse)
   108   apply (simp_all add: explode_Elem explode_mem_zet) 
   109   done
   110 
   111 lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A"
   112   apply (simp add: zimage_def)
   113   apply (subst Abs_zet_inverse)
   114   apply (simp_all add: comp_image_eq zet_image_mem Rep_zet)
   115   done
   116     
   117 constdefs
   118   zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet"
   119   "zunion a b \<equiv> Abs_zet ((Rep_zet a) \<union> (Rep_zet b))"
   120   zsubset :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> bool"
   121   "zsubset a b \<equiv> ! x. zin x a \<longrightarrow> zin x b"
   122 
   123 lemma explode_union: "explode (union a b) = (explode a) \<union> (explode b)"
   124   apply (rule set_ext)
   125   apply (simp add: explode_def union)
   126   done
   127 
   128 lemma Rep_zet_zunion: "Rep_zet (zunion a b) = (Rep_zet a) \<union> (Rep_zet b)"
   129 proof -
   130   from Rep_zet[of a] have "? f z. inj_on f (Rep_zet a) \<and> f ` (Rep_zet a) = explode z"
   131     by (auto simp add: zet_def')
   132   then obtain fa za where a:"inj_on fa (Rep_zet a) \<and> fa ` (Rep_zet a) = explode za"
   133     by blast
   134   from a have fa: "inj_on fa (Rep_zet a)" by blast
   135   from a have za: "fa ` (Rep_zet a) = explode za" by blast
   136   from Rep_zet[of b] have "? f z. inj_on f (Rep_zet b) \<and> f ` (Rep_zet b) = explode z"
   137     by (auto simp add: zet_def')
   138   then obtain fb zb where b:"inj_on fb (Rep_zet b) \<and> fb ` (Rep_zet b) = explode zb"
   139     by blast
   140   from b have fb: "inj_on fb (Rep_zet b)" by blast
   141   from b have zb: "fb ` (Rep_zet b) = explode zb" by blast 
   142   let ?f = "(\<lambda> x. if x \<in> (Rep_zet a) then Opair (fa x) (Empty) else Opair (fb x) (Singleton Empty))" 
   143   let ?z = "CartProd (union za zb) (Upair Empty (Singleton Empty))"
   144   have se: "Singleton Empty \<noteq> Empty"
   145     apply (auto simp add: Ext Singleton)
   146     apply (rule exI[where x=Empty])
   147     apply (simp add: Empty)
   148     done
   149   show ?thesis
   150     apply (simp add: zunion_def)
   151     apply (subst Abs_zet_inverse)
   152     apply (auto simp add: zet_def)
   153     apply (rule exI[where x = ?f])
   154     apply (rule conjI)
   155     apply (auto simp add: inj_on_def Opair inj_onD[OF fa] inj_onD[OF fb] se se[symmetric])
   156     apply (rule exI[where x = ?z])
   157     apply (insert za zb)
   158     apply (auto simp add: explode_def CartProd union Upair Opair)
   159     done
   160 qed
   161 
   162 lemma zunion: "zin x (zunion a b) = ((zin x a) \<or> (zin x b))"
   163   by (auto simp add: zin_def Rep_zet_zunion)
   164 
   165 lemma zimage_zexplode_eq: "zimage f (zexplode z) = zexplode (Repl z f)"
   166   by (simp add: zet_ext_eq zin_zexplode_eq Repl zimage_iff)
   167 
   168 lemma range_explode_eq_zet: "range explode = zet"
   169   apply (rule set_ext)
   170   apply (auto simp add: explode_mem_zet)
   171   apply (drule image_zet_rep)
   172   apply (simp add: image_def)
   173   apply auto
   174   apply (rule_tac x=z in exI)
   175   apply auto
   176   done
   177 
   178 lemma Elem_zimplode: "(Elem x (zimplode z)) = (zin x z)"
   179   apply (simp add: zimplode_def)
   180   apply (subst Elem_implode)
   181   apply (simp_all add: zin_def Rep_zet range_explode_eq_zet)
   182   done
   183 
   184 constdefs
   185   zempty :: "'a zet"
   186   "zempty \<equiv> Abs_zet {}"
   187 
   188 lemma zempty[simp]: "\<not> (zin x zempty)"
   189   by (auto simp add: zin_def zempty_def Abs_zet_inverse zet_def)
   190 
   191 lemma zimage_zempty[simp]: "zimage f zempty = zempty"
   192   by (auto simp add: zet_ext_eq zimage_iff)
   193 
   194 lemma zunion_zempty_left[simp]: "zunion zempty a = a"
   195   by (simp add: zet_ext_eq zunion)
   196 
   197 lemma zunion_zempty_right[simp]: "zunion a zempty = a"
   198   by (simp add: zet_ext_eq zunion)
   199 
   200 lemma zimage_id[simp]: "zimage id A = A"
   201   by (simp add: zet_ext_eq zimage_iff)
   202 
   203 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"
   204   by (auto simp add: zet_ext_eq zimage_iff)
   205 
   206 end