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