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