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