# HG changeset patch # User paulson # Date 1028021997 -7200 # Node ID 78b93a667c0151d8e785144b247aa7087b4bcd4f # Parent 47fe2d1ec99973bf585896af67885359fad6274a better sats rules for higher-order operators diff -r 47fe2d1ec999 -r 78b93a667c01 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Tue Jul 30 11:38:33 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Tue Jul 30 11:39:57 2002 +0200 @@ -248,15 +248,17 @@ done +lemma reflection_Lset: "reflection(Lset)" +apply (blast intro: reflection.intro Lset_mono_le Lset_cont Pair_in_Lset) + +done + theorem Ex_reflection: "REFLECTS[\x. P(fst(x),snd(x)), \a x. Q(a,fst(x),snd(x))] ==> REFLECTS[\x. \z. L(z) \ P(x,z), \a x. \z\Lset(a). Q(a,x,z)]" apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) apply (elim meta_exE) apply (rule meta_exI) -apply (rule reflection.Ex_reflection - [OF reflection.intro, OF Lset_mono_le Lset_cont Pair_in_Lset], - assumption+) +apply (erule reflection.Ex_reflection [OF reflection_Lset]) done theorem All_reflection: @@ -265,9 +267,7 @@ apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) apply (elim meta_exE) apply (rule meta_exI) -apply (rule reflection.All_reflection - [OF reflection.intro, OF Lset_mono_le Lset_cont Pair_in_Lset], - assumption+) +apply (erule reflection.All_reflection [OF reflection_Lset]) done theorem Rex_reflection: diff -r 47fe2d1ec999 -r 78b93a667c01 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Tue Jul 30 11:38:33 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Tue Jul 30 11:39:57 2002 +0200 @@ -239,8 +239,9 @@ xa \ r & MH(x, f_r_sx, y))" *) -constdefs is_recfun_fm :: "[[i,i,i]=>i, i, i, i]=>i" - "is_recfun_fm(p,r,a,f) == +text{*The three arguments of @{term p} are always 5, 0, 4.*} +constdefs is_recfun_fm :: "[i, i, i, i]=>i" + "is_recfun_fm(p,r,a,f) == Forall(Iff(Member(0,succ(f)), Exists(Exists(Exists(Exists(Exists(Exists( And(pair_fm(5,4,6), @@ -248,54 +249,54 @@ And(upair_fm(5,5,2), And(pre_image_fm(r#+7,2,1), And(restriction_fm(f#+7,1,0), - And(Member(3,r#+7), p(5,0,4)))))))))))))))" + And(Member(3,r#+7), p))))))))))))))" -lemma is_recfun_type_0: - "[| !!x y z. [| x \ nat; y \ nat; z \ nat |] ==> p(x,y,z) \ formula; - x \ nat; y \ nat; z \ nat |] - ==> is_recfun_fm(p,x,y,z) \ formula" -apply (unfold is_recfun_fm_def) -(*FIXME: FIND OUT why simp loops!*) -apply typecheck -by simp - lemma is_recfun_type [TC]: - "[| p(5,0,4) \ formula; - x \ nat; y \ nat; z \ nat |] + "[| p \ formula; x \ nat; y \ nat; z \ nat |] ==> is_recfun_fm(p,x,y,z) \ formula" by (simp add: is_recfun_fm_def) -lemma arity_is_recfun_fm [simp]: - "[| arity(p(5,0,4)) le 8; x \ nat; y \ nat; z \ nat |] - ==> arity(is_recfun_fm(p,x,y,z)) = succ(x) \ succ(y) \ succ(z)" -apply (frule lt_nat_in_nat, simp) -apply (simp add: is_recfun_fm_def succ_Un_distrib [symmetric] ) -apply (subst subset_Un_iff2 [of "arity(p(5,0,4))", THEN iffD1]) -apply (rule le_imp_subset) -apply (erule le_trans, simp) -apply (simp add: succ_Un_distrib [symmetric] Un_ac) -done - lemma sats_is_recfun_fm: - assumes MH_iff_sats: - "!!x y z env. - [| x \ nat; y \ nat; z \ nat; env \ list(A)|] - ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> sats(A, p(x,y,z), env)" - shows + assumes MH_iff_sats: + "!!a0 a1 a2 a3 a4 a5 a6. + [|a0\A; a1\A; a2\A; a3\A; a4\A; a5\A; a6\A|] ==> + MH(a5, a0, a4) <-> + sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,Cons(a5,Cons(a6,env))))))))" + shows "[|x \ nat; y \ nat; z \ nat; env \ list(A)|] ==> sats(A, is_recfun_fm(p,x,y,z), env) <-> M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))" by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym]) +(* +apply (rule ball_cong bex_cong iff_cong conj_cong refl iff_refl) + + sats(A, p, + Cons(xf, Cons(xe, Cons(xd, Cons(xc, Cons(xb, Cons(xaa, Cons(xa, env)))))))) +\ MH(xaa, xf, xb) + +MH(nth(5,env), nth(0,env), nth(4,env)) <-> sats(A, p, env); +*) + +(* "!!x y z. [|x\A; y\A; z\A|] ==> MH(x,y,z) <-> sats(A, p, env)" +*) lemma is_recfun_iff_sats: - "[| (!!x y z env. [| x \ nat; y \ nat; z \ nat; env \ list(A)|] - ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> - sats(A, p(x,y,z), env)); - nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + assumes MH_iff_sats: + "!!a0 a1 a2 a3 a4 a5 a6. + [|a0\A; a1\A; a2\A; a3\A; a4\A; a5\A; a6\A|] ==> + MH(a5, a0, a4) <-> + sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,Cons(a5,Cons(a6,env))))))))" + shows + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; i \ nat; j \ nat; k \ nat; env \ list(A)|] ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" -by (simp add: sats_is_recfun_fm [of A MH]) +apply (rule iff_sym) +apply (rule iff_trans) +apply (rule sats_is_recfun_fm [of A MH]) +apply (rule MH_iff_sats, simp_all) +done +(*FIXME: surely proof can be improved?*) + theorem is_recfun_reflection: assumes MH_reflection: @@ -588,6 +589,9 @@ subsubsection{*The Operator @{term is_nat_case}*} +text{*I could not get it to work with the more natural assumption that + @{term is_b} takes two arguments. Instead it must be a formula where 1 and 0 + stand for @{term m} and @{term b}, respectively.*} (* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" "is_nat_case(M, a, is_b, k, z) == @@ -595,36 +599,24 @@ (\m[M]. successor(M,m,k) --> is_b(m,z)) & (is_quasinat(M,k) | empty(M,z))" *) text{*The formula @{term is_b} has free variables 1 and 0.*} -constdefs is_nat_case_fm :: "[i, [i,i]=>i, i, i]=>i" - "is_nat_case_fm(a,is_b,k,z) == +constdefs is_nat_case_fm :: "[i, i, i, i]=>i" + "is_nat_case_fm(a,is_b,k,z) == And(Implies(empty_fm(k), Equal(z,a)), - And(Forall(Implies(succ_fm(0,succ(k)), - Forall(Implies(Equal(0,succ(succ(z))), is_b(1,0))))), + And(Forall(Implies(succ_fm(0,succ(k)), + Forall(Implies(Equal(0,succ(succ(z))), is_b)))), Or(quasinat_fm(k), empty_fm(z))))" lemma is_nat_case_type [TC]: - "[| is_b(1,0) \ formula; - x \ nat; y \ nat; z \ nat |] + "[| is_b \ formula; + x \ nat; y \ nat; z \ nat |] ==> is_nat_case_fm(x,is_b,y,z) \ formula" by (simp add: is_nat_case_fm_def) -lemma arity_is_nat_case_fm [simp]: - "[| is_b(1,0) \ formula; x \ nat; y \ nat; z \ nat |] - ==> arity(is_nat_case_fm(x,is_b,y,z)) = - succ(x) \ succ(y) \ succ(z) \ (arity(is_b(1,0)) #- 2)" -apply (subgoal_tac "arity(is_b(1,0)) \ nat") -apply typecheck -(*FIXME: could nat_diff_split work?*) -apply (auto simp add: diff_def raw_diff_succ is_nat_case_fm_def nat_imp_quasinat - succ_Un_distrib [symmetric] Un_ac - split: split_nat_case) -done - lemma sats_is_nat_case_fm: - assumes is_b_iff_sats: - "!!a b. [| a \ A; b \ A|] - ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env)))" - shows + assumes is_b_iff_sats: + "!!a. a \ A ==> is_b(a,nth(z, env)) <-> + sats(A, p, Cons(nth(z,env), Cons(a, env)))" + shows "[|x \ nat; y \ nat; z < length(env); env \ list(A)|] ==> sats(A, is_nat_case_fm(x,p,y,z), env) <-> is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))" @@ -633,9 +625,9 @@ done lemma is_nat_case_iff_sats: - "[| (!!a b. [| a \ A; b \ A|] - ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env)))); - nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + "[| (!!a. a \ A ==> is_b(a,z) <-> + sats(A, p, Cons(z, Cons(a,env)))); + nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; i \ nat; j \ nat; k < length(env); env \ list(A)|] ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)" by (simp add: sats_is_nat_case_fm [of A is_b]) @@ -663,59 +655,51 @@ "iterates_MH(M,isF,v,n,g,z) == is_nat_case(M, v, \m u. \gm[M]. fun_apply(M,g,m,gm) & isF(gm,u), n, z)" *) -constdefs iterates_MH_fm :: "[[i,i]=>i, i, i, i, i]=>i" - "iterates_MH_fm(isF,v,n,g,z) == - is_nat_case_fm(v, - \m u. Exists(And(fun_apply_fm(succ(succ(succ(g))),succ(m),0), - Forall(Implies(Equal(0,succ(succ(u))), isF(1,0))))), +constdefs iterates_MH_fm :: "[i, i, i, i, i]=>i" + "iterates_MH_fm(isF,v,n,g,z) == + is_nat_case_fm(v, + Exists(And(fun_apply_fm(succ(succ(succ(g))),2,0), + Forall(Implies(Equal(0,2), isF)))), n, z)" lemma iterates_MH_type [TC]: - "[| p(1,0) \ formula; - v \ nat; x \ nat; y \ nat; z \ nat |] + "[| p \ formula; + v \ nat; x \ nat; y \ nat; z \ nat |] ==> iterates_MH_fm(p,v,x,y,z) \ formula" by (simp add: iterates_MH_fm_def) - -lemma arity_iterates_MH_fm [simp]: - "[| p(1,0) \ formula; - v \ nat; x \ nat; y \ nat; z \ nat |] - ==> arity(iterates_MH_fm(p,v,x,y,z)) = - succ(v) \ succ(x) \ succ(y) \ succ(z) \ (arity(p(1,0)) #- 4)" -apply (subgoal_tac "arity(p(1,0)) \ nat") -apply typecheck -apply (simp add: nat_imp_quasinat iterates_MH_fm_def Un_ac - split: split_nat_case, clarify) -apply (rename_tac i j) -apply (drule eq_succ_imp_eq_m1, simp) -apply (drule eq_succ_imp_eq_m1, simp) -apply (simp add: diff_Un_distrib succ_Un_distrib Un_ac diff_diff_left) -done - lemma sats_iterates_MH_fm: assumes is_F_iff_sats: "!!a b c d. [| a \ A; b \ A; c \ A; d \ A|] ==> is_F(a,b) <-> - sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env)))))" - shows + sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))" + shows "[|v \ nat; x \ nat; y \ nat; z < length(env); env \ list(A)|] ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <-> iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))" -by (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm +apply (frule lt_length_in_nat, assumption) +apply (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm is_F_iff_sats [symmetric]) +apply (rule is_nat_case_cong) +apply (simp_all add: setclass_def) +done + lemma iterates_MH_iff_sats: "[| (!!a b c d. [| a \ A; b \ A; c \ A; d \ A|] ==> is_F(a,b) <-> - sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env)))))); - nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))); + nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; i' \ nat; i \ nat; j \ nat; k < length(env); env \ list(A)|] ==> iterates_MH(**A, is_F, v, x, y, z) <-> sats(A, iterates_MH_fm(p,i',i,j,k), env)" -apply (rule iff_sym) +apply (rule iff_sym) apply (rule iff_trans) -apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all) +apply (rule sats_iterates_MH_fm [of A is_F], blast) +apply simp_all done +(*FIXME: surely proof can be improved?*) + theorem iterates_MH_reflection: assumes p_reflection: @@ -811,12 +795,11 @@ apply (rule bex_iff_sats conj_iff_sats)+ apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats) apply (rule sep_rules | simp)+ -txt{*Can't get sat rules to work for higher-order operators, so just expand them!*} -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def) -apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+ +apply (simp add: is_wfrec_def) +apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats + is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done - lemma list_replacement2_Reflects: "REFLECTS [\x. \u[L]. u \ B \ u \ nat \ @@ -855,8 +838,9 @@ apply (rule bex_iff_sats conj_iff_sats)+ apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats) apply (rule sep_rules | simp)+ -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def) -apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+ +apply (simp add: is_wfrec_def) +apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats + is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done @@ -936,10 +920,9 @@ apply (rule bex_iff_sats conj_iff_sats)+ apply (rule_tac env = "[u,v,n,B,0,Memrel(succ(n))]" in mem_iff_sats) apply (rule sep_rules | simp)+ -txt{*Can't get sat rules to work for higher-order operators, so just expand them!*} -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def) -apply (rule sep_rules formula_functor_iff_sats quasinat_iff_sats | simp)+ -txt{*SLOW: like 40 seconds!*} +apply (simp add: is_wfrec_def) +apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats + is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done lemma formula_replacement2_Reflects: @@ -980,8 +963,9 @@ apply (rule bex_iff_sats conj_iff_sats)+ apply (rule_tac env = "[u,v,B,0,nat]" in mem_iff_sats) apply (rule sep_rules | simp)+ -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def) -apply (rule sep_rules formula_functor_iff_sats quasinat_iff_sats | simp)+ +apply (simp add: is_wfrec_def) +apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats + is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done text{*NB The proofs for type @{term formula} are virtually identical to those @@ -1206,8 +1190,9 @@ apply (rule bex_iff_sats conj_iff_sats)+ apply (rule_tac env = "[u,v,A,z,w,Memrel(succ(n))]" in mem_iff_sats) apply (rule sep_rules | simp)+ -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def) -apply (rule sep_rules quasinat_iff_sats tl_iff_sats | simp)+ +apply (simp add: is_wfrec_def) +apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats + is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done @@ -1271,9 +1256,9 @@ apply (rule bex_iff_sats conj_iff_sats)+ apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats) apply (rule sep_rules | simp)+ -txt{*Can't get sat rules to work for higher-order operators, so just expand them!*} -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def) -apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+ +apply (simp add: is_wfrec_def) +apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats + is_recfun_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+ done @@ -1314,8 +1299,9 @@ apply (rule bex_iff_sats conj_iff_sats)+ apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats) apply (rule sep_rules | simp)+ -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def) -apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+ +apply (simp add: is_wfrec_def) +apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats + is_recfun_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+ done diff -r 47fe2d1ec999 -r 78b93a667c01 src/ZF/Constructible/Reflection.thy --- a/src/ZF/Constructible/Reflection.thy Tue Jul 30 11:38:33 2002 +0200 +++ b/src/ZF/Constructible/Reflection.thy Tue Jul 30 11:39:57 2002 +0200 @@ -40,13 +40,20 @@ defines "F0(P,y) == \b. (\z. M(z) \ P()) --> (\z\Mset(b). P())" and "FF(P) == \a. \y\Mset(a). F0(P,y)" - and "ClEx(P) == \a. Limit(a) \ normalize(FF(P),a) = a" + and "ClEx(P,a) == Limit(a) \ normalize(FF(P),a) = a" lemma (in reflection) Mset_mono: "i\j ==> Mset(i) <= Mset(j)" apply (insert Mset_mono_le) apply (simp add: mono_le_subset_def leI) done +text{*Awkward: we need a version of @{text ClEx_def} as an equality + at the level of classes, which do not really exist*} +lemma (in reflection) ClEx_eq: + "ClEx(P) == \a. Limit(a) \ normalize(FF(P),a) = a" +by (simp add: ClEx_def [symmetric]) + + subsection{*Easy Cases of the Reflection Theorem*} theorem (in reflection) Triv_reflection [intro]: @@ -157,7 +164,7 @@ text{*...and it is closed and unbounded*} lemma (in ex_reflection) ZF_Closed_Unbounded_ClEx: "Closed_Unbounded(ClEx(P))" -apply (simp add: ClEx_def) +apply (simp add: ClEx_eq) apply (fast intro: Closed_Unbounded_Int Normal_imp_fp_Closed_Unbounded Closed_Unbounded_Limit Normal_normalize) done @@ -176,13 +183,20 @@ apply (simp_all add: Mset_mono_le Mset_cont Pair_in_Mset) done +(*Alternative proof, less unfolding: +apply (rule Reflection.ZF_ClEx_iff [of Mset _ _ Cl, folded M_def]) +apply (fold ClEx_def FF_def F0_def) +apply (rule ex_reflection.intro, assumption) +apply (simp add: ex_reflection_axioms.intro, assumption+) +*) + lemma (in reflection) Closed_Unbounded_ClEx: "(!!a. [| Cl(a); Ord(a) |] ==> \x\Mset(a). P(x) <-> Q(a,x)) ==> Closed_Unbounded(ClEx(P))" -apply (unfold ClEx_def FF_def F0_def M_def) -apply (rule ex_reflection.ZF_Closed_Unbounded_ClEx - [OF ex_reflection.intro, OF reflection.intro ex_reflection_axioms.intro]) -apply (simp_all add: Mset_mono_le Mset_cont Pair_in_Mset) +apply (unfold ClEx_eq FF_def F0_def M_def) +apply (rule Reflection.ZF_Closed_Unbounded_ClEx [of Mset _ _ Cl]) +apply (rule ex_reflection.intro, assumption) +apply (blast intro: ex_reflection_axioms.intro) done subsection{*Packaging the Quantifier Reflection Rules*} diff -r 47fe2d1ec999 -r 78b93a667c01 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Tue Jul 30 11:38:33 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Tue Jul 30 11:39:57 2002 +0200 @@ -746,7 +746,7 @@ (*NOT for the simplifier. The assumption M(z') is apparently necessary, but causes the error "Failed congruence proof!" It may be better to replace is_nat_case by nat_case before attempting congruence reasoning.*) -lemma (in M_triv_axioms) is_nat_case_cong: +lemma is_nat_case_cong: "[| a = a'; k = k'; z = z'; M(z'); !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |] ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"