# HG changeset patch # User paulson # Date 1034956213 -7200 # Node ID 95b95cdb47047ab884b4d6e110bbce9c4a462b35 # Parent b0d8bad27f429256bf48bf97e8a196f2dbc94ce2 Tidying up. New primitives is_iterates and is_iterates_fm. diff -r b0d8bad27f42 -r 95b95cdb4704 src/ZF/Constructible/DPow_absolute.thy --- a/src/ZF/Constructible/DPow_absolute.thy Fri Oct 18 09:53:18 2002 +0200 +++ b/src/ZF/Constructible/DPow_absolute.thy Fri Oct 18 17:50:13 2002 +0200 @@ -71,7 +71,7 @@ \i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]" shows "REFLECTS[\x. is_formula_rec(L, MH(L,x), f(x), h(x)), \i x. is_formula_rec(**Lset(i), MH(**Lset(i),x), f(x), h(x))]" -apply (simp (no_asm_use) only: is_formula_rec_def setclass_simps) +apply (simp (no_asm_use) only: is_formula_rec_def) apply (intro FOL_reflections function_reflections fun_plus_reflections depth_reflection is_transrec_reflection MH_reflection) done @@ -103,7 +103,7 @@ theorem satisfies_reflection: "REFLECTS[\x. is_satisfies(L,f(x),g(x),h(x)), \i x. is_satisfies(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_satisfies_def setclass_simps) +apply (simp only: is_satisfies_def) apply (intro formula_rec_reflection satisfies_MH_reflection) done @@ -351,7 +351,7 @@ \i x. is_P(**Lset(i), f(x), g(x))]" shows "REFLECTS[\x. is_Collect(L, f(x), is_P(L,x), g(x)), \i x. is_Collect(**Lset(i), f(x), is_P(**Lset(i), x), g(x))]" -apply (simp (no_asm_use) only: is_Collect_def setclass_simps) +apply (simp (no_asm_use) only: is_Collect_def) apply (intro FOL_reflections is_P_reflection) done @@ -403,7 +403,7 @@ \i x. is_P(**Lset(i), f(x), g(x), h(x))]" shows "REFLECTS[\x. is_Replace(L, f(x), is_P(L,x), g(x)), \i x. is_Replace(**Lset(i), f(x), is_P(**Lset(i), x), g(x))]" -apply (simp (no_asm_use) only: is_Replace_def setclass_simps) +apply (simp (no_asm_use) only: is_Replace_def) apply (intro FOL_reflections is_P_reflection) done @@ -447,7 +447,7 @@ theorem DPow'_reflection: "REFLECTS[\x. is_DPow'(L,f(x),g(x)), \i x. is_DPow'(**Lset(i),f(x),g(x))]" -apply (simp only: is_DPow'_def setclass_simps) +apply (simp only: is_DPow'_def) apply (intro FOL_reflections function_reflections mem_formula_reflection mem_list_reflection Collect_reflection DPow_body_reflection) done @@ -574,7 +574,7 @@ \gy \ Lset(i). y \ x & fun_apply(**Lset(i),f,y,gy) & is_DPow'(**Lset(i),gy,z), r) & big_union(**Lset(i),r,u), mr, v, y))]" -apply (simp only: setclass_simps [symmetric]) +apply (simp only: rex_setclass_is_bex [symmetric]) --{*Convert @{text "\y\Lset(i)"} to @{text "\y[**Lset(i)]"} within the body of the @{term is_wfrec} application. *} apply (intro FOL_reflections function_reflections diff -r b0d8bad27f42 -r 95b95cdb4704 src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Fri Oct 18 09:53:18 2002 +0200 +++ b/src/ZF/Constructible/Datatype_absolute.thy Fri Oct 18 17:50:13 2002 +0200 @@ -125,6 +125,11 @@ \n[M]. n\nat --> wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))" + is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o" + "is_iterates(M,isF,v,n,Z) == + \sn[M]. \msn[M]. successor(M,n,sn) & membership(M,sn,msn) & + is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)" + lemma (in M_basic) iterates_MH_abs: "[| relation1(M,isF,F); M(n); M(g); M(z) |] ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \m. F(g`m), n)" @@ -140,11 +145,10 @@ theorem (in M_trancl) iterates_abs: "[| iterates_replacement(M,isF,v); relation1(M,isF,F); n \ nat; M(v); M(z); \x[M]. M(F(x)) |] - ==> is_wfrec(M, iterates_MH(M,isF,v), Memrel(succ(n)), n, z) <-> - z = iterates(F,n,v)" + ==> is_iterates(M,isF,v,n,z) <-> z = iterates(F,n,v)" apply (frule iterates_imp_wfrec_replacement, assumption+) apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M - relation2_def iterates_MH_abs + is_iterates_def relation2_def iterates_MH_abs iterates_nat_def recursor_def transrec_def eclose_sing_Ord_eq nat_into_M trans_wfrec_abs [of _ _ _ _ "\n g. nat_case(v, \m. F(g`m), n)"]) @@ -338,10 +342,8 @@ constdefs is_list_N :: "[i=>o,i,i,i] => o" "is_list_N(M,A,n,Z) == - \zero[M]. \sn[M]. \msn[M]. - empty(M,zero) & - successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)" + \zero[M]. empty(M,zero) & + is_iterates(M, is_list_functor(M,A), zero, n, Z)" mem_list :: "[i=>o,i,i] => o" "mem_list(M,A,l) == @@ -442,11 +444,9 @@ constdefs is_formula_N :: "[i=>o,i,i] => o" "is_formula_N(M,n,Z) == - \zero[M]. \sn[M]. \msn[M]. - empty(M,zero) & - successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)" - + \zero[M]. empty(M,zero) & + is_iterates(M, is_formula_functor(M), zero, n, Z)" + constdefs @@ -459,40 +459,34 @@ "is_formula(M,Z) == \p[M]. p \ Z <-> mem_formula(M,p)" locale M_datatypes = M_trancl + - assumes list_replacement1: + assumes list_replacement1: "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)" - and list_replacement2: - "M(A) ==> strong_replacement(M, - \n y. n\nat & - (\sn[M]. \msn[M]. successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M,is_list_functor(M,A), 0), - msn, n, y)))" - and formula_replacement1: + and list_replacement2: + "M(A) ==> strong_replacement(M, + \n y. n\nat & is_iterates(M, is_list_functor(M,A), 0, n, y))" + and formula_replacement1: "iterates_replacement(M, is_formula_functor(M), 0)" - and formula_replacement2: - "strong_replacement(M, - \n y. n\nat & - (\sn[M]. \msn[M]. successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M,is_formula_functor(M), 0), - msn, n, y)))" + and formula_replacement2: + "strong_replacement(M, + \n y. n\nat & is_iterates(M, is_formula_functor(M), 0, n, y))" and nth_replacement: "M(l) ==> iterates_replacement(M, %l t. is_tl(M,l,t), l)" - + subsubsection{*Absoluteness of the List Construction*} -lemma (in M_datatypes) list_replacement2': +lemma (in M_datatypes) list_replacement2': "M(A) ==> strong_replacement(M, \n y. n\nat & y = (\X. {0} + A * X)^n (0))" -apply (insert list_replacement2 [of A]) -apply (rule strong_replacement_cong [THEN iffD1]) -apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]]) -apply (simp_all add: list_replacement1 relation1_def) +apply (insert list_replacement2 [of A]) +apply (rule strong_replacement_cong [THEN iffD1]) +apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]]) +apply (simp_all add: list_replacement1 relation1_def) done lemma (in M_datatypes) list_closed [intro,simp]: "M(A) ==> M(list(A))" apply (insert list_replacement1) -by (simp add: RepFun_closed2 list_eq_Union +by (simp add: RepFun_closed2 list_eq_Union list_replacement2' relation1_def iterates_closed [of "is_list_functor(M,A)"]) @@ -500,7 +494,7 @@ lemmas (in M_datatypes) list_into_M = transM [OF _ list_closed] lemma (in M_datatypes) list_N_abs [simp]: - "[|M(A); n\nat; M(Z)|] + "[|M(A); n\nat; M(Z)|] ==> is_list_N(M,A,n,Z) <-> Z = list_N(A,n)" apply (insert list_replacement1) apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M @@ -518,7 +512,7 @@ "M(A) ==> mem_list(M,A,l) <-> l \ list(A)" apply (insert list_replacement1) apply (simp add: mem_list_def list_N_def relation1_def list_eq_Union - iterates_closed [of "is_list_functor(M,A)"]) + iterates_closed [of "is_list_functor(M,A)"]) done lemma (in M_datatypes) list_abs [simp]: @@ -529,18 +523,18 @@ subsubsection{*Absoluteness of Formulas*} -lemma (in M_datatypes) formula_replacement2': +lemma (in M_datatypes) formula_replacement2': "strong_replacement(M, \n y. n\nat & y = (\X. ((nat*nat) + (nat*nat)) + (X*X + X))^n (0))" -apply (insert formula_replacement2) -apply (rule strong_replacement_cong [THEN iffD1]) -apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]]) -apply (simp_all add: formula_replacement1 relation1_def) +apply (insert formula_replacement2) +apply (rule strong_replacement_cong [THEN iffD1]) +apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]]) +apply (simp_all add: formula_replacement1 relation1_def) done lemma (in M_datatypes) formula_closed [intro,simp]: "M(formula)" apply (insert formula_replacement1) -apply (simp add: RepFun_closed2 formula_eq_Union +apply (simp add: RepFun_closed2 formula_eq_Union formula_replacement2' relation1_def iterates_closed [of "is_formula_functor(M)"]) done @@ -548,11 +542,11 @@ lemmas (in M_datatypes) formula_into_M = transM [OF _ formula_closed] lemma (in M_datatypes) formula_N_abs [simp]: - "[|n\nat; M(Z)|] + "[|n\nat; M(Z)|] ==> is_formula_N(M,n,Z) <-> Z = formula_N(n)" apply (insert formula_replacement1) apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M - iterates_abs [of "is_formula_functor(M)" _ + iterates_abs [of "is_formula_functor(M)" _ "\X. ((nat*nat) + (nat*nat)) + (X*X + X)"]) done @@ -567,7 +561,7 @@ "mem_formula(M,l) <-> l \ formula" apply (insert formula_replacement1) apply (simp add: mem_formula_def relation1_def formula_eq_Union formula_N_def - iterates_closed [of "is_formula_functor(M)"]) + iterates_closed [of "is_formula_functor(M)"]) done lemma (in M_datatypes) formula_abs [simp]: @@ -582,24 +576,21 @@ text{*Re-expresses eclose using "iterates"*} lemma eclose_eq_Union: "eclose(A) = (\n\nat. Union^n (A))" -apply (simp add: eclose_def) -apply (rule UN_cong) +apply (simp add: eclose_def) +apply (rule UN_cong) apply (rule refl) apply (induct_tac n) -apply (simp add: nat_rec_0) -apply (simp add: nat_rec_succ) +apply (simp add: nat_rec_0) +apply (simp add: nat_rec_succ) done constdefs is_eclose_n :: "[i=>o,i,i,i] => o" - "is_eclose_n(M,A,n,Z) == - \sn[M]. \msn[M]. - successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M, big_union(M), A), msn, n, Z)" - + "is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z)" + mem_eclose :: "[i=>o,i,i] => o" - "mem_eclose(M,A,l) == - \n[M]. \eclosen[M]. + "mem_eclose(M,A,l) == + \n[M]. \eclosen[M]. finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \ eclosen" is_eclose :: "[i=>o,i,i] => o" @@ -607,27 +598,24 @@ locale M_eclose = M_datatypes + - assumes eclose_replacement1: + assumes eclose_replacement1: "M(A) ==> iterates_replacement(M, big_union(M), A)" - and eclose_replacement2: - "M(A) ==> strong_replacement(M, - \n y. n\nat & - (\sn[M]. \msn[M]. successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M,big_union(M), A), - msn, n, y)))" + and eclose_replacement2: + "M(A) ==> strong_replacement(M, + \n y. n\nat & is_iterates(M, big_union(M), A, n, y))" -lemma (in M_eclose) eclose_replacement2': +lemma (in M_eclose) eclose_replacement2': "M(A) ==> strong_replacement(M, \n y. n\nat & y = Union^n (A))" -apply (insert eclose_replacement2 [of A]) -apply (rule strong_replacement_cong [THEN iffD1]) -apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]]) -apply (simp_all add: eclose_replacement1 relation1_def) +apply (insert eclose_replacement2 [of A]) +apply (rule strong_replacement_cong [THEN iffD1]) +apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]]) +apply (simp_all add: eclose_replacement1 relation1_def) done lemma (in M_eclose) eclose_closed [intro,simp]: "M(A) ==> M(eclose(A))" apply (insert eclose_replacement1) -by (simp add: RepFun_closed2 eclose_eq_Union +by (simp add: RepFun_closed2 eclose_eq_Union eclose_replacement2' relation1_def iterates_closed [of "big_union(M)"]) @@ -642,7 +630,7 @@ "M(A) ==> mem_eclose(M,A,l) <-> l \ eclose(A)" apply (insert eclose_replacement1) apply (simp add: mem_eclose_def relation1_def eclose_eq_Union - iterates_closed [of "big_union(M)"]) + iterates_closed [of "big_union(M)"]) done lemma (in M_eclose) eclose_abs [simp]: @@ -652,54 +640,52 @@ done - - subsection {*Absoluteness for @{term transrec}*} - text{* @{term "transrec(a,H) \ wfrec(Memrel(eclose({a})), a, H)"} *} constdefs is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o" - "is_transrec(M,MH,a,z) == - \sa[M]. \esa[M]. \mesa[M]. + "is_transrec(M,MH,a,z) == + \sa[M]. \esa[M]. \mesa[M]. upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) & is_wfrec(M,MH,mesa,a,z)" transrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o" "transrec_replacement(M,MH,a) == - \sa[M]. \esa[M]. \mesa[M]. + \sa[M]. \esa[M]. \mesa[M]. upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) & wfrec_replacement(M,MH,mesa)" -text{*The condition @{term "Ord(i)"} lets us use the simpler +text{*The condition @{term "Ord(i)"} lets us use the simpler @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"}, which I haven't even proved yet. *} theorem (in M_eclose) transrec_abs: "[|transrec_replacement(M,MH,i); relation2(M,MH,H); Ord(i); M(i); M(z); - \x[M]. \g[M]. function(g) --> M(H(x,g))|] - ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" + \x[M]. \g[M]. function(g) --> M(H(x,g))|] + ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel) theorem (in M_eclose) transrec_closed: "[|transrec_replacement(M,MH,i); relation2(M,MH,H); - Ord(i); M(i); - \x[M]. \g[M]. function(g) --> M(H(x,g))|] + Ord(i); M(i); + \x[M]. \g[M]. function(g) --> M(H(x,g))|] ==> M(transrec(i,H))" by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel) text{*Helps to prove instances of @{term transrec_replacement}*} -lemma (in M_eclose) transrec_replacementI: +lemma (in M_eclose) transrec_replacementI: "[|M(a); - strong_replacement (M, - \x z. \y[M]. pair(M, x, y, z) \ is_wfrec(M,MH,Memrel(eclose({a})),x,y))|] + strong_replacement (M, + \x z. \y[M]. pair(M, x, y, z) & + is_wfrec(M,MH,Memrel(eclose({a})),x,y))|] ==> transrec_replacement(M,MH,a)" -by (simp add: transrec_replacement_def wfrec_replacement_def) +by (simp add: transrec_replacement_def wfrec_replacement_def) subsection{*Absoluteness for the List Operator @{term length}*} @@ -707,8 +693,8 @@ constdefs is_length :: "[i=>o,i,i,i] => o" - "is_length(M,A,l,n) == - \sn[M]. \list_n[M]. \list_sn[M]. + "is_length(M,A,l,n) == + \sn[M]. \list_n[M]. \list_sn[M]. is_list_N(M,A,n,list_n) & l \ list_n & successor(M,n,sn) & is_list_N(M,A,sn,list_sn) & l \ list_sn" @@ -716,7 +702,7 @@ lemma (in M_datatypes) length_abs [simp]: "[|M(A); l \ list(A); n \ nat|] ==> is_length(M,A,l,n) <-> n = length(l)" apply (subgoal_tac "M(l) & M(n)") - prefer 2 apply (blast dest: transM) + prefer 2 apply (blast dest: transM) apply (simp add: is_length_def) apply (blast intro: list_imp_list_N nat_into_Ord list_N_imp_eq_length dest: list_N_imp_length_lt) @@ -725,29 +711,29 @@ text{*Proof is trivial since @{term length} returns natural numbers.*} lemma (in M_trivial) length_closed [intro,simp]: "l \ list(A) ==> M(length(l))" -by (simp add: nat_into_M) +by (simp add: nat_into_M) subsection {*Absoluteness for the List Operator @{term nth}*} lemma nth_eq_hd_iterates_tl [rule_format]: "xs \ list(A) ==> \n \ nat. nth(n,xs) = hd' (tl'^n (xs))" -apply (induct_tac xs) -apply (simp add: iterates_tl_Nil hd'_Nil, clarify) +apply (induct_tac xs) +apply (simp add: iterates_tl_Nil hd'_Nil, clarify) apply (erule natE) -apply (simp add: hd'_Cons) -apply (simp add: tl'_Cons iterates_commute) +apply (simp add: hd'_Cons) +apply (simp add: tl'_Cons iterates_commute) done lemma (in M_basic) iterates_tl'_closed: "[|n \ nat; M(x)|] ==> M(tl'^n (x))" -apply (induct_tac n, simp) -apply (simp add: tl'_Cons tl'_closed) +apply (induct_tac n, simp) +apply (simp add: tl'_Cons tl'_closed) done text{*Immediate by type-checking*} lemma (in M_datatypes) nth_closed [intro,simp]: - "[|xs \ list(A); n \ nat; M(A)|] ==> M(nth(n,xs))" + "[|xs \ list(A); n \ nat; M(A)|] ==> M(nth(n,xs))" apply (case_tac "n < length(xs)") apply (blast intro: nth_type transM) apply (simp add: not_lt_iff_le nth_eq_0) @@ -755,19 +741,16 @@ constdefs is_nth :: "[i=>o,i,i,i] => o" - "is_nth(M,n,l,Z) == - \X[M]. \sn[M]. \msn[M]. - successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) & - is_hd(M,X,Z)" - + "is_nth(M,n,l,Z) == + \X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" + lemma (in M_datatypes) nth_abs [simp]: - "[|M(A); n \ nat; l \ list(A); M(Z)|] + "[|M(A); n \ nat; l \ list(A); M(Z)|] ==> is_nth(M,n,l,Z) <-> Z = nth(n,l)" -apply (subgoal_tac "M(l)") +apply (subgoal_tac "M(l)") prefer 2 apply (blast intro: transM) apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M - tl'_closed iterates_tl'_closed + tl'_closed iterates_tl'_closed iterates_abs [OF _ relation1_tl] nth_replacement) done @@ -786,7 +769,7 @@ lemma (in M_trivial) Member_in_M_iff [iff]: "M(Member(x,y)) <-> M(x) & M(y)" -by (simp add: Member_def) +by (simp add: Member_def) constdefs is_Equal :: "[i=>o,i,i,i] => o" @@ -799,7 +782,7 @@ by (simp add: is_Equal_def Equal_def) lemma (in M_trivial) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)" -by (simp add: Equal_def) +by (simp add: Equal_def) constdefs is_Nand :: "[i=>o,i,i,i] => o" @@ -812,7 +795,7 @@ by (simp add: is_Nand_def Nand_def) lemma (in M_trivial) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)" -by (simp add: Nand_def) +by (simp add: Nand_def) constdefs is_Forall :: "[i=>o,i,i] => o" @@ -836,7 +819,7 @@ --{* the instance of @{term formula_case} in @{term formula_rec}*} "formula_rec_case(a,b,c,d,h) == formula_case (a, b, - \u v. c(u, v, h ` succ(depth(u)) ` u, + \u v. c(u, v, h ` succ(depth(u)) ` u, h ` succ(depth(v)) ` v), \u. d(u, h ` succ(depth(u)) ` u))" @@ -845,21 +828,21 @@ neither of which is absolute.*} lemma (in M_trivial) formula_rec_eq: "p \ formula ==> - formula_rec(a,b,c,d,p) = + formula_rec(a,b,c,d,p) = transrec (succ(depth(p)), \x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p" apply (simp add: formula_rec_case_def) apply (induct_tac p) txt{*Base case for @{term Member}*} - apply (subst transrec, simp add: formula.intros) + apply (subst transrec, simp add: formula.intros) txt{*Base case for @{term Equal}*} apply (subst transrec, simp add: formula.intros) txt{*Inductive step for @{term Nand}*} - apply (subst transrec) + apply (subst transrec) apply (simp add: succ_Un_distrib formula.intros) txt{*Inductive step for @{term Forall}*} -apply (subst transrec) -apply (simp add: formula_imp_formula_N formula.intros) +apply (subst transrec) +apply (simp add: formula_imp_formula_N formula.intros) done @@ -867,8 +850,8 @@ constdefs is_depth :: "[i=>o,i,i] => o" - "is_depth(M,p,n) == - \sn[M]. \formula_n[M]. \formula_sn[M]. + "is_depth(M,p,n) == + \sn[M]. \formula_n[M]. \formula_sn[M]. is_formula_N(M,n,formula_n) & p \ formula_n & successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \ formula_sn" @@ -876,7 +859,7 @@ lemma (in M_datatypes) depth_abs [simp]: "[|p \ formula; n \ nat|] ==> is_depth(M,p,n) <-> n = depth(p)" apply (subgoal_tac "M(p) & M(n)") - prefer 2 apply (blast dest: transM) + prefer 2 apply (blast dest: transM) apply (simp add: is_depth_def) apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth dest: formula_N_imp_depth_lt) @@ -885,43 +868,43 @@ text{*Proof is trivial since @{term depth} returns natural numbers.*} lemma (in M_trivial) depth_closed [intro,simp]: "p \ formula ==> M(depth(p))" -by (simp add: nat_into_M) +by (simp add: nat_into_M) subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*} constdefs - 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" --{*no constraint on non-formulas*} - "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == - (\x[M]. \y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) --> + "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == + (\x[M]. \y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) --> is_Member(M,x,y,p) --> is_a(x,y,z)) & - (\x[M]. \y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) --> + (\x[M]. \y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) --> is_Equal(M,x,y,p) --> is_b(x,y,z)) & - (\x[M]. \y[M]. mem_formula(M,x) --> mem_formula(M,y) --> + (\x[M]. \y[M]. mem_formula(M,x) --> mem_formula(M,y) --> is_Nand(M,x,y,p) --> is_c(x,y,z)) & (\x[M]. mem_formula(M,x) --> is_Forall(M,x,p) --> is_d(x,z))" -lemma (in M_datatypes) formula_case_abs [simp]: - "[| Relation2(M,nat,nat,is_a,a); Relation2(M,nat,nat,is_b,b); - Relation2(M,formula,formula,is_c,c); Relation1(M,formula,is_d,d); - p \ formula; M(z) |] - ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <-> +lemma (in M_datatypes) formula_case_abs [simp]: + "[| Relation2(M,nat,nat,is_a,a); Relation2(M,nat,nat,is_b,b); + Relation2(M,formula,formula,is_c,c); Relation1(M,formula,is_d,d); + p \ 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: Relation1_def Relation2_def) +apply (erule formula.cases) + apply (simp_all add: Relation1_def Relation2_def) done lemma (in M_datatypes) formula_case_closed [intro,simp]: - "[|p \ formula; - \x[M]. \y[M]. x\nat --> y\nat --> M(a(x,y)); - \x[M]. \y[M]. x\nat --> y\nat --> M(b(x,y)); - \x[M]. \y[M]. x\formula --> y\formula --> M(c(x,y)); + "[|p \ formula; + \x[M]. \y[M]. x\nat --> y\nat --> M(a(x,y)); + \x[M]. \y[M]. x\nat --> y\nat --> M(b(x,y)); + \x[M]. \y[M]. x\formula --> y\formula --> M(c(x,y)); \x[M]. x\formula --> M(d(x))|] ==> M(formula_case(a,b,c,d,p))" -by (erule formula.cases, simp_all) +by (erule formula.cases, simp_all) subsubsection {*Absoluteness for @{term formula_rec}: Final Results*} @@ -930,7 +913,7 @@ 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) == - \dp[M]. \i[M]. \f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & + \dp[M]. \i[M]. \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)" @@ -939,16 +922,16 @@ lemma (in M_datatypes) Relation1_formula_rec_case: "[|Relation2(M, nat, nat, is_a, a); Relation2(M, nat, nat, is_b, b); - Relation2 (M, formula, formula, + Relation2 (M, formula, formula, is_c, \u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v)); - Relation1(M, formula, + Relation1(M, formula, is_d, \u. d(u, h ` succ(depth(u)) ` u)); - M(h) |] + M(h) |] ==> Relation1(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 Relation1_def) -apply (simp add: formula_case_abs) +apply (simp (no_asm) add: formula_rec_case_def Relation1_def) +apply (simp add: formula_case_abs) done @@ -970,12 +953,12 @@ and c_closed: "[|x \ formula; y \ formula; M(gx); M(gy)|] ==> M(c(x, y, gx, gy))" and c_rel: - "M(f) ==> + "M(f) ==> Relation2 (M, formula, formula, is_c(f), \u v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))" and d_closed: "[|x \ formula; M(gx)|] ==> M(d(x, gx))" and d_rel: - "M(f) ==> + "M(f) ==> Relation1(M, formula, is_d(f), \u. d(u, f ` succ(depth(u)) ` u))" and fr_replace: "n \ nat ==> transrec_replacement(M,MH,n)" and fr_lam_replace: @@ -986,7 +969,7 @@ lemma (in Formula_Rec) formula_rec_case_closed: "[|M(g); p \ 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) +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)))" @@ -995,29 +978,29 @@ lemma (in Formula_Rec) MH_rel2: "relation2 (M, MH, \x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))" -apply (simp add: relation2_def MH_def, clarify) -apply (rule lambda_abs2) +apply (simp add: relation2_def MH_def, clarify) +apply (rule lambda_abs2) apply (rule fr_lam_replace, assumption) -apply (rule Relation1_formula_rec_case) -apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed) +apply (rule Relation1_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 \ nat ==> M(transrec (n, \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) +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 \ formula ==> M(formula_rec(a,b,c,d,p))" -by (simp add: formula_rec_eq fr_transrec_closed +by (simp add: formula_rec_eq fr_transrec_closed transM [OF _ formula_closed]) theorem (in Formula_Rec) formula_rec_abs: - "[| p \ formula; M(z)|] - ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)" + "[| p \ 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_eq transM [OF _ formula_closed] transrec_abs [OF fr_replace MH_rel2] depth_type fr_transrec_closed formula_rec_lam_closed eq_commute) diff -r b0d8bad27f42 -r 95b95cdb4704 src/ZF/Constructible/Internalize.thy --- a/src/ZF/Constructible/Internalize.thy Fri Oct 18 09:53:18 2002 +0200 +++ b/src/ZF/Constructible/Internalize.thy Fri Oct 18 17:50:13 2002 +0200 @@ -31,7 +31,7 @@ theorem Inl_reflection: "REFLECTS[\x. is_Inl(L,f(x),h(x)), \i x. is_Inl(**Lset(i),f(x),h(x))]" -apply (simp only: is_Inl_def setclass_simps) +apply (simp only: is_Inl_def) apply (intro FOL_reflections function_reflections) done @@ -60,7 +60,7 @@ theorem Inr_reflection: "REFLECTS[\x. is_Inr(L,f(x),h(x)), \i x. is_Inr(**Lset(i),f(x),h(x))]" -apply (simp only: is_Inr_def setclass_simps) +apply (simp only: is_Inr_def) apply (intro FOL_reflections function_reflections) done @@ -88,7 +88,7 @@ theorem Nil_reflection: "REFLECTS[\x. is_Nil(L,f(x)), \i x. is_Nil(**Lset(i),f(x))]" -apply (simp only: is_Nil_def setclass_simps) +apply (simp only: is_Nil_def) apply (intro FOL_reflections function_reflections Inl_reflection) done @@ -120,7 +120,7 @@ theorem Cons_reflection: "REFLECTS[\x. is_Cons(L,f(x),g(x),h(x)), \i x. is_Cons(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_Cons_def setclass_simps) +apply (simp only: is_Cons_def) apply (intro FOL_reflections pair_reflection Inr_reflection) done @@ -148,7 +148,7 @@ theorem quasilist_reflection: "REFLECTS[\x. is_quasilist(L,f(x)), \i x. is_quasilist(**Lset(i),f(x))]" -apply (simp only: is_quasilist_def setclass_simps) +apply (simp only: is_quasilist_def) apply (intro FOL_reflections Nil_reflection Cons_reflection) done @@ -186,7 +186,7 @@ theorem hd_reflection: "REFLECTS[\x. is_hd(L,f(x),g(x)), \i x. is_hd(**Lset(i),f(x),g(x))]" -apply (simp only: is_hd_def setclass_simps) +apply (simp only: is_hd_def) apply (intro FOL_reflections Nil_reflection Cons_reflection quasilist_reflection empty_reflection) done @@ -222,7 +222,7 @@ theorem tl_reflection: "REFLECTS[\x. is_tl(L,f(x),g(x)), \i x. is_tl(**Lset(i),f(x),g(x))]" -apply (simp only: is_tl_def setclass_simps) +apply (simp only: is_tl_def) apply (intro FOL_reflections Nil_reflection Cons_reflection quasilist_reflection empty_reflection) done @@ -260,7 +260,7 @@ "REFLECTS [P(L), \i. P(**Lset(i))] ==> REFLECTS[\x. is_bool_of_o(L, P(L,x), f(x)), \i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]" -apply (simp (no_asm) only: is_bool_of_o_def setclass_simps) +apply (simp (no_asm) only: is_bool_of_o_def) apply (intro FOL_reflections function_reflections, assumption+) done @@ -301,24 +301,13 @@ is_lambda(**A, nth(x,env), is_b, nth(y,env))" by (simp add: lambda_fm_def is_lambda_def is_b_iff_sats [THEN iff_sym]) -lemma is_lambda_iff_sats: - assumes is_b_iff_sats: - "!!a0 a1 a2. - [|a0\A; a1\A; a2\A|] - ==> is_b(a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))" - shows - "[|nth(i,env) = x; nth(j,env) = y; - i \ nat; j \ nat; env \ list(A)|] - ==> is_lambda(**A, x, is_b, y) <-> sats(A, lambda_fm(p,i,j), env)" -by (simp add: sats_lambda_fm [OF is_b_iff_sats]) - theorem is_lambda_reflection: assumes is_b_reflection: "!!f' f g h. REFLECTS[\x. is_b(L, f'(x), f(x), g(x)), \i x. is_b(**Lset(i), f'(x), f(x), g(x))]" shows "REFLECTS[\x. is_lambda(L, A(x), is_b(L,x), f(x)), \i x. is_lambda(**Lset(i), A(x), is_b(**Lset(i),x), f(x))]" -apply (simp (no_asm_use) only: is_lambda_def setclass_simps) +apply (simp (no_asm_use) only: is_lambda_def) apply (intro FOL_reflections is_b_reflection pair_reflection) done @@ -350,7 +339,7 @@ theorem Member_reflection: "REFLECTS[\x. is_Member(L,f(x),g(x),h(x)), \i x. is_Member(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_Member_def setclass_simps) +apply (simp only: is_Member_def) apply (intro FOL_reflections pair_reflection Inl_reflection) done @@ -382,7 +371,7 @@ theorem Equal_reflection: "REFLECTS[\x. is_Equal(L,f(x),g(x),h(x)), \i x. is_Equal(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_Equal_def setclass_simps) +apply (simp only: is_Equal_def) apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection) done @@ -414,7 +403,7 @@ theorem Nand_reflection: "REFLECTS[\x. is_Nand(L,f(x),g(x),h(x)), \i x. is_Nand(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_Nand_def setclass_simps) +apply (simp only: is_Nand_def) apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection) done @@ -444,7 +433,7 @@ theorem Forall_reflection: "REFLECTS[\x. is_Forall(L,f(x),g(x)), \i x. is_Forall(**Lset(i),f(x),g(x))]" -apply (simp only: is_Forall_def setclass_simps) +apply (simp only: is_Forall_def) apply (intro FOL_reflections pair_reflection Inr_reflection) done @@ -477,7 +466,7 @@ theorem is_and_reflection: "REFLECTS[\x. is_and(L,f(x),g(x),h(x)), \i x. is_and(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_and_def setclass_simps) +apply (simp only: is_and_def) apply (intro FOL_reflections function_reflections) done @@ -511,7 +500,7 @@ theorem is_or_reflection: "REFLECTS[\x. is_or(L,f(x),g(x),h(x)), \i x. is_or(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_or_def setclass_simps) +apply (simp only: is_or_def) apply (intro FOL_reflections function_reflections) done @@ -544,7 +533,7 @@ theorem is_not_reflection: "REFLECTS[\x. is_not(L,f(x),g(x)), \i x. is_not(**Lset(i),f(x),g(x))]" -apply (simp only: is_not_def setclass_simps) +apply (simp only: is_not_def) apply (intro FOL_reflections function_reflections) done @@ -555,13 +544,6 @@ is_lambda_reflection Member_reflection Equal_reflection Nand_reflection Forall_reflection is_and_reflection is_or_reflection is_not_reflection -lemmas extra_iff_sats = - Inl_iff_sats Inr_iff_sats Nil_iff_sats Cons_iff_sats quasilist_iff_sats - hd_iff_sats tl_iff_sats is_bool_of_o_iff_sats is_lambda_iff_sats - Member_iff_sats Equal_iff_sats Nand_iff_sats Forall_iff_sats - is_and_iff_sats is_or_iff_sats is_not_iff_sats - - subsection{*Well-Founded Recursion!*} subsubsection{*The Operator @{term M_is_recfun}*} @@ -643,14 +625,15 @@ \i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]" shows "REFLECTS[\x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)), \i x. M_is_recfun(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]" -apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps) +apply (simp (no_asm_use) only: M_is_recfun_def) apply (intro FOL_reflections function_reflections restriction_reflection MH_reflection) done subsubsection{*The Operator @{term is_wfrec}*} -text{*The three arguments of @{term p} are always 2, 1, 0*} +text{*The three arguments of @{term p} are always 2, 1, 0; + @{term p} is enclosed by 5 quantifiers.*} (* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o" "is_wfrec(M,MH,r,a,z) == @@ -704,7 +687,7 @@ \i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]" shows "REFLECTS[\x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)), \i x. is_wfrec(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]" -apply (simp (no_asm_use) only: is_wfrec_def setclass_simps) +apply (simp (no_asm_use) only: is_wfrec_def) apply (intro FOL_reflections MH_reflection is_recfun_reflection) done @@ -741,7 +724,7 @@ theorem cartprod_reflection: "REFLECTS[\x. cartprod(L,f(x),g(x),h(x)), \i x. cartprod(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: cartprod_def setclass_simps) +apply (simp only: cartprod_def) apply (intro FOL_reflections pair_reflection) done @@ -780,7 +763,7 @@ theorem sum_reflection: "REFLECTS[\x. is_sum(L,f(x),g(x),h(x)), \i x. is_sum(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_sum_def setclass_simps) +apply (simp only: is_sum_def) apply (intro FOL_reflections function_reflections cartprod_reflection) done @@ -809,7 +792,7 @@ theorem quasinat_reflection: "REFLECTS[\x. is_quasinat(L,f(x)), \i x. is_quasinat(**Lset(i),f(x))]" -apply (simp only: is_quasinat_def setclass_simps) +apply (simp only: is_quasinat_def) apply (intro FOL_reflections function_reflections) done @@ -868,7 +851,7 @@ \i x. is_b(**Lset(i), h(x), f(x), g(x))]" shows "REFLECTS[\x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)), \i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]" -apply (simp (no_asm_use) only: is_nat_case_def setclass_simps) +apply (simp (no_asm_use) only: is_nat_case_def) apply (intro FOL_reflections function_reflections restriction_reflection is_b_reflection quasinat_reflection) done @@ -931,33 +914,92 @@ shows "REFLECTS[\x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)), \i x. iterates_MH(**Lset(i), p(**Lset(i),x), e(x), f(x), g(x), h(x))]" apply (simp (no_asm_use) only: iterates_MH_def) -txt{*Must be careful: simplifying with @{text setclass_simps} above would - change @{text "\gm[**Lset(i)]"} into @{text "\gm \ Lset(i)"}, when - it would no longer match rule @{text is_nat_case_reflection}. *} -apply (rule is_nat_case_reflection) -apply (simp (no_asm_use) only: setclass_simps) apply (intro FOL_reflections function_reflections is_nat_case_reflection restriction_reflection p_reflection) done +subsubsection{*The Operator @{term is_iterates}*} + +text{*The three arguments of @{term p} are always 2, 1, 0; + @{term p} is enclosed by 9 (??) quantifiers.*} + +(* "is_iterates(M,isF,v,n,Z) == + \sn[M]. \msn[M]. successor(M,n,sn) & membership(M,sn,msn) & + 1 0 is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"*) + +constdefs is_iterates_fm :: "[i, i, i, i]=>i" + "is_iterates_fm(p,v,n,Z) == + Exists(Exists( + And(succ_fm(n#+2,1), + And(Memrel_fm(1,0), + is_wfrec_fm(iterates_MH_fm(p, v#+7, 2, 1, 0), + 0, n#+2, Z#+2)))))" + +text{*We call @{term p} with arguments a, f, z by equating them with + the corresponding quantified variables with de Bruijn indices 2, 1, 0.*} + + +lemma is_iterates_type [TC]: + "[| p \ formula; x \ nat; y \ nat; z \ nat |] + ==> is_iterates_fm(p,x,y,z) \ formula" +by (simp add: is_iterates_fm_def) + +lemma sats_is_iterates_fm: + assumes is_F_iff_sats: + "!!a b c d e f g h i j k. + [| a \ A; b \ A; c \ A; d \ A; e \ A; f \ A; + g \ A; h \ A; i \ A; j \ A; k \ A|] + ==> is_F(a,b) <-> + sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d, Cons(e, Cons(f, + Cons(g, Cons(h, Cons(i, Cons(j, Cons(k, env))))))))))))" + shows + "[|x \ nat; y < length(env); z < length(env); env \ list(A)|] + ==> sats(A, is_iterates_fm(p,x,y,z), env) <-> + is_iterates(**A, is_F, nth(x,env), nth(y,env), nth(z,env))" +apply (frule_tac x=z in lt_length_in_nat, assumption) +apply (frule lt_length_in_nat, assumption) +apply (simp add: is_iterates_fm_def is_iterates_def sats_is_nat_case_fm + is_F_iff_sats [symmetric] sats_is_wfrec_fm sats_iterates_MH_fm) +done + + +lemma is_iterates_iff_sats: + assumes is_F_iff_sats: + "!!a b c d e f g h i j k. + [| a \ A; b \ A; c \ A; d \ A; e \ A; f \ A; + g \ A; h \ A; i \ A; j \ A; k \ A|] + ==> is_F(a,b) <-> + sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d, Cons(e, Cons(f, + Cons(g, Cons(h, Cons(i, Cons(j, Cons(k, env))))))))))))" + shows + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j < length(env); k < length(env); env \ list(A)|] + ==> is_iterates(**A, is_F, x, y, z) <-> + sats(A, is_iterates_fm(p,i,j,k), env)" +by (simp add: sats_is_iterates_fm [OF is_F_iff_sats]) + +text{*The second argument of @{term p} gives it direct access to @{term x}, + which is essential for handling free variable references. Without this + argument, we cannot prove reflection for @{term list_N}.*} +theorem is_iterates_reflection: + assumes p_reflection: + "!!f g h. REFLECTS[\x. p(L, h(x), f(x), g(x)), + \i x. p(**Lset(i), h(x), f(x), g(x))]" + shows "REFLECTS[\x. is_iterates(L, p(L,x), f(x), g(x), h(x)), + \i x. is_iterates(**Lset(i), p(**Lset(i),x), f(x), g(x), h(x))]" +apply (simp (no_asm_use) only: is_iterates_def) +apply (intro FOL_reflections function_reflections p_reflection + is_wfrec_reflection iterates_MH_reflection) +done + subsubsection{*The Formula @{term is_eclose_n}, Internalized*} -(* is_eclose_n(M,A,n,Z) == - \sn[M]. \msn[M]. - 1 0 - successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M, big_union(M), A), msn, n, Z) *) +(* is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z) *) constdefs eclose_n_fm :: "[i,i,i]=>i" - "eclose_n_fm(A,n,Z) == - Exists(Exists( - And(succ_fm(n#+2,1), - And(Memrel_fm(1,0), - is_wfrec_fm(iterates_MH_fm(big_union_fm(1,0), - A#+7, 2, 1, 0), - 0, n#+2, Z#+2)))))" + "eclose_n_fm(A,n,Z) == is_iterates_fm(big_union_fm(1,0), A, n, Z)" lemma eclose_n_fm_type [TC]: "[| x \ nat; y \ nat; z \ nat |] ==> eclose_n_fm(x,y,z) \ formula" @@ -969,8 +1011,8 @@ is_eclose_n(**A, nth(x,env), nth(y,env), nth(z,env))" apply (frule_tac x=z in lt_length_in_nat, assumption) apply (frule_tac x=y in lt_length_in_nat, assumption) -apply (simp add: eclose_n_fm_def is_eclose_n_def sats_is_wfrec_fm - sats_iterates_MH_fm) +apply (simp add: eclose_n_fm_def is_eclose_n_def + sats_is_iterates_fm) done lemma eclose_n_iff_sats: @@ -982,9 +1024,8 @@ theorem eclose_n_reflection: "REFLECTS[\x. is_eclose_n(L, f(x), g(x), h(x)), \i x. is_eclose_n(**Lset(i), f(x), g(x), h(x))]" -apply (simp only: is_eclose_n_def setclass_simps) -apply (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection) +apply (simp only: is_eclose_n_def) +apply (intro FOL_reflections function_reflections is_iterates_reflection) done @@ -1017,7 +1058,7 @@ theorem mem_eclose_reflection: "REFLECTS[\x. mem_eclose(L,f(x),g(x)), \i x. mem_eclose(**Lset(i),f(x),g(x))]" -apply (simp only: mem_eclose_def setclass_simps) +apply (simp only: mem_eclose_def) apply (intro FOL_reflections finite_ordinal_reflection eclose_n_reflection) done @@ -1047,7 +1088,7 @@ theorem is_eclose_reflection: "REFLECTS[\x. is_eclose(L,f(x),g(x)), \i x. is_eclose(**Lset(i),f(x),g(x))]" -apply (simp only: is_eclose_def setclass_simps) +apply (simp only: is_eclose_def) apply (intro FOL_reflections mem_eclose_reflection) done @@ -1082,7 +1123,7 @@ theorem list_functor_reflection: "REFLECTS[\x. is_list_functor(L,f(x),g(x),h(x)), \i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_list_functor_def setclass_simps) +apply (simp only: is_list_functor_def) apply (intro FOL_reflections number1_reflection cartprod_reflection sum_reflection) done @@ -1091,20 +1132,14 @@ subsubsection{*The Formula @{term is_list_N}, Internalized*} (* "is_list_N(M,A,n,Z) == - \zero[M]. \sn[M]. \msn[M]. - empty(M,zero) & - successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)" *) - + \zero[M]. empty(M,zero) & + is_iterates(M, is_list_functor(M,A), zero, n, Z)" *) + constdefs list_N_fm :: "[i,i,i]=>i" "list_N_fm(A,n,Z) == - Exists(Exists(Exists( - And(empty_fm(2), - And(succ_fm(n#+3,1), - And(Memrel_fm(1,0), - is_wfrec_fm(iterates_MH_fm(list_functor_fm(A#+9#+3,1,0), - 7,2,1,0), - 0, n#+3, Z#+3)))))))" + Exists( + And(empty_fm(0), + is_iterates_fm(list_functor_fm(A#+9#+3,1,0), 0, n#+1, Z#+1)))" lemma list_N_fm_type [TC]: "[| x \ nat; y \ nat; z \ nat |] ==> list_N_fm(x,y,z) \ formula" @@ -1116,8 +1151,7 @@ is_list_N(**A, nth(x,env), nth(y,env), nth(z,env))" apply (frule_tac x=z in lt_length_in_nat, assumption) apply (frule_tac x=y in lt_length_in_nat, assumption) -apply (simp add: list_N_fm_def is_list_N_def sats_is_wfrec_fm - sats_iterates_MH_fm) +apply (simp add: list_N_fm_def is_list_N_def sats_is_iterates_fm) done lemma list_N_iff_sats: @@ -1129,9 +1163,9 @@ theorem list_N_reflection: "REFLECTS[\x. is_list_N(L, f(x), g(x), h(x)), \i x. is_list_N(**Lset(i), f(x), g(x), h(x))]" -apply (simp only: is_list_N_def setclass_simps) -apply (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection list_functor_reflection) +apply (simp only: is_list_N_def) +apply (intro FOL_reflections function_reflections + is_iterates_reflection list_functor_reflection) done @@ -1165,7 +1199,7 @@ theorem mem_list_reflection: "REFLECTS[\x. mem_list(L,f(x),g(x)), \i x. mem_list(**Lset(i),f(x),g(x))]" -apply (simp only: mem_list_def setclass_simps) +apply (simp only: mem_list_def) apply (intro FOL_reflections finite_ordinal_reflection list_N_reflection) done @@ -1195,7 +1229,7 @@ theorem is_list_reflection: "REFLECTS[\x. is_list(L,f(x),g(x)), \i x. is_list(**Lset(i),f(x),g(x))]" -apply (simp only: is_list_def setclass_simps) +apply (simp only: is_list_def) apply (intro FOL_reflections mem_list_reflection) done @@ -1237,7 +1271,7 @@ theorem formula_functor_reflection: "REFLECTS[\x. is_formula_functor(L,f(x),g(x)), \i x. is_formula_functor(**Lset(i),f(x),g(x))]" -apply (simp only: is_formula_functor_def setclass_simps) +apply (simp only: is_formula_functor_def) apply (intro FOL_reflections omega_reflection cartprod_reflection sum_reflection) done @@ -1245,20 +1279,14 @@ subsubsection{*The Formula @{term is_formula_N}, Internalized*} -(* "is_formula_N(M,n,Z) == - \zero[M]. \sn[M]. \msn[M]. - 2 1 0 - empty(M,zero) & - successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)" *) +(* "is_formula_N(M,n,Z) == + \zero[M]. empty(M,zero) & + is_iterates(M, is_formula_functor(M), zero, n, Z)" *) constdefs formula_N_fm :: "[i,i]=>i" "formula_N_fm(n,Z) == - Exists(Exists(Exists( - And(empty_fm(2), - And(succ_fm(n#+3,1), - And(Memrel_fm(1,0), - is_wfrec_fm(iterates_MH_fm(formula_functor_fm(1,0),7,2,1,0), - 0, n#+3, Z#+3)))))))" + Exists( + And(empty_fm(0), + is_iterates_fm(formula_functor_fm(1,0), 0, n#+1, Z#+1)))" lemma formula_N_fm_type [TC]: "[| x \ nat; y \ nat |] ==> formula_N_fm(x,y) \ formula" @@ -1270,7 +1298,7 @@ is_formula_N(**A, nth(x,env), nth(y,env))" apply (frule_tac x=y in lt_length_in_nat, assumption) apply (frule lt_length_in_nat, assumption) -apply (simp add: formula_N_fm_def is_formula_N_def sats_is_wfrec_fm sats_iterates_MH_fm) +apply (simp add: formula_N_fm_def is_formula_N_def sats_is_iterates_fm) done lemma formula_N_iff_sats: @@ -1282,9 +1310,9 @@ theorem formula_N_reflection: "REFLECTS[\x. is_formula_N(L, f(x), g(x)), \i x. is_formula_N(**Lset(i), f(x), g(x))]" -apply (simp only: is_formula_N_def setclass_simps) -apply (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection formula_functor_reflection) +apply (simp only: is_formula_N_def) +apply (intro FOL_reflections function_reflections + is_iterates_reflection formula_functor_reflection) done @@ -1317,7 +1345,7 @@ theorem mem_formula_reflection: "REFLECTS[\x. mem_formula(L,f(x)), \i x. mem_formula(**Lset(i),f(x))]" -apply (simp only: mem_formula_def setclass_simps) +apply (simp only: mem_formula_def) apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection) done @@ -1346,7 +1374,7 @@ theorem is_formula_reflection: "REFLECTS[\x. is_formula(L,f(x)), \i x. is_formula(**Lset(i),f(x))]" -apply (simp only: is_formula_def setclass_simps) +apply (simp only: is_formula_def) apply (intro FOL_reflections mem_formula_reflection) done @@ -1413,7 +1441,7 @@ \i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]" shows "REFLECTS[\x. is_transrec(L, MH(L,x), f(x), h(x)), \i x. is_transrec(**Lset(i), MH(**Lset(i),x), f(x), h(x))]" -apply (simp (no_asm_use) only: is_transrec_def setclass_simps) +apply (simp (no_asm_use) only: is_transrec_def) apply (intro FOL_reflections function_reflections MH_reflection is_wfrec_reflection is_eclose_reflection) done diff -r b0d8bad27f42 -r 95b95cdb4704 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Fri Oct 18 09:53:18 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Fri Oct 18 17:50:13 2002 +0200 @@ -337,8 +337,6 @@ subsection{*Internalized Formulas for some Set-Theoretic Concepts*} -lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex - subsubsection{*Some numbers to help write de Bruijn indices*} syntax @@ -383,7 +381,7 @@ theorem empty_reflection: "REFLECTS[\x. empty(L,f(x)), \i x. empty(**Lset(i),f(x))]" -apply (simp only: empty_def setclass_simps) +apply (simp only: empty_def) apply (intro FOL_reflections) done @@ -467,7 +465,7 @@ theorem pair_reflection: "REFLECTS[\x. pair(L,f(x),g(x),h(x)), \i x. pair(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: pair_def setclass_simps) +apply (simp only: pair_def) apply (intro FOL_reflections upair_reflection) done @@ -498,7 +496,7 @@ theorem union_reflection: "REFLECTS[\x. union(L,f(x),g(x),h(x)), \i x. union(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: union_def setclass_simps) +apply (simp only: union_def) apply (intro FOL_reflections) done @@ -530,7 +528,7 @@ theorem cons_reflection: "REFLECTS[\x. is_cons(L,f(x),g(x),h(x)), \i x. is_cons(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_cons_def setclass_simps) +apply (simp only: is_cons_def) apply (intro FOL_reflections upair_reflection union_reflection) done @@ -559,7 +557,7 @@ theorem successor_reflection: "REFLECTS[\x. successor(L,f(x),g(x)), \i x. successor(**Lset(i),f(x),g(x))]" -apply (simp only: successor_def setclass_simps) +apply (simp only: successor_def) apply (intro cons_reflection) done @@ -588,7 +586,7 @@ theorem number1_reflection: "REFLECTS[\x. number1(L,f(x)), \i x. number1(**Lset(i),f(x))]" -apply (simp only: number1_def setclass_simps) +apply (simp only: number1_def) apply (intro FOL_reflections empty_reflection successor_reflection) done @@ -620,7 +618,7 @@ theorem big_union_reflection: "REFLECTS[\x. big_union(L,f(x),g(x)), \i x. big_union(**Lset(i),f(x),g(x))]" -apply (simp only: big_union_def setclass_simps) +apply (simp only: big_union_def) apply (intro FOL_reflections) done @@ -641,7 +639,7 @@ theorem subset_reflection: "REFLECTS[\x. subset(L,f(x),g(x)), \i x. subset(**Lset(i),f(x),g(x))]" -apply (simp only: Relative.subset_def setclass_simps) +apply (simp only: Relative.subset_def) apply (intro FOL_reflections) done @@ -653,7 +651,7 @@ theorem transitive_set_reflection: "REFLECTS[\x. transitive_set(L,f(x)), \i x. transitive_set(**Lset(i),f(x))]" -apply (simp only: transitive_set_def setclass_simps) +apply (simp only: transitive_set_def) apply (intro FOL_reflections subset_reflection) done @@ -669,7 +667,7 @@ theorem ordinal_reflection: "REFLECTS[\x. ordinal(L,f(x)), \i x. ordinal(**Lset(i),f(x))]" -apply (simp only: ordinal_def setclass_simps) +apply (simp only: ordinal_def) apply (intro FOL_reflections transitive_set_reflection) done @@ -703,7 +701,7 @@ theorem membership_reflection: "REFLECTS[\x. membership(L,f(x),g(x)), \i x. membership(**Lset(i),f(x),g(x))]" -apply (simp only: membership_def setclass_simps) +apply (simp only: membership_def) apply (intro FOL_reflections pair_reflection) done @@ -737,7 +735,7 @@ theorem pred_set_reflection: "REFLECTS[\x. pred_set(L,f(x),g(x),h(x),b(x)), \i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]" -apply (simp only: pred_set_def setclass_simps) +apply (simp only: pred_set_def) apply (intro FOL_reflections pair_reflection) done @@ -772,7 +770,7 @@ theorem domain_reflection: "REFLECTS[\x. is_domain(L,f(x),g(x)), \i x. is_domain(**Lset(i),f(x),g(x))]" -apply (simp only: is_domain_def setclass_simps) +apply (simp only: is_domain_def) apply (intro FOL_reflections pair_reflection) done @@ -806,7 +804,7 @@ theorem range_reflection: "REFLECTS[\x. is_range(L,f(x),g(x)), \i x. is_range(**Lset(i),f(x),g(x))]" -apply (simp only: is_range_def setclass_simps) +apply (simp only: is_range_def) apply (intro FOL_reflections pair_reflection) done @@ -841,7 +839,7 @@ theorem field_reflection: "REFLECTS[\x. is_field(L,f(x),g(x)), \i x. is_field(**Lset(i),f(x),g(x))]" -apply (simp only: is_field_def setclass_simps) +apply (simp only: is_field_def) apply (intro FOL_reflections domain_reflection range_reflection union_reflection) done @@ -877,7 +875,7 @@ theorem image_reflection: "REFLECTS[\x. image(L,f(x),g(x),h(x)), \i x. image(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: Relative.image_def setclass_simps) +apply (simp only: Relative.image_def) apply (intro FOL_reflections pair_reflection) done @@ -912,7 +910,7 @@ theorem pre_image_reflection: "REFLECTS[\x. pre_image(L,f(x),g(x),h(x)), \i x. pre_image(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: Relative.pre_image_def setclass_simps) +apply (simp only: Relative.pre_image_def) apply (intro FOL_reflections pair_reflection) done @@ -947,7 +945,7 @@ theorem fun_apply_reflection: "REFLECTS[\x. fun_apply(L,f(x),g(x),h(x)), \i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: fun_apply_def setclass_simps) +apply (simp only: fun_apply_def) apply (intro FOL_reflections upair_reflection image_reflection big_union_reflection) done @@ -979,7 +977,7 @@ theorem is_relation_reflection: "REFLECTS[\x. is_relation(L,f(x)), \i x. is_relation(**Lset(i),f(x))]" -apply (simp only: is_relation_def setclass_simps) +apply (simp only: is_relation_def) apply (intro FOL_reflections pair_reflection) done @@ -1015,7 +1013,7 @@ theorem is_function_reflection: "REFLECTS[\x. is_function(L,f(x)), \i x. is_function(**Lset(i),f(x))]" -apply (simp only: is_function_def setclass_simps) +apply (simp only: is_function_def) apply (intro FOL_reflections pair_reflection) done @@ -1073,7 +1071,7 @@ theorem typed_function_reflection: "REFLECTS[\x. typed_function(L,f(x),g(x),h(x)), \i x. typed_function(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: typed_function_def setclass_simps) +apply (simp only: typed_function_def) apply (intro FOL_reflections function_reflections) done @@ -1113,7 +1111,7 @@ theorem composition_reflection: "REFLECTS[\x. composition(L,f(x),g(x),h(x)), \i x. composition(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: composition_def setclass_simps) +apply (simp only: composition_def) apply (intro FOL_reflections pair_reflection) done @@ -1153,7 +1151,7 @@ theorem injection_reflection: "REFLECTS[\x. injection(L,f(x),g(x),h(x)), \i x. injection(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: injection_def setclass_simps) +apply (simp only: injection_def) apply (intro FOL_reflections function_reflections typed_function_reflection) done @@ -1190,7 +1188,7 @@ theorem surjection_reflection: "REFLECTS[\x. surjection(L,f(x),g(x),h(x)), \i x. surjection(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: surjection_def setclass_simps) +apply (simp only: surjection_def) apply (intro FOL_reflections function_reflections typed_function_reflection) done @@ -1222,7 +1220,7 @@ theorem bijection_reflection: "REFLECTS[\x. bijection(L,f(x),g(x),h(x)), \i x. bijection(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: bijection_def setclass_simps) +apply (simp only: bijection_def) apply (intro And_reflection injection_reflection surjection_reflection) done @@ -1258,7 +1256,7 @@ theorem restriction_reflection: "REFLECTS[\x. restriction(L,f(x),g(x),h(x)), \i x. restriction(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: restriction_def setclass_simps) +apply (simp only: restriction_def) apply (intro FOL_reflections pair_reflection) done @@ -1308,7 +1306,7 @@ theorem order_isomorphism_reflection: "REFLECTS[\x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)), \i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]" -apply (simp only: order_isomorphism_def setclass_simps) +apply (simp only: order_isomorphism_def) apply (intro FOL_reflections function_reflections bijection_reflection) done @@ -1346,7 +1344,7 @@ theorem limit_ordinal_reflection: "REFLECTS[\x. limit_ordinal(L,f(x)), \i x. limit_ordinal(**Lset(i),f(x))]" -apply (simp only: limit_ordinal_def setclass_simps) +apply (simp only: limit_ordinal_def) apply (intro FOL_reflections ordinal_reflection empty_reflection successor_reflection) done @@ -1381,7 +1379,7 @@ theorem finite_ordinal_reflection: "REFLECTS[\x. finite_ordinal(L,f(x)), \i x. finite_ordinal(**Lset(i),f(x))]" -apply (simp only: finite_ordinal_def setclass_simps) +apply (simp only: finite_ordinal_def) apply (intro FOL_reflections ordinal_reflection limit_ordinal_reflection) done @@ -1413,7 +1411,7 @@ theorem omega_reflection: "REFLECTS[\x. omega(L,f(x)), \i x. omega(**Lset(i),f(x))]" -apply (simp only: omega_def setclass_simps) +apply (simp only: omega_def) apply (intro FOL_reflections limit_ordinal_reflection) done diff -r b0d8bad27f42 -r 95b95cdb4704 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Fri Oct 18 09:53:18 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Fri Oct 18 17:50:13 2002 +0200 @@ -68,7 +68,7 @@ lemma rtran_closure_mem_reflection: "REFLECTS[\x. rtran_closure_mem(L,f(x),g(x),h(x)), \i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: rtran_closure_mem_def setclass_simps) +apply (simp only: rtran_closure_mem_def) apply (intro FOL_reflections function_reflections fun_plus_reflections) done @@ -113,7 +113,7 @@ theorem rtran_closure_reflection: "REFLECTS[\x. rtran_closure(L,f(x),g(x)), \i x. rtran_closure(**Lset(i),f(x),g(x))]" -apply (simp only: rtran_closure_def setclass_simps) +apply (simp only: rtran_closure_def) apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection) done @@ -145,7 +145,7 @@ theorem tran_closure_reflection: "REFLECTS[\x. tran_closure(L,f(x),g(x)), \i x. tran_closure(**Lset(i),f(x),g(x))]" -apply (simp only: tran_closure_def setclass_simps) +apply (simp only: tran_closure_def) apply (intro FOL_reflections function_reflections rtran_closure_reflection composition_reflection) done @@ -229,26 +229,16 @@ lemma list_replacement2_Reflects: "REFLECTS - [\x. \u[L]. u \ B \ u \ nat \ - (\sn[L]. \msn[L]. successor(L, u, sn) \ membership(L, sn, msn) \ - is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0), - msn, u, x)), - \i x. \u \ Lset(i). u \ B \ u \ nat \ - (\sn \ Lset(i). \msn \ Lset(i). - successor(**Lset(i), u, sn) \ membership(**Lset(i), sn, msn) \ - is_wfrec (**Lset(i), - iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0), - msn, u, x))]" -by (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection list_functor_reflection) - + [\x. \u[L]. u \ B & u \ nat & + is_iterates(L, is_list_functor(L, A), 0, u, x), + \i x. \u \ Lset(i). u \ B & u \ nat & + is_iterates(**Lset(i), is_list_functor(**Lset(i), A), 0, u, x)]" +by (intro FOL_reflections + is_iterates_reflection list_functor_reflection) lemma list_replacement2: "L(A) ==> strong_replacement(L, - \n y. n\nat & - (\sn[L]. \msn[L]. successor(L,n,sn) & membership(L,sn,msn) & - is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0), - msn, n, y)))" + \n y. n\nat & is_iterates(L, is_list_functor(L,A), 0, n, y))" apply (rule strong_replacementI) apply (rename_tac B) apply (rule_tac u="{A,B,0,nat}" @@ -258,8 +248,7 @@ apply (rule DPow_LsetI) apply (rule bex_iff_sats conj_iff_sats)+ apply (rule_tac env = "[u,x,A,B,0,nat]" in mem_iff_sats) -apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats - is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ +apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+ done @@ -267,11 +256,13 @@ subsubsection{*Instances of Replacement for Formulas*} +(*FIXME: could prove a lemma iterates_replacementI to eliminate the +need to expand iterates_replacement and wfrec_replacement*) lemma formula_replacement1_Reflects: "REFLECTS - [\x. \u[L]. u \ B \ (\y[L]. pair(L,u,y,x) \ + [\x. \u[L]. u \ B & (\y[L]. pair(L,u,y,x) & is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)), - \i x. \u \ Lset(i). u \ B \ (\y \ Lset(i). pair(**Lset(i), u, y, x) \ + \i x. \u \ Lset(i). u \ B & (\y \ Lset(i). pair(**Lset(i), u, y, x) & is_wfrec(**Lset(i), iterates_MH(**Lset(i), is_formula_functor(**Lset(i)), 0), memsn, u, y))]" @@ -296,26 +287,16 @@ lemma formula_replacement2_Reflects: "REFLECTS - [\x. \u[L]. u \ B \ u \ nat \ - (\sn[L]. \msn[L]. successor(L, u, sn) \ membership(L, sn, msn) \ - is_wfrec (L, iterates_MH (L, is_formula_functor(L), 0), - msn, u, x)), - \i x. \u \ Lset(i). u \ B \ u \ nat \ - (\sn \ Lset(i). \msn \ Lset(i). - successor(**Lset(i), u, sn) \ membership(**Lset(i), sn, msn) \ - is_wfrec (**Lset(i), - iterates_MH (**Lset(i), is_formula_functor(**Lset(i)), 0), - msn, u, x))]" -by (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection formula_functor_reflection) - + [\x. \u[L]. u \ B & u \ nat & + is_iterates(L, is_formula_functor(L), 0, u, x), + \i x. \u \ Lset(i). u \ B & u \ nat & + is_iterates(**Lset(i), is_formula_functor(**Lset(i)), 0, u, x)]" +by (intro FOL_reflections + is_iterates_reflection formula_functor_reflection) lemma formula_replacement2: "strong_replacement(L, - \n y. n\nat & - (\sn[L]. \msn[L]. successor(L,n,sn) & membership(L,sn,msn) & - is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0), - msn, n, y)))" + \n y. n\nat & is_iterates(L, is_formula_functor(L), 0, n, y))" apply (rule strong_replacementI) apply (rename_tac B) apply (rule_tac u="{B,0,nat}" @@ -325,8 +306,7 @@ apply (rule DPow_LsetI) apply (rule bex_iff_sats conj_iff_sats)+ apply (rule_tac env = "[u,x,B,0,nat]" in mem_iff_sats) -apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats - is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ +apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+ done text{*NB The proofs for type @{term formula} are virtually identical to those @@ -335,18 +315,12 @@ subsubsection{*The Formula @{term is_nth}, Internalized*} -(* "is_nth(M,n,l,Z) == - \X[M]. \sn[M]. \msn[M]. - 2 1 0 - successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) & - is_hd(M,X,Z)" *) +(* "is_nth(M,n,l,Z) == + \X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" *) constdefs nth_fm :: "[i,i,i]=>i" "nth_fm(n,l,Z) == - Exists(Exists(Exists( - And(succ_fm(n#+3,1), - And(Memrel_fm(1,0), - And(is_wfrec_fm(iterates_MH_fm(tl_fm(1,0),l#+8,2,1,0), 0, n#+3, 2), hd_fm(2,Z#+3)))))))" + Exists(And(is_iterates_fm(tl_fm(1,0), succ(l), succ(n), 0), + hd_fm(0,succ(Z))))" lemma nth_fm_type [TC]: "[| x \ nat; y \ nat; z \ nat |] ==> nth_fm(x,y,z) \ formula" @@ -357,7 +331,7 @@ ==> sats(A, nth_fm(x,y,z), env) <-> is_nth(**A, nth(x,env), nth(y,env), nth(z,env))" apply (frule lt_length_in_nat, assumption) -apply (simp add: nth_fm_def is_nth_def sats_is_wfrec_fm sats_iterates_MH_fm) +apply (simp add: nth_fm_def is_nth_def sats_is_iterates_fm) done lemma nth_iff_sats: @@ -369,27 +343,29 @@ theorem nth_reflection: "REFLECTS[\x. is_nth(L, f(x), g(x), h(x)), \i x. is_nth(**Lset(i), f(x), g(x), h(x))]" -apply (simp only: is_nth_def setclass_simps) -apply (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection hd_reflection tl_reflection) +apply (simp only: is_nth_def) +apply (intro FOL_reflections is_iterates_reflection + hd_reflection tl_reflection) done subsubsection{*An Instance of Replacement for @{term nth}*} +(*FIXME: could prove a lemma iterates_replacementI to eliminate the +need to expand iterates_replacement and wfrec_replacement*) lemma nth_replacement_Reflects: "REFLECTS - [\x. \u[L]. u \ B \ (\y[L]. pair(L,u,y,x) \ + [\x. \u[L]. u \ B & (\y[L]. pair(L,u,y,x) & is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)), - \i x. \u \ Lset(i). u \ B \ (\y \ Lset(i). pair(**Lset(i), u, y, x) \ + \i x. \u \ Lset(i). u \ B & (\y \ Lset(i). pair(**Lset(i), u, y, x) & is_wfrec(**Lset(i), iterates_MH(**Lset(i), is_tl(**Lset(i)), z), memsn, u, y))]" by (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection list_functor_reflection tl_reflection) + iterates_MH_reflection tl_reflection) lemma nth_replacement: - "L(w) ==> iterates_replacement(L, %l t. is_tl(L,l,t), w)" + "L(w) ==> iterates_replacement(L, is_tl(L), w)" apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) apply (rule strong_replacementI) apply (rule_tac u="{A,n,w,Memrel(succ(n))}" @@ -439,9 +415,9 @@ lemma eclose_replacement1_Reflects: "REFLECTS - [\x. \u[L]. u \ B \ (\y[L]. pair(L,u,y,x) \ + [\x. \u[L]. u \ B & (\y[L]. pair(L,u,y,x) & is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)), - \i x. \u \ Lset(i). u \ B \ (\y \ Lset(i). pair(**Lset(i), u, y, x) \ + \i x. \u \ Lset(i). u \ B & (\y \ Lset(i). pair(**Lset(i), u, y, x) & is_wfrec(**Lset(i), iterates_MH(**Lset(i), big_union(**Lset(i)), A), memsn, u, y))]" @@ -466,26 +442,15 @@ lemma eclose_replacement2_Reflects: "REFLECTS - [\x. \u[L]. u \ B \ u \ nat \ - (\sn[L]. \msn[L]. successor(L, u, sn) \ membership(L, sn, msn) \ - is_wfrec (L, iterates_MH (L, big_union(L), A), - msn, u, x)), - \i x. \u \ Lset(i). u \ B \ u \ nat \ - (\sn \ Lset(i). \msn \ Lset(i). - successor(**Lset(i), u, sn) \ membership(**Lset(i), sn, msn) \ - is_wfrec (**Lset(i), - iterates_MH (**Lset(i), big_union(**Lset(i)), A), - msn, u, x))]" -by (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection) - + [\x. \u[L]. u \ B & u \ nat & + is_iterates(L, big_union(L), A, u, x), + \i x. \u \ Lset(i). u \ B & u \ nat & + is_iterates(**Lset(i), big_union(**Lset(i)), A, u, x)]" +by (intro FOL_reflections function_reflections is_iterates_reflection) lemma eclose_replacement2: "L(A) ==> strong_replacement(L, - \n y. n\nat & - (\sn[L]. \msn[L]. successor(L,n,sn) & membership(L,sn,msn) & - is_wfrec(L, iterates_MH(L,big_union(L), A), - msn, n, y)))" + \n y. n\nat & is_iterates(L, big_union(L), A, n, y))" apply (rule strong_replacementI) apply (rename_tac B) apply (rule_tac u="{A,B,nat}" @@ -494,8 +459,7 @@ apply (rule DPow_LsetI) apply (rule bex_iff_sats conj_iff_sats)+ apply (rule_tac env = "[u,x,A,B,nat]" in mem_iff_sats) -apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats - is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+ +apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+ done diff -r b0d8bad27f42 -r 95b95cdb4704 src/ZF/Constructible/Satisfies_absolute.thy --- a/src/ZF/Constructible/Satisfies_absolute.thy Fri Oct 18 09:53:18 2002 +0200 +++ b/src/ZF/Constructible/Satisfies_absolute.thy Fri Oct 18 17:50:13 2002 +0200 @@ -45,7 +45,7 @@ theorem depth_reflection: "REFLECTS[\x. is_depth(L, f(x), g(x)), \i x. is_depth(**Lset(i), f(x), g(x))]" -apply (simp only: is_depth_def setclass_simps) +apply (simp only: is_depth_def) apply (intro FOL_reflections function_reflections formula_N_reflection) done @@ -161,7 +161,7 @@ \i x. is_d(**Lset(i), h(x), f(x), g(x))]" shows "REFLECTS[\x. is_formula_case(L, is_a(L,x), is_b(L,x), is_c(L,x), is_d(L,x), g(x), h(x)), \i x. is_formula_case(**Lset(i), is_a(**Lset(i), x), is_b(**Lset(i), x), is_c(**Lset(i), x), is_d(**Lset(i), x), g(x), h(x))]" -apply (simp (no_asm_use) only: is_formula_case_def setclass_simps) +apply (simp (no_asm_use) only: is_formula_case_def) apply (intro FOL_reflections function_reflections finite_ordinal_reflection mem_formula_reflection Member_reflection Equal_reflection Nand_reflection Forall_reflection @@ -530,7 +530,7 @@ lemma depth_apply_reflection: "REFLECTS[\x. is_depth_apply(L,f(x),g(x),h(x)), \i x. is_depth_apply(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_depth_apply_def setclass_simps) +apply (simp only: is_depth_apply_def) apply (intro FOL_reflections function_reflections depth_reflection finite_ordinal_reflection) done