author paulson Thu, 25 Jul 2002 18:29:04 +0200 changeset 13423 7ec771711c09 parent 13422 af9bc8d87a75 child 13424 584a4a4c30ed
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 (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 (elim disjE exE)
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)"
+
+lemma triv_Relativize2:
+     "Relativize2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
+

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 (rule iffI)
prefer 2 apply (simp add: lam_def)
apply (rule M_equalityI)
@@ -653,6 +685,13 @@
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')"
+
lemma (in M_triv_axioms) image_abs [simp]:
"[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
@@ -722,25 +761,6 @@

-subsection {*Absoluteness for Booleans*}
-
-lemma (in M_triv_axioms) bool_of_o_closed:
-     "M(bool_of_o(P))"
-
-lemma (in M_triv_axioms) and_closed:
-     "[| M(p); M(q) |] ==> M(p and q)"
-
-lemma (in M_triv_axioms) or_closed:
-     "[| M(p); M(q) |] ==> M(p or q)"
-
-lemma (in M_triv_axioms) not_closed:
-     "M(p) ==> M(not(p))"
-
-
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)"
+
+
+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))"
+
+lemma (in M_triv_axioms) and_closed [intro,simp]:
+     "[| M(p); M(q) |] ==> M(p and q)"