towards proving separation for L

--- a/src/ZF/Constructible/Formula.thy	Thu Jul 04 10:51:52 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy	Thu Jul 04 10:52:33 2002 +0200
@@ -2,8 +2,10 @@
 
 theory Formula = Main:
 
-(*Internalized formulas of FOL. De Bruijn representation. 
-  Unbound variables get their denotations from an environment.*)
+subsection{*Internalized formulas of FOL*}
+
+text{*De Bruijn representation.
+  Unbound variables get their denotations from an environment.*}
 
 consts   formula :: i
 datatype
@@ -21,6 +23,9 @@
 constdefs Implies :: "[i,i]=>i"
     "Implies(p,q) == Neg(And(p,Neg(q)))"
 
+constdefs Iff :: "[i,i]=>i"
+    "Iff(p,q) == And(Implies(p,q), Implies(q,p))"
+
 constdefs Exists :: "i=>i"
     "Exists(p) == Neg(Forall(Neg(p)))";
 
@@ -31,6 +36,10 @@
      "[| p \<in> formula; q \<in> formula |] ==> Implies(p,q) \<in> formula"
 by (simp add: Implies_def) 
 
+lemma Iff_type [TC]:
+     "[| p \<in> formula; q \<in> formula |] ==> Iff(p,q) \<in> formula"
+by (simp add: Iff_def) 
+
 lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"
 by (simp add: Exists_def) 
 
@@ -86,7 +95,7 @@
 
 declare satisfies.simps [simp del]; 
 
-(**** DIVIDING LINE BETWEEN PRIMITIVE AND DERIVED CONNECTIVES ****)
+subsubsection{*Dividing line between primitive and derived connectives*}
 
 lemma sats_Or_iff [simp]:
   "env \<in> list(A) 
@@ -96,8 +105,12 @@
 lemma sats_Implies_iff [simp]:
   "env \<in> list(A) 
    ==> (sats(A, Implies(p,q), env)) <-> (sats(A,p,env) --> sats(A,q,env))"
-apply (simp add: Implies_def, blast) 
-done
+by (simp add: Implies_def, blast) 
+
+lemma sats_Iff_iff [simp]:
+  "env \<in> list(A) 
+   ==> (sats(A, Iff(p,q), env)) <-> (sats(A,p,env) <-> sats(A,q,env))"
+by (simp add: Iff_def, blast) 
 
 lemma sats_Exists_iff [simp]:
   "env \<in> list(A) 
@@ -105,6 +118,48 @@
 by (simp add: Exists_def)
 
 
+subsubsection{*Derived rules to help build up formulas*}
+
+lemma mem_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
+       ==> (x\<in>y) <-> sats(A, Member(i,j), env)" 
+by (simp add: satisfies.simps)
+
+lemma conj_iff_sats:
+      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
+       ==> (P & Q) <-> sats(A, And(p,q), env)"
+by (simp add: sats_And_iff)
+
+lemma disj_iff_sats:
+      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
+       ==> (P | Q) <-> sats(A, Or(p,q), env)"
+by (simp add: sats_Or_iff)
+
+lemma imp_iff_sats:
+      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
+       ==> (P --> Q) <-> sats(A, Implies(p,q), env)"
+by (simp add: sats_Forall_iff) 
+
+lemma iff_iff_sats:
+      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
+       ==> (P <-> Q) <-> sats(A, Iff(p,q), env)"
+by (simp add: sats_Forall_iff) 
+
+lemma imp_iff_sats:
+      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
+       ==> (P --> Q) <-> sats(A, Implies(p,q), env)"
+by (simp add: sats_Forall_iff) 
+
+lemma ball_iff_sats:
+      "[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|]
+       ==> (\<forall>x\<in>A. P(x)) <-> sats(A, Forall(p), env)"
+by (simp add: sats_Forall_iff) 
+
+lemma bex_iff_sats:
+      "[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|]
+       ==> (\<exists>x\<in>A. P(x)) <-> sats(A, Exists(p), env)"
+by (simp add: sats_Exists_iff) 
+
 
 
 (*pretty but unnecessary
@@ -220,6 +275,9 @@
 lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
 by (simp add: Implies_def) 
 
+lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"
+by (simp add: Iff_def, blast)
+
 lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))"
 by (simp add: Exists_def) 
 
@@ -354,11 +412,17 @@
                  X = {x\<in>A. sats(A, p, Cons(x,env))}}"
 
 lemma DPowI:
-  "[|X <= A;  env \<in> list(A);  p \<in> formula; 
-     arity(p) \<le> succ(length(env))|]
+  "[|env \<in> list(A);  p \<in> formula;  arity(p) \<le> succ(length(env))|]
    ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
 by (simp add: DPow_def, blast) 
 
+text{*With this rule we can specify @{term p} later.*}
+lemma DPowI2 [rule_format]:
+  "[|\<forall>x\<in>A. P(x) <-> sats(A, p, Cons(x,env));
+     env \<in> list(A);  p \<in> formula;  arity(p) \<le> succ(length(env))|]
+   ==> {x\<in>A. P(x)} \<in> DPow(A)"
+by (simp add: DPow_def, blast) 
+
 lemma DPowD:
   "X \<in> DPow(A) 
    ==> X <= A &
@@ -500,6 +564,11 @@
 apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow)
 done
 
+lemma mem_Lset_imp_subset_Lset: "a \<in> Lset(i) ==> a \<subseteq> Lset(i)"
+apply (insert Transset_Lset) 
+apply (simp add: Transset_def) 
+done
+
 subsubsection{* Monotonicity *}
 
 text{*Kunen's VI, 1.6 (b)*}
@@ -521,6 +590,10 @@
 apply (blast intro: elem_subset_in_DPow dest: LsetD DPowD) 
 done
 
+text{*Useful with Reflection to bump up the ordinal*}
+lemma subset_Lset_ltD: "[|A \<subseteq> Lset(i); i < j|] ==> A \<subseteq> Lset(j)"
+by (blast dest: ltD [THEN Lset_mono_mem]) 
+
 subsubsection{* 0, successor and limit equations fof Lset *}
 
 lemma Lset_0 [simp]: "Lset(0) = 0"
@@ -880,6 +953,17 @@
 apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow) 
 done
 
+text{*Every set of constructible sets is included in some @{term Lset}*} 
+lemma subset_Lset:
+     "(\<forall>x\<in>A. L(x)) ==> \<exists>i. Ord(i) & A \<subseteq> Lset(i)"
+by (rule_tac x = "\<Union>x\<in>A. succ(lrank(x))" in exI, force)
+
+lemma subset_LsetE:
+     "[|\<forall>x\<in>A. L(x);
+        !!i. [|Ord(i); A \<subseteq> Lset(i)|] ==> P|]
+      ==> P"
+by (blast dest: subset_Lset) 
+
 subsection{*For L to satisfy the ZF axioms*}
 
 theorem Union_in_L: "L(X) ==> L(Union(X))"

--- a/src/ZF/Constructible/L_axioms.thy	Thu Jul 04 10:51:52 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Thu Jul 04 10:52:33 2002 +0200
@@ -67,12 +67,231 @@
 apply (simp add: Replace_iff univalent_def, blast) 
 done
 
+subsection{*Instantiation of the locale @{text M_triv_axioms}*}
+
+lemma Lset_mono_le: "mono_le_subset(Lset)"
+by (simp add: mono_le_subset_def le_imp_subset Lset_mono) 
+
+lemma Lset_cont: "cont_Ord(Lset)"
+by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord) 
+
+lemmas Pair_in_Lset = Formula.Pair_in_LLimit;
+
+lemmas L_nat = Ord_in_L [OF Ord_nat];
+
+ML
+{*
+val transL = thm "transL";
+val nonempty = thm "nonempty";
+val upair_ax = thm "upair_ax";
+val Union_ax = thm "Union_ax";
+val power_ax = thm "power_ax";
+val replacement = thm "replacement";
+val L_nat = thm "L_nat";
+
+fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st);
+
+fun trivaxL th =
+    kill_flex_triv_prems 
+       ([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat] 
+        MRS (inst "M" "L" th));
+
+bind_thm ("ball_abs", trivaxL (thm "M_triv_axioms.ball_abs"));
+bind_thm ("rall_abs", trivaxL (thm "M_triv_axioms.rall_abs"));
+bind_thm ("bex_abs", trivaxL (thm "M_triv_axioms.bex_abs"));
+bind_thm ("rex_abs", trivaxL (thm "M_triv_axioms.rex_abs"));
+bind_thm ("ball_iff_equiv", trivaxL (thm "M_triv_axioms.ball_iff_equiv"));
+bind_thm ("M_equalityI", trivaxL (thm "M_triv_axioms.M_equalityI"));
+bind_thm ("empty_abs", trivaxL (thm "M_triv_axioms.empty_abs"));
+bind_thm ("subset_abs", trivaxL (thm "M_triv_axioms.subset_abs"));
+bind_thm ("upair_abs", trivaxL (thm "M_triv_axioms.upair_abs"));
+bind_thm ("upair_in_M_iff", trivaxL (thm "M_triv_axioms.upair_in_M_iff"));
+bind_thm ("singleton_in_M_iff", trivaxL (thm "M_triv_axioms.singleton_in_M_iff"));
+bind_thm ("pair_abs", trivaxL (thm "M_triv_axioms.pair_abs"));
+bind_thm ("pair_in_M_iff", trivaxL (thm "M_triv_axioms.pair_in_M_iff"));
+bind_thm ("pair_components_in_M", trivaxL (thm "M_triv_axioms.pair_components_in_M"));
+bind_thm ("cartprod_abs", trivaxL (thm "M_triv_axioms.cartprod_abs"));
+bind_thm ("union_abs", trivaxL (thm "M_triv_axioms.union_abs"));
+bind_thm ("inter_abs", trivaxL (thm "M_triv_axioms.inter_abs"));
+bind_thm ("setdiff_abs", trivaxL (thm "M_triv_axioms.setdiff_abs"));
+bind_thm ("Union_abs", trivaxL (thm "M_triv_axioms.Union_abs"));
+bind_thm ("Union_closed", trivaxL (thm "M_triv_axioms.Union_closed"));
+bind_thm ("Un_closed", trivaxL (thm "M_triv_axioms.Un_closed"));
+bind_thm ("cons_closed", trivaxL (thm "M_triv_axioms.cons_closed"));
+bind_thm ("successor_abs", trivaxL (thm "M_triv_axioms.successor_abs"));
+bind_thm ("succ_in_M_iff", trivaxL (thm "M_triv_axioms.succ_in_M_iff"));
+bind_thm ("separation_closed", trivaxL (thm "M_triv_axioms.separation_closed"));
+bind_thm ("strong_replacementI", trivaxL (thm "M_triv_axioms.strong_replacementI"));
+bind_thm ("strong_replacement_closed", trivaxL (thm "M_triv_axioms.strong_replacement_closed"));
+bind_thm ("RepFun_closed", trivaxL (thm "M_triv_axioms.RepFun_closed"));
+bind_thm ("lam_closed", trivaxL (thm "M_triv_axioms.lam_closed"));
+bind_thm ("image_abs", trivaxL (thm "M_triv_axioms.image_abs"));
+bind_thm ("powerset_Pow", trivaxL (thm "M_triv_axioms.powerset_Pow"));
+bind_thm ("powerset_imp_subset_Pow", trivaxL (thm "M_triv_axioms.powerset_imp_subset_Pow"));
+bind_thm ("nat_into_M", trivaxL (thm "M_triv_axioms.nat_into_M"));
+bind_thm ("nat_case_closed", trivaxL (thm "M_triv_axioms.nat_case_closed"));
+bind_thm ("Inl_in_M_iff", trivaxL (thm "M_triv_axioms.Inl_in_M_iff"));
+bind_thm ("Inr_in_M_iff", trivaxL (thm "M_triv_axioms.Inr_in_M_iff"));
+bind_thm ("lt_closed", trivaxL (thm "M_triv_axioms.lt_closed"));
+bind_thm ("transitive_set_abs", trivaxL (thm "M_triv_axioms.transitive_set_abs"));
+bind_thm ("ordinal_abs", trivaxL (thm "M_triv_axioms.ordinal_abs"));
+bind_thm ("limit_ordinal_abs", trivaxL (thm "M_triv_axioms.limit_ordinal_abs"));
+bind_thm ("successor_ordinal_abs", trivaxL (thm "M_triv_axioms.successor_ordinal_abs"));
+bind_thm ("finite_ordinal_abs", trivaxL (thm "M_triv_axioms.finite_ordinal_abs"));
+bind_thm ("omega_abs", trivaxL (thm "M_triv_axioms.omega_abs"));
+bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
+bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
+bind_thm ("number3_abs", trivaxL (thm "M_triv_axioms.number3_abs"));
+*}
+
+declare ball_abs [simp] 
+declare rall_abs [simp] 
+declare bex_abs [simp] 
+declare rex_abs [simp] 
+declare empty_abs [simp] 
+declare subset_abs [simp] 
+declare upair_abs [simp] 
+declare upair_in_M_iff [iff]
+declare singleton_in_M_iff [iff]
+declare pair_abs [simp] 
+declare pair_in_M_iff [iff]
+declare cartprod_abs [simp] 
+declare union_abs [simp] 
+declare inter_abs [simp] 
+declare setdiff_abs [simp] 
+declare Union_abs [simp] 
+declare Union_closed [intro,simp]
+declare Un_closed [intro,simp]
+declare cons_closed [intro,simp]
+declare successor_abs [simp] 
+declare succ_in_M_iff [iff]
+declare separation_closed [intro,simp]
+declare strong_replacementI [rule_format]
+declare strong_replacement_closed [intro,simp]
+declare RepFun_closed [intro,simp]
+declare lam_closed [intro,simp]
+declare image_abs [simp] 
+declare nat_into_M [intro]
+declare Inl_in_M_iff [iff]
+declare Inr_in_M_iff [iff]
+declare transitive_set_abs [simp] 
+declare ordinal_abs [simp] 
+declare limit_ordinal_abs [simp] 
+declare successor_ordinal_abs [simp] 
+declare finite_ordinal_abs [simp] 
+declare omega_abs [simp] 
+declare number1_abs [simp] 
+declare number1_abs [simp] 
+declare number3_abs [simp]
+
+
+subsection{*Instantiation of the locale @{text reflection}*}
+
+text{*instances of locale constants*}
+constdefs
+  L_Reflects :: "[i=>o,i=>o,[i,i]=>o] => o"
+    "L_Reflects(Cl,P,Q) == Closed_Unbounded(Cl) &
+                           (\<forall>a. Cl(a) --> (\<forall>x \<in> Lset(a). P(x) <-> Q(a,x)))"
+
+  L_F0 :: "[i=>o,i] => i"
+    "L_F0(P,y) == \<mu>b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"
+
+  L_FF :: "[i=>o,i] => i"
+    "L_FF(P)   == \<lambda>a. \<Union>y\<in>Lset(a). L_F0(P,y)"
+
+  L_ClEx :: "[i=>o,i] => o"
+    "L_ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(L_FF(P),a) = a"
+
+theorem Triv_reflection [intro]:
+     "L_Reflects(Ord, P, \<lambda>a x. P(x))"
+by (simp add: L_Reflects_def)
+
+theorem Not_reflection [intro]:
+     "L_Reflects(Cl,P,Q) ==> L_Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
+by (simp add: L_Reflects_def) 
+
+theorem And_reflection [intro]:
+     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
+      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<and> P'(x), 
+                                      \<lambda>a x. Q(a,x) \<and> Q'(a,x))"
+by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
+
+theorem Or_reflection [intro]:
+     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
+      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<or> P'(x), 
+                                      \<lambda>a x. Q(a,x) \<or> Q'(a,x))"
+by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
+
+theorem Imp_reflection [intro]:
+     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
+      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
+                   \<lambda>x. P(x) --> P'(x), 
+                   \<lambda>a x. Q(a,x) --> Q'(a,x))"
+by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
+
+theorem Iff_reflection [intro]:
+     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
+      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
+                   \<lambda>x. P(x) <-> P'(x), 
+                   \<lambda>a x. Q(a,x) <-> Q'(a,x))"
+by (simp add: L_Reflects_def Closed_Unbounded_Int, blast) 
+
+
+theorem Ex_reflection [intro]:
+     "L_Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
+      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
+                   \<lambda>x. \<exists>z. L(z) \<and> P(x,z), 
+                   \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z))"
+apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
+apply (rule reflection.Ex_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],
+       assumption+)
+done
+
+theorem All_reflection [intro]:
+     "L_Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
+      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
+                   \<lambda>x. \<forall>z. L(z) --> P(x,z), 
+                   \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z))" 
+apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
+apply (rule reflection.All_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],
+       assumption+)
+done
+
+theorem Rex_reflection [intro]:
+     "L_Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
+      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
+                   \<lambda>x. \<exists>z[L]. P(x,z), 
+                   \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z))"
+by (unfold rex_def, blast) 
+
+theorem Rall_reflection [intro]:
+     "L_Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
+      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
+                   \<lambda>x. \<forall>z[L]. P(x,z), 
+                   \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z))" 
+by (unfold rall_def, blast) 
+
+lemma ReflectsD:
+     "[|L_Reflects(Cl,P,Q); Ord(i)|] 
+      ==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) <-> Q(j,x))"
+apply (simp add: L_Reflects_def Closed_Unbounded_def, clarify)
+apply (blast dest!: UnboundedD) 
+done
+
+lemma ReflectsE:
+     "[| L_Reflects(Cl,P,Q); Ord(i);
+         !!j. [|i<j;  \<forall>x \<in> Lset(j). P(x) <-> Q(j,x)|] ==> R |]
+      ==> R"
+by (blast dest!: ReflectsD) 
+
+lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B";
+by blast
+
+
 end
 
 (*
 
-  and Inter_separation:
-     "L(A) ==> separation(L, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
   and cartprod_separation:
      "[| L(A); L(B) |] 
       ==> separation(L, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(L,x,y,z))"