Constructible: some separation axioms
authorpaulson
Thu Jul 04 16:59:54 2002 +0200 (2002-07-04)
changeset 13298b4f370679c65
parent 13297 e4ae0732e2be
child 13299 3a932abf97e8
Constructible: some separation axioms
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Wellorderings.thy
src/ZF/OrdQuant.thy
     1.1 --- a/src/ZF/Constructible/Formula.thy	Thu Jul 04 16:48:21 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Formula.thy	Thu Jul 04 16:59:54 2002 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5  declare satisfies.simps [simp del]; 
     1.6  
     1.7 -subsubsection{*Dividing line between primitive and derived connectives*}
     1.8 +subsection{*Dividing line between primitive and derived connectives*}
     1.9  
    1.10  lemma sats_Or_iff [simp]:
    1.11    "env \<in> list(A) 
    1.12 @@ -125,6 +125,11 @@
    1.13         ==> (x\<in>y) <-> sats(A, Member(i,j), env)" 
    1.14  by (simp add: satisfies.simps)
    1.15  
    1.16 +lemma equal_iff_sats:
    1.17 +      "[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
    1.18 +       ==> (x=y) <-> sats(A, Equal(i,j), env)" 
    1.19 +by (simp add: satisfies.simps)
    1.20 +
    1.21  lemma conj_iff_sats:
    1.22        "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
    1.23         ==> (P & Q) <-> sats(A, And(p,q), env)"
    1.24 @@ -161,22 +166,6 @@
    1.25  by (simp add: sats_Exists_iff) 
    1.26  
    1.27  
    1.28 -
    1.29 -(*pretty but unnecessary
    1.30 -constdefs sat     :: "[i,i] => o"
    1.31 -  "sat(A,p) == satisfies(A,p)`[] = 1"
    1.32 -
    1.33 -syntax "_sat"  :: "[i,i] => o"    (infixl "|=" 50)
    1.34 -translations "A |= p" == "sat(A,p)"
    1.35 -
    1.36 -lemma [simp]: "(A |= Neg(p)) <-> ~ (A |= p)"
    1.37 -by (simp add: sat_def)
    1.38 -
    1.39 -lemma [simp]: "(A |= And(p,q)) <-> A|=p & A|=q"
    1.40 -by (simp add: sat_def)
    1.41 -*) 
    1.42 -
    1.43 -
    1.44  constdefs incr_var :: "[i,i]=>i"
    1.45      "incr_var(x,lev) == if x<lev then x else succ(x)"
    1.46  
    1.47 @@ -355,7 +344,7 @@
    1.48  done
    1.49  
    1.50  
    1.51 -(**** TRYING INCR_BV1 AGAIN ****)
    1.52 +subsection{*Renaming all but the first bound variable*}
    1.53  
    1.54  constdefs incr_bv1 :: "i => i"
    1.55      "incr_bv1(p) == incr_bv(p)`1"
    1.56 @@ -398,7 +387,7 @@
    1.57     ==> arity(incr_bv1^n(p)) =
    1.58           (if 1 < arity(p) then n #+ arity(p) else arity(p))"
    1.59  apply (induct_tac n) 
    1.60 -apply (simp_all add: arity_incr_bv1_eq )
    1.61 +apply (simp_all add: arity_incr_bv1_eq)
    1.62  apply (simp add: not_lt_iff_le)
    1.63  apply (blast intro: le_trans add_le_self2 arity_type) 
    1.64  done
    1.65 @@ -520,6 +509,76 @@
    1.66  oops
    1.67  *)
    1.68  
    1.69 +
    1.70 +subsection{*Internalized formulas for basic concepts*}
    1.71 +
    1.72 +subsubsection{*The subset relation*}
    1.73 +
    1.74 +lemma lt_length_in_nat:
    1.75 +   "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
    1.76 +apply (frule lt_nat_in_nat, typecheck) 
    1.77 +done
    1.78 +
    1.79 +constdefs subset_fm :: "[i,i]=>i"
    1.80 +    "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
    1.81 +
    1.82 +lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
    1.83 +by (simp add: subset_fm_def) 
    1.84 +
    1.85 +lemma arity_subset_fm [simp]:
    1.86 +     "[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
    1.87 +by (simp add: subset_fm_def succ_Un_distrib [symmetric]) 
    1.88 +
    1.89 +lemma sats_subset_fm [simp]:
    1.90 +   "[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|]
    1.91 +    ==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \<subseteq> nth(y,env)"
    1.92 +apply (frule lt_length_in_nat, assumption)  
    1.93 +apply (simp add: subset_fm_def Transset_def) 
    1.94 +apply (blast intro: nth_type) 
    1.95 +done
    1.96 +
    1.97 +subsubsection{*Transitive sets*}
    1.98 +
    1.99 +constdefs transset_fm :: "i=>i"
   1.100 +   "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
   1.101 +
   1.102 +lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
   1.103 +by (simp add: transset_fm_def) 
   1.104 +
   1.105 +lemma arity_transset_fm [simp]:
   1.106 +     "x \<in> nat ==> arity(transset_fm(x)) = succ(x)"
   1.107 +by (simp add: transset_fm_def succ_Un_distrib [symmetric]) 
   1.108 +
   1.109 +lemma sats_transset_fm [simp]:
   1.110 +   "[|x < length(env); env \<in> list(A); Transset(A)|]
   1.111 +    ==> sats(A, transset_fm(x), env) <-> Transset(nth(x,env))"
   1.112 +apply (frule lt_nat_in_nat, erule length_type) 
   1.113 +apply (simp add: transset_fm_def Transset_def) 
   1.114 +apply (blast intro: nth_type) 
   1.115 +done
   1.116 +
   1.117 +subsubsection{*Ordinals*}
   1.118 +
   1.119 +constdefs ordinal_fm :: "i=>i"
   1.120 +   "ordinal_fm(x) == 
   1.121 +      And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
   1.122 +
   1.123 +lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
   1.124 +by (simp add: ordinal_fm_def) 
   1.125 +
   1.126 +lemma arity_ordinal_fm [simp]:
   1.127 +     "x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"
   1.128 +by (simp add: ordinal_fm_def succ_Un_distrib [symmetric]) 
   1.129 +
   1.130 +lemma sats_ordinal_fm [simp]:
   1.131 +   "[|x < length(env); env \<in> list(A); Transset(A)|]
   1.132 +    ==> sats(A, ordinal_fm(x), env) <-> Ord(nth(x,env))"
   1.133 +apply (frule lt_nat_in_nat, erule length_type) 
   1.134 +apply (simp add: ordinal_fm_def Ord_def Transset_def)
   1.135 +apply (blast intro: nth_type) 
   1.136 +done
   1.137 +
   1.138 +
   1.139  subsection{* Constant Lset: Levels of the Constructible Universe *}
   1.140  
   1.141  constdefs Lset :: "i=>i"
   1.142 @@ -661,63 +720,7 @@
   1.143  done
   1.144  
   1.145  
   1.146 -
   1.147 -text{*Kunen's VI, 1.9 (b)*}
   1.148 -
   1.149 -constdefs subset_fm :: "[i,i]=>i"
   1.150 -    "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
   1.151 -
   1.152 -lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
   1.153 -by (simp add: subset_fm_def) 
   1.154 -
   1.155 -lemma arity_subset_fm [simp]:
   1.156 -     "[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
   1.157 -by (simp add: subset_fm_def succ_Un_distrib [symmetric]) 
   1.158 -
   1.159 -lemma sats_subset_fm [simp]:
   1.160 -   "[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|]
   1.161 -    ==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \<subseteq> nth(y,env)"
   1.162 -apply (frule lt_nat_in_nat, erule length_type) 
   1.163 -apply (simp add: subset_fm_def Transset_def) 
   1.164 -apply (blast intro: nth_type ) 
   1.165 -done
   1.166 -
   1.167 -constdefs transset_fm :: "i=>i"
   1.168 -   "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
   1.169 -
   1.170 -lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
   1.171 -by (simp add: transset_fm_def) 
   1.172 -
   1.173 -lemma arity_transset_fm [simp]:
   1.174 -     "x \<in> nat ==> arity(transset_fm(x)) = succ(x)"
   1.175 -by (simp add: transset_fm_def succ_Un_distrib [symmetric]) 
   1.176 -
   1.177 -lemma sats_transset_fm [simp]:
   1.178 -   "[|x < length(env); env \<in> list(A); Transset(A)|]
   1.179 -    ==> sats(A, transset_fm(x), env) <-> Transset(nth(x,env))"
   1.180 -apply (frule lt_nat_in_nat, erule length_type) 
   1.181 -apply (simp add: transset_fm_def Transset_def) 
   1.182 -apply (blast intro: nth_type ) 
   1.183 -done
   1.184 -
   1.185 -constdefs ordinal_fm :: "i=>i"
   1.186 -   "ordinal_fm(x) == 
   1.187 -      And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
   1.188 -
   1.189 -lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
   1.190 -by (simp add: ordinal_fm_def) 
   1.191 -
   1.192 -lemma arity_ordinal_fm [simp]:
   1.193 -     "x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"
   1.194 -by (simp add: ordinal_fm_def succ_Un_distrib [symmetric]) 
   1.195 -
   1.196 -lemma sats_ordinal_fm [simp]:
   1.197 -   "[|x < length(env); env \<in> list(A); Transset(A)|]
   1.198 -    ==> sats(A, ordinal_fm(x), env) <-> Ord(nth(x,env))"
   1.199 -apply (frule lt_nat_in_nat, erule length_type) 
   1.200 -apply (simp add: ordinal_fm_def Ord_def Transset_def)
   1.201 -apply (blast intro: nth_type ) 
   1.202 -done
   1.203 +subsection{*Constructible Ordinals: Kunen's VI, 1.9 (b)*}
   1.204  
   1.205  text{*The subset consisting of the ordinals is definable.*}
   1.206  lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Thu Jul 04 16:48:21 2002 +0200
     2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Thu Jul 04 16:59:54 2002 +0200
     2.3 @@ -288,30 +288,344 @@
     2.4  by blast
     2.5  
     2.6  
     2.7 +subsection{*Internalized formulas for some relativized ones*}
     2.8 +
     2.9 +subsubsection{*Unordered pairs*}
    2.10 +
    2.11 +constdefs upair_fm :: "[i,i,i]=>i"
    2.12 +    "upair_fm(x,y,z) == 
    2.13 +       And(Member(x,z), 
    2.14 +           And(Member(y,z),
    2.15 +               Forall(Implies(Member(0,succ(z)), 
    2.16 +                              Or(Equal(0,succ(x)), Equal(0,succ(y)))))))"
    2.17 +
    2.18 +lemma upair_type [TC]:
    2.19 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> upair_fm(x,y,z) \<in> formula"
    2.20 +by (simp add: upair_fm_def) 
    2.21 +
    2.22 +lemma arity_upair_fm [simp]:
    2.23 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
    2.24 +      ==> arity(upair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    2.25 +by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac) 
    2.26 +
    2.27 +lemma sats_upair_fm [simp]:
    2.28 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    2.29 +    ==> sats(A, upair_fm(x,y,z), env) <-> 
    2.30 +            upair(**A, nth(x,env), nth(y,env), nth(z,env))"
    2.31 +by (simp add: upair_fm_def upair_def)
    2.32 +
    2.33 +lemma upair_iff_sats:
    2.34 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    2.35 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    2.36 +       ==> upair(**A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)"
    2.37 +by (simp add: sats_upair_fm)
    2.38 +
    2.39 +text{*Useful? At least it refers to "real" unordered pairs*}
    2.40 +lemma sats_upair_fm2 [simp]:
    2.41 +   "[| x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A); Transset(A)|]
    2.42 +    ==> sats(A, upair_fm(x,y,z), env) <-> 
    2.43 +        nth(z,env) = {nth(x,env), nth(y,env)}"
    2.44 +apply (frule lt_length_in_nat, assumption)  
    2.45 +apply (simp add: upair_fm_def Transset_def, auto) 
    2.46 +apply (blast intro: nth_type) 
    2.47 +done
    2.48 +
    2.49 +subsubsection{*Ordered pairs*}
    2.50 +
    2.51 +constdefs pair_fm :: "[i,i,i]=>i"
    2.52 +    "pair_fm(x,y,z) == 
    2.53 +       Exists(And(upair_fm(succ(x),succ(x),0),
    2.54 +              Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0),
    2.55 +                         upair_fm(1,0,succ(succ(z)))))))"
    2.56 +
    2.57 +lemma pair_type [TC]:
    2.58 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pair_fm(x,y,z) \<in> formula"
    2.59 +by (simp add: pair_fm_def) 
    2.60 +
    2.61 +lemma arity_pair_fm [simp]:
    2.62 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
    2.63 +      ==> arity(pair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    2.64 +by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac) 
    2.65 +
    2.66 +lemma sats_pair_fm [simp]:
    2.67 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    2.68 +    ==> sats(A, pair_fm(x,y,z), env) <-> 
    2.69 +        pair(**A, nth(x,env), nth(y,env), nth(z,env))"
    2.70 +by (simp add: pair_fm_def pair_def)
    2.71 +
    2.72 +lemma pair_iff_sats:
    2.73 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    2.74 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    2.75 +       ==> pair(**A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)"
    2.76 +by (simp add: sats_pair_fm)
    2.77 +
    2.78 +
    2.79 +
    2.80 +subsection{*Proving instances of Separation using Reflection!*}
    2.81 +
    2.82 +text{*Helps us solve for de Bruijn indices!*}
    2.83 +lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
    2.84 +by simp
    2.85 +
    2.86 +
    2.87 +lemma Collect_conj_in_DPow:
    2.88 +     "[| {x\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |] 
    2.89 +      ==> {x\<in>A. P(x) & Q(x)} \<in> DPow(A)"
    2.90 +by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric]) 
    2.91 +
    2.92 +lemma Collect_conj_in_DPow_Lset:
    2.93 +     "[|z \<in> Lset(j); {x \<in> Lset(j). P(x)} \<in> DPow(Lset(j))|]
    2.94 +      ==> {x \<in> Lset(j). x \<in> z & P(x)} \<in> DPow(Lset(j))"
    2.95 +apply (frule mem_Lset_imp_subset_Lset)
    2.96 +apply (simp add: Collect_conj_in_DPow Collect_mem_eq 
    2.97 +                 subset_Int_iff2 elem_subset_in_DPow)
    2.98 +done
    2.99 +
   2.100 +lemma separation_CollectI:
   2.101 +     "(\<And>z. L(z) ==> L({x \<in> z . P(x)})) ==> separation(L, \<lambda>x. P(x))"
   2.102 +apply (unfold separation_def, clarify) 
   2.103 +apply (rule_tac x="{x\<in>z. P(x)}" in rexI) 
   2.104 +apply simp_all
   2.105 +done
   2.106 +
   2.107 +text{*Reduces the original comprehension to the reflected one*}
   2.108 +lemma reflection_imp_L_separation:
   2.109 +      "[| \<forall>x\<in>Lset(j). P(x) <-> Q(x);
   2.110 +          {x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j)); 
   2.111 +          Ord(j);  z \<in> Lset(j)|] ==> L({x \<in> z . P(x)})"
   2.112 +apply (rule_tac i = "succ(j)" in L_I)
   2.113 + prefer 2 apply simp
   2.114 +apply (subgoal_tac "{x \<in> z. P(x)} = {x \<in> Lset(j). x \<in> z & (Q(x))}")
   2.115 + prefer 2
   2.116 + apply (blast dest: mem_Lset_imp_subset_Lset) 
   2.117 +apply (simp add: Lset_succ Collect_conj_in_DPow_Lset)
   2.118 +done
   2.119 +
   2.120 +
   2.121 +subsubsection{*Separation for Intersection*}
   2.122 +
   2.123 +lemma Inter_Reflects:
   2.124 +     "L_Reflects(?Cl, \<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y, 
   2.125 +               \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y)"
   2.126 +by fast
   2.127 +
   2.128 +lemma Inter_separation:
   2.129 +     "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
   2.130 +apply (rule separation_CollectI) 
   2.131 +apply (rule_tac A="{A,z}" in subset_LsetE, blast ) 
   2.132 +apply (rule ReflectsE [OF Inter_Reflects], assumption)
   2.133 +apply (drule subset_Lset_ltD, assumption) 
   2.134 +apply (erule reflection_imp_L_separation)
   2.135 +  apply (simp_all add: lt_Ord2, clarify)
   2.136 +apply (rule DPowI2) 
   2.137 +apply (rule ball_iff_sats) 
   2.138 +apply (rule imp_iff_sats)
   2.139 +apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats)
   2.140 +apply (rule_tac i=0 and j=2 in mem_iff_sats)
   2.141 +apply (simp_all add: succ_Un_distrib [symmetric])
   2.142 +done
   2.143 +
   2.144 +subsubsection{*Separation for Cartesian Product*}
   2.145 +
   2.146 +text{*The @{text simplified} attribute tidies up the reflecting class.*}
   2.147 +theorem upair_reflection [simplified,intro]:
   2.148 +     "L_Reflects(?Cl, \<lambda>x. upair(L,f(x),g(x),h(x)), 
   2.149 +                    \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x)))" 
   2.150 +by (simp add: upair_def, fast) 
   2.151 +
   2.152 +theorem pair_reflection [simplified,intro]:
   2.153 +     "L_Reflects(?Cl, \<lambda>x. pair(L,f(x),g(x),h(x)), 
   2.154 +                    \<lambda>i x. pair(**Lset(i),f(x),g(x),h(x)))"
   2.155 +by (simp only: pair_def rex_setclass_is_bex, fast) 
   2.156 +
   2.157 +lemma cartprod_Reflects [simplified]:
   2.158 +     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
   2.159 +                \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B & 
   2.160 +                               pair(**Lset(i),x,y,z)))"
   2.161 +by fast
   2.162 +
   2.163 +lemma cartprod_separation:
   2.164 +     "[| L(A); L(B) |] 
   2.165 +      ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
   2.166 +apply (rule separation_CollectI) 
   2.167 +apply (rule_tac A="{A,B,z}" in subset_LsetE, blast ) 
   2.168 +apply (rule ReflectsE [OF cartprod_Reflects], assumption)
   2.169 +apply (drule subset_Lset_ltD, assumption) 
   2.170 +apply (erule reflection_imp_L_separation)
   2.171 +  apply (simp_all add: lt_Ord2, clarify) 
   2.172 +apply (rule DPowI2)
   2.173 +apply (rename_tac u)  
   2.174 +apply (rule bex_iff_sats) 
   2.175 +apply (rule conj_iff_sats)
   2.176 +apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)
   2.177 +apply (rule bex_iff_sats) 
   2.178 +apply (rule conj_iff_sats)
   2.179 +apply (rule mem_iff_sats)
   2.180 +apply (blast intro: nth_0 nth_ConsI) 
   2.181 +apply (blast intro: nth_0 nth_ConsI, simp_all)
   2.182 +apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)
   2.183 +apply (simp_all add: succ_Un_distrib [symmetric])
   2.184 +done
   2.185 +
   2.186 +subsubsection{*Separation for Image*}
   2.187 +
   2.188 +text{*No @{text simplified} here: it simplifies the occurrence of 
   2.189 +      the predicate @{term pair}!*}
   2.190 +lemma image_Reflects:
   2.191 +     "L_Reflects(?Cl, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
   2.192 +           \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p)))"
   2.193 +by fast
   2.194 +
   2.195 +
   2.196 +lemma image_separation:
   2.197 +     "[| L(A); L(r) |] 
   2.198 +      ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
   2.199 +apply (rule separation_CollectI) 
   2.200 +apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) 
   2.201 +apply (rule ReflectsE [OF image_Reflects], assumption)
   2.202 +apply (drule subset_Lset_ltD, assumption) 
   2.203 +apply (erule reflection_imp_L_separation)
   2.204 +  apply (simp_all add: lt_Ord2, clarify)
   2.205 +apply (rule DPowI2)
   2.206 +apply (rule bex_iff_sats) 
   2.207 +apply (rule conj_iff_sats)
   2.208 +apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
   2.209 +apply (blast intro: nth_0 nth_ConsI) 
   2.210 +apply (blast intro: nth_0 nth_ConsI, simp_all)
   2.211 +apply (rule bex_iff_sats) 
   2.212 +apply (rule conj_iff_sats)
   2.213 +apply (rule mem_iff_sats)
   2.214 +apply (blast intro: nth_0 nth_ConsI) 
   2.215 +apply (blast intro: nth_0 nth_ConsI, simp_all)
   2.216 +apply (rule pair_iff_sats)
   2.217 +apply (blast intro: nth_0 nth_ConsI) 
   2.218 +apply (blast intro: nth_0 nth_ConsI) 
   2.219 +apply (blast intro: nth_0 nth_ConsI)
   2.220 +apply (simp_all add: succ_Un_distrib [symmetric])
   2.221 +done
   2.222 +
   2.223 +
   2.224 +subsubsection{*Separation for Converse*}
   2.225 +
   2.226 +lemma converse_Reflects:
   2.227 +     "L_Reflects(?Cl, 
   2.228 +        \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
   2.229 +     \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). 
   2.230 +                     pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z)))"
   2.231 +by fast
   2.232 +
   2.233 +lemma converse_separation:
   2.234 +     "L(r) ==> separation(L, 
   2.235 +         \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
   2.236 +apply (rule separation_CollectI) 
   2.237 +apply (rule_tac A="{r,z}" in subset_LsetE, blast ) 
   2.238 +apply (rule ReflectsE [OF converse_Reflects], assumption)
   2.239 +apply (drule subset_Lset_ltD, assumption) 
   2.240 +apply (erule reflection_imp_L_separation)
   2.241 +  apply (simp_all add: lt_Ord2, clarify)
   2.242 +apply (rule DPowI2)
   2.243 +apply (rename_tac u) 
   2.244 +apply (rule bex_iff_sats) 
   2.245 +apply (rule conj_iff_sats)
   2.246 +apply (rule_tac i=0 and j="2" and env="[p,u,r]" in mem_iff_sats, simp_all)
   2.247 +apply (rule bex_iff_sats) 
   2.248 +apply (rule bex_iff_sats) 
   2.249 +apply (rule conj_iff_sats)
   2.250 +apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats, simp_all)
   2.251 +apply (rule pair_iff_sats)
   2.252 +apply (blast intro: nth_0 nth_ConsI) 
   2.253 +apply (blast intro: nth_0 nth_ConsI) 
   2.254 +apply (blast intro: nth_0 nth_ConsI)
   2.255 +apply (simp_all add: succ_Un_distrib [symmetric])
   2.256 +done
   2.257 +
   2.258 +
   2.259 +subsubsection{*Separation for Restriction*}
   2.260 +
   2.261 +lemma restrict_Reflects:
   2.262 +     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
   2.263 +        \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z)))"
   2.264 +by fast
   2.265 +
   2.266 +lemma restrict_separation:
   2.267 +   "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
   2.268 +apply (rule separation_CollectI) 
   2.269 +apply (rule_tac A="{A,z}" in subset_LsetE, blast ) 
   2.270 +apply (rule ReflectsE [OF restrict_Reflects], assumption)
   2.271 +apply (drule subset_Lset_ltD, assumption) 
   2.272 +apply (erule reflection_imp_L_separation)
   2.273 +  apply (simp_all add: lt_Ord2, clarify)
   2.274 +apply (rule DPowI2)
   2.275 +apply (rename_tac u) 
   2.276 +apply (rule bex_iff_sats) 
   2.277 +apply (rule conj_iff_sats)
   2.278 +apply (rule_tac i=0 and j="2" and env="[x,u,A]" in mem_iff_sats, simp_all)
   2.279 +apply (rule bex_iff_sats) 
   2.280 +apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)
   2.281 +apply (simp_all add: succ_Un_distrib [symmetric])
   2.282 +done
   2.283 +
   2.284 +
   2.285 +subsubsection{*Separation for Composition*}
   2.286 +
   2.287 +lemma comp_Reflects:
   2.288 +     "L_Reflects(?Cl, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. 
   2.289 +		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & 
   2.290 +                  xy\<in>s & yz\<in>r,
   2.291 +        \<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i). 
   2.292 +		  pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) & 
   2.293 +                  pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r)"
   2.294 +by fast
   2.295 +
   2.296 +lemma comp_separation:
   2.297 +     "[| L(r); L(s) |]
   2.298 +      ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. 
   2.299 +		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & 
   2.300 +                  xy\<in>s & yz\<in>r)"
   2.301 +apply (rule separation_CollectI) 
   2.302 +apply (rule_tac A="{r,s,z}" in subset_LsetE, blast ) 
   2.303 +apply (rule ReflectsE [OF comp_Reflects], assumption)
   2.304 +apply (drule subset_Lset_ltD, assumption) 
   2.305 +apply (erule reflection_imp_L_separation)
   2.306 +  apply (simp_all add: lt_Ord2, clarify)
   2.307 +apply (rule DPowI2)
   2.308 +apply (rename_tac u) 
   2.309 +apply (rule bex_iff_sats)+
   2.310 +apply (rename_tac x y z)  
   2.311 +apply (rule conj_iff_sats)
   2.312 +apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
   2.313 +apply (blast intro: nth_0 nth_ConsI) 
   2.314 +apply (blast intro: nth_0 nth_ConsI) 
   2.315 +apply (blast intro: nth_0 nth_ConsI, simp_all)
   2.316 +apply (rule bex_iff_sats) 
   2.317 +apply (rule conj_iff_sats)
   2.318 +apply (rule pair_iff_sats)
   2.319 +apply (blast intro: nth_0 nth_ConsI) 
   2.320 +apply (blast intro: nth_0 nth_ConsI) 
   2.321 +apply (blast intro: nth_0 nth_ConsI, simp_all)
   2.322 +apply (rule bex_iff_sats) 
   2.323 +apply (rule conj_iff_sats)
   2.324 +apply (rule pair_iff_sats)
   2.325 +apply (blast intro: nth_0 nth_ConsI) 
   2.326 +apply (blast intro: nth_0 nth_ConsI) 
   2.327 +apply (blast intro: nth_0 nth_ConsI, simp_all) 
   2.328 +apply (rule conj_iff_sats)
   2.329 +apply (rule mem_iff_sats) 
   2.330 +apply (blast intro: nth_0 nth_ConsI) 
   2.331 +apply (blast intro: nth_0 nth_ConsI, simp) 
   2.332 +apply (rule mem_iff_sats) 
   2.333 +apply (blast intro: nth_0 nth_ConsI) 
   2.334 +apply (blast intro: nth_0 nth_ConsI)
   2.335 +apply (simp_all add: succ_Un_distrib [symmetric])
   2.336 +done
   2.337 +
   2.338 +
   2.339 +
   2.340 +
   2.341  end
   2.342  
   2.343  (*
   2.344  
   2.345 -  and cartprod_separation:
   2.346 -     "[| L(A); L(B) |] 
   2.347 -      ==> separation(L, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(L,x,y,z))"
   2.348 -  and image_separation:
   2.349 -     "[| L(A); L(r) |] 
   2.350 -      ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(L,x,y,p)))"
   2.351 -  and vimage_separation:
   2.352 -     "[| L(A); L(r) |] 
   2.353 -      ==> separation(L, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(L,x,y,p)))"
   2.354 -  and converse_separation:
   2.355 -     "L(r) ==> separation(L, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) & 
   2.356 -				     pair(L,x,y,p) & pair(L,y,x,z)))"
   2.357 -  and restrict_separation:
   2.358 -     "L(A) 
   2.359 -      ==> separation(L, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(L,x,y,z)))"
   2.360 -  and comp_separation:
   2.361 -     "[| L(r); L(s) |]
   2.362 -      ==> separation(L, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
   2.363 -			   (\<exists>xy\<in>s. \<exists>yz\<in>r. L(xy) & L(yz) & 
   2.364 -		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz)))"
   2.365    and pred_separation:
   2.366       "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & pair(L,y,x,p))"
   2.367    and Memrel_separation:
     3.1 --- a/src/ZF/Constructible/Relative.thy	Thu Jul 04 16:48:21 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Relative.thy	Thu Jul 04 16:59:54 2002 +0200
     3.3 @@ -9,10 +9,10 @@
     3.4      "empty(M,z) == \<forall>x[M]. x \<notin> z"
     3.5  
     3.6    subset :: "[i=>o,i,i] => o"
     3.7 -    "subset(M,A,B) == \<forall>x\<in>A. M(x) --> x \<in> B"
     3.8 +    "subset(M,A,B) == \<forall>x[M]. x\<in>A --> x \<in> B"
     3.9  
    3.10    upair :: "[i=>o,i,i,i] => o"
    3.11 -    "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x\<in>z. M(x) --> x = a | x = b)"
    3.12 +    "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z --> x = a | x = b)"
    3.13  
    3.14    pair :: "[i=>o,i,i,i] => o"
    3.15      "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & 
    3.16 @@ -34,35 +34,34 @@
    3.17      "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"
    3.18  
    3.19    big_union :: "[i=>o,i,i] => o"
    3.20 -    "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y)"
    3.21 +    "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)"
    3.22  
    3.23    big_inter :: "[i=>o,i,i] => o"
    3.24      "big_inter(M,A,z) == 
    3.25               (A=0 --> z=0) &
    3.26 -	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y)))"
    3.27 +	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y[M]. y\<in>A --> x \<in> y)))"
    3.28  
    3.29    cartprod :: "[i=>o,i,i,i] => o"
    3.30      "cartprod(M,A,B,z) == 
    3.31 -	\<forall>u[M]. u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u)))"
    3.32 +	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
    3.33  
    3.34    is_converse :: "[i=>o,i,i] => o"
    3.35      "is_converse(M,r,z) == 
    3.36  	\<forall>x. M(x) --> 
    3.37              (x \<in> z <-> 
    3.38 -             (\<exists>w\<in>r. M(w) & 
    3.39 -              (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x))))"
    3.40 +             (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x))))"
    3.41  
    3.42    pre_image :: "[i=>o,i,i,i] => o"
    3.43      "pre_image(M,r,A,z) == 
    3.44 -	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y\<in>A. M(y) & pair(M,x,y,w))))"
    3.45 +	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w))))"
    3.46  
    3.47    is_domain :: "[i=>o,i,i] => o"
    3.48      "is_domain(M,r,z) == 
    3.49 -	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y. M(y) & pair(M,x,y,w))))"
    3.50 +	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))"
    3.51  
    3.52    image :: "[i=>o,i,i,i] => o"
    3.53      "image(M,r,A,z) == 
    3.54 -        \<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x\<in>A. M(x) & pair(M,x,y,w))))"
    3.55 +        \<forall>y. M(y) --> (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))"
    3.56  
    3.57    is_range :: "[i=>o,i,i] => o"
    3.58      --{*the cleaner 
    3.59 @@ -70,16 +69,16 @@
    3.60        unfortunately needs an instance of separation in order to prove 
    3.61          @{term "M(converse(r))"}.*}
    3.62      "is_range(M,r,z) == 
    3.63 -	\<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x. M(x) & pair(M,x,y,w))))"
    3.64 +	\<forall>y. M(y) --> (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))"
    3.65  
    3.66    is_field :: "[i=>o,i,i] => o"
    3.67      "is_field(M,r,z) == 
    3.68 -	\<exists>dr. M(dr) & is_domain(M,r,dr) & 
    3.69 -            (\<exists>rr. M(rr) & is_range(M,r,rr) & union(M,dr,rr,z))"
    3.70 +	\<exists>dr[M]. is_domain(M,r,dr) & 
    3.71 +            (\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))"
    3.72  
    3.73    is_relation :: "[i=>o,i] => o"
    3.74      "is_relation(M,r) == 
    3.75 -        (\<forall>z\<in>r. M(z) --> (\<exists>x y. M(x) & M(y) & pair(M,x,y,z)))"
    3.76 +        (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
    3.77  
    3.78    is_function :: "[i=>o,i] => o"
    3.79      "is_function(M,r) == 
    3.80 @@ -713,13 +712,13 @@
    3.81       "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
    3.82    and cartprod_separation:
    3.83       "[| M(A); M(B) |] 
    3.84 -      ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. M(x) & M(y) & pair(M,x,y,z))"
    3.85 +      ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
    3.86    and image_separation:
    3.87       "[| M(A); M(r) |] 
    3.88        ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
    3.89    and converse_separation:
    3.90 -     "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. 
    3.91 -                    M(p) & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
    3.92 +     "M(r) ==> separation(M, 
    3.93 +         \<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
    3.94    and restrict_separation:
    3.95       "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
    3.96    and comp_separation:
    3.97 @@ -728,9 +727,9 @@
    3.98  		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
    3.99                    xy\<in>s & yz\<in>r)"
   3.100    and pred_separation:
   3.101 -     "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & pair(M,y,x,p))"
   3.102 +     "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))"
   3.103    and Memrel_separation:
   3.104 -     "separation(M, \<lambda>z. \<exists>x y. M(x) & M(y) & pair(M,x,y,z) & x \<in> y)"
   3.105 +     "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
   3.106    and obase_separation:
   3.107       --{*part of the order type formalization*}
   3.108       "[| M(A); M(r) |] 
     4.1 --- a/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 16:48:21 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 16:59:54 2002 +0200
     4.3 @@ -192,7 +192,7 @@
     4.4  
     4.5  lemma (in M_axioms) M_Memrel_iff:
     4.6       "M(A) ==> 
     4.7 -      Memrel(A) = {z \<in> A*A. \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> z = \<langle>x,y\<rangle> \<and> x \<in> y)}"
     4.8 +      Memrel(A) = {z \<in> A*A. \<exists>x[M]. \<exists>y[M]. z = \<langle>x,y\<rangle> & x \<in> y}"
     4.9  apply (simp add: Memrel_def) 
    4.10  apply (blast dest: transM)
    4.11  done 
     5.1 --- a/src/ZF/OrdQuant.thy	Thu Jul 04 16:48:21 2002 +0200
     5.2 +++ b/src/ZF/OrdQuant.thy	Thu Jul 04 16:59:54 2002 +0200
     5.3 @@ -10,18 +10,18 @@
     5.4  subsection {*Quantifiers and union operator for ordinals*}
     5.5  
     5.6  constdefs
     5.7 -  
     5.8 +
     5.9    (* Ordinal Quantifiers *)
    5.10    oall :: "[i, i => o] => o"
    5.11      "oall(A, P) == ALL x. x<A --> P(x)"
    5.12 -  
    5.13 +
    5.14    oex :: "[i, i => o] => o"
    5.15      "oex(A, P)  == EX x. x<A & P(x)"
    5.16  
    5.17    (* Ordinal Union *)
    5.18    OUnion :: "[i, i => i] => i"
    5.19      "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
    5.20 -  
    5.21 +
    5.22  syntax
    5.23    "@oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
    5.24    "@oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
    5.25 @@ -42,29 +42,29 @@
    5.26  
    5.27  
    5.28  (*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize
    5.29 -  is proved.  Ord_atomize would convert this rule to 
    5.30 +  is proved.  Ord_atomize would convert this rule to
    5.31      x < 0 ==> P(x) == True, which causes dire effects!*)
    5.32  lemma [simp]: "(ALL x<0. P(x))"
    5.33 -by (simp add: oall_def) 
    5.34 +by (simp add: oall_def)
    5.35  
    5.36  lemma [simp]: "~(EX x<0. P(x))"
    5.37 -by (simp add: oex_def) 
    5.38 +by (simp add: oex_def)
    5.39  
    5.40  lemma [simp]: "(ALL x<succ(i). P(x)) <-> (Ord(i) --> P(i) & (ALL x<i. P(x)))"
    5.41 -apply (simp add: oall_def le_iff) 
    5.42 -apply (blast intro: lt_Ord2) 
    5.43 +apply (simp add: oall_def le_iff)
    5.44 +apply (blast intro: lt_Ord2)
    5.45  done
    5.46  
    5.47  lemma [simp]: "(EX x<succ(i). P(x)) <-> (Ord(i) & (P(i) | (EX x<i. P(x))))"
    5.48 -apply (simp add: oex_def le_iff) 
    5.49 -apply (blast intro: lt_Ord2) 
    5.50 +apply (simp add: oex_def le_iff)
    5.51 +apply (blast intro: lt_Ord2)
    5.52  done
    5.53  
    5.54  (** Union over ordinals **)
    5.55  
    5.56  lemma Ord_OUN [intro,simp]:
    5.57       "[| !!x. x<A ==> Ord(B(x)) |] ==> Ord(\<Union>x<A. B(x))"
    5.58 -by (simp add: OUnion_def ltI Ord_UN) 
    5.59 +by (simp add: OUnion_def ltI Ord_UN)
    5.60  
    5.61  lemma OUN_upper_lt:
    5.62       "[| a<A;  i < b(a);  Ord(\<Union>x<A. b(x)) |] ==> i < (\<Union>x<A. b(x))"
    5.63 @@ -74,7 +74,7 @@
    5.64       "[| a<A;  i\<le>b(a);  Ord(\<Union>x<A. b(x)) |] ==> i \<le> (\<Union>x<A. b(x))"
    5.65  apply (unfold OUnion_def, auto)
    5.66  apply (rule UN_upper_le )
    5.67 -apply (auto simp add: lt_def) 
    5.68 +apply (auto simp add: lt_def)
    5.69  done
    5.70  
    5.71  lemma Limit_OUN_eq: "Limit(i) ==> (UN x<i. x) = i"
    5.72 @@ -97,12 +97,12 @@
    5.73  lemma OUN_UN_eq:
    5.74       "(!!x. x:A ==> Ord(B(x)))
    5.75        ==> (UN z < (UN x:A. B(x)). C(z)) = (UN  x:A. UN z < B(x). C(z))"
    5.76 -by (simp add: OUnion_def) 
    5.77 +by (simp add: OUnion_def)
    5.78  
    5.79  lemma OUN_Union_eq:
    5.80       "(!!x. x:X ==> Ord(x))
    5.81        ==> (UN z < Union(X). C(z)) = (UN x:X. UN z < x. C(z))"
    5.82 -by (simp add: OUnion_def) 
    5.83 +by (simp add: OUnion_def)
    5.84  
    5.85  (*So that rule_format will get rid of ALL x<A...*)
    5.86  lemma atomize_oall [symmetric, rulify]:
    5.87 @@ -113,20 +113,18 @@
    5.88  
    5.89  lemma oallI [intro!]:
    5.90      "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"
    5.91 -by (simp add: oall_def) 
    5.92 +by (simp add: oall_def)
    5.93  
    5.94  lemma ospec: "[| ALL x<A. P(x);  x<A |] ==> P(x)"
    5.95 -by (simp add: oall_def) 
    5.96 +by (simp add: oall_def)
    5.97  
    5.98  lemma oallE:
    5.99      "[| ALL x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q"
   5.100 -apply (simp add: oall_def, blast) 
   5.101 -done
   5.102 +by (simp add: oall_def, blast)
   5.103  
   5.104  lemma rev_oallE [elim]:
   5.105      "[| ALL x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q"
   5.106 -apply (simp add: oall_def, blast)  
   5.107 -done
   5.108 +by (simp add: oall_def, blast)
   5.109  
   5.110  
   5.111  (*Trival rewrite rule;   (ALL x<a.P)<->P holds only if a is not 0!*)
   5.112 @@ -135,7 +133,7 @@
   5.113  
   5.114  (*Congruence rule for rewriting*)
   5.115  lemma oall_cong [cong]:
   5.116 -    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] 
   5.117 +    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |]
   5.118       ==> oall(a, %x. P(x)) <-> oall(a', %x. P'(x))"
   5.119  by (simp add: oall_def)
   5.120  
   5.121 @@ -144,22 +142,22 @@
   5.122  
   5.123  lemma oexI [intro]:
   5.124      "[| P(x);  x<A |] ==> EX x<A. P(x)"
   5.125 -apply (simp add: oex_def, blast) 
   5.126 +apply (simp add: oex_def, blast)
   5.127  done
   5.128  
   5.129  (*Not of the general form for such rules; ~EX has become ALL~ *)
   5.130  lemma oexCI:
   5.131     "[| ALL x<A. ~P(x) ==> P(a);  a<A |] ==> EX x<A. P(x)"
   5.132 -apply (simp add: oex_def, blast) 
   5.133 +apply (simp add: oex_def, blast)
   5.134  done
   5.135  
   5.136  lemma oexE [elim!]:
   5.137      "[| EX x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q |] ==> Q"
   5.138 -apply (simp add: oex_def, blast) 
   5.139 +apply (simp add: oex_def, blast)
   5.140  done
   5.141  
   5.142  lemma oex_cong [cong]:
   5.143 -    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] 
   5.144 +    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |]
   5.145       ==> oex(a, %x. P(x)) <-> oex(a', %x. P'(x))"
   5.146  apply (simp add: oex_def cong add: conj_cong)
   5.147  done
   5.148 @@ -182,11 +180,11 @@
   5.149      "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
   5.150  by (simp add: OUnion_def lt_def OUN_iff)
   5.151  
   5.152 -lemma lt_induct: 
   5.153 +lemma lt_induct:
   5.154      "[| i<k;  !!x.[| x<k;  ALL y<x. P(y) |] ==> P(x) |]  ==>  P(i)"
   5.155  apply (simp add: lt_def oall_def)
   5.156 -apply (erule conjE) 
   5.157 -apply (erule Ord_induct, assumption, blast) 
   5.158 +apply (erule conjE)
   5.159 +apply (erule Ord_induct, assumption, blast)
   5.160  done
   5.161  
   5.162  
   5.163 @@ -211,7 +209,8 @@
   5.164    "ALL x[M]. P"  == "rall(M, %x. P)"
   5.165    "EX x[M]. P"   == "rex(M, %x. P)"
   5.166  
   5.167 -(*** Relativized universal quantifier ***)
   5.168 +
   5.169 +subsubsection{*Relativized universal quantifier*}
   5.170  
   5.171  lemma rallI [intro!]: "[| !!x. M(x) ==> P(x) |] ==> ALL x[M]. P(x)"
   5.172  by (simp add: rall_def)
   5.173 @@ -220,9 +219,9 @@
   5.174  by (simp add: rall_def)
   5.175  
   5.176  (*Instantiates x first: better for automatic theorem proving?*)
   5.177 -lemma rev_rallE [elim]: 
   5.178 +lemma rev_rallE [elim]:
   5.179      "[| ALL x[M]. P(x);  ~ M(x) ==> Q;  P(x) ==> Q |] ==> Q"
   5.180 -by (simp add: rall_def, blast) 
   5.181 +by (simp add: rall_def, blast)
   5.182  
   5.183  lemma rallE: "[| ALL x[M]. P(x);  P(x) ==> Q;  ~ M(x) ==> Q |] ==> Q"
   5.184  by blast
   5.185 @@ -233,11 +232,12 @@
   5.186  
   5.187  (*Congruence rule for rewriting*)
   5.188  lemma rall_cong [cong]:
   5.189 -    "(!!x. M(x) ==> P(x) <-> P'(x)) 
   5.190 +    "(!!x. M(x) ==> P(x) <-> P'(x))
   5.191       ==> rall(M, %x. P(x)) <-> rall(M, %x. P'(x))"
   5.192  by (simp add: rall_def)
   5.193  
   5.194 -(*** Relativized existential quantifier ***)
   5.195 +
   5.196 +subsubsection{*Relativized existential quantifier*}
   5.197  
   5.198  lemma rexI [intro]: "[| P(x); M(x) |] ==> EX x[M]. P(x)"
   5.199  by (simp add: rex_def, blast)
   5.200 @@ -258,7 +258,7 @@
   5.201  by (simp add: rex_def)
   5.202  
   5.203  lemma rex_cong [cong]:
   5.204 -    "(!!x. M(x) ==> P(x) <-> P'(x)) 
   5.205 +    "(!!x. M(x) ==> P(x) <-> P'(x))
   5.206       ==> rex(M, %x. P(x)) <-> rex(M, %x. P'(x))"
   5.207  by (simp add: rex_def cong: conj_cong)
   5.208  
   5.209 @@ -277,7 +277,7 @@
   5.210       "(ALL x[M]. P(x) & Q)   <-> (ALL x[M]. P(x)) & ((ALL x[M]. False) | Q)"
   5.211       "(ALL x[M]. P(x) | Q)   <-> ((ALL x[M]. P(x)) | Q)"
   5.212       "(ALL x[M]. P(x) --> Q) <-> ((EX x[M]. P(x)) --> Q)"
   5.213 -     "(~(ALL x[M]. P(x))) <-> (EX x[M]. ~P(x))" 
   5.214 +     "(~(ALL x[M]. P(x))) <-> (EX x[M]. ~P(x))"
   5.215  by blast+
   5.216  
   5.217  lemma rall_simps2:
   5.218 @@ -312,7 +312,7 @@
   5.219  by blast
   5.220  
   5.221  
   5.222 -(** One-point rule for bounded quantifiers: see HOL/Set.ML **)
   5.223 +subsubsection{*One-point rule for bounded quantifiers*}
   5.224  
   5.225  lemma rex_triv_one_point1 [simp]: "(EX x[M]. x=a) <-> ( M(a))"
   5.226  by blast
   5.227 @@ -333,6 +333,20 @@
   5.228  by blast
   5.229  
   5.230  
   5.231 +subsubsection{*Sets as Classes*}
   5.232 +
   5.233 +constdefs setclass :: "[i,i] => o"       ("**_")
   5.234 +   "setclass(A,x) == x : A"
   5.235 +
   5.236 +declare setclass_def [simp]
   5.237 +
   5.238 +lemma rall_setclass_is_ball [simp]: "(\<forall>x[**A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
   5.239 +by auto
   5.240 +
   5.241 +lemma rex_setclass_is_bex [simp]: "(\<exists>x[**A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
   5.242 +by auto
   5.243 +
   5.244 +
   5.245  ML
   5.246  {*
   5.247  val oall_def = thm "oall_def"
   5.248 @@ -370,7 +384,7 @@
   5.249  
   5.250  val Ord_atomize =
   5.251      atomize ([("OrdQuant.oall", [ospec]),("OrdQuant.rall", [rspec])]@
   5.252 -                 ZF_conn_pairs, 
   5.253 +                 ZF_conn_pairs,
   5.254               ZF_mem_pairs);
   5.255  simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
   5.256  *}
   5.257 @@ -391,7 +405,7 @@
   5.258  val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
   5.259                                   ("ALL x[M]. P(x) --> Q(x)", FOLogic.oT)
   5.260  
   5.261 -val prove_rall_tac = rewtac rall_def THEN 
   5.262 +val prove_rall_tac = rewtac rall_def THEN
   5.263                       Quantifier1.prove_one_point_all_tac;
   5.264  
   5.265  val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;