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