More lemmas, working towards relativization of "satisfies"

--- a/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 25 10:56:35 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 25 18:29:04 2002 +0200
@@ -400,6 +400,9 @@
                list_replacement2' relativize1_def
                iterates_closed [of "is_list_functor(M,A)"])
 
+text{*WARNING: use only with @{text "dest:"} or with variables fixed!*}
+lemmas (in M_datatypes) list_into_M = transM [OF _ list_closed]
+
 lemma (in M_datatypes) list_N_abs [simp]:
      "[|M(A); n\<in>nat; M(Z)|] 
       ==> is_list_N(M,A,n,Z) <-> Z = list_N(A,n)"
@@ -446,6 +449,8 @@
                   iterates_closed [of "is_formula_functor(M)"])
 done
 
+lemmas (in M_datatypes) formula_into_M = transM [OF _ formula_closed]
+
 lemma (in M_datatypes) is_formula_n_abs [simp]:
      "[|n\<in>nat; M(Z)|] 
       ==> is_formula_n(M,n,Z) <-> 
@@ -718,6 +723,32 @@
 
 subsection {*Absoluteness for @{term formula_rec}*}
 
+subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
+
+constdefs
+
+ is_formula_case :: 
+    "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
+  --{*no constraint on non-formulas*}
+  "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == 
+      (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Member(M,x,y,p) --> is_a(x,y,z)) &
+      (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Equal(M,x,y,p) --> is_b(x,y,z)) &
+      (\<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> 
+                     is_Nand(M,x,y,p) --> is_c(x,y,z)) &
+      (\<forall>x[M]. x\<in>formula --> is_Forall(M,x,p) --> is_d(x,z))"
+
+lemma (in M_datatypes) formula_case_abs [simp]: 
+     "[| Relativize2(M,nat,nat,is_a,a); Relativize2(M,nat,nat,is_b,b); 
+         Relativize2(M,formula,formula,is_c,c); Relativize1(M,formula,is_d,d); 
+         p \<in> formula; M(z) |] 
+      ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <-> 
+          z = formula_case(a,b,c,d,p)"
+apply (simp add: formula_into_M is_formula_case_def)
+apply (erule formula.cases) 
+   apply (simp_all add: Relativize1_def Relativize2_def) 
+done
+
+
 subsubsection{*@{term quasiformula}: For Case-Splitting with @{term formula_case'}*}
 
 constdefs
@@ -762,10 +793,10 @@
     "formula_case'(a,b,c,d,p) == 
        if quasiformula(p) then formula_case(a,b,c,d,p) else 0"  
 
-  is_formula_case :: 
+  is_formula_case' :: 
       "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
     --{*Returns 0 for non-formulas*}
-    "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == 
+    "is_formula_case'(M, is_a, is_b, is_c, is_d, p, z) == 
 	(\<forall>x[M]. \<forall>y[M]. is_Member(M,x,y,p) --> is_a(x,y,z)) &
 	(\<forall>x[M]. \<forall>y[M]. is_Equal(M,x,y,p) --> is_b(x,y,z)) &
 	(\<forall>x[M]. \<forall>y[M]. is_Nand(M,x,y,p) --> is_c(x,y,z)) &
@@ -818,16 +849,16 @@
      \<forall>x[M]. x\<in>formula --> M(d(x))|] ==> M(formula_case(a,b,c,d,p))"
 by (erule formula.cases, simp_all) 
 
-lemma (in M_triv_axioms) formula_case_abs [simp]: 
+lemma (in M_triv_axioms) formula_case'_abs [simp]: 
      "[| relativize2(M,is_a,a); relativize2(M,is_b,b); 
          relativize2(M,is_c,c); relativize1(M,is_d,d); M(p); M(z) |] 
-      ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <-> 
+      ==> is_formula_case'(M,is_a,is_b,is_c,is_d,p,z) <-> 
           z = formula_case'(a,b,c,d,p)"
 apply (case_tac "quasiformula(p)") 
  prefer 2 
- apply (simp add: is_formula_case_def non_formula_case) 
+ apply (simp add: is_formula_case'_def non_formula_case) 
  apply (force simp add: quasiformula_def) 
-apply (simp add: quasiformula_def is_formula_case_def)
+apply (simp add: quasiformula_def is_formula_case'_def)
 apply (elim disjE exE) 
  apply (simp_all add: relativize1_def relativize2_def) 
 done

--- a/src/ZF/Constructible/Relative.thy	Thu Jul 25 10:56:35 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Thu Jul 25 18:29:04 2002 +0200
@@ -2,6 +2,10 @@
 
 theory Relative = Main:
 
+(*????????????????for IFOL.thy????????????????*)
+lemma eq_commute: "a=b <-> b=a"
+by blast 
+
 subsection{* Relativized versions of standard set-theoretic concepts *}
 
 constdefs
@@ -188,13 +192,41 @@
   relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o"
     "relativize1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
 
+  Relativize1 :: "[i=>o, i, [i,i]=>o, i=>i] => o"
+    --{*as above, but typed*}
+    "Relativize1(M,A,is_f,f) == 
+        \<forall>x[M]. \<forall>y[M]. x\<in>A --> is_f(x,y) <-> y = f(x)"
+
   relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
     "relativize2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
 
+  Relativize2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o"
+    "Relativize2(M,A,B,is_f,f) ==
+        \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. x\<in>A --> y\<in>B --> is_f(x,y,z) <-> z = f(x,y)"
+
   relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
     "relativize3(M,is_f,f) == 
        \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
 
+  Relativize3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o"
+    "Relativize3(M,A,B,C,is_f,f) == 
+       \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. 
+         x\<in>A --> y\<in>B --> z\<in>C --> is_f(x,y,z,u) <-> u = f(x,y,z)"
+
+  relativize4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o"
+    "relativize4(M,is_f,f) == 
+       \<forall>u[M]. \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>a[M]. is_f(u,x,y,z,a) <-> a = f(u,x,y,z)"
+
+
+text{*Useful when absoluteness reasoning has replaced the predicates by terms*}
+lemma triv_Relativize1:
+     "Relativize1(M, A, \<lambda>x y. y = f(x), f)"
+by (simp add: Relativize1_def) 
+
+lemma triv_Relativize2:
+     "Relativize2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
+by (simp add: Relativize2_def) 
+
 
 subsection {*The relativized ZF axioms*}
 constdefs
@@ -643,9 +675,9 @@
 
 lemma (in M_triv_axioms) lambda_abs2 [simp]: 
      "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
-         relativize1(M,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |] 
+         Relativize1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |] 
       ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
-apply (simp add: relativize1_def is_lambda_def)
+apply (simp add: Relativize1_def is_lambda_def)
 apply (rule iffI)
  prefer 2 apply (simp add: lam_def) 
 apply (rule M_equalityI)
@@ -653,6 +685,13 @@
  apply (simp add: lam_closed2)+
 done
 
+lemma is_lambda_cong [cong]:
+     "[| A=A';  z=z'; 
+         !!x y. [| x\<in>A; M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |] 
+      ==> is_lambda(M, A, %x y. is_b(x,y), z) <-> 
+          is_lambda(M, A', %x y. is_b'(x,y), z')" 
+by (simp add: is_lambda_def) 
+
 lemma (in M_triv_axioms) image_abs [simp]: 
      "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
 apply (simp add: image_def)
@@ -722,25 +761,6 @@
 by (simp add: Inr_def)
 
 
-subsection {*Absoluteness for Booleans*}
-
-lemma (in M_triv_axioms) bool_of_o_closed:
-     "M(bool_of_o(P))"
-by (simp add: bool_of_o_def) 
-
-lemma (in M_triv_axioms) and_closed:
-     "[| M(p); M(q) |] ==> M(p and q)"
-by (simp add: and_def cond_def) 
-
-lemma (in M_triv_axioms) or_closed:
-     "[| M(p); M(q) |] ==> M(p or q)"
-by (simp add: or_def cond_def) 
-
-lemma (in M_triv_axioms) not_closed:
-     "M(p) ==> M(not(p))"
-by (simp add: Bool.not_def cond_def) 
-
-
 subsection{*Absoluteness for Ordinals*}
 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
 
@@ -1228,6 +1248,59 @@
 done
 
 
+subsection{*Relativization and Absoluteness for Boolean Operators*}
+
+constdefs
+  is_bool_of_o :: "[i=>o, o, i] => o"
+   "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))"
+
+  is_not :: "[i=>o, i, i] => o"
+   "is_not(M,a,z) == (number1(M,a)  & empty(M,z)) | 
+                     (~number1(M,a) & number1(M,z))"
+
+  is_and :: "[i=>o, i, i, i] => o"
+   "is_and(M,a,b,z) == (number1(M,a)  & z=b) | 
+                       (~number1(M,a) & empty(M,z))"
+
+  is_or :: "[i=>o, i, i, i] => o"
+   "is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) | 
+                      (~number1(M,a) & z=b)"
+
+lemma (in M_triv_axioms) bool_of_o_abs [simp]: 
+     "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)" 
+by (simp add: is_bool_of_o_def bool_of_o_def) 
+
+
+lemma (in M_triv_axioms) not_abs [simp]: 
+     "[| M(a); M(z)|] ==> is_not(M,a,z) <-> z = not(a)"
+by (simp add: Bool.not_def cond_def is_not_def) 
+
+lemma (in M_triv_axioms) and_abs [simp]: 
+     "[| M(a); M(b); M(z)|] ==> is_and(M,a,b,z) <-> z = a and b"
+by (simp add: Bool.and_def cond_def is_and_def) 
+
+lemma (in M_triv_axioms) or_abs [simp]: 
+     "[| M(a); M(b); M(z)|] ==> is_or(M,a,b,z) <-> z = a or b"
+by (simp add: Bool.or_def cond_def is_or_def)
+
+
+lemma (in M_triv_axioms) bool_of_o_closed [intro,simp]:
+     "M(bool_of_o(P))"
+by (simp add: bool_of_o_def) 
+
+lemma (in M_triv_axioms) and_closed [intro,simp]:
+     "[| M(p); M(q) |] ==> M(p and q)"
+by (simp add: and_def cond_def) 
+
+lemma (in M_triv_axioms) or_closed [intro,simp]:
+     "[| M(p); M(q) |] ==> M(p or q)"
+by (simp add: or_def cond_def) 
+
+lemma (in M_triv_axioms) not_closed [intro,simp]:
+     "M(p) ==> M(not(p))"
+by (simp add: Bool.not_def cond_def) 
+
+
 subsection{*Relativization and Absoluteness for List Operators*}
 
 constdefs