# HG changeset patch # User paulson # Date 1028119240 -7200 # Node ID 01b3fc0cc1b893948f216b15cc81d9fae3678a46 # Parent 8fd1d803a3d3703568830fa5c3a6e460dfb39c47 separate "axioms" proofs: more flexible for locale reasoning diff -r 8fd1d803a3d3 -r 01b3fc0cc1b8 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Wed Jul 31 14:39:47 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Wed Jul 31 14:40:40 2002 +0200 @@ -1,3 +1,10 @@ +(* Title: ZF/Constructible/Rec_Separation.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2002 University of Cambridge + +FIXME: define nth_fm and prove its "sats" theorem +*) header {*Separation for Facts About Recursion*} @@ -199,14 +206,15 @@ subsubsection{*Instantiating the locale @{text M_trancl}*} -theorem M_trancl_L: "PROP M_trancl(L)" - apply (rule M_trancl.intro) - apply (rule M_axioms.axioms [OF M_axioms_L])+ +lemma M_trancl_axioms_L: "M_trancl_axioms(L)" apply (rule M_trancl_axioms.intro) - apply (assumption | rule - rtrancl_separation wellfounded_trancl_separation)+ + apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+ done +theorem M_trancl_L: "PROP M_trancl(L)" +by (rule M_trancl.intro + [OF M_triv_axioms_L M_axioms_axioms_L M_trancl_axioms_L]) + lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L] and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L] and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L] @@ -298,12 +306,15 @@ (*FIXME: surely proof can be improved?*) +text{*The additional variable in the premise, namely @{term f'}, is essential. +It lets @{term MH} depend upon @{term x}, which seems often necessary. +The same thing occurs in @{text is_wfrec_reflection}.*} theorem is_recfun_reflection: assumes MH_reflection: - "!!f g h. REFLECTS[\x. MH(L, f(x), g(x), h(x)), - \i x. MH(**Lset(i), f(x), g(x), h(x))]" - shows "REFLECTS[\x. M_is_recfun(L, MH(L), f(x), g(x), h(x)), - \i x. M_is_recfun(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]" + "!!f' f g h. REFLECTS[\x. MH(L, f'(x), f(x), g(x), h(x)), + \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 (intro FOL_reflections function_reflections restriction_reflection MH_reflection) @@ -311,13 +322,13 @@ 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.*} +of the @{text MH}-term. *} theorem is_wfrec_reflection: assumes MH_reflection: - "!!f g h. REFLECTS[\x. MH(L, f(x), g(x), h(x)), - \i x. MH(**Lset(i), f(x), g(x), h(x))]" - shows "REFLECTS[\x. is_wfrec(L, MH(L), f(x), g(x), h(x)), - \i x. is_wfrec(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]" + "!!f' f g h. REFLECTS[\x. MH(L, f'(x), f(x), g(x), h(x)), + \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 (intro FOL_reflections MH_reflection is_recfun_reflection) done @@ -435,12 +446,16 @@ subsubsection{*Instantiating the locale @{text M_wfrank}*} +lemma M_wfrank_axioms_L: "M_wfrank_axioms(L)" + apply (rule M_wfrank_axioms.intro) + apply (assumption | rule + wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+ + done + theorem M_wfrank_L: "PROP M_wfrank(L)" apply (rule M_wfrank.intro) apply (rule M_trancl.axioms [OF M_trancl_L])+ - apply (rule M_wfrank_axioms.intro) - apply (assumption | rule - wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+ + apply (rule M_wfrank_axioms_L) done lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L] @@ -1123,6 +1138,42 @@ subsection{*Absoluteness for the Function @{term nth}*} +subsubsection{*The Formula @{term is_hd}, Internalized*} + +(* "is_hd(M,xs,H) == + (is_Nil(M,xs) --> empty(M,H)) & + (\x[M]. \l[M]. ~ is_Cons(M,x,l,xs) | H=x) & + (is_quasilist(M,xs) | empty(M,H))" *) +constdefs hd_fm :: "[i,i]=>i" + "hd_fm(xs,H) == + And(Implies(Nil_fm(xs), empty_fm(H)), + And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(H#+2,1)))), + Or(quasilist_fm(xs), empty_fm(H))))" + +lemma hd_type [TC]: + "[| x \ nat; y \ nat |] ==> hd_fm(x,y) \ formula" +by (simp add: hd_fm_def) + +lemma sats_hd_fm [simp]: + "[| x \ nat; y \ nat; env \ list(A)|] + ==> sats(A, hd_fm(x,y), env) <-> is_hd(**A, nth(x,env), nth(y,env))" +by (simp add: hd_fm_def is_hd_def) + +lemma hd_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; j \ nat; env \ list(A)|] + ==> is_hd(**A, x, y) <-> sats(A, hd_fm(i,j), env)" +by simp + +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 (intro FOL_reflections Nil_reflection Cons_reflection + quasilist_reflection empty_reflection) +done + + subsubsection{*The Formula @{term is_tl}, Internalized*} (* "is_tl(M,xs,T) == @@ -1159,6 +1210,38 @@ done +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)" +constdefs nth_fm :: "[i,i,i]=>i" + "nth_fm(n,l,Z) == + Exists(Exists(Exists( + And(successor_fm(n#+3,1), + And(membership_fm(1,0), + And( + *) + +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) +done + +theorem bool_of_o_reflection: + "REFLECTS[\x. is_bool_of_o(L, P(x), f(x)), + \i x. is_bool_of_o(**Lset(i), P(x), f(x))]" +apply (simp only: is_bool_of_o_def setclass_simps) +apply (intro FOL_reflections function_reflections) +done + + subsubsection{*An Instance of Replacement for @{term nth}*} lemma nth_replacement_Reflects: @@ -1199,9 +1282,7 @@ subsubsection{*Instantiating the locale @{text M_datatypes}*} -theorem M_datatypes_L: "PROP M_datatypes(L)" - apply (rule M_datatypes.intro) - apply (rule M_wfrank.axioms [OF M_wfrank_L])+ +lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)" apply (rule M_datatypes_axioms.intro) apply (assumption | rule list_replacement1 list_replacement2 @@ -1209,6 +1290,12 @@ nth_replacement)+ done +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); + done + lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L] and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L] and list_abs = M_datatypes.list_abs [OF M_datatypes_L] @@ -1307,11 +1394,15 @@ subsubsection{*Instantiating the locale @{text M_eclose}*} +lemma M_eclose_axioms_L: "M_eclose_axioms(L)" + apply (rule M_eclose_axioms.intro) + apply (assumption | rule eclose_replacement1 eclose_replacement2)+ + done + theorem M_eclose_L: "PROP M_eclose(L)" apply (rule M_eclose.intro) apply (rule M_datatypes.axioms [OF M_datatypes_L])+ - apply (rule M_eclose_axioms.intro) - apply (assumption | rule eclose_replacement1 eclose_replacement2)+ + apply (rule M_eclose_axioms_L) done lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L] diff -r 8fd1d803a3d3 -r 01b3fc0cc1b8 src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Wed Jul 31 14:39:47 2002 +0200 +++ b/src/ZF/Constructible/Separation.thy Wed Jul 31 14:40:40 2002 +0200 @@ -1,3 +1,9 @@ +(* Title: ZF/Constructible/Separation.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2002 University of Cambridge +*) + header{*Early Instances of Separation and Strong Replacement*} theory Separation = L_axioms + WF_absolute: @@ -69,6 +75,26 @@ apply (simp_all add: succ_Un_distrib [symmetric]) done +subsection{*Separation for Set Difference*} + +lemma Diff_Reflects: + "REFLECTS[\x. x \ B, \i x. x \ B]" +by (intro FOL_reflections) + +lemma Diff_separation: + "L(B) ==> separation(L, \x. x \ B)" +apply (rule separation_CollectI) +apply (rule_tac A="{B,z}" in subset_LsetE, blast ) +apply (rule ReflectsE [OF Diff_Reflects], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2, clarify) +apply (rule DPow_LsetI) +apply (rule not_iff_sats) +apply (rule_tac env="[x,B]" in mem_iff_sats) +apply (rule sep_rules | simp)+ +done + subsection{*Separation for Cartesian Product*} lemma cartprod_Reflects: @@ -448,19 +474,21 @@ text{*Separation (and Strong Replacement) for basic set-theoretic constructions such as intersection, Cartesian Product and image.*} -theorem M_axioms_L: "PROP M_axioms(L)" - apply (rule M_axioms.intro) - apply (rule M_triv_axioms_L) +lemma M_axioms_axioms_L: "M_axioms_axioms(L)" apply (rule M_axioms_axioms.intro) - apply (assumption | rule - Inter_separation cartprod_separation image_separation - converse_separation restrict_separation - comp_separation pred_separation Memrel_separation - funspace_succ_replacement well_ord_iso_separation - obase_separation obase_equals_separation - omap_replacement is_recfun_separation)+ + apply (assumption | rule + Inter_separation Diff_separation cartprod_separation image_separation + converse_separation restrict_separation + comp_separation pred_separation Memrel_separation + funspace_succ_replacement well_ord_iso_separation + obase_separation obase_equals_separation + omap_replacement is_recfun_separation)+ done +theorem M_axioms_L: "PROP M_axioms(L)" +by (rule M_axioms.intro [OF M_triv_axioms_L M_axioms_axioms_L]) + + lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L] and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L] and sum_closed = M_axioms.sum_closed [OF M_axioms_L]