# HG changeset patch # User paulson # Date 1034154433 -7200 # Node ID 99a593b49b04c4252719b369658ce466790cd068 # Parent b03a36b8d528dff93a680ffa075f0d96c06e8601 Re-organization of Constructible theories diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/AC_in_L.thy --- a/src/ZF/Constructible/AC_in_L.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/AC_in_L.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/AC_in_L.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {* The Axiom of Choice Holds in L! *} diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/DPow_absolute.thy --- a/src/ZF/Constructible/DPow_absolute.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/DPow_absolute.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/DPow_absolute.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {*Absoluteness for the Definable Powerset Function*} @@ -522,14 +521,14 @@ ==> is_Lset(M,i,z) <-> z = Lset(i)" apply (simp add: is_Lset_def Lset_eq_transrec_DPow') apply (rule transrec_abs) -apply (simp_all add: transrec_rep' relativize2_def RepFun_DPow_apply_closed) +apply (simp_all add: transrec_rep' relation2_def RepFun_DPow_apply_closed) done lemma (in M_Lset) Lset_closed: "[|Ord(i); M(i)|] ==> M(Lset(i))" apply (simp add: Lset_eq_transrec_DPow') apply (rule transrec_closed [OF transrec_rep']) -apply (simp_all add: relativize2_def RepFun_DPow_apply_closed) +apply (simp_all add: relation2_def RepFun_DPow_apply_closed) done @@ -629,7 +628,6 @@ "constructible(M,x) == \i[M]. \Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \ Li" - theorem V_equals_L_in_L: "L(x) ==> constructible(L,x)" apply (simp add: constructible_def Lset_abs Lset_closed) @@ -637,5 +635,4 @@ apply (blast intro: Ord_in_L) done - end diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/Datatype_absolute.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/Datatype_absolute.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {*Absoluteness Properties for Recursive Datatypes*} @@ -127,38 +126,38 @@ wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))" lemma (in M_basic) iterates_MH_abs: - "[| relativize1(M,isF,F); M(n); M(g); M(z) |] + "[| 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)" by (simp add: nat_case_abs [of _ "\m. F(g ` m)"] - relativize1_def iterates_MH_def) + relation1_def iterates_MH_def) lemma (in M_basic) iterates_imp_wfrec_replacement: - "[|relativize1(M,isF,F); n \ nat; iterates_replacement(M,isF,v)|] + "[|relation1(M,isF,F); n \ nat; iterates_replacement(M,isF,v)|] ==> wfrec_replacement(M, \n f z. z = nat_case(v, \m. F(f`m), n), Memrel(succ(n)))" by (simp add: iterates_replacement_def iterates_MH_abs) theorem (in M_trancl) iterates_abs: - "[| iterates_replacement(M,isF,v); relativize1(M,isF,F); + "[| 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)" apply (frule iterates_imp_wfrec_replacement, assumption+) apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M - relativize2_def iterates_MH_abs + 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)"]) done -lemma (in M_wfrank) iterates_closed [intro,simp]: - "[| iterates_replacement(M,isF,v); relativize1(M,isF,F); +lemma (in M_trancl) iterates_closed [intro,simp]: + "[| iterates_replacement(M,isF,v); relation1(M,isF,F); n \ nat; M(v); \x[M]. M(F(x)) |] ==> M(iterates(F,n,v))" apply (frule iterates_imp_wfrec_replacement, assumption+) apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M - relativize2_def iterates_MH_abs + relation2_def iterates_MH_abs iterates_nat_def recursor_def transrec_def eclose_sing_Ord_eq nat_into_M trans_wfrec_closed [of _ _ _ "\n g. nat_case(v, \m. F(g`m), n)"]) @@ -459,7 +458,7 @@ is_formula :: "[i=>o,i] => o" "is_formula(M,Z) == \p[M]. p \ Z <-> mem_formula(M,p)" -locale M_datatypes = M_wfrank + +locale M_datatypes = M_trancl + assumes list_replacement1: "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)" and list_replacement2: @@ -487,14 +486,14 @@ 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 relativize1_def) +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 - list_replacement2' relativize1_def + list_replacement2' relation1_def iterates_closed [of "is_list_functor(M,A)"]) text{*WARNING: use only with @{text "dest:"} or with variables fixed!*} @@ -504,21 +503,21 @@ "[|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 relativize1_def nat_into_M +apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M iterates_abs [of "is_list_functor(M,A)" _ "\X. {0} + A*X"]) done lemma (in M_datatypes) list_N_closed [intro,simp]: "[|M(A); n\nat|] ==> M(list_N(A,n))" apply (insert list_replacement1) -apply (simp add: is_list_N_def list_N_def relativize1_def nat_into_M +apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M iterates_closed [of "is_list_functor(M,A)"]) done lemma (in M_datatypes) mem_list_abs [simp]: "M(A) ==> mem_list(M,A,l) <-> l \ list(A)" apply (insert list_replacement1) -apply (simp add: mem_list_def list_N_def relativize1_def list_eq_Union +apply (simp add: mem_list_def list_N_def relation1_def list_eq_Union iterates_closed [of "is_list_functor(M,A)"]) done @@ -535,14 +534,14 @@ 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 relativize1_def) +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 - formula_replacement2' relativize1_def + formula_replacement2' relation1_def iterates_closed [of "is_formula_functor(M)"]) done @@ -552,7 +551,7 @@ "[|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 relativize1_def nat_into_M +apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M iterates_abs [of "is_formula_functor(M)" _ "\X. ((nat*nat) + (nat*nat)) + (X*X + X)"]) done @@ -560,14 +559,14 @@ lemma (in M_datatypes) formula_N_closed [intro,simp]: "n\nat ==> M(formula_N(n))" apply (insert formula_replacement1) -apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M +apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M iterates_closed [of "is_formula_functor(M)"]) done lemma (in M_datatypes) mem_formula_abs [simp]: "mem_formula(M,l) <-> l \ formula" apply (insert formula_replacement1) -apply (simp add: mem_formula_def relativize1_def formula_eq_Union formula_N_def +apply (simp add: mem_formula_def relation1_def formula_eq_Union formula_N_def iterates_closed [of "is_formula_functor(M)"]) done @@ -624,27 +623,27 @@ 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 relativize1_def) +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 - eclose_replacement2' relativize1_def + eclose_replacement2' relation1_def iterates_closed [of "big_union(M)"]) lemma (in M_eclose) is_eclose_n_abs [simp]: "[|M(A); n\nat; M(Z)|] ==> is_eclose_n(M,A,n,Z) <-> Z = Union^n (A)" apply (insert eclose_replacement1) -apply (simp add: is_eclose_n_def relativize1_def nat_into_M +apply (simp add: is_eclose_n_def relation1_def nat_into_M iterates_abs [of "big_union(M)" _ "Union"]) done lemma (in M_eclose) mem_eclose_abs [simp]: "M(A) ==> mem_eclose(M,A,l) <-> l \ eclose(A)" apply (insert eclose_replacement1) -apply (simp add: mem_eclose_def relativize1_def eclose_eq_Union +apply (simp add: mem_eclose_def relation1_def eclose_eq_Union iterates_closed [of "big_union(M)"]) done @@ -679,7 +678,7 @@ @{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); relativize2(M,MH,H); + "[|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)" @@ -688,7 +687,7 @@ theorem (in M_eclose) transrec_closed: - "[|transrec_replacement(M,MH,i); relativize2(M,MH,H); + "[|transrec_replacement(M,MH,i); relation2(M,MH,H); Ord(i); M(i); \x[M]. \g[M]. function(g) --> M(H(x,g))|] ==> M(transrec(i,H))" @@ -770,7 +769,7 @@ 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 - iterates_abs [OF _ relativize1_tl] nth_replacement) + iterates_abs [OF _ relation1_tl] nth_replacement) done @@ -848,14 +847,14 @@ (\x[M]. mem_formula(M,x) --> is_Forall(M,x,p) --> is_d(x,z))" lemma (in M_datatypes) formula_case_abs [simp]: - "[| Relativize2(M,nat,nat,is_a,a); Relativize2(M,nat,nat,is_b,b); - Relativize2(M,formula,formula,is_c,c); Relativize1(M,formula,is_d,d); + "[| 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: Relativize1_def Relativize2_def) + apply (simp_all add: Relation1_def Relation2_def) done lemma (in M_datatypes) formula_case_closed [intro,simp]: @@ -935,18 +934,18 @@ text{*Sufficient conditions to relative the instance of @{term formula_case} in @{term formula_rec}*} -lemma (in M_datatypes) Relativize1_formula_rec_case: - "[|Relativize2(M, nat, nat, is_a, a); - Relativize2(M, nat, nat, is_b, b); - Relativize2 (M, formula, formula, +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, is_c, \u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v)); - Relativize1(M, formula, + Relation1(M, formula, is_d, \u. d(u, h ` succ(depth(u)) ` u)); M(h) |] - ==> Relativize1(M, formula, + ==> 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 Relativize1_def) +apply (simp (no_asm) add: formula_rec_case_def Relation1_def) apply (simp add: formula_case_abs) done @@ -963,19 +962,19 @@ (M, fml, is_formula_case (M, is_a, is_b, is_c(f), is_d(f)), z)" assumes a_closed: "[|x\nat; y\nat|] ==> M(a(x,y))" - and a_rel: "Relativize2(M, nat, nat, is_a, a)" + and a_rel: "Relation2(M, nat, nat, is_a, a)" and b_closed: "[|x\nat; y\nat|] ==> M(b(x,y))" - and b_rel: "Relativize2(M, nat, nat, is_b, b)" + and b_rel: "Relation2(M, nat, nat, is_b, b)" and c_closed: "[|x \ formula; y \ formula; M(gx); M(gy)|] ==> M(c(x, y, gx, gy))" and c_rel: "M(f) ==> - Relativize2 (M, formula, formula, is_c(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) ==> - Relativize1(M, formula, is_d(f), \u. d(u, f ` succ(depth(u)) ` u))" + 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: "M(g) ==> @@ -992,12 +991,12 @@ by (simp add: lam_closed2 fr_lam_replace formula_rec_case_closed) lemma (in Formula_Rec) MH_rel2: - "relativize2 (M, MH, + "relation2 (M, MH, \x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))" -apply (simp add: relativize2_def MH_def, clarify) +apply (simp add: relation2_def MH_def, clarify) apply (rule lambda_abs2) apply (rule fr_lam_replace, assumption) -apply (rule Relativize1_formula_rec_case) +apply (rule Relation1_formula_rec_case) apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed) done diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Formula.thy --- a/src/ZF/Constructible/Formula.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/Formula.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/Formula.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {* First-Order Formulas and the Definition of the Class L *} diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Internalize.thy --- a/src/ZF/Constructible/Internalize.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/Internalize.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/Internalize.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) theory Internalize = L_axioms + Datatype_absolute: diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/L_axioms.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {* The ZF Axioms (Except Separation) in L *} diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/MetaExists.thy --- a/src/ZF/Constructible/MetaExists.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/MetaExists.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/MetaExists.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header{*The meta-existential quantifier*} diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Normal.thy --- a/src/ZF/Constructible/Normal.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/Normal.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/Normal.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {*Closed Unbounded Classes and Normal Functions*} diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/ROOT.ML --- a/src/ZF/Constructible/ROOT.ML Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/ROOT.ML Wed Oct 09 11:07:13 2002 +0200 @@ -8,3 +8,4 @@ use_thy "DPow_absolute"; use_thy "AC_in_L"; +use_thy "Rank_Separation"; diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Rank.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Constructible/Rank.thy Wed Oct 09 11:07:13 2002 +0200 @@ -0,0 +1,935 @@ +(* Title: ZF/Constructible/Rank.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory +*) + +header {*Absoluteness for Order Types, Rank Functions and Well-Founded + Relations*} + +theory Rank = WF_absolute: + +subsection {*Order Types: A Direct Construction by Replacement*} + +locale M_ordertype = M_basic + +assumes well_ord_iso_separation: + "[| M(A); M(f); M(r) |] + ==> separation (M, \x. x\A --> (\y[M]. (\p[M]. + fun_apply(M,f,x,y) & pair(M,y,x,p) & p \ r)))" + and obase_separation: + --{*part of the order type formalization*} + "[| M(A); M(r) |] + ==> separation(M, \a. \x[M]. \g[M]. \mx[M]. \par[M]. + ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) & + order_isomorphism(M,par,r,x,mx,g))" + and obase_equals_separation: + "[| M(A); M(r) |] + ==> separation (M, \x. x\A --> ~(\y[M]. \g[M]. + ordinal(M,y) & (\my[M]. \pxr[M]. + membership(M,y,my) & pred_set(M,A,x,r,pxr) & + order_isomorphism(M,pxr,r,y,my,g))))" + and omap_replacement: + "[| M(A); M(r) |] + ==> strong_replacement(M, + \a z. \x[M]. \g[M]. \mx[M]. \par[M]. + ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & + pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))" + + +text{*Inductive argument for Kunen's Lemma I 6.1, etc. + Simple proof from Halmos, page 72*} +lemma (in M_ordertype) wellordered_iso_subset_lemma: + "[| wellordered(M,A,r); f \ ord_iso(A,r, A',r); A'<= A; y \ A; + M(A); M(f); M(r) |] ==> ~ \ r" +apply (unfold wellordered_def ord_iso_def) +apply (elim conjE CollectE) +apply (erule wellfounded_on_induct, assumption+) + apply (insert well_ord_iso_separation [of A f r]) + apply (simp, clarify) +apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast) +done + + +text{*Kunen's Lemma I 6.1, page 14: + there's no order-isomorphism to an initial segment of a well-ordering*} +lemma (in M_ordertype) wellordered_iso_predD: + "[| wellordered(M,A,r); f \ ord_iso(A, r, Order.pred(A,x,r), r); + M(A); M(f); M(r) |] ==> x \ A" +apply (rule notI) +apply (frule wellordered_iso_subset_lemma, assumption) +apply (auto elim: predE) +(*Now we know ~ (f`x < x) *) +apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) +(*Now we also know f`x \ pred(A,x,r); contradiction! *) +apply (simp add: Order.pred_def) +done + + +lemma (in M_ordertype) wellordered_iso_pred_eq_lemma: + "[| f \ \Order.pred(A,y,r), r\ \ \Order.pred(A,x,r), r\; + wellordered(M,A,r); x\A; y\A; M(A); M(f); M(r) |] ==> \ r" +apply (frule wellordered_is_trans_on, assumption) +apply (rule notI) +apply (drule_tac x2=y and x=x and r2=r in + wellordered_subset [OF _ pred_subset, THEN wellordered_iso_predD]) +apply (simp add: trans_pred_pred_eq) +apply (blast intro: predI dest: transM)+ +done + + +text{*Simple consequence of Lemma 6.1*} +lemma (in M_ordertype) wellordered_iso_pred_eq: + "[| wellordered(M,A,r); + f \ ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r); + M(A); M(f); M(r); a\A; c\A |] ==> a=c" +apply (frule wellordered_is_trans_on, assumption) +apply (frule wellordered_is_linear, assumption) +apply (erule_tac x=a and y=c in linearE, auto) +apply (drule ord_iso_sym) +(*two symmetric cases*) +apply (blast dest: wellordered_iso_pred_eq_lemma)+ +done + + +text{*Following Kunen's Theorem I 7.6, page 17. Note that this material is +not required elsewhere.*} + +text{*Can't use @{text well_ord_iso_preserving} because it needs the +strong premise @{term "well_ord(A,r)"}*} +lemma (in M_ordertype) ord_iso_pred_imp_lt: + "[| f \ ord_iso(Order.pred(A,x,r), r, i, Memrel(i)); + g \ ord_iso(Order.pred(A,y,r), r, j, Memrel(j)); + wellordered(M,A,r); x \ A; y \ A; M(A); M(r); M(f); M(g); M(j); + Ord(i); Ord(j); \x,y\ \ r |] + ==> i < j" +apply (frule wellordered_is_trans_on, assumption) +apply (frule_tac y=y in transM, assumption) +apply (rule_tac i=i and j=j in Ord_linear_lt, auto) +txt{*case @{term "i=j"} yields a contradiction*} + apply (rule_tac x1=x and A1="Order.pred(A,y,r)" in + wellordered_iso_predD [THEN notE]) + apply (blast intro: wellordered_subset [OF _ pred_subset]) + apply (simp add: trans_pred_pred_eq) + apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) + apply (simp_all add: pred_iff pred_closed converse_closed comp_closed) +txt{*case @{term "j Order.pred(A,x,r)"}*} +apply (simp add: pred_iff) +apply (subgoal_tac + "\h[M]. h \ ord_iso(Order.pred(A,y,r), r, + Order.pred(A, converse(f)`j, r), r)") + apply (clarify, frule wellordered_iso_pred_eq, assumption+) + apply (blast dest: wellordered_asym) +apply (intro rexI) + apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)+ +done + + +lemma ord_iso_converse1: + "[| f: ord_iso(A,r,B,s); : s; a:A; b:B |] + ==> : r" +apply (frule ord_iso_converse, assumption+) +apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype]) +apply (simp add: left_inverse_bij [OF ord_iso_is_bij]) +done + + +constdefs + + obase :: "[i=>o,i,i] => i" + --{*the domain of @{text om}, eventually shown to equal @{text A}*} + "obase(M,A,r) == {a\A. \x[M]. \g[M]. Ord(x) & + g \ ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}" + + omap :: "[i=>o,i,i,i] => o" + --{*the function that maps wosets to order types*} + "omap(M,A,r,f) == + \z[M]. + z \ f <-> (\a\A. \x[M]. \g[M]. z = & Ord(x) & + g \ ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))" + + + otype :: "[i=>o,i,i,i] => o" --{*the order types themselves*} + "otype(M,A,r,i) == \f[M]. omap(M,A,r,f) & is_range(M,f,i)" + + +text{*Can also be proved with the premise @{term "M(z)"} instead of + @{term "M(f)"}, but that version is less useful. This lemma + is also more useful than the definition, @{text omap_def}.*} +lemma (in M_ordertype) omap_iff: + "[| omap(M,A,r,f); M(A); M(f) |] + ==> z \ f <-> + (\a\A. \x[M]. \g[M]. z = & Ord(x) & + g \ ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))" +apply (simp add: omap_def Memrel_closed pred_closed) +apply (rule iffI) + apply (drule_tac [2] x=z in rspec) + apply (drule_tac x=z in rspec) + apply (blast dest: transM)+ +done + +lemma (in M_ordertype) omap_unique: + "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" +apply (rule equality_iffI) +apply (simp add: omap_iff) +done + +lemma (in M_ordertype) omap_yields_Ord: + "[| omap(M,A,r,f); \a,x\ \ f; M(a); M(x) |] ==> Ord(x)" + by (simp add: omap_def) + +lemma (in M_ordertype) otype_iff: + "[| otype(M,A,r,i); M(A); M(r); M(i) |] + ==> x \ i <-> + (M(x) & Ord(x) & + (\a\A. \g[M]. g \ ord_iso(Order.pred(A,a,r),r,x,Memrel(x))))" +apply (auto simp add: omap_iff otype_def) + apply (blast intro: transM) +apply (rule rangeI) +apply (frule transM, assumption) +apply (simp add: omap_iff, blast) +done + +lemma (in M_ordertype) otype_eq_range: + "[| omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) |] + ==> i = range(f)" +apply (auto simp add: otype_def omap_iff) +apply (blast dest: omap_unique) +done + + +lemma (in M_ordertype) Ord_otype: + "[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)" +apply (rule OrdI) +prefer 2 + apply (simp add: Ord_def otype_def omap_def) + apply clarify + apply (frule pair_components_in_M, assumption) + apply blast +apply (auto simp add: Transset_def otype_iff) + apply (blast intro: transM) + apply (blast intro: Ord_in_Ord) +apply (rename_tac y a g) +apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun, + THEN apply_funtype], assumption) +apply (rule_tac x="converse(g)`y" in bexI) + apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption) +apply (safe elim!: predE) +apply (blast intro: restrict_ord_iso ord_iso_sym ltI dest: transM) +done + +lemma (in M_ordertype) domain_omap: + "[| omap(M,A,r,f); M(A); M(r); M(B); M(f) |] + ==> domain(f) = obase(M,A,r)" +apply (simp add: domain_closed obase_def) +apply (rule equality_iffI) +apply (simp add: domain_iff omap_iff, blast) +done + +lemma (in M_ordertype) omap_subset: + "[| omap(M,A,r,f); otype(M,A,r,i); + M(A); M(r); M(f); M(B); M(i) |] ==> f \ obase(M,A,r) * i" +apply clarify +apply (simp add: omap_iff obase_def) +apply (force simp add: otype_iff) +done + +lemma (in M_ordertype) omap_funtype: + "[| omap(M,A,r,f); otype(M,A,r,i); + M(A); M(r); M(f); M(i) |] ==> f \ obase(M,A,r) -> i" +apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) +apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) +done + + +lemma (in M_ordertype) wellordered_omap_bij: + "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); + M(A); M(r); M(f); M(i) |] ==> f \ bij(obase(M,A,r),i)" +apply (insert omap_funtype [of A r f i]) +apply (auto simp add: bij_def inj_def) +prefer 2 apply (blast intro: fun_is_surj dest: otype_eq_range) +apply (frule_tac a=w in apply_Pair, assumption) +apply (frule_tac a=x in apply_Pair, assumption) +apply (simp add: omap_iff) +apply (blast intro: wellordered_iso_pred_eq ord_iso_sym ord_iso_trans) +done + + +text{*This is not the final result: we must show @{term "oB(A,r) = A"}*} +lemma (in M_ordertype) omap_ord_iso: + "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); + M(A); M(r); M(f); M(i) |] ==> f \ ord_iso(obase(M,A,r),r,i,Memrel(i))" +apply (rule ord_isoI) + apply (erule wellordered_omap_bij, assumption+) +apply (insert omap_funtype [of A r f i], simp) +apply (frule_tac a=x in apply_Pair, assumption) +apply (frule_tac a=y in apply_Pair, assumption) +apply (auto simp add: omap_iff) + txt{*direction 1: assuming @{term "\x,y\ \ r"}*} + apply (blast intro: ltD ord_iso_pred_imp_lt) + txt{*direction 2: proving @{term "\x,y\ \ r"} using linearity of @{term r}*} +apply (rename_tac x y g ga) +apply (frule wellordered_is_linear, assumption, + erule_tac x=x and y=y in linearE, assumption+) +txt{*the case @{term "x=y"} leads to immediate contradiction*} +apply (blast elim: mem_irrefl) +txt{*the case @{term "\y,x\ \ r"}: handle like the opposite direction*} +apply (blast dest: ord_iso_pred_imp_lt ltD elim: mem_asym) +done + +lemma (in M_ordertype) Ord_omap_image_pred: + "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); + M(A); M(r); M(f); M(i); b \ A |] ==> Ord(f `` Order.pred(A,b,r))" +apply (frule wellordered_is_trans_on, assumption) +apply (rule OrdI) + prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast) +txt{*Hard part is to show that the image is a transitive set.*} +apply (simp add: Transset_def, clarify) +apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f i]]) +apply (rename_tac c j, clarify) +apply (frule omap_funtype [of A r f, THEN apply_funtype], assumption+) +apply (subgoal_tac "j : i") + prefer 2 apply (blast intro: Ord_trans Ord_otype) +apply (subgoal_tac "converse(f) ` j : obase(M,A,r)") + prefer 2 + apply (blast dest: wellordered_omap_bij [THEN bij_converse_bij, + THEN bij_is_fun, THEN apply_funtype]) +apply (rule_tac x="converse(f) ` j" in bexI) + apply (simp add: right_inverse_bij [OF wellordered_omap_bij]) +apply (intro predI conjI) + apply (erule_tac b=c in trans_onD) + apply (rule ord_iso_converse1 [OF omap_ord_iso [of A r f i]]) +apply (auto simp add: obase_def) +done + +lemma (in M_ordertype) restrict_omap_ord_iso: + "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); + D \ obase(M,A,r); M(A); M(r); M(f); M(i) |] + ==> restrict(f,D) \ (\D,r\ \ \f``D, Memrel(f``D)\)" +apply (frule ord_iso_restrict_image [OF omap_ord_iso [of A r f i]], + assumption+) +apply (drule ord_iso_sym [THEN subset_ord_iso_Memrel]) +apply (blast dest: subsetD [OF omap_subset]) +apply (drule ord_iso_sym, simp) +done + +lemma (in M_ordertype) obase_equals: + "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); + M(A); M(r); M(f); M(i) |] ==> obase(M,A,r) = A" +apply (rule equalityI, force simp add: obase_def, clarify) +apply (unfold obase_def, simp) +apply (frule wellordered_is_wellfounded_on, assumption) +apply (erule wellfounded_on_induct, assumption+) + apply (frule obase_equals_separation [of A r], assumption) + apply (simp, clarify) +apply (rename_tac b) +apply (subgoal_tac "Order.pred(A,b,r) <= obase(M,A,r)") + apply (blast intro!: restrict_omap_ord_iso Ord_omap_image_pred) +apply (force simp add: pred_iff obase_def) +done + + + +text{*Main result: @{term om} gives the order-isomorphism + @{term "\A,r\ \ \i, Memrel(i)\"} *} +theorem (in M_ordertype) omap_ord_iso_otype: + "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); + M(A); M(r); M(f); M(i) |] ==> f \ ord_iso(A, r, i, Memrel(i))" +apply (frule omap_ord_iso, assumption+) +apply (simp add: obase_equals) +done + +lemma (in M_ordertype) obase_exists: + "[| M(A); M(r) |] ==> M(obase(M,A,r))" +apply (simp add: obase_def) +apply (insert obase_separation [of A r]) +apply (simp add: separation_def) +done + +lemma (in M_ordertype) omap_exists: + "[| M(A); M(r) |] ==> \z[M]. omap(M,A,r,z)" +apply (simp add: omap_def) +apply (insert omap_replacement [of A r]) +apply (simp add: strong_replacement_def) +apply (drule_tac x="obase(M,A,r)" in rspec) + apply (simp add: obase_exists) +apply (simp add: Memrel_closed pred_closed obase_def) +apply (erule impE) + apply (clarsimp simp add: univalent_def) + apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify) +apply (rule_tac x=Y in rexI) +apply (simp add: Memrel_closed pred_closed obase_def, blast, assumption) +done + +declare rall_simps [simp] rex_simps [simp] + +lemma (in M_ordertype) otype_exists: + "[| wellordered(M,A,r); M(A); M(r) |] ==> \i[M]. otype(M,A,r,i)" +apply (insert omap_exists [of A r]) +apply (simp add: otype_def, safe) +apply (rule_tac x="range(x)" in rexI) +apply blast+ +done + +lemma (in M_ordertype) ordertype_exists: + "[| wellordered(M,A,r); M(A); M(r) |] + ==> \f[M]. (\i[M]. Ord(i) & f \ ord_iso(A, r, i, Memrel(i)))" +apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify) +apply (rename_tac i) +apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) +apply (rule Ord_otype) + apply (force simp add: otype_def range_closed) + apply (simp_all add: wellordered_is_trans_on) +done + + +lemma (in M_ordertype) relativized_imp_well_ord: + "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" +apply (insert ordertype_exists [of A r], simp) +apply (blast intro: well_ord_ord_iso well_ord_Memrel) +done + +subsection {*Kunen's theorem 5.4, page 127*} + +text{*(a) The notion of Wellordering is absolute*} +theorem (in M_ordertype) well_ord_abs [simp]: + "[| M(A); M(r) |] ==> wellordered(M,A,r) <-> well_ord(A,r)" +by (blast intro: well_ord_imp_relativized relativized_imp_well_ord) + + +text{*(b) Order types are absolute*} +theorem (in M_ordertype) + "[| wellordered(M,A,r); f \ ord_iso(A, r, i, Memrel(i)); + M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)" +by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso + Ord_iso_implies_eq ord_iso_sym ord_iso_trans) + + +subsection{*Ordinal Arithmetic: Two Examples of Recursion*} + +text{*Note: the remainder of this theory is not needed elsewhere.*} + +subsubsection{*Ordinal Addition*} + +(*FIXME: update to use new techniques!!*) +constdefs + (*This expresses ordinal addition in the language of ZF. It also + provides an abbreviation that can be used in the instance of strong + replacement below. Here j is used to define the relation, namely + Memrel(succ(j)), while x determines the domain of f.*) + is_oadd_fun :: "[i=>o,i,i,i,i] => o" + "is_oadd_fun(M,i,j,x,f) == + (\sj msj. M(sj) --> M(msj) --> + successor(M,j,sj) --> membership(M,sj,msj) --> + M_is_recfun(M, + %x g y. \gx[M]. image(M,g,x,gx) & union(M,i,gx,y), + msj, x, f))" + + is_oadd :: "[i=>o,i,i,i] => o" + "is_oadd(M,i,j,k) == + (~ ordinal(M,i) & ~ ordinal(M,j) & k=0) | + (~ ordinal(M,i) & ordinal(M,j) & k=j) | + (ordinal(M,i) & ~ ordinal(M,j) & k=i) | + (ordinal(M,i) & ordinal(M,j) & + (\f fj sj. M(f) & M(fj) & M(sj) & + successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) & + fun_apply(M,f,j,fj) & fj = k))" + + (*NEEDS RELATIVIZATION*) + omult_eqns :: "[i,i,i,i] => o" + "omult_eqns(i,x,g,z) == + Ord(x) & + (x=0 --> z=0) & + (\j. x = succ(j) --> z = g`j ++ i) & + (Limit(x) --> z = \(g``x))" + + is_omult_fun :: "[i=>o,i,i,i] => o" + "is_omult_fun(M,i,j,f) == + (\df. M(df) & is_function(M,f) & + is_domain(M,f,df) & subset(M, j, df)) & + (\x\j. omult_eqns(i,x,f,f`x))" + + is_omult :: "[i=>o,i,i,i] => o" + "is_omult(M,i,j,k) == + \f fj sj. M(f) & M(fj) & M(sj) & + successor(M,j,sj) & is_omult_fun(M,i,sj,f) & + fun_apply(M,f,j,fj) & fj = k" + + +locale M_ord_arith = M_ordertype + + assumes oadd_strong_replacement: + "[| M(i); M(j) |] ==> + strong_replacement(M, + \x z. \y[M]. pair(M,x,y,z) & + (\f[M]. \fx[M]. is_oadd_fun(M,i,j,x,f) & + image(M,f,x,fx) & y = i Un fx))" + + and omult_strong_replacement': + "[| M(i); M(j) |] ==> + strong_replacement(M, + \x z. \y[M]. z = & + (\g[M]. is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & + y = (THE z. omult_eqns(i, x, g, z))))" + + + +text{*@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF*} +lemma (in M_ord_arith) is_oadd_fun_iff: + "[| a\j; M(i); M(j); M(a); M(f) |] + ==> is_oadd_fun(M,i,j,a,f) <-> + f \ a \ range(f) & (\x. M(x) --> x < a --> f`x = i Un f``x)" +apply (frule lt_Ord) +apply (simp add: is_oadd_fun_def Memrel_closed Un_closed + relation2_def is_recfun_abs [of "%x g. i Un g``x"] + image_closed is_recfun_iff_equation + Ball_def lt_trans [OF ltI, of _ a] lt_Memrel) +apply (simp add: lt_def) +apply (blast dest: transM) +done + + +lemma (in M_ord_arith) oadd_strong_replacement': + "[| M(i); M(j) |] ==> + strong_replacement(M, + \x z. \y[M]. z = & + (\g[M]. is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & + y = i Un g``x))" +apply (insert oadd_strong_replacement [of i j]) +apply (simp add: is_oadd_fun_def relation2_def + is_recfun_abs [of "%x g. i Un g``x"]) +done + + +lemma (in M_ord_arith) exists_oadd: + "[| Ord(j); M(i); M(j) |] + ==> \f[M]. is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)" +apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) + apply (simp_all add: Memrel_type oadd_strong_replacement') +done + +lemma (in M_ord_arith) exists_oadd_fun: + "[| Ord(j); M(i); M(j) |] ==> \f[M]. is_oadd_fun(M,i,succ(j),succ(j),f)" +apply (rule exists_oadd [THEN rexE]) +apply (erule Ord_succ, assumption, simp) +apply (rename_tac f) +apply (frule is_recfun_type) +apply (rule_tac x=f in rexI) + apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def + is_oadd_fun_iff Ord_trans [OF _ succI1], assumption) +done + +lemma (in M_ord_arith) is_oadd_fun_apply: + "[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |] + ==> f`x = i Un (\k\x. {f ` k})" +apply (simp add: is_oadd_fun_iff lt_Ord2, clarify) +apply (frule lt_closed, simp) +apply (frule leI [THEN le_imp_subset]) +apply (simp add: image_fun, blast) +done + +lemma (in M_ord_arith) is_oadd_fun_iff_oadd [rule_format]: + "[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] + ==> j f`j = i++j" +apply (erule_tac i=j in trans_induct, clarify) +apply (subgoal_tac "\k\x. k is_oadd(M,i,j,k) <-> k = i++j" +apply (simp add: is_oadd_def is_oadd_fun_iff_oadd) +apply (frule exists_oadd_fun [of j i], blast+) +done + +lemma (in M_ord_arith) oadd_abs: + "[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j" +apply (case_tac "Ord(i) & Ord(j)") + apply (simp add: Ord_oadd_abs) +apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd) +done + +lemma (in M_ord_arith) oadd_closed [intro,simp]: + "[| M(i); M(j) |] ==> M(i++j)" +apply (simp add: oadd_eq_if_raw_oadd, clarify) +apply (simp add: raw_oadd_eq_oadd) +apply (frule exists_oadd_fun [of j i], auto) +apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric]) +done + + +subsubsection{*Ordinal Multiplication*} + +lemma omult_eqns_unique: + "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'"; +apply (simp add: omult_eqns_def, clarify) +apply (erule Ord_cases, simp_all) +done + +lemma omult_eqns_0: "omult_eqns(i,0,g,z) <-> z=0" +by (simp add: omult_eqns_def) + +lemma the_omult_eqns_0: "(THE z. omult_eqns(i,0,g,z)) = 0" +by (simp add: omult_eqns_0) + +lemma omult_eqns_succ: "omult_eqns(i,succ(j),g,z) <-> Ord(j) & z = g`j ++ i" +by (simp add: omult_eqns_def) + +lemma the_omult_eqns_succ: + "Ord(j) ==> (THE z. omult_eqns(i,succ(j),g,z)) = g`j ++ i" +by (simp add: omult_eqns_succ) + +lemma omult_eqns_Limit: + "Limit(x) ==> omult_eqns(i,x,g,z) <-> z = \(g``x)" +apply (simp add: omult_eqns_def) +apply (blast intro: Limit_is_Ord) +done + +lemma the_omult_eqns_Limit: + "Limit(x) ==> (THE z. omult_eqns(i,x,g,z)) = \(g``x)" +by (simp add: omult_eqns_Limit) + +lemma omult_eqns_Not: "~ Ord(x) ==> ~ omult_eqns(i,x,g,z)" +by (simp add: omult_eqns_def) + + +lemma (in M_ord_arith) the_omult_eqns_closed: + "[| M(i); M(x); M(g); function(g) |] + ==> M(THE z. omult_eqns(i, x, g, z))" +apply (case_tac "Ord(x)") + prefer 2 apply (simp add: omult_eqns_Not) --{*trivial, non-Ord case*} +apply (erule Ord_cases) + apply (simp add: omult_eqns_0) + apply (simp add: omult_eqns_succ apply_closed oadd_closed) +apply (simp add: omult_eqns_Limit) +done + +lemma (in M_ord_arith) exists_omult: + "[| Ord(j); M(i); M(j) |] + ==> \f[M]. is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)" +apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) + apply (simp_all add: Memrel_type omult_strong_replacement') +apply (blast intro: the_omult_eqns_closed) +done + +lemma (in M_ord_arith) exists_omult_fun: + "[| Ord(j); M(i); M(j) |] ==> \f[M]. is_omult_fun(M,i,succ(j),f)" +apply (rule exists_omult [THEN rexE]) +apply (erule Ord_succ, assumption, simp) +apply (rename_tac f) +apply (frule is_recfun_type) +apply (rule_tac x=f in rexI) +apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def + is_omult_fun_def Ord_trans [OF _ succI1]) + apply (force dest: Ord_in_Ord' + simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ + the_omult_eqns_Limit, assumption) +done + +lemma (in M_ord_arith) is_omult_fun_apply_0: + "[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0" +by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib) + +lemma (in M_ord_arith) is_omult_fun_apply_succ: + "[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i" +by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast) + +lemma (in M_ord_arith) is_omult_fun_apply_Limit: + "[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |] + ==> f ` x = (\y\x. f`y)" +apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify) +apply (drule subset_trans [OF OrdmemD], assumption+) +apply (simp add: ball_conj_distrib omult_Limit image_function) +done + +lemma (in M_ord_arith) is_omult_fun_eq_omult: + "[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |] + ==> j f`j = i**j" +apply (erule_tac i=j in trans_induct3) +apply (safe del: impCE) + apply (simp add: is_omult_fun_apply_0) + apply (subgoal_tac "xk\x. k is_omult(M,i,j,k) <-> k = i**j" +apply (simp add: is_omult_def is_omult_fun_eq_omult) +apply (frule exists_omult_fun [of j i], blast+) +done + + + +locale M_wfrank = M_trancl + + assumes wfrank_separation: + "M(r) ==> + separation (M, \x. + \rplus[M]. tran_closure(M,r,rplus) --> + ~ (\f[M]. M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f)))" + and wfrank_strong_replacement: + "M(r) ==> + strong_replacement(M, \x z. + \rplus[M]. tran_closure(M,r,rplus) --> + (\y[M]. \f[M]. pair(M,x,y,z) & + M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f) & + is_range(M,f,y)))" + and Ord_wfrank_separation: + "M(r) ==> + separation (M, \x. + \rplus[M]. tran_closure(M,r,rplus) --> + ~ (\f[M]. \rangef[M]. + is_range(M,f,rangef) --> + M_is_recfun(M, \x f y. is_range(M,f,y), rplus, x, f) --> + ordinal(M,rangef)))" + + +text{*Proving that the relativized instances of Separation or Replacement +agree with the "real" ones.*} + +lemma (in M_wfrank) wfrank_separation': + "M(r) ==> + separation + (M, \x. ~ (\f[M]. is_recfun(r^+, x, %x f. range(f), f)))" +apply (insert wfrank_separation [of r]) +apply (simp add: relation2_def is_recfun_abs [of "%x. range"]) +done + +lemma (in M_wfrank) wfrank_strong_replacement': + "M(r) ==> + strong_replacement(M, \x z. \y[M]. \f[M]. + pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) & + y = range(f))" +apply (insert wfrank_strong_replacement [of r]) +apply (simp add: relation2_def is_recfun_abs [of "%x. range"]) +done + +lemma (in M_wfrank) Ord_wfrank_separation': + "M(r) ==> + separation (M, \x. + ~ (\f[M]. is_recfun(r^+, x, \x. range, f) --> Ord(range(f))))" +apply (insert Ord_wfrank_separation [of r]) +apply (simp add: relation2_def is_recfun_abs [of "%x. range"]) +done + +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[M]. \f[M]. + p = & is_recfun(r^+, x, %x f. range(f), f) & + y = range(f)}" + +lemma (in M_wfrank) exists_wfrank: + "[| wellfounded(M,r); M(a); M(r) |] + ==> \f[M]. is_recfun(r^+, a, %x f. range(f), f)" +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_wfrank) M_wellfoundedrank: + "[| 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_trancl) + apply (rule trans_trancl) + apply (simp add: trancl_subset_times) +apply (blast dest: transM) +done + +lemma (in M_wfrank) Ord_wfrank_range [rule_format]: + "[| wellfounded(M,r); a\A; M(r); M(A) |] + ==> \f[M]. is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))" +apply (drule wellfounded_trancl, assumption) +apply (rule wellfounded_induct, assumption, erule (1) transM) + apply simp + apply (blast intro: Ord_wfrank_separation', clarify) +txt{*The reasoning in both cases is that we get @{term y} such 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 clarify + apply (frule apply_recfun2, assumption) + apply (force simp add: restrict_iff) +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) + (*simp_all won't work*) + 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 rspec) +apply assumption + apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) +apply (blast dest: pair_components_in_M) +done + +lemma (in M_wfrank) Ord_range_wellfoundedrank: + "[| wellfounded(M,r); r \ A*A; M(r); M(A) |] + ==> Ord (range(wellfoundedrank(M,r,A)))" +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{*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_tac x=u in ReplaceI) + apply simp + apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI) + apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2) + apply simp +apply blast +txt{*Unicity requirement of Replacement*} +apply clarify +apply (frule apply_recfun2, assumption) +apply (simp add: trans_trancl is_recfun_cut) +done + +lemma (in M_wfrank) function_wellfoundedrank: + "[| wellfounded(M,r); M(r); M(A)|] + ==> function(wellfoundedrank(M,r,A))" +apply (simp add: wellfoundedrank_def function_def, clarify) +txt{*Uniqueness: repeated below!*} +apply (drule is_recfun_functional, assumption) + apply (blast intro: wellfounded_trancl) + apply (simp_all add: trancl_subset_times trans_trancl) +done + +lemma (in M_wfrank) domain_wellfoundedrank: + "[| wellfounded(M,r); M(r); M(A)|] + ==> domain(wellfoundedrank(M,r,A)) = A" +apply (simp add: wellfoundedrank_def function_def) +apply (rule equalityI, auto) +apply (frule transM, assumption) +apply (frule_tac a=x in exists_wfrank, assumption+, clarify) +apply (rule_tac b="range(f)" in domainI) +apply (rule_tac x=x in ReplaceI) + apply simp + apply (rule_tac x=f in rexI, blast, simp_all) +txt{*Uniqueness (for Replacement): repeated above!*} +apply clarify +apply (drule is_recfun_functional, assumption) + apply (blast intro: wellfounded_trancl) + apply (simp_all add: trancl_subset_times trans_trancl) +done + +lemma (in M_wfrank) wellfoundedrank_type: + "[| wellfounded(M,r); M(r); M(A)|] + ==> wellfoundedrank(M,r,A) \ A -> range(wellfoundedrank(M,r,A))" +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_wfrank) Ord_wellfoundedrank: + "[| 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_wfrank) wellfoundedrank_eq: + "[| is_recfun(r^+, a, %x. range, f); + 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 (simp add: wellfoundedrank_def) +apply (rule ReplaceI) + apply (rule_tac x="range(f)" in rexI) + apply blast + apply simp_all +txt{*Unicity requirement of Replacement*} +apply clarify +apply (drule is_recfun_functional, assumption) + apply (blast intro: wellfounded_trancl) + apply (simp_all add: trancl_subset_times trans_trancl) +done + + +lemma (in M_wfrank) wellfoundedrank_lt: + "[| \ r; + wellfounded(M,r); r \ A*A; M(r); M(A)|] + ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b" +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], erule (1) transM, assumption) +apply clarify +apply (rename_tac fb) +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 (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) +done + + +lemma (in M_wfrank) wellfounded_imp_subset_rvimage: + "[|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: rvimage_iff wellfoundedrank_lt [THEN ltD]) +apply (blast intro: apply_rangeI wellfoundedrank_type) +done + +lemma (in M_wfrank) 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_wfrank) 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) +done + + +theorem (in M_wfrank) wf_abs: + "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)" +by (blast intro: wellfounded_imp_wf wf_imp_relativized) + +theorem (in M_wfrank) wf_on_abs: + "[|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) + +end \ No newline at end of file diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Rank_Separation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Constructible/Rank_Separation.thy Wed Oct 09 11:07:13 2002 +0200 @@ -0,0 +1,265 @@ +(* Title: ZF/Constructible/Rank_Separation.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory +*) + +header {*Separation for Facts About Order Types, Rank Functions and + Well-Founded Relations*} + +theory Rank_Separation = Rank + Rec_Separation: + + +text{*This theory proves all instances needed for locales + @{text "M_ordertype"} and @{text "M_wfrank"}*} + +subsection{*The Locale @{text "M_ordertype"}*} + +subsubsection{*Separation for Order-Isomorphisms*} + +lemma well_ord_iso_Reflects: + "REFLECTS[\x. x\A --> + (\y[L]. \p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \ r), + \i x. x\A --> (\y \ Lset(i). \p \ Lset(i). + fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \ r)]" +by (intro FOL_reflections function_reflections) + +lemma well_ord_iso_separation: + "[| L(A); L(f); L(r) |] + ==> separation (L, \x. x\A --> (\y[L]. (\p[L]. + fun_apply(L,f,x,y) & pair(L,y,x,p) & p \ r)))" +apply (rule gen_separation [OF well_ord_iso_Reflects, of "{A,f,r}"], simp) +apply (drule mem_Lset_imp_subset_Lset, clarsimp) +apply (rule DPow_LsetI) +apply (rule imp_iff_sats) +apply (rule_tac env = "[x,A,f,r]" in mem_iff_sats) +apply (rule sep_rules | simp)+ +done + + +subsubsection{*Separation for @{term "obase"}*} + +lemma obase_reflects: + "REFLECTS[\a. \x[L]. \g[L]. \mx[L]. \par[L]. + ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & + order_isomorphism(L,par,r,x,mx,g), + \i a. \x \ Lset(i). \g \ Lset(i). \mx \ Lset(i). \par \ Lset(i). + ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & + order_isomorphism(**Lset(i),par,r,x,mx,g)]" +by (intro FOL_reflections function_reflections fun_plus_reflections) + +lemma obase_separation: + --{*part of the order type formalization*} + "[| L(A); L(r) |] + ==> separation(L, \a. \x[L]. \g[L]. \mx[L]. \par[L]. + ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & + order_isomorphism(L,par,r,x,mx,g))" +apply (rule gen_separation [OF obase_reflects, of "{A,r}"], simp) +apply (drule mem_Lset_imp_subset_Lset, clarsimp) +apply (rule DPow_LsetI) +apply (rule bex_iff_sats conj_iff_sats)+ +apply (rule_tac env = "[x,a,A,r]" in ordinal_iff_sats) +apply (rule sep_rules | simp)+ +done + + +subsubsection{*Separation for a Theorem about @{term "obase"}*} + +lemma obase_equals_reflects: + "REFLECTS[\x. x\A --> ~(\y[L]. \g[L]. + ordinal(L,y) & (\my[L]. \pxr[L]. + membership(L,y,my) & pred_set(L,A,x,r,pxr) & + order_isomorphism(L,pxr,r,y,my,g))), + \i x. x\A --> ~(\y \ Lset(i). \g \ Lset(i). + ordinal(**Lset(i),y) & (\my \ Lset(i). \pxr \ Lset(i). + membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) & + order_isomorphism(**Lset(i),pxr,r,y,my,g)))]" +by (intro FOL_reflections function_reflections fun_plus_reflections) + +lemma obase_equals_separation: + "[| L(A); L(r) |] + ==> separation (L, \x. x\A --> ~(\y[L]. \g[L]. + ordinal(L,y) & (\my[L]. \pxr[L]. + membership(L,y,my) & pred_set(L,A,x,r,pxr) & + order_isomorphism(L,pxr,r,y,my,g))))" +apply (rule gen_separation [OF obase_equals_reflects, of "{A,r}"], simp) +apply (drule mem_Lset_imp_subset_Lset, clarsimp) +apply (rule DPow_LsetI) +apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+ +apply (rule_tac env = "[x,A,r]" in mem_iff_sats) +apply (rule sep_rules | simp)+ +done + + +subsubsection{*Replacement for @{term "omap"}*} + +lemma omap_reflects: + "REFLECTS[\z. \a[L]. a\B & (\x[L]. \g[L]. \mx[L]. \par[L]. + ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & + pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)), + \i z. \a \ Lset(i). a\B & (\x \ Lset(i). \g \ Lset(i). \mx \ Lset(i). + \par \ Lset(i). + ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) & + membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & + order_isomorphism(**Lset(i),par,r,x,mx,g))]" +by (intro FOL_reflections function_reflections fun_plus_reflections) + +lemma omap_replacement: + "[| L(A); L(r) |] + ==> strong_replacement(L, + \a z. \x[L]. \g[L]. \mx[L]. \par[L]. + ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & + pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))" +apply (rule strong_replacementI) +apply (rename_tac B) +apply (rule_tac u="{A,r,B}" in gen_separation [OF omap_reflects], simp) +apply (drule mem_Lset_imp_subset_Lset, clarsimp) +apply (rule DPow_LsetI) +apply (rule bex_iff_sats conj_iff_sats)+ +apply (rule_tac env = "[a,z,A,B,r]" in mem_iff_sats) +apply (rule sep_rules | simp)+ +done + + + +subsection{*Instantiating the locale @{text M_ordertype}*} +text{*Separation (and Strong Replacement) for basic set-theoretic constructions +such as intersection, Cartesian Product and image.*} + +lemma M_ordertype_axioms_L: "M_ordertype_axioms(L)" + apply (rule M_ordertype_axioms.intro) + apply (assumption | rule well_ord_iso_separation + obase_separation obase_equals_separation + omap_replacement)+ + done + +theorem M_ordertype_L: "PROP M_ordertype(L)" +apply (rule M_ordertype.intro) + apply (rule M_basic.axioms [OF M_basic_L])+ +apply (rule M_ordertype_axioms_L) +done + + +subsection{*The Locale @{text "M_wfrank"}*} + +subsubsection{*Separation for @{term "wfrank"}*} + +lemma wfrank_Reflects: + "REFLECTS[\x. \rplus[L]. tran_closure(L,r,rplus) --> + ~ (\f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)), + \i x. \rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> + ~ (\f \ Lset(i). + M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), + rplus, x, f))]" +by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection) + +lemma wfrank_separation: + "L(r) ==> + separation (L, \x. \rplus[L]. tran_closure(L,r,rplus) --> + ~ (\f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))" +apply (rule gen_separation [OF wfrank_Reflects], simp) +apply (rule DPow_LsetI) +apply (rule ball_iff_sats imp_iff_sats)+ +apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats) +apply (rule sep_rules is_recfun_iff_sats | simp)+ +done + + +subsubsection{*Replacement for @{term "wfrank"}*} + +lemma wfrank_replacement_Reflects: + "REFLECTS[\z. \x[L]. x \ A & + (\rplus[L]. tran_closure(L,r,rplus) --> + (\y[L]. \f[L]. pair(L,x,y,z) & + M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & + is_range(L,f,y))), + \i z. \x \ Lset(i). x \ A & + (\rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> + (\y \ Lset(i). \f \ Lset(i). pair(**Lset(i),x,y,z) & + M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) & + is_range(**Lset(i),f,y)))]" +by (intro FOL_reflections function_reflections fun_plus_reflections + is_recfun_reflection tran_closure_reflection) + +lemma wfrank_strong_replacement: + "L(r) ==> + strong_replacement(L, \x z. + \rplus[L]. tran_closure(L,r,rplus) --> + (\y[L]. \f[L]. pair(L,x,y,z) & + M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & + is_range(L,f,y)))" +apply (rule strong_replacementI) +apply (rule_tac u="{r,A}" in gen_separation [OF wfrank_replacement_Reflects], + simp) +apply (drule mem_Lset_imp_subset_Lset, clarsimp) +apply (rule DPow_LsetI) +apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+ +apply (rule_tac env = "[x,z,A,r]" in mem_iff_sats) +apply (rule sep_rules list.intros app_type tran_closure_iff_sats + is_recfun_iff_sats | simp)+ +done + + +subsubsection{*Separation for Proving @{text Ord_wfrank_range}*} + +lemma Ord_wfrank_Reflects: + "REFLECTS[\x. \rplus[L]. tran_closure(L,r,rplus) --> + ~ (\f[L]. \rangef[L]. + is_range(L,f,rangef) --> + M_is_recfun(L, \x f y. is_range(L,f,y), rplus, x, f) --> + ordinal(L,rangef)), + \i x. \rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> + ~ (\f \ Lset(i). \rangef \ Lset(i). + is_range(**Lset(i),f,rangef) --> + M_is_recfun(**Lset(i), \x f y. is_range(**Lset(i),f,y), + rplus, x, f) --> + ordinal(**Lset(i),rangef))]" +by (intro FOL_reflections function_reflections is_recfun_reflection + tran_closure_reflection ordinal_reflection) + +lemma Ord_wfrank_separation: + "L(r) ==> + separation (L, \x. + \rplus[L]. tran_closure(L,r,rplus) --> + ~ (\f[L]. \rangef[L]. + is_range(L,f,rangef) --> + M_is_recfun(L, \x f y. is_range(L,f,y), rplus, x, f) --> + ordinal(L,rangef)))" +apply (rule gen_separation [OF Ord_wfrank_Reflects], simp) +apply (rule DPow_LsetI) +apply (rule ball_iff_sats imp_iff_sats)+ +apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats) +apply (rule sep_rules is_recfun_iff_sats | simp)+ +done + + +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_L) + done + +lemmas exists_wfrank = M_wfrank.exists_wfrank [OF M_wfrank_L] + and M_wellfoundedrank = M_wfrank.M_wellfoundedrank [OF M_wfrank_L] + and Ord_wfrank_range = M_wfrank.Ord_wfrank_range [OF M_wfrank_L] + and Ord_range_wellfoundedrank = M_wfrank.Ord_range_wellfoundedrank [OF M_wfrank_L] + and function_wellfoundedrank = M_wfrank.function_wellfoundedrank [OF M_wfrank_L] + and domain_wellfoundedrank = M_wfrank.domain_wellfoundedrank [OF M_wfrank_L] + and wellfoundedrank_type = M_wfrank.wellfoundedrank_type [OF M_wfrank_L] + and Ord_wellfoundedrank = M_wfrank.Ord_wellfoundedrank [OF M_wfrank_L] + and wellfoundedrank_eq = M_wfrank.wellfoundedrank_eq [OF M_wfrank_L] + and wellfoundedrank_lt = M_wfrank.wellfoundedrank_lt [OF M_wfrank_L] + and wellfounded_imp_subset_rvimage = M_wfrank.wellfounded_imp_subset_rvimage [OF M_wfrank_L] + and wellfounded_imp_wf = M_wfrank.wellfounded_imp_wf [OF M_wfrank_L] + and wellfounded_on_imp_wf_on = M_wfrank.wellfounded_on_imp_wf_on [OF M_wfrank_L] + and wf_abs = M_wfrank.wf_abs [OF M_wfrank_L] + and wf_on_abs = M_wfrank.wf_on_abs [OF M_wfrank_L] + +end \ No newline at end of file diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/Rec_Separation.thy - ID: $Id$ + ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {*Separation for Facts About Recursion*} @@ -9,7 +8,7 @@ theory Rec_Separation = Separation + Internalize: text{*This theory proves all instances needed for locales @{text -"M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*} +"M_trancl"} and @{text "M_datatypes"}*} lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> jx. \rplus[L]. tran_closure(L,r,rplus) --> - ~ (\f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)), - \i x. \rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> - ~ (\f \ Lset(i). - M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), - rplus, x, f))]" -by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection) - -lemma wfrank_separation: - "L(r) ==> - separation (L, \x. \rplus[L]. tran_closure(L,r,rplus) --> - ~ (\f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))" -apply (rule gen_separation [OF wfrank_Reflects], simp) -apply (rule DPow_LsetI) -apply (rule ball_iff_sats imp_iff_sats)+ -apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats) -apply (rule sep_rules is_recfun_iff_sats | simp)+ -done - - -subsubsection{*Replacement for @{term "wfrank"}*} - -lemma wfrank_replacement_Reflects: - "REFLECTS[\z. \x[L]. x \ A & - (\rplus[L]. tran_closure(L,r,rplus) --> - (\y[L]. \f[L]. pair(L,x,y,z) & - M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & - is_range(L,f,y))), - \i z. \x \ Lset(i). x \ A & - (\rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> - (\y \ Lset(i). \f \ Lset(i). pair(**Lset(i),x,y,z) & - M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) & - is_range(**Lset(i),f,y)))]" -by (intro FOL_reflections function_reflections fun_plus_reflections - is_recfun_reflection tran_closure_reflection) - -lemma wfrank_strong_replacement: - "L(r) ==> - strong_replacement(L, \x z. - \rplus[L]. tran_closure(L,r,rplus) --> - (\y[L]. \f[L]. pair(L,x,y,z) & - M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & - is_range(L,f,y)))" -apply (rule strong_replacementI) -apply (rule_tac u="{r,A}" in gen_separation [OF wfrank_replacement_Reflects], - simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[x,z,A,r]" in mem_iff_sats) -apply (rule sep_rules list.intros app_type tran_closure_iff_sats - is_recfun_iff_sats | simp)+ -done - - -subsubsection{*Separation for Proving @{text Ord_wfrank_range}*} - -lemma Ord_wfrank_Reflects: - "REFLECTS[\x. \rplus[L]. tran_closure(L,r,rplus) --> - ~ (\f[L]. \rangef[L]. - is_range(L,f,rangef) --> - M_is_recfun(L, \x f y. is_range(L,f,y), rplus, x, f) --> - ordinal(L,rangef)), - \i x. \rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> - ~ (\f \ Lset(i). \rangef \ Lset(i). - is_range(**Lset(i),f,rangef) --> - M_is_recfun(**Lset(i), \x f y. is_range(**Lset(i),f,y), - rplus, x, f) --> - ordinal(**Lset(i),rangef))]" -by (intro FOL_reflections function_reflections is_recfun_reflection - tran_closure_reflection ordinal_reflection) - -lemma Ord_wfrank_separation: - "L(r) ==> - separation (L, \x. - \rplus[L]. tran_closure(L,r,rplus) --> - ~ (\f[L]. \rangef[L]. - is_range(L,f,rangef) --> - M_is_recfun(L, \x f y. is_range(L,f,y), rplus, x, f) --> - ordinal(L,rangef)))" -apply (rule gen_separation [OF Ord_wfrank_Reflects], simp) -apply (rule DPow_LsetI) -apply (rule ball_iff_sats imp_iff_sats)+ -apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats) -apply (rule sep_rules is_recfun_iff_sats | simp)+ -done - - -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_L) - done - -lemmas iterates_closed = M_wfrank.iterates_closed [OF M_wfrank_L] - and exists_wfrank = M_wfrank.exists_wfrank [OF M_wfrank_L] - and M_wellfoundedrank = M_wfrank.M_wellfoundedrank [OF M_wfrank_L] - and Ord_wfrank_range = M_wfrank.Ord_wfrank_range [OF M_wfrank_L] - and Ord_range_wellfoundedrank = M_wfrank.Ord_range_wellfoundedrank [OF M_wfrank_L] - and function_wellfoundedrank = M_wfrank.function_wellfoundedrank [OF M_wfrank_L] - and domain_wellfoundedrank = M_wfrank.domain_wellfoundedrank [OF M_wfrank_L] - and wellfoundedrank_type = M_wfrank.wellfoundedrank_type [OF M_wfrank_L] - and Ord_wellfoundedrank = M_wfrank.Ord_wellfoundedrank [OF M_wfrank_L] - and wellfoundedrank_eq = M_wfrank.wellfoundedrank_eq [OF M_wfrank_L] - and wellfoundedrank_lt = M_wfrank.wellfoundedrank_lt [OF M_wfrank_L] - and wellfounded_imp_subset_rvimage = M_wfrank.wellfounded_imp_subset_rvimage [OF M_wfrank_L] - and wellfounded_imp_wf = M_wfrank.wellfounded_imp_wf [OF M_wfrank_L] - and wellfounded_on_imp_wf_on = M_wfrank.wellfounded_on_imp_wf_on [OF M_wfrank_L] - and wf_abs = M_wfrank.wf_abs [OF M_wfrank_L] - and wf_on_abs = M_wfrank.wf_on_abs [OF M_wfrank_L] - and wfrec_replacement_iff = M_wfrank.wfrec_replacement_iff [OF M_wfrank_L] - and trans_wfrec_closed = M_wfrank.trans_wfrec_closed [OF M_wfrank_L] - and wfrec_closed = M_wfrank.wfrec_closed [OF M_wfrank_L] - -declare iterates_closed [intro,simp] -declare Ord_wfrank_range [rule_format] -declare wf_abs [simp] -declare wf_on_abs [simp] - - subsection{*@{term L} is Closed Under the Operator @{term list}*} subsubsection{*Instances of Replacement for Lists*} @@ -578,7 +444,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_trancl.axioms [OF M_trancl_L])+ apply (rule M_datatypes_axioms_L) done diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Reflection.thy --- a/src/ZF/Constructible/Reflection.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/Reflection.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/Reflection.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {* The Reflection Theorem*} diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/Relative.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {*Relativization and Absoluteness*} @@ -197,43 +196,43 @@ (\m[M]. successor(M,m,k) --> is_b(m,z)) & (is_quasinat(M,k) | empty(M,z))" - relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o" - "relativize1(M,is_f,f) == \x[M]. \y[M]. is_f(x,y) <-> y = f(x)" + relation1 :: "[i=>o, [i,i]=>o, i=>i] => o" + "relation1(M,is_f,f) == \x[M]. \y[M]. is_f(x,y) <-> y = f(x)" - Relativize1 :: "[i=>o, i, [i,i]=>o, i=>i] => o" + Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o" --{*as above, but typed*} - "Relativize1(M,A,is_f,f) == + "Relation1(M,A,is_f,f) == \x[M]. \y[M]. x\A --> is_f(x,y) <-> y = f(x)" - relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o" - "relativize2(M,is_f,f) == \x[M]. \y[M]. \z[M]. is_f(x,y,z) <-> z = f(x,y)" + relation2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o" + "relation2(M,is_f,f) == \x[M]. \y[M]. \z[M]. is_f(x,y,z) <-> z = f(x,y)" - Relativize2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o" - "Relativize2(M,A,B,is_f,f) == + Relation2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o" + "Relation2(M,A,B,is_f,f) == \x[M]. \y[M]. \z[M]. x\A --> y\B --> is_f(x,y,z) <-> z = f(x,y)" - relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o" - "relativize3(M,is_f,f) == + relation3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o" + "relation3(M,is_f,f) == \x[M]. \y[M]. \z[M]. \u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)" - Relativize3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o" - "Relativize3(M,A,B,C,is_f,f) == + Relation3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o" + "Relation3(M,A,B,C,is_f,f) == \x[M]. \y[M]. \z[M]. \u[M]. x\A --> y\B --> z\C --> is_f(x,y,z,u) <-> u = f(x,y,z)" - relativize4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o" - "relativize4(M,is_f,f) == + relation4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o" + "relation4(M,is_f,f) == \u[M]. \x[M]. \y[M]. \z[M]. \a[M]. is_f(u,x,y,z,a) <-> a = f(u,x,y,z)" text{*Useful when absoluteness reasoning has replaced the predicates by terms*} -lemma triv_Relativize1: - "Relativize1(M, A, \x y. y = f(x), f)" -by (simp add: Relativize1_def) +lemma triv_Relation1: + "Relation1(M, A, \x y. y = f(x), f)" +by (simp add: Relation1_def) -lemma triv_Relativize2: - "Relativize2(M, A, B, \x y a. a = f(x,y), f)" -by (simp add: Relativize2_def) +lemma triv_Relation2: + "Relation2(M, A, B, \x y a. a = f(x,y), f)" +by (simp add: Relation2_def) subsection {*The relativized ZF axioms*} @@ -730,9 +729,9 @@ lemma (in M_trivial) lambda_abs2 [simp]: "[| strong_replacement(M, \x y. x\A & y = \x, b(x)\); - Relativize1(M,A,is_b,b); M(A); \m[M]. m\A --> M(b(m)); M(z) |] + Relation1(M,A,is_b,b); M(A); \m[M]. m\A --> M(b(m)); M(z) |] ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)" -apply (simp add: Relativize1_def is_lambda_def) +apply (simp add: Relation1_def is_lambda_def) apply (rule iffI) prefer 2 apply (simp add: lam_def) apply (rule M_equalityI) @@ -787,7 +786,7 @@ by (auto simp add: is_quasinat_def quasinat_def) lemma (in M_trivial) nat_case_abs [simp]: - "[| relativize1(M,is_b,b); M(k); M(z) |] + "[| relation1(M,is_b,b); M(k); M(z) |] ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)" apply (case_tac "quasinat(k)") prefer 2 @@ -795,7 +794,7 @@ apply (force simp add: quasinat_def) apply (simp add: quasinat_def is_nat_case_def) apply (elim disjE exE) - apply (simp_all add: relativize1_def) + apply (simp_all add: relation1_def) done (*NOT for the simplifier. The assumption M(z') is apparently necessary, but @@ -929,30 +928,8 @@ strong_replacement(M, \p z. \f[M]. \b[M]. \nb[M]. \cnbf[M]. pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) & upair(M,cnbf,cnbf,z))" - and well_ord_iso_separation: - "[| M(A); M(f); M(r) |] - ==> separation (M, \x. x\A --> (\y[M]. (\p[M]. - fun_apply(M,f,x,y) & pair(M,y,x,p) & p \ r)))" - and obase_separation: - --{*part of the order type formalization*} - "[| M(A); M(r) |] - ==> separation(M, \a. \x[M]. \g[M]. \mx[M]. \par[M]. - ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) & - order_isomorphism(M,par,r,x,mx,g))" - and obase_equals_separation: - "[| M(A); M(r) |] - ==> separation (M, \x. x\A --> ~(\y[M]. \g[M]. - ordinal(M,y) & (\my[M]. \pxr[M]. - membership(M,y,my) & pred_set(M,A,x,r,pxr) & - order_isomorphism(M,pxr,r,y,my,g))))" - and omap_replacement: - "[| M(A); M(r) |] - ==> strong_replacement(M, - \a z. \x[M]. \g[M]. \mx[M]. \par[M]. - ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & - pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))" and is_recfun_separation: - --{*for well-founded recursion*} + --{*for well-founded recursion: used to prove @{text is_recfun_equal}*} "[| M(r); M(f); M(g); M(a); M(b) |] ==> separation(M, \x. \xa[M]. \xb[M]. @@ -1490,7 +1467,7 @@ by (auto simp add: is_quasilist_def quasilist_def) lemma (in M_trivial) list_case_abs [simp]: - "[| relativize2(M,is_b,b); M(k); M(z) |] + "[| relation2(M,is_b,b); M(k); M(z) |] ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)" apply (case_tac "quasilist(k)") prefer 2 @@ -1498,7 +1475,7 @@ apply (force simp add: quasilist_def) apply (simp add: quasilist_def is_list_case_def) apply (elim disjE exE) - apply (simp_all add: relativize2_def) + apply (simp_all add: relation2_def) done @@ -1536,8 +1513,8 @@ apply (elim disjE exE, auto) done -lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')" -by (simp add: relativize1_def) +lemma (in M_trivial) relation1_tl: "relation1(M, is_tl(M), tl')" +by (simp add: relation1_def) lemma hd'_Nil: "hd'([]) = 0" by (simp add: hd'_def) diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Satisfies_absolute.thy --- a/src/ZF/Constructible/Satisfies_absolute.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/Satisfies_absolute.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/Satisfies_absolute.thy - ID: $Id$ + ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {*Absoluteness for the Satisfies Relation on Formulas*} @@ -367,9 +366,9 @@ done lemma (in M_satisfies) a_rel: - "M(A) ==> Relativize2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))" -apply (simp add: Relativize2_def satisfies_is_a_def satisfies_a_def) -apply (simp add: lambda_abs2 [OF Member_replacement'] Relativize1_def) + "M(A) ==> Relation2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))" +apply (simp add: Relation2_def satisfies_is_a_def satisfies_a_def) +apply (simp add: lambda_abs2 [OF Member_replacement'] Relation1_def) done lemma (in M_satisfies) b_closed: @@ -379,9 +378,9 @@ done lemma (in M_satisfies) b_rel: - "M(A) ==> Relativize2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))" -apply (simp add: Relativize2_def satisfies_is_b_def satisfies_b_def) -apply (simp add: lambda_abs2 [OF Equal_replacement'] Relativize1_def) + "M(A) ==> Relation2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))" +apply (simp add: Relation2_def satisfies_is_b_def satisfies_b_def) +apply (simp add: lambda_abs2 [OF Equal_replacement'] Relation1_def) done lemma (in M_satisfies) c_closed: @@ -395,12 +394,12 @@ lemma (in M_satisfies) c_rel: "[|M(A); M(f)|] ==> - Relativize2 (M, formula, formula, + Relation2 (M, formula, formula, satisfies_is_c(M,A,f), \u v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))" -apply (simp add: Relativize2_def satisfies_is_c_def satisfies_c_def) -apply (simp add: lambda_abs2 [OF Nand_replacement' triv_Relativize1] +apply (simp add: Relation2_def satisfies_is_c_def satisfies_c_def) +apply (simp add: lambda_abs2 [OF Nand_replacement' triv_Relation1] formula_into_M) done @@ -414,11 +413,11 @@ lemma (in M_satisfies) d_rel: "[|M(A); M(f)|] ==> - Relativize1(M, formula, satisfies_is_d(M,A,f), + Relation1(M, formula, satisfies_is_d(M,A,f), \u. satisfies_d(A, u, f ` succ(depth(u)) ` u))" apply (simp del: rall_abs - add: Relativize1_def satisfies_is_d_def satisfies_d_def) -apply (simp add: lambda_abs2 [OF Forall_replacement' triv_Relativize1] + add: Relation1_def satisfies_is_d_def satisfies_d_def) +apply (simp add: lambda_abs2 [OF Forall_replacement' triv_Relation1] formula_into_M) done diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/Separation.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* 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*} @@ -270,113 +269,7 @@ done -subsection{*Separation for Order-Isomorphisms*} - -lemma well_ord_iso_Reflects: - "REFLECTS[\x. x\A --> - (\y[L]. \p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \ r), - \i x. x\A --> (\y \ Lset(i). \p \ Lset(i). - fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \ r)]" -by (intro FOL_reflections function_reflections) - -lemma well_ord_iso_separation: - "[| L(A); L(f); L(r) |] - ==> separation (L, \x. x\A --> (\y[L]. (\p[L]. - fun_apply(L,f,x,y) & pair(L,y,x,p) & p \ r)))" -apply (rule gen_separation [OF well_ord_iso_Reflects, of "{A,f,r}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule imp_iff_sats) -apply (rule_tac env = "[x,A,f,r]" in mem_iff_sats) -apply (rule sep_rules | simp)+ -done - - -subsection{*Separation for @{term "obase"}*} - -lemma obase_reflects: - "REFLECTS[\a. \x[L]. \g[L]. \mx[L]. \par[L]. - ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & - order_isomorphism(L,par,r,x,mx,g), - \i a. \x \ Lset(i). \g \ Lset(i). \mx \ Lset(i). \par \ Lset(i). - ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & - order_isomorphism(**Lset(i),par,r,x,mx,g)]" -by (intro FOL_reflections function_reflections fun_plus_reflections) - -lemma obase_separation: - --{*part of the order type formalization*} - "[| L(A); L(r) |] - ==> separation(L, \a. \x[L]. \g[L]. \mx[L]. \par[L]. - ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & - order_isomorphism(L,par,r,x,mx,g))" -apply (rule gen_separation [OF obase_reflects, of "{A,r}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[x,a,A,r]" in ordinal_iff_sats) -apply (rule sep_rules | simp)+ -done - - -subsection{*Separation for a Theorem about @{term "obase"}*} - -lemma obase_equals_reflects: - "REFLECTS[\x. x\A --> ~(\y[L]. \g[L]. - ordinal(L,y) & (\my[L]. \pxr[L]. - membership(L,y,my) & pred_set(L,A,x,r,pxr) & - order_isomorphism(L,pxr,r,y,my,g))), - \i x. x\A --> ~(\y \ Lset(i). \g \ Lset(i). - ordinal(**Lset(i),y) & (\my \ Lset(i). \pxr \ Lset(i). - membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) & - order_isomorphism(**Lset(i),pxr,r,y,my,g)))]" -by (intro FOL_reflections function_reflections fun_plus_reflections) - -lemma obase_equals_separation: - "[| L(A); L(r) |] - ==> separation (L, \x. x\A --> ~(\y[L]. \g[L]. - ordinal(L,y) & (\my[L]. \pxr[L]. - membership(L,y,my) & pred_set(L,A,x,r,pxr) & - order_isomorphism(L,pxr,r,y,my,g))))" -apply (rule gen_separation [OF obase_equals_reflects, of "{A,r}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+ -apply (rule_tac env = "[x,A,r]" in mem_iff_sats) -apply (rule sep_rules | simp)+ -done - - -subsection{*Replacement for @{term "omap"}*} - -lemma omap_reflects: - "REFLECTS[\z. \a[L]. a\B & (\x[L]. \g[L]. \mx[L]. \par[L]. - ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & - pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)), - \i z. \a \ Lset(i). a\B & (\x \ Lset(i). \g \ Lset(i). \mx \ Lset(i). - \par \ Lset(i). - ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) & - membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & - order_isomorphism(**Lset(i),par,r,x,mx,g))]" -by (intro FOL_reflections function_reflections fun_plus_reflections) - -lemma omap_replacement: - "[| L(A); L(r) |] - ==> strong_replacement(L, - \a z. \x[L]. \g[L]. \mx[L]. \par[L]. - ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & - pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))" -apply (rule strong_replacementI) -apply (rename_tac B) -apply (rule_tac u="{A,r,B}" in gen_separation [OF omap_reflects], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[a,z,A,B,r]" in mem_iff_sats) -apply (rule sep_rules | simp)+ -done - - -subsection{*Separation for a Theorem about @{term "obase"}*} +subsection{*Separation for a Theorem about @{term "is_recfun"}*} lemma is_recfun_reflects: "REFLECTS[\x. \xa[L]. \xb[L]. @@ -416,9 +309,7 @@ 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)+ + funspace_succ_replacement is_recfun_separation)+ done theorem M_basic_L: "PROP M_basic(L)" @@ -469,7 +360,6 @@ and is_recfun_relativize = M_basic.is_recfun_relativize [OF M_basic_L] and is_recfun_restrict = M_basic.is_recfun_restrict [OF M_basic_L] and univalent_is_recfun = M_basic.univalent_is_recfun [OF M_basic_L] - and exists_is_recfun_indstep = M_basic.exists_is_recfun_indstep [OF M_basic_L] and wellfounded_exists_is_recfun = M_basic.wellfounded_exists_is_recfun [OF M_basic_L] and wf_exists_is_recfun = M_basic.wf_exists_is_recfun [OF M_basic_L] and is_recfun_abs = M_basic.is_recfun_abs [OF M_basic_L] @@ -499,34 +389,8 @@ and membership_abs = M_basic.membership_abs [OF M_basic_L] and M_Memrel_iff = M_basic.M_Memrel_iff [OF M_basic_L] and Memrel_closed = M_basic.Memrel_closed [OF M_basic_L] - and wellordered_iso_predD = M_basic.wellordered_iso_predD [OF M_basic_L] - and wellordered_iso_pred_eq = M_basic.wellordered_iso_pred_eq [OF M_basic_L] and wellfounded_on_asym = M_basic.wellfounded_on_asym [OF M_basic_L] and wellordered_asym = M_basic.wellordered_asym [OF M_basic_L] - and ord_iso_pred_imp_lt = M_basic.ord_iso_pred_imp_lt [OF M_basic_L] - and obase_iff = M_basic.obase_iff [OF M_basic_L] - and omap_iff = M_basic.omap_iff [OF M_basic_L] - and omap_unique = M_basic.omap_unique [OF M_basic_L] - and omap_yields_Ord = M_basic.omap_yields_Ord [OF M_basic_L] - and otype_iff = M_basic.otype_iff [OF M_basic_L] - and otype_eq_range = M_basic.otype_eq_range [OF M_basic_L] - and Ord_otype = M_basic.Ord_otype [OF M_basic_L] - and domain_omap = M_basic.domain_omap [OF M_basic_L] - and omap_subset = M_basic.omap_subset [OF M_basic_L] - and omap_funtype = M_basic.omap_funtype [OF M_basic_L] - and wellordered_omap_bij = M_basic.wellordered_omap_bij [OF M_basic_L] - and omap_ord_iso = M_basic.omap_ord_iso [OF M_basic_L] - and Ord_omap_image_pred = M_basic.Ord_omap_image_pred [OF M_basic_L] - and restrict_omap_ord_iso = M_basic.restrict_omap_ord_iso [OF M_basic_L] - and obase_equals = M_basic.obase_equals [OF M_basic_L] - and omap_ord_iso_otype = M_basic.omap_ord_iso_otype [OF M_basic_L] - and obase_exists = M_basic.obase_exists [OF M_basic_L] - and omap_exists = M_basic.omap_exists [OF M_basic_L] - and otype_exists = M_basic.otype_exists [OF M_basic_L] - and omap_ord_iso_otype' = M_basic.omap_ord_iso_otype' [OF M_basic_L] - and ordertype_exists = M_basic.ordertype_exists [OF M_basic_L] - and relativized_imp_well_ord = M_basic.relativized_imp_well_ord [OF M_basic_L] - and well_ord_abs = M_basic.well_ord_abs [OF M_basic_L] declare cartprod_closed [intro, simp] declare sum_closed [intro, simp] diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,68 +1,12 @@ (* Title: ZF/Constructible/WF_absolute.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {*Absoluteness for Well-Founded Relations and Well-Founded Recursion*} theory WF_absolute = WFrec: -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) - - -constdefs - wfrank :: "[i,i]=>i" - "wfrank(r,a) == wfrec(r, a, %x f. \y \ r-``{x}. succ(f`y))" - -constdefs - wftype :: "i=>i" - "wftype(r) == \y \ range(r). succ(wfrank(r,y))" - -lemma wfrank: "wf(r) ==> wfrank(r,a) = (\y \ r-``{a}. succ(wfrank(r,y)))" -by (subst wfrank_def [THEN def_wfrec], simp_all) - -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) -done - -lemma wfrank_lt: "[|wf(r); \ r|] ==> wfrank(r,a) < wfrank(r,b)" -apply (rule_tac a1 = b in wfrank [THEN ssubst], assumption) -apply (rule UN_I [THEN ltI]) -apply (simp add: Ord_wfrank vimage_iff)+ -done - -lemma Ord_wftype: "wf(r) ==> Ord(wftype(r))" -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]) -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 (simp add: rvimage_iff wfrank_lt [THEN ltD]) -apply (blast intro: wftypeI) -done - -theorem wf_iff_subset_rvimage: - "relation(r) ==> wf(r) <-> (\i f A. Ord(i) & r <= rvimage(A, f, Memrel(i)))" -by (blast dest!: relation_field_times_field wf_imp_subset_rvimage - intro: wf_rvimage_Ord [THEN wf_subset]) - - subsection{*Transitive closure without fixedpoints*} constdefs @@ -236,271 +180,6 @@ rank function.*} -locale M_wfrank = M_trancl + - assumes wfrank_separation: - "M(r) ==> - separation (M, \x. - \rplus[M]. tran_closure(M,r,rplus) --> - ~ (\f[M]. M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f)))" - and wfrank_strong_replacement: - "M(r) ==> - strong_replacement(M, \x z. - \rplus[M]. tran_closure(M,r,rplus) --> - (\y[M]. \f[M]. pair(M,x,y,z) & - M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f) & - is_range(M,f,y)))" - and Ord_wfrank_separation: - "M(r) ==> - separation (M, \x. - \rplus[M]. tran_closure(M,r,rplus) --> - ~ (\f[M]. \rangef[M]. - is_range(M,f,rangef) --> - M_is_recfun(M, \x f y. is_range(M,f,y), rplus, x, f) --> - ordinal(M,rangef)))" - -text{*Proving that the relativized instances of Separation or Replacement -agree with the "real" ones.*} - -lemma (in M_wfrank) wfrank_separation': - "M(r) ==> - separation - (M, \x. ~ (\f[M]. is_recfun(r^+, x, %x f. range(f), f)))" -apply (insert wfrank_separation [of r]) -apply (simp add: relativize2_def is_recfun_abs [of "%x. range"]) -done - -lemma (in M_wfrank) wfrank_strong_replacement': - "M(r) ==> - strong_replacement(M, \x z. \y[M]. \f[M]. - pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) & - y = range(f))" -apply (insert wfrank_strong_replacement [of r]) -apply (simp add: relativize2_def is_recfun_abs [of "%x. range"]) -done - -lemma (in M_wfrank) Ord_wfrank_separation': - "M(r) ==> - separation (M, \x. - ~ (\f[M]. is_recfun(r^+, x, \x. range, f) --> Ord(range(f))))" -apply (insert Ord_wfrank_separation [of r]) -apply (simp add: relativize2_def is_recfun_abs [of "%x. range"]) -done - -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[M]. \f[M]. - p = & is_recfun(r^+, x, %x f. range(f), f) & - y = range(f)}" - -lemma (in M_wfrank) exists_wfrank: - "[| wellfounded(M,r); M(a); M(r) |] - ==> \f[M]. is_recfun(r^+, a, %x f. range(f), f)" -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_wfrank) M_wellfoundedrank: - "[| 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_trancl) - apply (rule trans_trancl) - apply (simp add: trancl_subset_times) -apply (blast dest: transM) -done - -lemma (in M_wfrank) Ord_wfrank_range [rule_format]: - "[| wellfounded(M,r); a\A; M(r); M(A) |] - ==> \f[M]. is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))" -apply (drule wellfounded_trancl, assumption) -apply (rule wellfounded_induct, assumption, erule (1) transM) - apply simp - apply (blast intro: Ord_wfrank_separation', clarify) -txt{*The reasoning in both cases is that we get @{term y} such 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 clarify - apply (frule apply_recfun2, assumption) - apply (force simp add: restrict_iff) -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) - (*simp_all won't work*) - 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 rspec) -apply assumption - apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) -apply (blast dest: pair_components_in_M) -done - -lemma (in M_wfrank) Ord_range_wellfoundedrank: - "[| wellfounded(M,r); r \ A*A; M(r); M(A) |] - ==> Ord (range(wellfoundedrank(M,r,A)))" -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{*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_tac x=u in ReplaceI) - apply simp - apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI) - apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2) - apply simp -apply blast -txt{*Unicity requirement of Replacement*} -apply clarify -apply (frule apply_recfun2, assumption) -apply (simp add: trans_trancl is_recfun_cut) -done - -lemma (in M_wfrank) function_wellfoundedrank: - "[| wellfounded(M,r); M(r); M(A)|] - ==> function(wellfoundedrank(M,r,A))" -apply (simp add: wellfoundedrank_def function_def, clarify) -txt{*Uniqueness: repeated below!*} -apply (drule is_recfun_functional, assumption) - apply (blast intro: wellfounded_trancl) - apply (simp_all add: trancl_subset_times trans_trancl) -done - -lemma (in M_wfrank) domain_wellfoundedrank: - "[| wellfounded(M,r); M(r); M(A)|] - ==> domain(wellfoundedrank(M,r,A)) = A" -apply (simp add: wellfoundedrank_def function_def) -apply (rule equalityI, auto) -apply (frule transM, assumption) -apply (frule_tac a=x in exists_wfrank, assumption+, clarify) -apply (rule_tac b="range(f)" in domainI) -apply (rule_tac x=x in ReplaceI) - apply simp - apply (rule_tac x=f in rexI, blast, simp_all) -txt{*Uniqueness (for Replacement): repeated above!*} -apply clarify -apply (drule is_recfun_functional, assumption) - apply (blast intro: wellfounded_trancl) - apply (simp_all add: trancl_subset_times trans_trancl) -done - -lemma (in M_wfrank) wellfoundedrank_type: - "[| wellfounded(M,r); M(r); M(A)|] - ==> wellfoundedrank(M,r,A) \ A -> range(wellfoundedrank(M,r,A))" -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_wfrank) Ord_wellfoundedrank: - "[| 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_wfrank) wellfoundedrank_eq: - "[| is_recfun(r^+, a, %x. range, f); - 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 (simp add: wellfoundedrank_def) -apply (rule ReplaceI) - apply (rule_tac x="range(f)" in rexI) - apply blast - apply simp_all -txt{*Unicity requirement of Replacement*} -apply clarify -apply (drule is_recfun_functional, assumption) - apply (blast intro: wellfounded_trancl) - apply (simp_all add: trancl_subset_times trans_trancl) -done - - -lemma (in M_wfrank) wellfoundedrank_lt: - "[| \ r; - wellfounded(M,r); r \ A*A; M(r); M(A)|] - ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b" -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], erule (1) transM, assumption) -apply clarify -apply (rename_tac fb) -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 (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) -done - - -lemma (in M_wfrank) wellfounded_imp_subset_rvimage: - "[|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: rvimage_iff wellfoundedrank_lt [THEN ltD]) -apply (blast intro: apply_rangeI wellfoundedrank_type) -done - -lemma (in M_wfrank) 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_wfrank) 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) -done - - -theorem (in M_wfrank) wf_abs [simp]: - "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)" -by (blast intro: wellfounded_imp_wf wf_imp_relativized) - -theorem (in M_wfrank) 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) - text{*absoluteness for wfrec-defined functions.*} @@ -531,7 +210,7 @@ before we can replace @{term "r^+"} by @{term r}. *} theorem (in M_trancl) trans_wfrec_relativize: "[|wf(r); trans(r); relation(r); M(r); M(a); - wfrec_replacement(M,MH,r); relativize2(M,MH,H); + wfrec_replacement(M,MH,r); relation2(M,MH,H); \x[M]. \g[M]. function(g) --> M(H(x,g))|] ==> wfrec(r,a,H) = z <-> (\f[M]. is_recfun(r,a,H,f) & z = H(a,f))" apply (frule wfrec_replacement', assumption+) @@ -542,15 +221,15 @@ theorem (in M_trancl) trans_wfrec_abs: "[|wf(r); trans(r); relation(r); M(r); M(a); M(z); - wfrec_replacement(M,MH,r); relativize2(M,MH,H); + wfrec_replacement(M,MH,r); relation2(M,MH,H); \x[M]. \g[M]. function(g) --> M(H(x,g))|] ==> is_wfrec(M,MH,r,a,z) <-> z=wfrec(r,a,H)" -apply (simp add: trans_wfrec_relativize [THEN iff_sym] is_wfrec_abs, blast) -done +by (simp add: trans_wfrec_relativize [THEN iff_sym] is_wfrec_abs, blast) + lemma (in M_trancl) trans_eq_pair_wfrec_iff: "[|wf(r); trans(r); relation(r); M(r); M(y); - wfrec_replacement(M,MH,r); relativize2(M,MH,H); + wfrec_replacement(M,MH,r); relation2(M,MH,H); \x[M]. \g[M]. function(g) --> M(H(x,g))|] ==> y = <-> (\f[M]. is_recfun(r,x,H,f) & y = )" @@ -565,7 +244,7 @@ subsection{*M is closed under well-founded recursion*} text{*Lemma with the awkward premise mentioning @{text wfrec}.*} -lemma (in M_wfrank) wfrec_closed_lemma [rule_format]: +lemma (in M_trancl) wfrec_closed_lemma [rule_format]: "[|wf(r); M(r); strong_replacement(M, \x y. y = \x, wfrec(r, x, H)\); \x[M]. \g[M]. function(g) --> M(H(x,g)) |] @@ -579,7 +258,7 @@ done text{*Eliminates one instance of replacement.*} -lemma (in M_wfrank) wfrec_replacement_iff: +lemma (in M_trancl) wfrec_replacement_iff: "strong_replacement(M, \x z. \y[M]. pair(M,x,y,z) & (\g[M]. is_recfun(r,x,H,g) & y = H(x,g))) <-> strong_replacement(M, @@ -589,9 +268,9 @@ done text{*Useful version for transitive relations*} -theorem (in M_wfrank) trans_wfrec_closed: +theorem (in M_trancl) trans_wfrec_closed: "[|wf(r); trans(r); relation(r); M(r); M(a); - wfrec_replacement(M,MH,r); relativize2(M,MH,H); + wfrec_replacement(M,MH,r); relation2(M,MH,H); \x[M]. \g[M]. function(g) --> M(H(x,g)) |] ==> M(wfrec(r,a,H))" apply (frule wfrec_replacement', assumption+) @@ -619,10 +298,10 @@ done text{*Full version not assuming transitivity, but maybe not very useful.*} -theorem (in M_wfrank) wfrec_closed: +theorem (in M_trancl) wfrec_closed: "[|wf(r); M(r); M(a); wfrec_replacement(M,MH,r^+); - relativize2(M,MH, \x f. H(x, restrict(f, r -`` {x}))); + relation2(M,MH, \x f. H(x, restrict(f, r -`` {x}))); \x[M]. \g[M]. function(g) --> M(H(x,g)) |] ==> M(wfrec(r,a,H))" apply (frule wfrec_replacement' diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/WFrec.thy --- a/src/ZF/Constructible/WFrec.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/WFrec.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/WFrec.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header{*Relativized Well-Founded Recursion*} @@ -292,9 +291,9 @@ lemma (in M_basic) is_recfun_abs: "[| \x[M]. \g[M]. function(g) --> M(H(x,g)); M(r); M(a); M(f); - relativize2(M,MH,H) |] + relation2(M,MH,H) |] ==> M_is_recfun(M,MH,r,a,f) <-> is_recfun(r,a,H,f)" -apply (simp add: M_is_recfun_def relativize2_def is_recfun_relativize) +apply (simp add: M_is_recfun_def relation2_def is_recfun_relativize) apply (rule rall_cong) apply (blast dest: transM) done @@ -307,16 +306,16 @@ lemma (in M_basic) is_wfrec_abs: "[| \x[M]. \g[M]. function(g) --> M(H(x,g)); - relativize2(M,MH,H); M(r); M(a); M(z) |] + relation2(M,MH,H); M(r); M(a); M(z) |] ==> is_wfrec(M,MH,r,a,z) <-> (\g[M]. is_recfun(r,a,H,g) & z = H(a,g))" -by (simp add: is_wfrec_def relativize2_def is_recfun_abs) +by (simp add: is_wfrec_def relation2_def is_recfun_abs) text{*Relating @{term wfrec_replacement} to native constructs*} lemma (in M_basic) wfrec_replacement': "[|wfrec_replacement(M,MH,r); \x[M]. \g[M]. function(g) --> M(H(x,g)); - relativize2(M,MH,H); M(r)|] + relation2(M,MH,H); M(r)|] ==> strong_replacement(M, \x z. \y[M]. pair(M,x,y,z) & (\g[M]. is_recfun(r,x,H,g) & y = H(x,g)))" by (simp add: wfrec_replacement_def is_wfrec_abs) @@ -329,259 +328,5 @@ by (simp add: is_wfrec_def wfrec_replacement_def) -subsection{*Ordinal Arithmetic: Two Examples of Recursion*} - -subsubsection{*Ordinal Addition*} - -(*FIXME: update to use new techniques!!*) -constdefs - (*This expresses ordinal addition in the language of ZF. It also - provides an abbreviation that can be used in the instance of strong - replacement below. Here j is used to define the relation, namely - Memrel(succ(j)), while x determines the domain of f.*) - is_oadd_fun :: "[i=>o,i,i,i,i] => o" - "is_oadd_fun(M,i,j,x,f) == - (\sj msj. M(sj) --> M(msj) --> - successor(M,j,sj) --> membership(M,sj,msj) --> - M_is_recfun(M, - %x g y. \gx[M]. image(M,g,x,gx) & union(M,i,gx,y), - msj, x, f))" - - is_oadd :: "[i=>o,i,i,i] => o" - "is_oadd(M,i,j,k) == - (~ ordinal(M,i) & ~ ordinal(M,j) & k=0) | - (~ ordinal(M,i) & ordinal(M,j) & k=j) | - (ordinal(M,i) & ~ ordinal(M,j) & k=i) | - (ordinal(M,i) & ordinal(M,j) & - (\f fj sj. M(f) & M(fj) & M(sj) & - successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) & - fun_apply(M,f,j,fj) & fj = k))" - - (*NEEDS RELATIVIZATION*) - omult_eqns :: "[i,i,i,i] => o" - "omult_eqns(i,x,g,z) == - Ord(x) & - (x=0 --> z=0) & - (\j. x = succ(j) --> z = g`j ++ i) & - (Limit(x) --> z = \(g``x))" - - is_omult_fun :: "[i=>o,i,i,i] => o" - "is_omult_fun(M,i,j,f) == - (\df. M(df) & is_function(M,f) & - is_domain(M,f,df) & subset(M, j, df)) & - (\x\j. omult_eqns(i,x,f,f`x))" - - is_omult :: "[i=>o,i,i,i] => o" - "is_omult(M,i,j,k) == - \f fj sj. M(f) & M(fj) & M(sj) & - successor(M,j,sj) & is_omult_fun(M,i,sj,f) & - fun_apply(M,f,j,fj) & fj = k" - - -locale M_ord_arith = M_basic + - assumes oadd_strong_replacement: - "[| M(i); M(j) |] ==> - strong_replacement(M, - \x z. \y[M]. pair(M,x,y,z) & - (\f[M]. \fx[M]. is_oadd_fun(M,i,j,x,f) & - image(M,f,x,fx) & y = i Un fx))" - - and omult_strong_replacement': - "[| M(i); M(j) |] ==> - strong_replacement(M, - \x z. \y[M]. z = & - (\g[M]. is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & - y = (THE z. omult_eqns(i, x, g, z))))" - - - -text{*@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF*} -lemma (in M_ord_arith) is_oadd_fun_iff: - "[| a\j; M(i); M(j); M(a); M(f) |] - ==> is_oadd_fun(M,i,j,a,f) <-> - f \ a \ range(f) & (\x. M(x) --> x < a --> f`x = i Un f``x)" -apply (frule lt_Ord) -apply (simp add: is_oadd_fun_def Memrel_closed Un_closed - relativize2_def is_recfun_abs [of "%x g. i Un g``x"] - image_closed is_recfun_iff_equation - Ball_def lt_trans [OF ltI, of _ a] lt_Memrel) -apply (simp add: lt_def) -apply (blast dest: transM) -done - - -lemma (in M_ord_arith) oadd_strong_replacement': - "[| M(i); M(j) |] ==> - strong_replacement(M, - \x z. \y[M]. z = & - (\g[M]. is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & - y = i Un g``x))" -apply (insert oadd_strong_replacement [of i j]) -apply (simp add: is_oadd_fun_def relativize2_def is_recfun_abs [of "%x g. i Un g``x"]) -done - - -lemma (in M_ord_arith) exists_oadd: - "[| Ord(j); M(i); M(j) |] - ==> \f[M]. is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)" -apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) - apply (simp_all add: Memrel_type oadd_strong_replacement') -done - -lemma (in M_ord_arith) exists_oadd_fun: - "[| Ord(j); M(i); M(j) |] ==> \f[M]. is_oadd_fun(M,i,succ(j),succ(j),f)" -apply (rule exists_oadd [THEN rexE]) -apply (erule Ord_succ, assumption, simp) -apply (rename_tac f) -apply (frule is_recfun_type) -apply (rule_tac x=f in rexI) - apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def - is_oadd_fun_iff Ord_trans [OF _ succI1], assumption) -done - -lemma (in M_ord_arith) is_oadd_fun_apply: - "[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |] - ==> f`x = i Un (\k\x. {f ` k})" -apply (simp add: is_oadd_fun_iff lt_Ord2, clarify) -apply (frule lt_closed, simp) -apply (frule leI [THEN le_imp_subset]) -apply (simp add: image_fun, blast) -done - -lemma (in M_ord_arith) is_oadd_fun_iff_oadd [rule_format]: - "[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] - ==> j f`j = i++j" -apply (erule_tac i=j in trans_induct, clarify) -apply (subgoal_tac "\k\x. k is_oadd(M,i,j,k) <-> k = i++j" -apply (simp add: is_oadd_def is_oadd_fun_iff_oadd) -apply (frule exists_oadd_fun [of j i], blast+) -done - -lemma (in M_ord_arith) oadd_abs: - "[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j" -apply (case_tac "Ord(i) & Ord(j)") - apply (simp add: Ord_oadd_abs) -apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd) -done - -lemma (in M_ord_arith) oadd_closed [intro,simp]: - "[| M(i); M(j) |] ==> M(i++j)" -apply (simp add: oadd_eq_if_raw_oadd, clarify) -apply (simp add: raw_oadd_eq_oadd) -apply (frule exists_oadd_fun [of j i], auto) -apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric]) -done - - -subsubsection{*Ordinal Multiplication*} - -lemma omult_eqns_unique: - "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'"; -apply (simp add: omult_eqns_def, clarify) -apply (erule Ord_cases, simp_all) -done - -lemma omult_eqns_0: "omult_eqns(i,0,g,z) <-> z=0" -by (simp add: omult_eqns_def) - -lemma the_omult_eqns_0: "(THE z. omult_eqns(i,0,g,z)) = 0" -by (simp add: omult_eqns_0) - -lemma omult_eqns_succ: "omult_eqns(i,succ(j),g,z) <-> Ord(j) & z = g`j ++ i" -by (simp add: omult_eqns_def) - -lemma the_omult_eqns_succ: - "Ord(j) ==> (THE z. omult_eqns(i,succ(j),g,z)) = g`j ++ i" -by (simp add: omult_eqns_succ) - -lemma omult_eqns_Limit: - "Limit(x) ==> omult_eqns(i,x,g,z) <-> z = \(g``x)" -apply (simp add: omult_eqns_def) -apply (blast intro: Limit_is_Ord) -done - -lemma the_omult_eqns_Limit: - "Limit(x) ==> (THE z. omult_eqns(i,x,g,z)) = \(g``x)" -by (simp add: omult_eqns_Limit) - -lemma omult_eqns_Not: "~ Ord(x) ==> ~ omult_eqns(i,x,g,z)" -by (simp add: omult_eqns_def) - - -lemma (in M_ord_arith) the_omult_eqns_closed: - "[| M(i); M(x); M(g); function(g) |] - ==> M(THE z. omult_eqns(i, x, g, z))" -apply (case_tac "Ord(x)") - prefer 2 apply (simp add: omult_eqns_Not) --{*trivial, non-Ord case*} -apply (erule Ord_cases) - apply (simp add: omult_eqns_0) - apply (simp add: omult_eqns_succ apply_closed oadd_closed) -apply (simp add: omult_eqns_Limit) -done - -lemma (in M_ord_arith) exists_omult: - "[| Ord(j); M(i); M(j) |] - ==> \f[M]. is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)" -apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) - apply (simp_all add: Memrel_type omult_strong_replacement') -apply (blast intro: the_omult_eqns_closed) -done - -lemma (in M_ord_arith) exists_omult_fun: - "[| Ord(j); M(i); M(j) |] ==> \f[M]. is_omult_fun(M,i,succ(j),f)" -apply (rule exists_omult [THEN rexE]) -apply (erule Ord_succ, assumption, simp) -apply (rename_tac f) -apply (frule is_recfun_type) -apply (rule_tac x=f in rexI) -apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def - is_omult_fun_def Ord_trans [OF _ succI1]) - apply (force dest: Ord_in_Ord' - simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ - the_omult_eqns_Limit, assumption) -done - -lemma (in M_ord_arith) is_omult_fun_apply_0: - "[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0" -by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib) - -lemma (in M_ord_arith) is_omult_fun_apply_succ: - "[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i" -by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast) - -lemma (in M_ord_arith) is_omult_fun_apply_Limit: - "[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |] - ==> f ` x = (\y\x. f`y)" -apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify) -apply (drule subset_trans [OF OrdmemD], assumption+) -apply (simp add: ball_conj_distrib omult_Limit image_function) -done - -lemma (in M_ord_arith) is_omult_fun_eq_omult: - "[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |] - ==> j f`j = i**j" -apply (erule_tac i=j in trans_induct3) -apply (safe del: impCE) - apply (simp add: is_omult_fun_apply_0) - apply (subgoal_tac "xk\x. k is_omult(M,i,j,k) <-> k = i**j" -apply (simp add: is_omult_def is_omult_fun_eq_omult) -apply (frule exists_omult_fun [of j i], blast+) -done - end diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Wellorderings.thy --- a/src/ZF/Constructible/Wellorderings.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/Wellorderings.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/Wellorderings.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {*Relativized Wellorderings*} @@ -220,60 +219,6 @@ wellfounded_on_subset) done -text{*Inductive argument for Kunen's Lemma 6.1, etc. - Simple proof from Halmos, page 72*} -lemma (in M_basic) wellordered_iso_subset_lemma: - "[| wellordered(M,A,r); f \ ord_iso(A,r, A',r); A'<= A; y \ A; - M(A); M(f); M(r) |] ==> ~ \ r" -apply (unfold wellordered_def ord_iso_def) -apply (elim conjE CollectE) -apply (erule wellfounded_on_induct, assumption+) - apply (insert well_ord_iso_separation [of A f r]) - apply (simp, clarify) -apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast) -done - - -text{*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment - of a well-ordering*} -lemma (in M_basic) wellordered_iso_predD: - "[| wellordered(M,A,r); f \ ord_iso(A, r, Order.pred(A,x,r), r); - M(A); M(f); M(r) |] ==> x \ A" -apply (rule notI) -apply (frule wellordered_iso_subset_lemma, assumption) -apply (auto elim: predE) -(*Now we know ~ (f`x < x) *) -apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) -(*Now we also know f`x \ pred(A,x,r); contradiction! *) -apply (simp add: Order.pred_def) -done - - -lemma (in M_basic) wellordered_iso_pred_eq_lemma: - "[| f \ \Order.pred(A,y,r), r\ \ \Order.pred(A,x,r), r\; - wellordered(M,A,r); x\A; y\A; M(A); M(f); M(r) |] ==> \ r" -apply (frule wellordered_is_trans_on, assumption) -apply (rule notI) -apply (drule_tac x2=y and x=x and r2=r in - wellordered_subset [OF _ pred_subset, THEN wellordered_iso_predD]) -apply (simp add: trans_pred_pred_eq) -apply (blast intro: predI dest: transM)+ -done - - -text{*Simple consequence of Lemma 6.1*} -lemma (in M_basic) wellordered_iso_pred_eq: - "[| wellordered(M,A,r); - f \ ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r); - M(A); M(f); M(r); a\A; c\A |] ==> a=c" -apply (frule wellordered_is_trans_on, assumption) -apply (frule wellordered_is_linear, assumption) -apply (erule_tac x=a and y=c in linearE, auto) -apply (drule ord_iso_sym) -(*two symmetric cases*) -apply (blast dest: wellordered_iso_pred_eq_lemma)+ -done - lemma (in M_basic) wellfounded_on_asym: "[| wellfounded_on(M,A,r); \r; a\A; x\A; M(A) |] ==> \r" apply (simp add: wellfounded_on_def) @@ -285,353 +230,4 @@ "[| wellordered(M,A,r); \r; a\A; x\A; M(A) |] ==> \r" by (simp add: wellordered_def, blast dest: wellfounded_on_asym) - -text{*Can't use @{text well_ord_iso_preserving} because it needs the -strong premise @{term "well_ord(A,r)"}*} -lemma (in M_basic) ord_iso_pred_imp_lt: - "[| f \ ord_iso(Order.pred(A,x,r), r, i, Memrel(i)); - g \ ord_iso(Order.pred(A,y,r), r, j, Memrel(j)); - wellordered(M,A,r); x \ A; y \ A; M(A); M(r); M(f); M(g); M(j); - Ord(i); Ord(j); \x,y\ \ r |] - ==> i < j" -apply (frule wellordered_is_trans_on, assumption) -apply (frule_tac y=y in transM, assumption) -apply (rule_tac i=i and j=j in Ord_linear_lt, auto) -txt{*case @{term "i=j"} yields a contradiction*} - apply (rule_tac x1=x and A1="Order.pred(A,y,r)" in - wellordered_iso_predD [THEN notE]) - apply (blast intro: wellordered_subset [OF _ pred_subset]) - apply (simp add: trans_pred_pred_eq) - apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) - apply (simp_all add: pred_iff pred_closed converse_closed comp_closed) -txt{*case @{term "j Order.pred(A,x,r)"}*} -apply (simp add: pred_iff) -apply (subgoal_tac - "\h[M]. h \ ord_iso(Order.pred(A,y,r), r, - Order.pred(A, converse(f)`j, r), r)") - apply (clarify, frule wellordered_iso_pred_eq, assumption+) - apply (blast dest: wellordered_asym) -apply (intro rexI) - apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)+ -done - - -lemma ord_iso_converse1: - "[| f: ord_iso(A,r,B,s); : s; a:A; b:B |] - ==> : r" -apply (frule ord_iso_converse, assumption+) -apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype]) -apply (simp add: left_inverse_bij [OF ord_iso_is_bij]) -done - - -subsection {* Order Types: A Direct Construction by Replacement*} - -text{*This follows Kunen's Theorem I 7.6, page 17.*} - -constdefs - - obase :: "[i=>o,i,i,i] => o" - --{*the domain of @{text om}, eventually shown to equal @{text A}*} - "obase(M,A,r,z) == - \a[M]. - a \ z <-> - (a\A & (\x[M]. \g[M]. Ord(x) & - order_isomorphism(M,Order.pred(A,a,r),r,x,Memrel(x),g)))" - - - omap :: "[i=>o,i,i,i] => o" - --{*the function that maps wosets to order types*} - "omap(M,A,r,f) == - \z[M]. - z \ f <-> - (\a[M]. a\A & - (\x[M]. \g[M]. \mx[M]. \par[M]. - ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & - pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g)))" - - - otype :: "[i=>o,i,i,i] => o" --{*the order types themselves*} - "otype(M,A,r,i) == \f[M]. omap(M,A,r,f) & is_range(M,f,i)" - - - -lemma (in M_basic) obase_iff: - "[| M(A); M(r); M(z) |] - ==> obase(M,A,r,z) <-> - z = {a\A. \x[M]. \g[M]. Ord(x) & - g \ ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}" -apply (simp add: obase_def Memrel_closed pred_closed) -apply (rule iffI) - prefer 2 apply blast -apply (rule equalityI) - apply (clarify, frule transM, assumption, simp) -apply (clarify, frule transM, assumption, force) -done - -text{*Can also be proved with the premise @{term "M(z)"} instead of - @{term "M(f)"}, but that version is less useful.*} -lemma (in M_basic) omap_iff: - "[| omap(M,A,r,f); M(A); M(r); M(f) |] - ==> z \ f <-> - (\a\A. \x[M]. \g[M]. z = & Ord(x) & - g \ ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))" -apply (simp add: omap_def Memrel_closed pred_closed) -apply (rule iffI) - apply (drule_tac [2] x=z in rspec) - apply (drule_tac x=z in rspec) - apply (blast dest: transM)+ -done - -lemma (in M_basic) omap_unique: - "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" -apply (rule equality_iffI) -apply (simp add: omap_iff) -done - -lemma (in M_basic) omap_yields_Ord: - "[| omap(M,A,r,f); \a,x\ \ f; M(a); M(x) |] ==> Ord(x)" - by (simp add: omap_def) - -lemma (in M_basic) otype_iff: - "[| otype(M,A,r,i); M(A); M(r); M(i) |] - ==> x \ i <-> - (M(x) & Ord(x) & - (\a\A. \g[M]. g \ ord_iso(Order.pred(A,a,r),r,x,Memrel(x))))" -apply (auto simp add: omap_iff otype_def) - apply (blast intro: transM) -apply (rule rangeI) -apply (frule transM, assumption) -apply (simp add: omap_iff, blast) -done - -lemma (in M_basic) otype_eq_range: - "[| omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) |] - ==> i = range(f)" -apply (auto simp add: otype_def omap_iff) -apply (blast dest: omap_unique) -done - - -lemma (in M_basic) Ord_otype: - "[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)" -apply (rule OrdI) -prefer 2 - apply (simp add: Ord_def otype_def omap_def) - apply clarify - apply (frule pair_components_in_M, assumption) - apply blast -apply (auto simp add: Transset_def otype_iff) - apply (blast intro: transM) - apply (blast intro: Ord_in_Ord) -apply (rename_tac y a g) -apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun, - THEN apply_funtype], assumption) -apply (rule_tac x="converse(g)`y" in bexI) - apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption) -apply (safe elim!: predE) -apply (blast intro: restrict_ord_iso ord_iso_sym ltI dest: transM) -done - -lemma (in M_basic) domain_omap: - "[| omap(M,A,r,f); obase(M,A,r,B); M(A); M(r); M(B); M(f) |] - ==> domain(f) = B" -apply (simp add: domain_closed obase_iff) -apply (rule equality_iffI) -apply (simp add: domain_iff omap_iff, blast) -done - -lemma (in M_basic) omap_subset: - "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); - M(A); M(r); M(f); M(B); M(i) |] ==> f \ B * i" -apply clarify -apply (simp add: omap_iff obase_iff) -apply (force simp add: otype_iff) -done - -lemma (in M_basic) omap_funtype: - "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); - M(A); M(r); M(f); M(B); M(i) |] ==> f \ B -> i" -apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) -apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) -done - - -lemma (in M_basic) wellordered_omap_bij: - "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); - M(A); M(r); M(f); M(B); M(i) |] ==> f \ bij(B,i)" -apply (insert omap_funtype [of A r f B i]) -apply (auto simp add: bij_def inj_def) -prefer 2 apply (blast intro: fun_is_surj dest: otype_eq_range) -apply (frule_tac a=w in apply_Pair, assumption) -apply (frule_tac a=x in apply_Pair, assumption) -apply (simp add: omap_iff) -apply (blast intro: wellordered_iso_pred_eq ord_iso_sym ord_iso_trans) -done - - -text{*This is not the final result: we must show @{term "oB(A,r) = A"}*} -lemma (in M_basic) omap_ord_iso: - "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); - M(A); M(r); M(f); M(B); M(i) |] ==> f \ ord_iso(B,r,i,Memrel(i))" -apply (rule ord_isoI) - apply (erule wellordered_omap_bij, assumption+) -apply (insert omap_funtype [of A r f B i], simp) -apply (frule_tac a=x in apply_Pair, assumption) -apply (frule_tac a=y in apply_Pair, assumption) -apply (auto simp add: omap_iff) - txt{*direction 1: assuming @{term "\x,y\ \ r"}*} - apply (blast intro: ltD ord_iso_pred_imp_lt) - txt{*direction 2: proving @{term "\x,y\ \ r"} using linearity of @{term r}*} -apply (rename_tac x y g ga) -apply (frule wellordered_is_linear, assumption, - erule_tac x=x and y=y in linearE, assumption+) -txt{*the case @{term "x=y"} leads to immediate contradiction*} -apply (blast elim: mem_irrefl) -txt{*the case @{term "\y,x\ \ r"}: handle like the opposite direction*} -apply (blast dest: ord_iso_pred_imp_lt ltD elim: mem_asym) -done - -lemma (in M_basic) Ord_omap_image_pred: - "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); - M(A); M(r); M(f); M(B); M(i); b \ A |] ==> Ord(f `` Order.pred(A,b,r))" -apply (frule wellordered_is_trans_on, assumption) -apply (rule OrdI) - prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast) -txt{*Hard part is to show that the image is a transitive set.*} -apply (simp add: Transset_def, clarify) -apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f B i]]) -apply (rename_tac c j, clarify) -apply (frule omap_funtype [of A r f B, THEN apply_funtype], assumption+) -apply (subgoal_tac "j : i") - prefer 2 apply (blast intro: Ord_trans Ord_otype) -apply (subgoal_tac "converse(f) ` j : B") - prefer 2 - apply (blast dest: wellordered_omap_bij [THEN bij_converse_bij, - THEN bij_is_fun, THEN apply_funtype]) -apply (rule_tac x="converse(f) ` j" in bexI) - apply (simp add: right_inverse_bij [OF wellordered_omap_bij]) -apply (intro predI conjI) - apply (erule_tac b=c in trans_onD) - apply (rule ord_iso_converse1 [OF omap_ord_iso [of A r f B i]]) -apply (auto simp add: obase_iff) -done - -lemma (in M_basic) restrict_omap_ord_iso: - "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); - D \ B; M(A); M(r); M(f); M(B); M(i) |] - ==> restrict(f,D) \ (\D,r\ \ \f``D, Memrel(f``D)\)" -apply (frule ord_iso_restrict_image [OF omap_ord_iso [of A r f B i]], - assumption+) -apply (drule ord_iso_sym [THEN subset_ord_iso_Memrel]) -apply (blast dest: subsetD [OF omap_subset]) -apply (drule ord_iso_sym, simp) -done - -lemma (in M_basic) obase_equals: - "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); - M(A); M(r); M(f); M(B); M(i) |] ==> B = A" -apply (rule equalityI, force simp add: obase_iff, clarify) -apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp) -apply (frule wellordered_is_wellfounded_on, assumption) -apply (erule wellfounded_on_induct, assumption+) - apply (frule obase_equals_separation [of A r], assumption) - apply (simp, clarify) -apply (rename_tac b) -apply (subgoal_tac "Order.pred(A,b,r) <= B") - apply (blast intro!: restrict_omap_ord_iso Ord_omap_image_pred) -apply (force simp add: pred_iff obase_iff) -done - - - -text{*Main result: @{term om} gives the order-isomorphism - @{term "\A,r\ \ \i, Memrel(i)\"} *} -theorem (in M_basic) omap_ord_iso_otype: - "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); - M(A); M(r); M(f); M(B); M(i) |] ==> f \ ord_iso(A, r, i, Memrel(i))" -apply (frule omap_ord_iso, assumption+) -apply (frule obase_equals, assumption+, blast) -done - -lemma (in M_basic) obase_exists: - "[| M(A); M(r) |] ==> \z[M]. obase(M,A,r,z)" -apply (simp add: obase_def) -apply (insert obase_separation [of A r]) -apply (simp add: separation_def) -done - -lemma (in M_basic) omap_exists: - "[| M(A); M(r) |] ==> \z[M]. omap(M,A,r,z)" -apply (insert obase_exists [of A r]) -apply (simp add: omap_def) -apply (insert omap_replacement [of A r]) -apply (simp add: strong_replacement_def, clarify) -apply (drule_tac x=x in rspec, clarify) -apply (simp add: Memrel_closed pred_closed obase_iff) -apply (erule impE) - apply (clarsimp simp add: univalent_def) - apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify) -apply (rule_tac x=Y in rexI) -apply (simp add: Memrel_closed pred_closed obase_iff, blast, assumption) -done - -declare rall_simps [simp] rex_simps [simp] - -lemma (in M_basic) otype_exists: - "[| wellordered(M,A,r); M(A); M(r) |] ==> \i[M]. otype(M,A,r,i)" -apply (insert omap_exists [of A r]) -apply (simp add: otype_def, safe) -apply (rule_tac x="range(x)" in rexI) -apply blast+ -done - -theorem (in M_basic) omap_ord_iso_otype': - "[| wellordered(M,A,r); M(A); M(r) |] - ==> \f[M]. (\i[M]. Ord(i) & f \ ord_iso(A, r, i, Memrel(i)))" -apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify) -apply (rename_tac i) -apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) -apply (rule Ord_otype) - apply (force simp add: otype_def range_closed) - apply (simp_all add: wellordered_is_trans_on) -done - -lemma (in M_basic) ordertype_exists: - "[| wellordered(M,A,r); M(A); M(r) |] - ==> \f[M]. (\i[M]. Ord(i) & f \ ord_iso(A, r, i, Memrel(i)))" -apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify) -apply (rename_tac i) -apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype') -apply (rule Ord_otype) - apply (force simp add: otype_def range_closed) - apply (simp_all add: wellordered_is_trans_on) -done - - -lemma (in M_basic) relativized_imp_well_ord: - "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" -apply (insert ordertype_exists [of A r], simp) -apply (blast intro: well_ord_ord_iso well_ord_Memrel) -done - -subsection {*Kunen's theorem 5.4, poage 127*} - -text{*(a) The notion of Wellordering is absolute*} -theorem (in M_basic) well_ord_abs [simp]: - "[| M(A); M(r) |] ==> wellordered(M,A,r) <-> well_ord(A,r)" -by (blast intro: well_ord_imp_relativized relativized_imp_well_ord) - - -text{*(b) Order types are absolute*} -lemma (in M_basic) - "[| wellordered(M,A,r); f \ ord_iso(A, r, i, Memrel(i)); - M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)" -by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso - Ord_iso_implies_eq ord_iso_sym ord_iso_trans) - end diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/IsaMakefile Wed Oct 09 11:07:13 2002 +0200 @@ -83,6 +83,7 @@ Constructible/AC_in_L.thy Constructible/Relative.thy \ Constructible/L_axioms.thy Constructible/Wellorderings.thy \ Constructible/MetaExists.thy Constructible/Normal.thy \ + Constructible/Rank.thy Constructible/Rank_Separation.thy \ Constructible/Rec_Separation.thy Constructible/Separation.thy \ Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \ Constructible/Reflection.thy Constructible/WFrec.thy \ diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/OrderArith.thy --- a/src/ZF/OrderArith.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/OrderArith.thy Wed Oct 09 11:07:13 2002 +0200 @@ -398,6 +398,61 @@ by (unfold ord_iso_def rvimage_def, blast) +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) + + +constdefs + wfrank :: "[i,i]=>i" + "wfrank(r,a) == wfrec(r, a, %x f. \y \ r-``{x}. succ(f`y))" + +constdefs + wftype :: "i=>i" + "wftype(r) == \y \ range(r). succ(wfrank(r,y))" + +lemma wfrank: "wf(r) ==> wfrank(r,a) = (\y \ r-``{a}. succ(wfrank(r,y)))" +by (subst wfrank_def [THEN def_wfrec], simp_all) + +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) +done + +lemma wfrank_lt: "[|wf(r); \ r|] ==> wfrank(r,a) < wfrank(r,b)" +apply (rule_tac a1 = b in wfrank [THEN ssubst], assumption) +apply (rule UN_I [THEN ltI]) +apply (simp add: Ord_wfrank vimage_iff)+ +done + +lemma Ord_wftype: "wf(r) ==> Ord(wftype(r))" +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]) +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 (simp add: rvimage_iff wfrank_lt [THEN ltD]) +apply (blast intro: wftypeI) +done + +theorem wf_iff_subset_rvimage: + "relation(r) ==> wf(r) <-> (\i f A. Ord(i) & r <= rvimage(A, f, Memrel(i)))" +by (blast dest!: relation_field_times_field wf_imp_subset_rvimage + intro: wf_rvimage_Ord [THEN wf_subset]) + + subsection{*Other Results*} lemma wf_times: "A Int B = 0 ==> wf(A*B)" diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/WF.thy --- a/src/ZF/WF.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/WF.thy Wed Oct 09 11:07:13 2002 +0200 @@ -47,7 +47,7 @@ subsection{*Well-Founded Relations*} -(** Equivalences between wf and wf_on **) +subsubsection{*Equivalences between @{term wf} and @{term wf_on}*} lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)" apply (unfold wf_def wf_on_def, clarify) (*needed for blast's efficiency*) @@ -72,10 +72,11 @@ lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)" by (simp add: wf_def, fast) -(** Introduction rules for wf_on **) +subsubsection{*Introduction Rules for @{term wf_on}*} +text{*If every non-empty subset of @{term A} has an @{term r}-minimal element + then we have @{term "wf[A](r)"}.*} lemma wf_onI: -(*If every non-empty subset of A has an r-minimal element then wf[A](r).*) assumes prem: "!!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. :r |] ==> False" shows "wf[A](r)" apply (unfold wf_on_def wf_def) @@ -83,9 +84,9 @@ apply (rule_tac Z = "Z" in prem, blast+) done -(*If r allows well-founded induction over A then wf[A](r) - Premise is equivalent to - !!B. ALL x:A. (ALL y. : r --> y:B) --> x:B ==> A<=B *) +text{*If @{term r} allows well-founded induction over @{term A} + then we have @{term "wf[A](r)"}. Premise is equivalent to + @{term "!!B. ALL x:A. (ALL y. : r --> y:B) --> x:B ==> A<=B"} *} lemma wf_onI2: assumes prem: "!!y B. [| ALL x:A. (ALL y:A. :r --> y:B) --> x:B; y:A |] ==> y:B" @@ -97,13 +98,14 @@ done -(** Well-founded Induction **) +subsubsection{*Well-founded Induction*} -(*Consider the least z in domain(r) such that P(z) does not hold...*) +text{*Consider the least @{term z} in @{term "domain(r)"} such that + @{term "P(z)"} does not hold...*} lemma wf_induct [induct set: wf]: "[| wf(r); - !!x.[| ALL y. : r --> P(y) |] ==> P(x) - |] ==> P(a)" + !!x.[| ALL y. : r --> P(y) |] ==> P(x) |] + ==> P(a)" apply (unfold wf_def) apply (erule_tac x = "{z : domain(r). ~ P(z)}" in allE) apply blast @@ -111,7 +113,7 @@ lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf] -(*The form of this rule is designed to match wfI*) +text{*The form of this rule is designed to match @{text wfI}*} lemma wf_induct2: "[| wf(r); a:A; field(r)<=A; !!x.[| x: A; ALL y. : r --> P(y) |] ==> P(x) |] @@ -136,7 +138,8 @@ wf_on_induct [rule_format, consumes 2, induct set: wf_on] -(*If r allows well-founded induction then wf(r)*) +text{*If @{term r} allows well-founded induction + then we have @{term "wf(r)"}.*} lemma wfI: "[| field(r)<=A; !!y B. [| ALL x:A. (ALL y:A. :r --> y:B) --> x:B; y:A|] @@ -185,8 +188,8 @@ - -(*transitive closure of a WF relation is WF provided A is downwards closed*) +text{*transitive closure of a WF relation is WF provided + @{term A} is downward closed*} lemma wf_on_trancl: "[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)" apply (rule wf_onI2) @@ -204,13 +207,13 @@ done - -(** r-``{a} is the set of everything under a in r **) +text{*@{term "r-``{a}"} is the set of everything under @{term a} in @{term r}*} lemmas underI = vimage_singleton_iff [THEN iffD2, standard] lemmas underD = vimage_singleton_iff [THEN iffD1, standard] -(** is_recfun **) + +subsection{*The Predicate @{term is_recfun}*} lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)" apply (unfold is_recfun_def) @@ -281,7 +284,7 @@ apply (rule_tac f = "lam y: r-``{a1}. wftrec (r,y,H)" in is_the_recfun) apply typecheck apply (unfold is_recfun_def wftrec_def) -(*Applying the substitution: must keep the quantified assumption!!*) + --{*Applying the substitution: must keep the quantified assumption!*} apply (rule lam_cong [OF refl]) apply (drule underD) apply (fold is_recfun_def) @@ -316,7 +319,8 @@ apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut) done -(** Removal of the premise trans(r) **) + +subsubsection{*Removal of the Premise @{term "trans(r)"}*} (*NOT SUITABLE FOR REWRITING: it is recursive!*) lemma wfrec: @@ -355,11 +359,11 @@ apply (simp add: vimage_Int_square cons_subset_iff) done -(*Minimal-element characterization of well-foundedness*) +text{*Minimal-element characterization of well-foundedness*} lemma wf_eq_minimal: "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. :r --> y~:Q))" -apply (unfold wf_def, blast) -done +by (unfold wf_def, blast) + ML {*