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