--- a/src/ZF/Constructible/Satisfies_absolute.thy Tue Sep 03 18:43:15 2002 +0200
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Tue Sep 03 18:49:10 2002 +0200
@@ -171,122 +171,6 @@
-subsection {*Absoluteness for @{term formula_rec}*}
-
-constdefs
-
- formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
- --{* the instance of @{term formula_case} in @{term formula_rec}*}
- "formula_rec_case(a,b,c,d,h) ==
- formula_case (a, b,
- \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u,
- h ` succ(depth(v)) ` v),
- \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
-
- is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
- --{* predicate to relativize the functional @{term formula_rec}*}
- "is_formula_rec(M,MH,p,z) ==
- \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
- successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
-
-text{*Unfold @{term formula_rec} to @{term formula_rec_case}*}
-lemma (in M_triv_axioms) formula_rec_eq2:
- "p \<in> formula ==>
- formula_rec(a,b,c,d,p) =
- transrec (succ(depth(p)),
- \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
-by (simp add: formula_rec_eq formula_rec_case_def)
-
-
-text{*Sufficient conditions to relative the instance of @{term formula_case}
- in @{term formula_rec}*}
-lemma (in M_datatypes) Relativize1_formula_rec_case:
- "[|Relativize2(M, nat, nat, is_a, a);
- Relativize2(M, nat, nat, is_b, b);
- Relativize2 (M, formula, formula,
- is_c, \<lambda>u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v));
- Relativize1(M, formula,
- is_d, \<lambda>u. d(u, h ` succ(depth(u)) ` u));
- M(h) |]
- ==> Relativize1(M, formula,
- is_formula_case (M, is_a, is_b, is_c, is_d),
- formula_rec_case(a, b, c, d, h))"
-apply (simp (no_asm) add: formula_rec_case_def Relativize1_def)
-apply (simp add: formula_case_abs)
-done
-
-
-text{*This locale packages the premises of the following theorems,
- which is the normal purpose of locales. It doesn't accumulate
- constraints on the class @{term M}, as in most of this deveopment.*}
-locale Formula_Rec = M_eclose +
- fixes a and is_a and b and is_b and c and is_c and d and is_d and MH
- defines
- "MH(u::i,f,z) ==
- \<forall>fml[M]. is_formula(M,fml) -->
- is_lambda
- (M, fml, is_formula_case (M, is_a, is_b, is_c(f), is_d(f)), z)"
-
- assumes a_closed: "[|x\<in>nat; y\<in>nat|] ==> M(a(x,y))"
- and a_rel: "Relativize2(M, nat, nat, is_a, a)"
- and b_closed: "[|x\<in>nat; y\<in>nat|] ==> M(b(x,y))"
- and b_rel: "Relativize2(M, nat, nat, is_b, b)"
- and c_closed: "[|x \<in> formula; y \<in> formula; M(gx); M(gy)|]
- ==> M(c(x, y, gx, gy))"
- and c_rel:
- "M(f) ==>
- Relativize2 (M, formula, formula, is_c(f),
- \<lambda>u v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))"
- and d_closed: "[|x \<in> formula; M(gx)|] ==> M(d(x, gx))"
- and d_rel:
- "M(f) ==>
- Relativize1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))"
- and fr_replace: "n \<in> nat ==> transrec_replacement(M,MH,n)"
- and fr_lam_replace:
- "M(g) ==>
- strong_replacement
- (M, \<lambda>x y. x \<in> formula &
- y = \<langle>x, formula_rec_case(a,b,c,d,g,x)\<rangle>)";
-
-lemma (in Formula_Rec) formula_rec_case_closed:
- "[|M(g); p \<in> formula|] ==> M(formula_rec_case(a, b, c, d, g, p))"
-by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed)
-
-lemma (in Formula_Rec) formula_rec_lam_closed:
- "M(g) ==> M(Lambda (formula, formula_rec_case(a,b,c,d,g)))"
-by (simp add: lam_closed2 fr_lam_replace formula_rec_case_closed)
-
-lemma (in Formula_Rec) MH_rel2:
- "relativize2 (M, MH,
- \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
-apply (simp add: relativize2_def MH_def, clarify)
-apply (rule lambda_abs2)
-apply (rule fr_lam_replace, assumption)
-apply (rule Relativize1_formula_rec_case)
-apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed)
-done
-
-lemma (in Formula_Rec) fr_transrec_closed:
- "n \<in> nat
- ==> M(transrec
- (n, \<lambda>x h. Lambda(formula, formula_rec_case(a, b, c, d, h))))"
-by (simp add: transrec_closed [OF fr_replace MH_rel2]
- nat_into_M formula_rec_lam_closed)
-
-text{*The main two results: @{term formula_rec} is absolute for @{term M}.*}
-theorem (in Formula_Rec) formula_rec_closed:
- "p \<in> formula ==> M(formula_rec(a,b,c,d,p))"
-by (simp add: formula_rec_eq2 fr_transrec_closed
- transM [OF _ formula_closed])
-
-theorem (in Formula_Rec) formula_rec_abs:
- "[| p \<in> formula; M(z)|]
- ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)"
-by (simp add: is_formula_rec_def formula_rec_eq2 transM [OF _ formula_closed]
- transrec_abs [OF fr_replace MH_rel2] depth_type
- fr_transrec_closed formula_rec_lam_closed eq_commute)
-
-
subsection {*Absoluteness for the Function @{term satisfies}*}
constdefs