# HG changeset patch # User paulson # Date 1025109080 -7200 # Node ID 74cb2af8811eef63b1d895630137aef58e66d69a # Parent efd5db7dc7ccfcbff372f4bedcb16556f3320e5a new treatment of wfrec, replacing wf[A](r) by wf(r) diff -r efd5db7dc7cc -r 74cb2af8811e src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Wed Jun 26 12:17:21 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Wed Jun 26 18:31:20 2002 +0200 @@ -432,7 +432,7 @@ and is_recfun_separation: --{*for well-founded recursion. NEEDS RELATIVIZATION*} "[| M(A); M(f); M(g); M(a); M(b) |] - ==> separation(M, \x. x \ A --> \x,a\ \ r & \x,b\ \ r & f`x \ g`x)" + ==> separation(M, \x. \x,a\ \ r & \x,b\ \ r & f`x \ g`x)" and omap_replacement: "[| M(A); M(r) |] ==> strong_replacement(M, diff -r efd5db7dc7cc -r 74cb2af8811e src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Wed Jun 26 12:17:21 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Wed Jun 26 18:31:20 2002 +0200 @@ -1,10 +1,10 @@ theory WF_absolute = WFrec: -subsection{*Every well-founded relation is a subset of some inverse image of +subsection{*Every well-founded relation is a subset of some inverse image of an ordinal*} lemma wf_rvimage_Ord: "Ord(i) \ wf(rvimage(A, f, Memrel(i)))" -by (blast intro: wf_rvimage wf_Memrel ) +by (blast intro: wf_rvimage wf_Memrel) constdefs @@ -21,7 +21,7 @@ lemma Ord_wfrank: "wf(r) ==> Ord(wfrank(r,a))" apply (rule_tac a="a" in wf_induct, assumption) apply (subst wfrank, assumption) -apply (rule Ord_succ [THEN Ord_UN], blast) +apply (rule Ord_succ [THEN Ord_UN], blast) done lemma wfrank_lt: "[|wf(r); \ r|] ==> wfrank(r,a) < wfrank(r,b)" @@ -34,19 +34,19 @@ by (simp add: wftype_def Ord_wfrank) lemma wftypeI: "\wf(r); x \ field(r)\ \ wfrank(r,x) \ wftype(r)" -apply (simp add: wftype_def) -apply (blast intro: wfrank_lt [THEN ltD]) +apply (simp add: wftype_def) +apply (blast intro: wfrank_lt [THEN ltD]) done lemma wf_imp_subset_rvimage: "[|wf(r); r \ A*A|] ==> \i f. Ord(i) & r <= rvimage(A, f, Memrel(i))" -apply (rule_tac x="wftype(r)" in exI) -apply (rule_tac x="\x\A. wfrank(r,x)" in exI) -apply (simp add: Ord_wftype, clarify) -apply (frule subsetD, assumption, clarify) +apply (rule_tac x="wftype(r)" in exI) +apply (rule_tac x="\x\A. wfrank(r,x)" in exI) +apply (simp add: Ord_wftype, clarify) +apply (frule subsetD, assumption, clarify) apply (simp add: rvimage_iff wfrank_lt [THEN ltD]) -apply (blast intro: wftypeI ) +apply (blast intro: wftypeI) done theorem wf_iff_subset_rvimage: @@ -59,65 +59,65 @@ constdefs rtrancl_alt :: "[i,i]=>i" - "rtrancl_alt(A,r) == + "rtrancl_alt(A,r) == {p \ A*A. \n\nat. \f \ succ(n) -> A. (\x y. p = & f`0 = x & f`n = y) & (\i\n. \ r)}" -lemma alt_rtrancl_lemma1 [rule_format]: +lemma alt_rtrancl_lemma1 [rule_format]: "n \ nat - ==> \f \ succ(n) -> field(r). + ==> \f \ succ(n) -> field(r). (\i\n. \f`i, f ` succ(i)\ \ r) --> \f`0, f`n\ \ r^*" -apply (induct_tac n) -apply (simp_all add: apply_funtype rtrancl_refl, clarify) -apply (rename_tac n f) -apply (rule rtrancl_into_rtrancl) +apply (induct_tac n) +apply (simp_all add: apply_funtype rtrancl_refl, clarify) +apply (rename_tac n f) +apply (rule rtrancl_into_rtrancl) prefer 2 apply assumption apply (drule_tac x="restrict(f,succ(n))" in bspec) - apply (blast intro: restrict_type2) -apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) + apply (blast intro: restrict_type2) +apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) done lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*" apply (simp add: rtrancl_alt_def) -apply (blast intro: alt_rtrancl_lemma1 ) +apply (blast intro: alt_rtrancl_lemma1) done lemma rtrancl_subset_rtrancl_alt: "r^* <= rtrancl_alt(field(r),r)" -apply (simp add: rtrancl_alt_def, clarify) -apply (frule rtrancl_type [THEN subsetD], clarify, simp) -apply (erule rtrancl_induct) +apply (simp add: rtrancl_alt_def, clarify) +apply (frule rtrancl_type [THEN subsetD], clarify, simp) +apply (erule rtrancl_induct) txt{*Base case, trivial*} - apply (rule_tac x=0 in bexI) - apply (rule_tac x="lam x:1. xa" in bexI) - apply simp_all + apply (rule_tac x=0 in bexI) + apply (rule_tac x="lam x:1. xa" in bexI) + apply simp_all txt{*Inductive step*} -apply clarify -apply (rename_tac n f) -apply (rule_tac x="succ(n)" in bexI) +apply clarify +apply (rename_tac n f) +apply (rule_tac x="succ(n)" in bexI) apply (rule_tac x="lam i:succ(succ(n)). if i=succ(n) then z else f`i" in bexI) - apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) - apply (blast intro: mem_asym) - apply typecheck - apply auto + apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) + apply (blast intro: mem_asym) + apply typecheck + apply auto done lemma rtrancl_alt_eq_rtrancl: "rtrancl_alt(field(r),r) = r^*" by (blast del: subsetI - intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt) + intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt) constdefs rtran_closure :: "[i=>o,i,i] => o" - "rtran_closure(M,r,s) == + "rtran_closure(M,r,s) == \A. M(A) --> is_field(M,r,A) --> - (\p. M(p) --> - (p \ s <-> - (\n\nat. M(n) & + (\p. M(p) --> + (p \ s <-> + (\n\nat. M(n) & (\n'. M(n') & successor(M,n,n') & (\f. M(f) & typed_function(M,n',A,f) & - (\x\A. M(x) & (\y\A. M(y) & pair(M,x,y,p) & + (\x\A. M(x) & (\y\A. M(y) & pair(M,x,y,p) & fun_apply(M,f,0,x) & fun_apply(M,f,n,y))) & (\i\n. M(i) --> (\i'. M(i') --> successor(M,i,i') --> @@ -126,7 +126,7 @@ (\q. M(q) --> pair(M,fi,fi',q) --> q \ r))))))))))" tran_closure :: "[i=>o,i,i] => o" - "tran_closure(M,r,t) == + "tran_closure(M,r,t) == \s. M(s) & rtran_closure(M,r,s) & composition(M,r,s,t)" @@ -142,335 +142,350 @@ "[| M(r); M(Z) |] ==> separation (M, \x. \w. M(w) & \w,x\ \ r^+ & w \ Z)" -lemma (in M_trancl) rtran_closure_rtrancl: +lemma (in M_trancl) rtran_closure_rtrancl: "M(r) ==> rtran_closure(M,r,rtrancl(r))" -apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] +apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def field_closed typed_apply_abs apply_closed - Ord_succ_mem_iff M_nat nat_0_le [THEN ltD], clarify) -apply (rule iffI) - apply clarify - apply simp - apply (rename_tac n f) - apply (rule_tac x=n in bexI) - apply (rule_tac x=f in exI) + Ord_succ_mem_iff M_nat nat_0_le [THEN ltD], clarify) +apply (rule iffI) + apply clarify + apply simp + apply (rename_tac n f) + apply (rule_tac x=n in bexI) + apply (rule_tac x=f in exI) apply simp apply (blast dest: finite_fun_closed dest: transM) apply assumption apply clarify -apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast) +apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast) done -lemma (in M_trancl) rtrancl_closed [intro,simp]: +lemma (in M_trancl) rtrancl_closed [intro,simp]: "M(r) ==> M(rtrancl(r))" -apply (insert rtrancl_separation [of r "field(r)"]) -apply (simp add: rtrancl_alt_eq_rtrancl [symmetric] +apply (insert rtrancl_separation [of r "field(r)"]) +apply (simp add: rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def field_closed typed_apply_abs apply_closed Ord_succ_mem_iff M_nat nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype) done -lemma (in M_trancl) rtrancl_abs [simp]: +lemma (in M_trancl) rtrancl_abs [simp]: "[| M(r); M(z) |] ==> rtran_closure(M,r,z) <-> z = rtrancl(r)" apply (rule iffI) txt{*Proving the right-to-left implication*} - prefer 2 apply (blast intro: rtran_closure_rtrancl) + prefer 2 apply (blast intro: rtran_closure_rtrancl) apply (rule M_equalityI) -apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] +apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def field_closed typed_apply_abs apply_closed Ord_succ_mem_iff M_nat - nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype) + nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype) prefer 2 apply assumption prefer 2 apply blast -apply (rule iffI, clarify) -apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast, clarify, simp) - apply (rename_tac n f) - apply (rule_tac x=n in bexI) +apply (rule iffI, clarify) +apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast, clarify, simp) + apply (rename_tac n f) + apply (rule_tac x=n in bexI) apply (rule_tac x=f in exI) apply (blast dest!: finite_fun_closed, assumption) done -lemma (in M_trancl) trancl_closed [intro,simp]: +lemma (in M_trancl) trancl_closed [intro,simp]: "M(r) ==> M(trancl(r))" -by (simp add: trancl_def comp_closed rtrancl_closed) +by (simp add: trancl_def comp_closed rtrancl_closed) -lemma (in M_trancl) trancl_abs [simp]: +lemma (in M_trancl) trancl_abs [simp]: "[| M(r); M(z) |] ==> tran_closure(M,r,z) <-> z = trancl(r)" -by (simp add: tran_closure_def trancl_def) +by (simp add: tran_closure_def trancl_def) -text{*Alternative proof of @{text wf_on_trancl}; inspiration for the +text{*Alternative proof of @{text wf_on_trancl}; inspiration for the relativized version. Original version is on theory WF.*} lemma "[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)" -apply (simp add: wf_on_def wf_def) +apply (simp add: wf_on_def wf_def) apply (safe intro!: equalityI) -apply (drule_tac x = "{x\A. \w. \w,x\ \ r^+ & w \ Z}" in spec) -apply (blast elim: tranclE) +apply (drule_tac x = "{x\A. \w. \w,x\ \ r^+ & w \ Z}" in spec) +apply (blast elim: tranclE) done lemma (in M_trancl) wellfounded_on_trancl: "[| wellfounded_on(M,A,r); r-``A <= A; M(r); M(A) |] - ==> wellfounded_on(M,A,r^+)" -apply (simp add: wellfounded_on_def) + ==> wellfounded_on(M,A,r^+)" +apply (simp add: wellfounded_on_def) apply (safe intro!: equalityI) apply (rename_tac Z x) -apply (subgoal_tac "M({x\A. \w. M(w) & \w,x\ \ r^+ & w \ Z})") - prefer 2 - apply (simp add: wellfounded_trancl_separation) -apply (drule_tac x = "{x\A. \w. M(w) & \w,x\ \ r^+ & w \ Z}" in spec) +apply (subgoal_tac "M({x\A. \w. M(w) & \w,x\ \ r^+ & w \ Z})") + prefer 2 + apply (simp add: wellfounded_trancl_separation) +apply (drule_tac x = "{x\A. \w. M(w) & \w,x\ \ r^+ & w \ Z}" in spec) apply safe -apply (blast dest: transM, simp) -apply (rename_tac y w) +apply (blast dest: transM, simp) +apply (rename_tac y w) apply (drule_tac x=w in bspec, assumption, clarify) apply (erule tranclE) apply (blast dest: transM) (*transM is needed to prove M(xa)*) - apply blast + apply blast done +(*????move to Wellorderings.thy*) +lemma (in M_axioms) wellfounded_on_field_imp_wellfounded: + "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)" +by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast) + +lemma (in M_axioms) wellfounded_iff_wellfounded_on_field: + "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)" +by (blast intro: wellfounded_imp_wellfounded_on + wellfounded_on_field_imp_wellfounded) + +lemma (in M_axioms) wellfounded_on_subset_A: + "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)" +by (simp add: wellfounded_on_def, blast) + + + +lemma (in M_trancl) wellfounded_trancl: + "[|wellfounded(M,r); M(r)|] ==> wellfounded(M,r^+)" +apply (rotate_tac -1) +apply (simp add: wellfounded_iff_wellfounded_on_field) +apply (rule wellfounded_on_subset_A, erule wellfounded_on_trancl) + apply blast + apply (simp_all add: trancl_type [THEN field_rel_subset]) +done text{*Relativized to M: Every well-founded relation is a subset of some -inverse image of an ordinal. Key step is the construction (in M) of a +inverse image of an ordinal. Key step is the construction (in M) of a rank function.*} (*NEEDS RELATIVIZATION*) locale M_recursion = M_trancl + assumes wfrank_separation': - "[| M(r); M(A) |] ==> + "M(r) ==> separation - (M, \x. x \ A --> - ~(\f. M(f) \ is_recfun(r^+, x, %x f. range(f), f)))" + (M, \x. ~ (\f. M(f) & is_recfun(r^+, x, %x f. range(f), f)))" and wfrank_strong_replacement': "M(r) ==> strong_replacement(M, \x z. \y f. M(y) & M(f) & - pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) & + pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) & y = range(f))" and Ord_wfrank_separation: - "[| M(r); M(A) |] ==> - separation (M, \x. x \ A \ - \ (\f. M(f) \ + "M(r) ==> + separation (M, \x. ~ (\f. M(f) \ is_recfun(r^+, x, \x. range, f) \ Ord(range(f))))" -constdefs +text{*This function, defined using replacement, is a rank function for +well-founded relations within the class M.*} +constdefs wellfoundedrank :: "[i=>o,i,i] => i" - "wellfoundedrank(M,r,A) == - {p. x\A, \y f. M(y) & M(f) & - p = & is_recfun(r^+, x, %x f. range(f), f) & + "wellfoundedrank(M,r,A) == + {p. x\A, \y f. M(y) & M(f) & + p = & is_recfun(r^+, x, %x f. range(f), f) & y = range(f)}" lemma (in M_recursion) exists_wfrank: - "[| wellfounded(M,r); r \ A*A; a\A; M(r); M(A) |] + "[| wellfounded(M,r); M(a); M(r) |] ==> \f. M(f) & is_recfun(r^+, a, %x f. range(f), f)" -apply (rule wellfounded_exists_is_recfun [of A]) -apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on) -apply (rule trans_trancl [THEN trans_imp_trans_on], assumption+) -apply (simp_all add: trancl_subset_times) +apply (rule wellfounded_exists_is_recfun) + apply (blast intro: wellfounded_trancl) + apply (rule trans_trancl) + apply (erule wfrank_separation') + apply (erule wfrank_strong_replacement') +apply (simp_all add: trancl_subset_times) done lemma (in M_recursion) M_wellfoundedrank: - "[| wellfounded(M,r); r \ A*A; M(r); M(A) |] - ==> M(wellfoundedrank(M,r,A))" -apply (insert wfrank_strong_replacement' [of r]) -apply (simp add: wellfoundedrank_def) -apply (rule strong_replacement_closed) + "[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))" +apply (insert wfrank_strong_replacement' [of r]) +apply (simp add: wellfoundedrank_def) +apply (rule strong_replacement_closed) apply assumption+ - apply (rule univalent_is_recfun) - apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on) - apply (rule trans_on_trancl) - apply (simp add: trancl_subset_times) - apply blast+ + apply (rule univalent_is_recfun) + apply (blast intro: wellfounded_trancl) + apply (rule trans_trancl) + apply (simp add: trancl_subset_times) +apply blast done lemma (in M_recursion) Ord_wfrank_range [rule_format]: - "[| wellfounded(M,r); r \ A*A; a\A; M(r); M(A) |] + "[| wellfounded(M,r); a\A; M(r); M(A) |] ==> \f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))" -apply (subgoal_tac "wellfounded_on(M, A, r^+)") - prefer 2 - apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on) -apply (erule wellfounded_on_induct2, assumption+) -apply (simp add: trancl_subset_times) -apply (blast intro: Ord_wfrank_separation, clarify) +apply (drule wellfounded_trancl, assumption) +apply (rule wellfounded_induct, assumption+) + apply (simp add:); + apply (blast intro: Ord_wfrank_separation); +apply (clarify) txt{*The reasoning in both cases is that we get @{term y} such that - @{term "\y, x\ \ r^+"}. We find that + @{term "\y, x\ \ r^+"}. We find that @{term "f`y = restrict(f, r^+ -`` {y})"}. *} apply (rule OrdI [OF _ Ord_is_Transset]) txt{*An ordinal is a transitive set...*} - apply (simp add: Transset_def) + apply (simp add: Transset_def) apply clarify - apply (frule apply_recfun2, assumption) + apply (frule apply_recfun2, assumption) apply (force simp add: restrict_iff) -txt{*...of ordinals. This second case requires the induction hyp.*} -apply clarify +txt{*...of ordinals. This second case requires the induction hyp.*} +apply clarify apply (rename_tac i y) -apply (frule apply_recfun2, assumption) -apply (frule is_recfun_imp_in_r, assumption) -apply (frule is_recfun_restrict) +apply (frule apply_recfun2, assumption) +apply (frule is_recfun_imp_in_r, assumption) +apply (frule is_recfun_restrict) (*simp_all won't work*) - apply (simp add: trans_on_trancl trancl_subset_times)+ + apply (simp add: trans_trancl trancl_subset_times)+ apply (drule spec [THEN mp], assumption) apply (subgoal_tac "M(restrict(f, r^+ -`` {y}))") - apply (drule_tac x="restrict(f, r^+ -`` {y})" in spec) + apply (drule_tac x="restrict(f, r^+ -`` {y})" in spec) apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) apply (blast dest: pair_components_in_M) done lemma (in M_recursion) Ord_range_wellfoundedrank: - "[| wellfounded(M,r); r \ A*A; M(r); M(A) |] + "[| wellfounded(M,r); r \ A*A; M(r); M(A) |] ==> Ord (range(wellfoundedrank(M,r,A)))" -apply (subgoal_tac "wellfounded_on(M, A, r^+)") - prefer 2 - apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on) -apply (frule trancl_subset_times) +apply (frule wellfounded_trancl, assumption) +apply (frule trancl_subset_times) apply (simp add: wellfoundedrank_def) apply (rule OrdI [OF _ Ord_is_Transset]) prefer 2 - txt{*by our previous result the range consists of ordinals.*} - apply (blast intro: Ord_wfrank_range) + txt{*by our previous result the range consists of ordinals.*} + apply (blast intro: Ord_wfrank_range) txt{*We still must show that the range is a transitive set.*} apply (simp add: Transset_def, clarify, simp) -apply (rename_tac x i f u) -apply (frule is_recfun_imp_in_r, assumption) -apply (subgoal_tac "M(u) & M(i) & M(x)") - prefer 2 apply (blast dest: transM, clarify) -apply (rule_tac a=u in rangeI) -apply (rule ReplaceI) - apply (rule_tac x=i in exI, simp) +apply (rename_tac x i f u) +apply (frule is_recfun_imp_in_r, assumption) +apply (subgoal_tac "M(u) & M(i) & M(x)") + prefer 2 apply (blast dest: transM, clarify) +apply (rule_tac a=u in rangeI) +apply (rule ReplaceI) + apply (rule_tac x=i in exI, simp) apply (rule_tac x="restrict(f, r^+ -`` {u})" in exI) - apply (blast intro: is_recfun_restrict trans_on_trancl dest: apply_recfun2) + apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2) apply blast -txt{*Unicity requirement of Replacement*} +txt{*Unicity requirement of Replacement*} apply clarify -apply (frule apply_recfun2, assumption) -apply (simp add: trans_on_trancl is_recfun_cut)+ +apply (frule apply_recfun2, assumption) +apply (simp add: trans_trancl is_recfun_cut)+ done lemma (in M_recursion) function_wellfoundedrank: - "[| wellfounded(M,r); r \ A*A; M(r); M(A)|] + "[| wellfounded(M,r); M(r); M(A)|] ==> function(wellfoundedrank(M,r,A))" -apply (simp add: wellfoundedrank_def function_def, clarify) +apply (simp add: wellfoundedrank_def function_def, clarify) txt{*Uniqueness: repeated below!*} apply (drule is_recfun_functional, assumption) - apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on) - apply (simp_all add: trancl_subset_times - trans_trancl [THEN trans_imp_trans_on]) -apply (blast dest: transM) + apply (blast intro: wellfounded_trancl) + apply (simp_all add: trancl_subset_times trans_trancl) done lemma (in M_recursion) domain_wellfoundedrank: - "[| wellfounded(M,r); r \ A*A; M(r); M(A)|] + "[| wellfounded(M,r); M(r); M(A)|] ==> domain(wellfoundedrank(M,r,A)) = A" -apply (simp add: wellfoundedrank_def function_def) +apply (simp add: wellfoundedrank_def function_def) apply (rule equalityI, auto) -apply (frule transM, assumption) -apply (frule exists_wfrank, assumption+, clarify) -apply (rule domainI) +apply (frule transM, assumption) +apply (frule_tac a=x in exists_wfrank, assumption+, clarify) +apply (rule domainI) apply (rule ReplaceI) -apply (rule_tac x="range(f)" in exI) -apply simp -apply (rule_tac x=f in exI, blast, assumption) + apply (rule_tac x="range(f)" in exI) + apply simp + apply (rule_tac x=f in exI, blast, assumption) txt{*Uniqueness (for Replacement): repeated above!*} apply clarify apply (drule is_recfun_functional, assumption) - apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on) - apply (simp_all add: trancl_subset_times - trans_trancl [THEN trans_imp_trans_on]) + apply (blast intro: wellfounded_trancl) + apply (simp_all add: trancl_subset_times trans_trancl) done lemma (in M_recursion) wellfoundedrank_type: - "[| wellfounded(M,r); r \ A*A; M(r); M(A)|] + "[| wellfounded(M,r); M(r); M(A)|] ==> wellfoundedrank(M,r,A) \ A -> range(wellfoundedrank(M,r,A))" -apply (frule function_wellfoundedrank, assumption+) -apply (frule function_imp_Pi) - apply (simp add: wellfoundedrank_def relation_def) - apply blast +apply (frule function_wellfoundedrank [of r A], assumption+) +apply (frule function_imp_Pi) + apply (simp add: wellfoundedrank_def relation_def) + apply blast apply (simp add: domain_wellfoundedrank) done lemma (in M_recursion) Ord_wellfoundedrank: - "[| wellfounded(M,r); a \ A; r \ A*A; M(r); M(A) |] + "[| wellfounded(M,r); a \ A; r \ A*A; M(r); M(A) |] ==> Ord(wellfoundedrank(M,r,A) ` a)" by (blast intro: apply_funtype [OF wellfoundedrank_type] Ord_in_Ord [OF Ord_range_wellfoundedrank]) lemma (in M_recursion) wellfoundedrank_eq: "[| is_recfun(r^+, a, %x. range, f); - wellfounded(M,r); a \ A; r \ A*A; M(f); M(r); M(A)|] + wellfounded(M,r); a \ A; M(f); M(r); M(A)|] ==> wellfoundedrank(M,r,A) ` a = range(f)" -apply (rule apply_equality) - prefer 2 apply (blast intro: wellfoundedrank_type ) +apply (rule apply_equality) + prefer 2 apply (blast intro: wellfoundedrank_type) apply (simp add: wellfoundedrank_def) apply (rule ReplaceI) - apply (rule_tac x="range(f)" in exI) - apply blast + apply (rule_tac x="range(f)" in exI) + apply blast apply assumption -txt{*Unicity requirement of Replacement*} +txt{*Unicity requirement of Replacement*} apply clarify apply (drule is_recfun_functional, assumption) - apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on) - apply (simp_all add: trancl_subset_times - trans_trancl [THEN trans_imp_trans_on]) -apply (blast dest: transM) + apply (blast intro: wellfounded_trancl) + apply (simp_all add: trancl_subset_times trans_trancl) done lemma (in M_recursion) wellfoundedrank_lt: "[| \ r; - wellfounded(M,r); r \ A*A; M(r); M(A)|] + wellfounded(M,r); r \ A*A; M(r); M(A)|] ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b" -apply (subgoal_tac "wellfounded_on(M, A, r^+)") - prefer 2 - apply (blast intro: wellfounded_on_trancl wellfounded_imp_wellfounded_on) +apply (frule wellfounded_trancl, assumption) apply (subgoal_tac "a\A & b\A") prefer 2 apply blast -apply (simp add: lt_def Ord_wellfoundedrank, clarify) -apply (frule exists_wfrank [of concl: _ b], assumption+, clarify) +apply (simp add: lt_def Ord_wellfoundedrank, clarify) +apply (frule exists_wfrank [of concl: _ b], assumption+, clarify) apply (rename_tac fb) -apply (frule is_recfun_restrict [of concl: _ a]) - apply (rule trans_on_trancl, assumption) - apply (simp_all add: r_into_trancl trancl_subset_times) +apply (frule is_recfun_restrict [of concl: "r^+" a]) + apply (rule trans_trancl, assumption) + apply (simp_all add: r_into_trancl trancl_subset_times) txt{*Still the same goal, but with new @{text is_recfun} assumptions.*} -apply (simp add: wellfoundedrank_eq) +apply (simp add: wellfoundedrank_eq) apply (frule_tac a=a in wellfoundedrank_eq, assumption+) apply (simp_all add: transM [of a]) txt{*We have used equations for wellfoundedrank and now must use some for @{text is_recfun}. *} -apply (rule_tac a=a in rangeI) -apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff - r_into_trancl apply_recfun r_into_trancl) +apply (rule_tac a=a in rangeI) +apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff + r_into_trancl apply_recfun r_into_trancl) done lemma (in M_recursion) wellfounded_imp_subset_rvimage: - "[|wellfounded(M,r); r \ A*A; M(r); M(A)|] + "[|wellfounded(M,r); r \ A*A; M(r); M(A)|] ==> \i f. Ord(i) & r <= rvimage(A, f, Memrel(i))" apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI) apply (rule_tac x="wellfoundedrank(M,r,A)" in exI) -apply (simp add: Ord_range_wellfoundedrank, clarify) -apply (frule subsetD, assumption, clarify) +apply (simp add: Ord_range_wellfoundedrank, clarify) +apply (frule subsetD, assumption, clarify) apply (simp add: rvimage_iff wellfoundedrank_lt [THEN ltD]) -apply (blast intro: apply_rangeI wellfoundedrank_type) +apply (blast intro: apply_rangeI wellfoundedrank_type) done -lemma (in M_recursion) wellfounded_imp_wf: - "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)" +lemma (in M_recursion) wellfounded_imp_wf: + "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)" by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage intro: wf_rvimage_Ord [THEN wf_subset]) -lemma (in M_recursion) wellfounded_on_imp_wf_on: - "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)" -apply (simp add: wellfounded_on_iff_wellfounded wf_on_def) +lemma (in M_recursion) wellfounded_on_imp_wf_on: + "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)" +apply (simp add: wellfounded_on_iff_wellfounded wf_on_def) apply (rule wellfounded_imp_wf) -apply (simp_all add: relation_def) +apply (simp_all add: relation_def) done -theorem (in M_recursion) wf_abs [simp]: +theorem (in M_recursion) wf_abs [simp]: "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)" -by (blast intro: wellfounded_imp_wf wf_imp_relativized) +by (blast intro: wellfounded_imp_wf wf_imp_relativized) -theorem (in M_recursion) wf_on_abs [simp]: +theorem (in M_recursion) wf_on_abs [simp]: "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)" -by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized) +by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized) end diff -r efd5db7dc7cc -r 74cb2af8811e src/ZF/Constructible/WFrec.thy --- a/src/ZF/Constructible/WFrec.thy Wed Jun 26 12:17:21 2002 +0200 +++ b/src/ZF/Constructible/WFrec.thy Wed Jun 26 18:31:20 2002 +0200 @@ -37,71 +37,75 @@ apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) done -lemma trans_on_Int_eq [simp]: - "[| trans[A](r); \ r; r \ A*A |] +(*????GET RID OF [simp]*) +lemma trans_Int_eq [simp]: + "[| trans(r); \ r |] ==> r -`` {y} \ r -`` {x} = r -`` {y}" -by (blast intro: trans_onD) +by (blast intro: transD) -lemma trans_on_Int_eq2 [simp]: - "[| trans[A](r); \ r; r \ A*A |] +lemma trans_Int_eq2 [simp]: + "[| trans(r); \ r |] ==> r -`` {x} \ r -`` {y} = r -`` {y}" -by (blast intro: trans_onD) +by (blast intro: transD) -text{*Stated using @{term "trans[A](r)"} rather than +text{*Stated using @{term "trans(r)"} rather than @{term "transitive_rel(M,A,r)"} because the latter rewrites to the former anyway, by @{text transitive_rel_abs}. - As always, theorems should be expressed in simplified form.*} + As always, theorems should be expressed in simplified form. + The last three M-premises are redundant because of @{term "M(r)"}, + but without them we'd have to undertake + more work to set up the induction formula.*} lemma (in M_axioms) is_recfun_equal [rule_format]: "[|is_recfun(r,a,H,f); is_recfun(r,b,H,g); - wellfounded_on(M,A,r); trans[A](r); - M(A); M(f); M(g); M(a); M(b); - r \ A*A; x\A |] + wellfounded(M,r); trans(r); + M(f); M(g); M(r); M(x); M(a); M(b) |] ==> \ r --> \ r --> f`x=g`x" apply (frule_tac f="f" in is_recfun_type) apply (frule_tac f="g" in is_recfun_type) apply (simp add: is_recfun_def) -apply (erule wellfounded_on_induct2, assumption+) -apply (force intro: is_recfun_separation, clarify) +apply (erule_tac a=x in wellfounded_induct) +apply assumption+ +txt{*Separation to justify the induction*} + apply (force intro: is_recfun_separation) +txt{*Now the inductive argument itself*} +apply (clarify ); apply (erule ssubst)+ apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def) apply (rename_tac x1) apply (rule_tac t="%z. H(x1,z)" in subst_context) apply (subgoal_tac "ALL y : r-``{x1}. ALL z. :f <-> :g") - apply (blast intro: trans_onD) + apply (blast intro: transD) apply (simp add: apply_iff) -apply (blast intro: trans_onD sym) +apply (blast intro: transD sym) done lemma (in M_axioms) is_recfun_cut: "[|is_recfun(r,a,H,f); is_recfun(r,b,H,g); - wellfounded_on(M,A,r); trans[A](r); - M(A); M(f); M(g); M(a); M(b); - r \ A*A; \r |] + wellfounded(M,r); trans(r); + M(f); M(g); M(r); \ r |] ==> restrict(f, r-``{b}) = g" apply (frule_tac f="f" in is_recfun_type) apply (rule fun_extension) -apply (blast intro: trans_onD restrict_type2) +apply (blast intro: transD restrict_type2) apply (erule is_recfun_type, simp) -apply (blast intro: is_recfun_equal trans_onD) +apply (blast intro: is_recfun_equal transD dest: transM) done lemma (in M_axioms) is_recfun_functional: "[|is_recfun(r,a,H,f); is_recfun(r,a,H,g); - wellfounded_on(M,A,r); trans[A](r); - M(A); M(f); M(g); M(a); - r \ A*A |] + wellfounded(M,r); trans(r); + M(f); M(g); M(r) |] ==> f=g" apply (rule fun_extension) apply (erule is_recfun_type)+ -apply (blast intro!: is_recfun_equal) +apply (blast intro!: is_recfun_equal dest: transM) done text{*Tells us that is_recfun can (in principle) be relativized.*} lemma (in M_axioms) is_recfun_relativize: - "[| M(r); M(a); M(f); - \x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] ==> - is_recfun(r,a,H,f) <-> + "[| M(r); M(f); \x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] + ==> is_recfun(r,a,H,f) <-> (\z. z \ f <-> (\x y. M(x) & M(y) & z= & \ r & y = H(x, restrict(f, r-``{x}))))"; apply (simp add: is_recfun_def vimage_closed restrict_closed lam_def) @@ -118,7 +122,7 @@ prefer 2 apply (simp add: function_def) apply (frule pair_components_in_M, assumption) - apply (simp add: is_recfun_imp_function function_restrictI restrict_closed vimage_closed) + apply (simp add: is_recfun_imp_function function_restrictI) done (* ideas for further weaking the H-closure premise: @@ -136,23 +140,23 @@ *) lemma (in M_axioms) is_recfun_restrict: - "[| wellfounded_on(M,A,r); trans[A](r); is_recfun(r,x,H,f); \y,x\ \ r; - M(A); M(r); M(f); - \x g. M(x) & M(g) & function(g) --> M(H(x,g)); r \ A * A |] + "[| wellfounded(M,r); trans(r); is_recfun(r,x,H,f); \y,x\ \ r; + M(r); M(f); + \x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] ==> is_recfun(r, y, H, restrict(f, r -`` {y}))" apply (frule pair_components_in_M, assumption, clarify) apply (simp (no_asm_simp) add: is_recfun_relativize restrict_iff) apply safe apply (simp_all add: vimage_singleton_iff is_recfun_type [THEN apply_iff]) apply (frule_tac x=xa in pair_components_in_M, assumption) - apply (frule_tac x=xa in apply_recfun, blast intro: trans_onD) + apply (frule_tac x=xa in apply_recfun, blast intro: transD) apply (simp add: is_recfun_type [THEN apply_iff] - is_recfun_imp_function function_restrictI) -apply (blast intro: apply_recfun dest: trans_onD)+ + is_recfun_imp_function function_restrictI) +apply (blast intro: apply_recfun dest: transD) done lemma (in M_axioms) restrict_Y_lemma: - "[| wellfounded_on(M,A,r); trans[A](r); M(A); M(r); r \ A \ A; + "[| wellfounded(M,r); trans(r); M(r); \x g. M(x) \ M(g) & function(g) --> M(H(x,g)); M(Y); \b. M(b) --> b \ Y <-> @@ -161,10 +165,10 @@ (\g. M(g) \ b = \x,y\ \ is_recfun(r,x,H,g) \ y = H(x,g))); \x,a1\ \ r; M(f); is_recfun(r,x,H,f) |] ==> restrict(Y, r -`` {x}) = f" -apply (subgoal_tac "ALL y : r-``{x}. ALL z. :Y <-> :f") -apply (simp (no_asm_simp) add: restrict_def) -apply (thin_tac "All(?P)")+ --{*essential for efficiency*} -apply (frule is_recfun_type [THEN fun_is_rel], blast) +apply (subgoal_tac "\y \ r-``{x}. \z. :Y <-> :f") + apply (simp (no_asm_simp) add: restrict_def) + apply (thin_tac "All(?P)")+ --{*essential for efficiency*} + apply (frule is_recfun_type [THEN fun_is_rel], blast) apply (frule pair_components_in_M, assumption, clarify) apply (rule iffI) apply (frule_tac y="" in transM, assumption ) @@ -174,17 +178,16 @@ txt{*Opposite inclusion: something in f, show in Y*} apply (frule_tac y="" in transM, assumption, simp) apply (rule_tac x=y in bexI) -prefer 2 apply (blast dest: trans_onD) +prefer 2 apply (blast dest: transD) apply (rule_tac x=z in exI, simp) apply (rule_tac x="restrict(f, r -`` {y})" in exI) apply (simp add: vimage_closed restrict_closed is_recfun_restrict apply_recfun is_recfun_type [THEN apply_iff]) done -(*FIXME: use this lemma just below*) text{*For typical applications of Replacement for recursive definitions*} lemma (in M_axioms) univalent_is_recfun: - "[|wellfounded_on(M,A,r); trans[A](r); r \ A*A; M(r); M(A)|] + "[|wellfounded(M,r); trans(r); M(r)|] ==> univalent (M, A, \x p. \y. M(y) & (\f. M(f) & p = \x, y\ & is_recfun(r,x,H,f) & y = H(x,f)))" apply (simp add: univalent_def) @@ -194,69 +197,67 @@ text{*Proof of the inductive step for @{text exists_is_recfun}, since we must prove two versions.*} lemma (in M_axioms) exists_is_recfun_indstep: - "[|a1 \ A; \y. \y, a1\ \ r --> (\f. M(f) & is_recfun(r, y, H, f)); - wellfounded_on(M,A,r); trans[A](r); + "[|\y. \y, a1\ \ r --> (\f. M(f) & is_recfun(r, y, H, f)); + wellfounded(M,r); trans(r); M(r); M(a1); strong_replacement(M, \x z. \y g. M(y) & M(g) & pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); - M(A); M(r); r \ A * A; \x g. M(x) & M(g) & function(g) --> M(H(x,g))|] ==> \f. M(f) & is_recfun(r,a1,H,f)" -apply (frule_tac y=a1 in transM, assumption) apply (drule_tac A="r-``{a1}" in strong_replacementD) - apply blast + apply blast txt{*Discharge the "univalent" obligation of Replacement*} - apply (clarsimp simp add: univalent_def) - apply (blast dest!: is_recfun_functional) + apply (simp add: univalent_is_recfun) txt{*Show that the constructed object satisfies @{text is_recfun}*} apply clarify apply (rule_tac x=Y in exI) -apply (simp (no_asm_simp) add: is_recfun_relativize vimage_closed restrict_closed) +apply (simp (no_asm_simp) add: is_recfun_relativize) (*Tried using is_recfun_iff2 here. Much more simplification takes place because an assumption can kick in. Not sure how to relate the new proof state to the current one.*) apply safe -txt{*Show that elements of @{term Y} are in the right relationship.*} -apply (frule_tac x=z and P="%b. M(b) --> ?Q(b)" in spec) -apply (erule impE, blast intro: transM) -txt{*We have an element of @{term Y}, so we have x, y, z*} -apply (frule_tac y=z in transM, assumption, clarify) -apply (simp add: vimage_closed restrict_closed restrict_Y_lemma [of A r H]) + txt{*Show that elements of @{term Y} are in the right relationship.*} + apply (frule_tac x=z and P="%b. M(b) --> ?Q(b)" in spec) + apply (erule impE, blast intro: transM) + txt{*We have an element of @{term Y}, so we have x, y, z*} + apply (frule_tac y=z in transM, assumption, clarify) + apply (simp add: restrict_Y_lemma [of r H]) txt{*one more case*} -apply (simp add: vimage_closed restrict_closed ) +apply (simp) apply (rule_tac x=x in bexI) -prefer 2 apply blast + prefer 2 apply blast apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in exI) -apply (simp add: vimage_closed restrict_closed ) +apply (simp) apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) apply (rule_tac x=f in exI) -apply (simp add: restrict_Y_lemma [of A r H]) +apply (simp add: restrict_Y_lemma [of r H]) done - text{*Relativized version, when we have the (currently weaker) premise - @{term "wellfounded_on(M,A,r)"}*} + @{term "wellfounded(M,r)"}*} lemma (in M_axioms) wellfounded_exists_is_recfun: - "[|wellfounded_on(M,A,r); trans[A](r); a\A; - separation(M, \x. x \ A --> ~ (\f. M(f) \ is_recfun(r, x, H, f))); + "[|wellfounded(M,r); trans(r); + separation(M, \x. ~ (\f. M(f) \ is_recfun(r, x, H, f))); strong_replacement(M, \x z. \y g. M(y) & M(g) & pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); - M(A); M(r); r \ A*A; + M(r); M(a); \x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] ==> \f. M(f) & is_recfun(r,a,H,f)" -apply (rule wellfounded_on_induct2, assumption+, clarify) +apply (rule wellfounded_induct, assumption+, clarify) apply (rule exists_is_recfun_indstep, assumption+) done -lemma (in M_axioms) wf_exists_is_recfun: - "[|wf[A](r); trans[A](r); a\A; +lemma (in M_axioms) wf_exists_is_recfun [rule_format]: + "[|wf(r); trans(r); strong_replacement(M, \x z. \y g. M(y) & M(g) & pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); - M(A); M(r); r \ A*A; + M(r); \x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] - ==> \f. M(f) & is_recfun(r,a,H,f)" -apply (rule wf_on_induct2, assumption+) -apply (frule wf_on_imp_relativized) -apply (rule exists_is_recfun_indstep, assumption+) + ==> M(a) --> (\f. M(f) & is_recfun(r,a,H,f))" +apply (rule wf_induct, assumption+) +apply (frule wf_imp_relativized) +apply (intro impI) +apply (rule exists_is_recfun_indstep) + apply (blast dest: pair_components_in_M)+ done constdefs @@ -377,12 +378,10 @@ lemma (in M_recursion) exists_oadd: "[| Ord(j); M(i); M(j) |] ==> \f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)" -apply (rule wf_exists_is_recfun) -apply (rule wf_Memrel [THEN wf_imp_wf_on]) -apply (rule trans_Memrel [THEN trans_imp_trans_on], simp) -apply (rule succI1) -apply (blast intro: oadd_strong_replacement') -apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed) +apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) + apply (simp add: ); + apply (blast intro: oadd_strong_replacement') + apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed) done lemma (in M_recursion) exists_oadd_fun: @@ -491,12 +490,10 @@ lemma (in M_recursion) exists_omult: "[| Ord(j); M(i); M(j) |] ==> \f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)" -apply (rule wf_exists_is_recfun) -apply (rule wf_Memrel [THEN wf_imp_wf_on]) -apply (rule trans_Memrel [THEN trans_imp_trans_on], simp) -apply (rule succI1) -apply (blast intro: omult_strong_replacement') -apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed) +apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) + apply (simp add: ); + apply (blast intro: omult_strong_replacement') + apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed) apply (blast intro: the_omult_eqns_closed) done diff -r efd5db7dc7cc -r 74cb2af8811e src/ZF/Constructible/Wellorderings.thy --- a/src/ZF/Constructible/Wellorderings.thy Wed Jun 26 12:17:21 2002 +0200 +++ b/src/ZF/Constructible/Wellorderings.thy Wed Jun 26 18:31:20 2002 +0200 @@ -85,6 +85,16 @@ "[|wellfounded_on(M,A,r); r \ A*A|] ==> wellfounded(M,r)" by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff) +(*Consider the least z in domain(r) such that P(z) does not hold...*) +lemma (in M_axioms) wellfounded_induct: + "[| wellfounded(M,r); M(a); M(r); separation(M, \x. ~P(x)); + \x. M(x) & (\y. \ r --> P(y)) --> P(x) |] + ==> P(a)"; +apply (simp (no_asm_use) add: wellfounded_def) +apply (drule_tac x="{z \ domain(r). ~P(z)}" in spec) +apply (blast dest: transM) +done + lemma (in M_axioms) wellfounded_on_induct: "[| a\A; wellfounded_on(M,A,r); M(A); separation(M, \x. x\A --> ~P(x));