author paulson Thu Jul 04 16:59:54 2002 +0200 (2002-07-04) changeset 13298 b4f370679c65 parent 13297 e4ae0732e2be child 13299 3a932abf97e8
Constructible: some separation axioms
 src/ZF/Constructible/Formula.thy file | annotate | diff | revisions src/ZF/Constructible/L_axioms.thy file | annotate | diff | revisions src/ZF/Constructible/Relative.thy file | annotate | diff | revisions src/ZF/Constructible/Wellorderings.thy file | annotate | diff | revisions src/ZF/OrdQuant.thy file | annotate | diff | revisions
```     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.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.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.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.38 -
1.39 -lemma [simp]: "(A |= And(p,q)) <-> A|=p & A|=q"
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.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.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.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.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.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.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.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.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.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.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.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.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.35
5.36  lemma [simp]: "~(EX x<0. P(x))"
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.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.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.93
5.94  lemma ospec: "[| ALL x<A. P(x);  x<A |] ==> P(x)"
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.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.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.173 @@ -220,9 +219,9 @@
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.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.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;
```