# HG changeset patch # User paulson # Date 1028218966 -7200 # Node ID d6d6206392435591d62b67cca208dab7d049ae9c # Parent cdde97e1db1cf6a69ca9f8a61794e4ac2468d937 better satisfies rules for is_recfun A satisfies rule for is_wfrec! diff -r cdde97e1db1c -r d6d620639243 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Wed Jul 31 18:30:25 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Thu Aug 01 18:22:46 2002 +0200 @@ -237,63 +237,69 @@ subsection{*Well-Founded Recursion!*} + +text{*Alternative definition, minimizing nesting of quantifiers around MH*} +lemma M_is_recfun_iff: + "M_is_recfun(M,MH,r,a,f) <-> + (\z[M]. z \ f <-> + (\x[M]. \f_r_sx[M]. \y[M]. + MH(x, f_r_sx, y) & pair(M,x,y,z) & + (\xa[M]. \sx[M]. \r_sx[M]. + pair(M,x,a,xa) & upair(M,x,x,sx) & + pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) & + xa \ r)))" +apply (simp add: M_is_recfun_def) +apply (rule rall_cong, blast) +done + + (* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o" "M_is_recfun(M,MH,r,a,f) == \z[M]. z \ f <-> - 5 4 3 2 1 0 - (\x[M]. \y[M]. \xa[M]. \sx[M]. \r_sx[M]. \f_r_sx[M]. - pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) & + 2 1 0 +new def (\x[M]. \f_r_sx[M]. \y[M]. + MH(x, f_r_sx, y) & pair(M,x,y,z) & + (\xa[M]. \sx[M]. \r_sx[M]. + pair(M,x,a,xa) & upair(M,x,x,sx) & pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) & - xa \ r & MH(x, f_r_sx, y))" + xa \ r)" *) -text{*The three arguments of @{term p} are always 5, 0, 4.*} +text{*The three arguments of @{term p} are always 2, 1, 0 and z*} 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), - And(pair_fm(5,a#+7,3), - 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))))))))))))))" - + Exists(Exists(Exists( + And(p, + And(pair_fm(2,0,3), + Exists(Exists(Exists( + And(pair_fm(5,a#+7,2), + And(upair_fm(5,5,1), + And(pre_image_fm(r#+7,1,0), + And(restriction_fm(f#+7,0,4), Member(2,r#+7)))))))))))))))" lemma is_recfun_type [TC]: "[| p \ formula; x \ nat; y \ nat; z \ nat |] ==> is_recfun_fm(p,x,y,z) \ formula" by (simp add: is_recfun_fm_def) + lemma sats_is_recfun_fm: 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))))))))" + "!!a0 a1 a2 a3. + [|a0\A; a1\A; a2\A; a3\A|] + ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,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)" -*) +by (simp add: is_recfun_fm_def M_is_recfun_iff MH_iff_sats [THEN iff_sym]) lemma is_recfun_iff_sats: 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))))))))" + "!!a0 a1 a2 a3. + [|a0\A; a1\A; a2\A; a3\A|] + ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))" shows "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; i \ nat; j \ nat; k \ nat; env \ list(A)|] @@ -320,9 +326,56 @@ restriction_reflection MH_reflection) done -text{*Currently, @{text sats}-theorems for higher-order operators don't seem -useful. Reflection theorems do work, though. This one avoids the repetition -of the @{text MH}-term. *} +subsubsection{*The Operator @{term is_wfrec}*} + +text{*The three arguments of @{term p} are always 2, 1, 0*} + +(* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o" + "is_wfrec(M,MH,r,a,z) == + \f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" *) +constdefs is_wfrec_fm :: "[i, i, i, i]=>i" + "is_wfrec_fm(p,r,a,z) == + Exists(And(is_recfun_fm(p, succ(r), succ(a), 0), + Exists(Exists(Exists(Exists( + And(Equal(2,a#+5), And(Equal(1,4), And(Equal(0,z#+5), p)))))))))" + +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.*} + +text{*There's an additional existential quantifier to ensure that the + environments in both calls to MH have the same length.*} + +lemma is_wfrec_type [TC]: + "[| p \ formula; x \ nat; y \ nat; z \ nat |] + ==> is_wfrec_fm(p,x,y,z) \ formula" +by (simp add: is_wfrec_fm_def) + +lemma sats_is_wfrec_fm: + assumes MH_iff_sats: + "!!a0 a1 a2 a3 a4. + [|a0\A; a1\A; a2\A; a3\A; a4\A|] + ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))" + shows + "[|x \ nat; y < length(env); z < length(env); env \ list(A)|] + ==> sats(A, is_wfrec_fm(p,x,y,z), env) <-> + is_wfrec(**A, MH, 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_wfrec_fm_def sats_is_recfun_fm is_wfrec_def MH_iff_sats [THEN iff_sym], blast) +done + + +lemma is_wfrec_iff_sats: + assumes MH_iff_sats: + "!!a0 a1 a2 a3 a4. + [|a0\A; a1\A; a2\A; a3\A; a4\A|] + ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,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_wfrec(**A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)" +by (simp add: sats_is_wfrec_fm [OF MH_iff_sats]) + theorem is_wfrec_reflection: assumes MH_reflection: "!!f' f g h. REFLECTS[\x. MH(L, f'(x), f(x), g(x), h(x)), @@ -360,6 +413,7 @@ apply (rename_tac u) apply (rule ball_iff_sats imp_iff_sats)+ apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats) +apply (rule sep_rules | simp)+ apply (rule sep_rules is_recfun_iff_sats | simp)+ done @@ -401,7 +455,7 @@ apply (rename_tac u) apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+ apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats) -apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+ +apply (rule sep_rules list.intros app_type tran_closure_iff_sats is_recfun_iff_sats | simp)+ done @@ -710,8 +764,7 @@ sats(A, iterates_MH_fm(p,i',i,j,k), env)" apply (rule iff_sym) apply (rule iff_trans) -apply (rule sats_iterates_MH_fm [of A is_F], blast) -apply simp_all +apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all) done (*FIXME: surely proof can be improved?*) @@ -790,6 +843,7 @@ by (intro FOL_reflections function_reflections is_wfrec_reflection iterates_MH_reflection list_functor_reflection) + lemma list_replacement1: "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)" apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) @@ -809,12 +863,11 @@ apply (rename_tac v) 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)+ -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)+ + is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done + lemma list_replacement2_Reflects: "REFLECTS [\x. \u[L]. u \ B \ u \ nat \ @@ -852,10 +905,8 @@ apply (rename_tac v) 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) 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)+ + is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done @@ -934,10 +985,8 @@ apply (rename_tac v) 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)+ -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)+ + is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done lemma formula_replacement2_Reflects: @@ -977,10 +1026,8 @@ apply (rename_tac v) 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) 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)+ + is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done text{*NB The proofs for type @{term formula} are virtually identical to those @@ -1239,8 +1286,7 @@ 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 (intro FOL_reflections function_reflections) -apply assumption+ +apply (intro FOL_reflections function_reflections, assumption+) done @@ -1274,10 +1320,8 @@ apply (rename_tac v) 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) apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats - is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ + is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done @@ -1295,7 +1339,7 @@ theorem M_datatypes_L: "PROP M_datatypes(L)" apply (rule M_datatypes.intro) apply (rule M_wfrank.axioms [OF M_wfrank_L])+ - apply (rule M_datatypes_axioms_L); + apply (rule M_datatypes_axioms_L) done lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L] @@ -1344,10 +1388,8 @@ apply (rename_tac v) 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)+ -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)+ + is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+ done @@ -1387,10 +1429,8 @@ apply (rename_tac v) 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) 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)+ + is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+ done