# HG changeset patch # User paulson # Date 1036748080 -3600 # Node ID c7cf8fa665341792165206892edb3cdb53af9eb9 # Parent 0a9228532106e110243f9432e14c6e7fa22efb79 Polishing. lambda_abs2 doesn't need an instance of replacement various renamings & restructurings diff -r 0a9228532106 -r c7cf8fa66534 src/ZF/Constructible/AC_in_L.thy --- a/src/ZF/Constructible/AC_in_L.thy Fri Nov 08 10:28:29 2002 +0100 +++ b/src/ZF/Constructible/AC_in_L.thy Fri Nov 08 10:34:40 2002 +0100 @@ -220,9 +220,7 @@ which are lists built over @{term "A"}. We combine it with the enumeration of formulas. The order type of the resulting wellordering gives us a map from (environment, formula) pairs into the ordinals. For each member of @{term -"DPow(A)"}, we take the minimum such ordinal. This yields a wellordering of -@{term "DPow(A)-A"}, namely the set of elements just introduced, which we then -extend to the full set @{term "DPow(A)"}.*} +"DPow(A)"}, we take the minimum such ordinal.*} constdefs env_form_r :: "[i,i,i]=>i" @@ -236,25 +234,21 @@ "env_form_map(f,r,A,z) == ordermap(list(A) * formula, env_form_r(f,r,A)) ` z" - DPow_new_ord :: "[i,i,i,i,i]=>o" + DPow_ord :: "[i,i,i,i,i]=>o" --{*predicate that holds if @{term k} is a valid index for @{term X}*} - "DPow_new_ord(f,r,A,X,k) == + "DPow_ord(f,r,A,X,k) == \env \ list(A). \p \ formula. arity(p) \ succ(length(env)) & X = {x\A. sats(A, p, Cons(x,env))} & env_form_map(f,r,A,) = k" - DPow_new_least :: "[i,i,i,i]=>i" + DPow_least :: "[i,i,i,i]=>i" --{*function yielding the smallest index for @{term X}*} - "DPow_new_least(f,r,A,X) == \k. DPow_new_ord(f,r,A,X,k)" - - DPow_new_r :: "[i,i,i]=>i" - --{*a wellordering on the difference set @{term "DPow(A)-A"}*} - "DPow_new_r(f,r,A) == measure(DPow(A)-A, DPow_new_least(f,r,A))" + "DPow_least(f,r,A,X) == \k. DPow_ord(f,r,A,X,k)" DPow_r :: "[i,i,i]=>i" --{*a wellordering on @{term "DPow(A)"}*} - "DPow_r(f,r,A) == (DPow_new_r(f,r,A) Un (A * (DPow(A)-A))) Un r" + "DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))" lemma (in Nat_Times_Nat) well_ord_env_form_r: @@ -267,23 +261,23 @@ ==> Ord(env_form_map(fn,r,A,z))" by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r) -lemma DPow_imp_ex_DPow_new_ord: - "X \ DPow(A) ==> \k. DPow_new_ord(fn,r,A,X,k)" -apply (simp add: DPow_new_ord_def) +lemma DPow_imp_ex_DPow_ord: + "X \ DPow(A) ==> \k. DPow_ord(fn,r,A,X,k)" +apply (simp add: DPow_ord_def) apply (blast dest!: DPowD) done -lemma (in Nat_Times_Nat) DPow_new_ord_imp_Ord: - "[|DPow_new_ord(fn,r,A,X,k); well_ord(A,r)|] ==> Ord(k)" -apply (simp add: DPow_new_ord_def, clarify) +lemma (in Nat_Times_Nat) DPow_ord_imp_Ord: + "[|DPow_ord(fn,r,A,X,k); well_ord(A,r)|] ==> Ord(k)" +apply (simp add: DPow_ord_def, clarify) apply (simp add: Ord_env_form_map) done -lemma (in Nat_Times_Nat) DPow_imp_DPow_new_least: +lemma (in Nat_Times_Nat) DPow_imp_DPow_least: "[|X \ DPow(A); well_ord(A,r)|] - ==> DPow_new_ord(fn, r, A, X, DPow_new_least(fn,r,A,X))" -apply (simp add: DPow_new_least_def) -apply (blast dest: DPow_imp_ex_DPow_new_ord intro: DPow_new_ord_imp_Ord LeastI) + ==> DPow_ord(fn, r, A, X, DPow_least(fn,r,A,X))" +apply (simp add: DPow_least_def) +apply (blast dest: DPow_imp_ex_DPow_ord intro: DPow_ord_imp_Ord LeastI) done lemma (in Nat_Times_Nat) env_form_map_inject: @@ -295,63 +289,26 @@ OF well_ord_env_form_r], assumption+) done - -lemma (in Nat_Times_Nat) DPow_new_ord_unique: - "[|DPow_new_ord(fn,r,A,X,k); DPow_new_ord(fn,r,A,Y,k); well_ord(A,r)|] +lemma (in Nat_Times_Nat) DPow_ord_unique: + "[|DPow_ord(fn,r,A,X,k); DPow_ord(fn,r,A,Y,k); well_ord(A,r)|] ==> X=Y" -apply (simp add: DPow_new_ord_def, clarify) +apply (simp add: DPow_ord_def, clarify) apply (drule env_form_map_inject, auto) done -lemma (in Nat_Times_Nat) well_ord_DPow_new_r: - "well_ord(A,r) ==> well_ord(DPow(A)-A, DPow_new_r(fn,r,A))" -apply (simp add: DPow_new_r_def) +lemma (in Nat_Times_Nat) well_ord_DPow_r: + "well_ord(A,r) ==> well_ord(DPow(A), DPow_r(fn,r,A))" +apply (simp add: DPow_r_def) apply (rule well_ord_measure) - apply (simp add: DPow_new_least_def Ord_Least, clarify) -apply (drule DPow_imp_DPow_new_least, assumption)+ + apply (simp add: DPow_least_def Ord_Least) +apply (drule DPow_imp_DPow_least, assumption)+ apply simp -apply (blast intro: DPow_new_ord_unique) -done - -lemma DPow_new_r_subset: "DPow_new_r(f,r,A) <= (DPow(A)-A) * (DPow(A)-A)" -by (simp add: DPow_new_r_def measure_type) - -lemma (in Nat_Times_Nat) linear_DPow_r: - "well_ord(A,r) - ==> linear(DPow(A), DPow_r(fn, r, A))" -apply (frule well_ord_DPow_new_r) -apply (drule well_ord_is_linear)+ -apply (auto simp add: linear_def DPow_r_def) -done - - -lemma (in Nat_Times_Nat) wf_DPow_new_r: - "well_ord(A,r) ==> wf(DPow_new_r(fn,r,A))" -apply (rule well_ord_DPow_new_r [THEN well_ord_is_wf, THEN wf_on_imp_wf], - assumption+) -apply (rule DPow_new_r_subset) -done - -lemma (in Nat_Times_Nat) well_ord_DPow_r: - "[|well_ord(A,r); r \ A * A|] - ==> well_ord(DPow(A), DPow_r(fn,r,A))" -apply (rule well_ordI [OF wf_imp_wf_on]) - prefer 2 apply (blast intro: linear_DPow_r) -apply (simp add: DPow_r_def) -apply (rule wf_Un) - apply (cut_tac DPow_new_r_subset [of fn r A], blast) - apply (rule wf_Un) - apply (cut_tac DPow_new_r_subset [of fn r A], blast) - apply (blast intro: wf_DPow_new_r) - apply (simp add: wf_times Diff_disjoint) -apply (blast intro: well_ord_is_wf wf_on_imp_wf) +apply (blast intro: DPow_ord_unique) done lemma (in Nat_Times_Nat) DPow_r_type: - "[|r \ A * A; A \ DPow(A)|] - ==> DPow_r(fn,r,A) \ DPow(A) * DPow(A)" -apply (simp add: DPow_r_def DPow_new_r_def measure_def, blast) -done + "DPow_r(fn,r,A) \ DPow(A) * DPow(A)" +by (simp add: DPow_r_def measure_def, blast) subsection{*Limit Construction for Well-Orderings*} @@ -362,29 +319,21 @@ constdefs rlimit :: "[i,i=>i]=>i" - --{*expresses the wellordering at limit ordinals.*} + --{*Expresses the wellordering at limit ordinals. The conditional + lets us remove the premise @{term "Limit(i)"} from some theorems.*} "rlimit(i,r) == - {z: Lset(i) * Lset(i). - \x' x. z = & - (lrank(x') < lrank(x) | - (lrank(x') = lrank(x) & \ r(succ(lrank(x)))))}" + if Limit(i) then + {z: Lset(i) * Lset(i). + \x' x. z = & + (lrank(x') < lrank(x) | + (lrank(x') = lrank(x) & \ r(succ(lrank(x)))))} + else 0" Lset_new :: "i=>i" --{*This constant denotes the set of elements introduced at level @{term "succ(i)"}*} "Lset_new(i) == {x \ Lset(succ(i)). lrank(x) = i}" -lemma Lset_new_iff_lrank_eq: - "Ord(i) ==> x \ Lset_new(i) <-> L(x) & lrank(x) = i" -by (auto simp add: Lset_new_def Lset_iff_lrank_lt) - -lemma Lset_new_eq: - "Ord(i) ==> Lset_new(i) = Lset(succ(i)) - Lset(i)" -apply (rule equality_iffI) -apply (simp add: Lset_new_iff_lrank_eq Lset_iff_lrank_lt, auto) -apply (blast elim: leE) -done - lemma Limit_Lset_eq2: "Limit(i) ==> Lset(i) = (\j\i. Lset_new(j))" apply (simp add: Limit_Lset_eq) @@ -404,11 +353,14 @@ "wf[Lset(succ(j))](r(succ(j))) ==> wf[Lset_new(j)](rlimit(i,r))" apply (simp add: wf_on_def Lset_new_def) apply (erule wf_subset) -apply (force simp add: rlimit_def) +apply (simp add: rlimit_def, force) done lemma wf_on_rlimit: - "[|Limit(i); \j wf[Lset(i)](rlimit(i,r))" + "(\j wf[Lset(i)](rlimit(i,r))" +apply (case_tac "Limit(i)") + prefer 2 + apply (simp add: rlimit_def wf_on_any_0) apply (simp add: Limit_Lset_eq2) apply (rule wf_on_Union) apply (rule wf_imp_wf_on [OF wf_Memrel [of i]]) @@ -438,51 +390,33 @@ by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf linear_rlimit well_ord_is_linear) +lemma rlimit_cong: + "(!!j. j r'(j) = r(j)) ==> rlimit(i,r) = rlimit(i,r')" +apply (simp add: rlimit_def, clarify) +apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+ +apply (simp add: Limit_is_Ord Lset_lrank_lt) +done + subsection{*Transfinite Definition of the Wellordering on @{term "L"}*} constdefs L_r :: "[i, i] => i" - "L_r(f,i) == - transrec(i, \x r. - if x=0 then 0 - else if Limit(x) then rlimit(x, \y. r`y) - else DPow_r(f, r ` Arith.pred(x), Lset(Arith.pred(x))))" + "L_r(f) == %i. + transrec3(i, 0, \x r. DPow_r(f, r, Lset(x)), + \x r. rlimit(x, \y. r`y))" subsubsection{*The Corresponding Recursion Equations*} lemma [simp]: "L_r(f,0) = 0" -by (simp add: def_transrec [OF L_r_def]) +by (simp add: L_r_def) -lemma [simp]: "Ord(i) ==> L_r(f, succ(i)) = DPow_r(f, L_r(f,i), Lset(i))" -by (simp add: def_transrec [OF L_r_def]) +lemma [simp]: "L_r(f, succ(i)) = DPow_r(f, L_r(f,i), Lset(i))" +by (simp add: L_r_def) -text{*Needed to handle the limit case*} -lemma L_r_eq: - "Ord(i) ==> - L_r(f, i) = - (if i = 0 then 0 - else if Limit(i) then rlimit(i, op `(Lambda(i, L_r(f)))) - else DPow_r (f, Lambda(i, L_r(f)) ` Arith.pred(i), - Lset(Arith.pred(i))))" -apply (induct i rule: trans_induct3_rule) -apply (simp_all add: def_transrec [OF L_r_def]) -done - -lemma rlimit_eqI: - "[|Limit(i); \j rlimit(i,r) = rlimit(i,r')" -apply (simp add: rlimit_def) -apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+ -apply (simp add: Limit_is_Ord Lset_lrank_lt) -done - -text{*I don't know why the limit case is so complicated.*} +text{*The limit case is non-trivial because of the distinction between +object-level and meta-level abstraction.*} lemma [simp]: "Limit(i) ==> L_r(f,i) = rlimit(i, L_r(f))" -apply (simp add: Limit_nonzero def_transrec [OF L_r_def]) -apply (rule rlimit_eqI, assumption) -apply (rule oallI) -apply (frule lt_Ord) -apply (simp only: beta ltD L_r_eq [symmetric]) -done +by (simp cong: rlimit_cong add: transrec3_Limit L_r_def ltD) lemma (in Nat_Times_Nat) L_r_type: "Ord(i) ==> L_r(fn,i) \ Lset(i) * Lset(i)" diff -r 0a9228532106 -r c7cf8fa66534 src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Fri Nov 08 10:28:29 2002 +0100 +++ b/src/ZF/Constructible/Datatype_absolute.thy Fri Nov 08 10:34:40 2002 +0100 @@ -980,7 +980,6 @@ \x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))" apply (simp add: relation2_def MH_def, clarify) apply (rule lambda_abs2) -apply (rule fr_lam_replace, assumption) 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 0a9228532106 -r c7cf8fa66534 src/ZF/Constructible/Internalize.thy --- a/src/ZF/Constructible/Internalize.thy Fri Nov 08 10:28:29 2002 +0100 +++ b/src/ZF/Constructible/Internalize.thy Fri Nov 08 10:34:40 2002 +0100 @@ -303,8 +303,8 @@ theorem is_lambda_reflection: assumes is_b_reflection: - "!!f' f g h. REFLECTS[\x. is_b(L, f'(x), f(x), g(x)), - \i x. is_b(**Lset(i), f'(x), f(x), g(x))]" + "!!f g h. REFLECTS[\x. is_b(L, f(x), g(x), h(x)), + \i x. is_b(**Lset(i), f(x), g(x), h(x))]" shows "REFLECTS[\x. is_lambda(L, A(x), is_b(L,x), f(x)), \i x. is_lambda(**Lset(i), A(x), is_b(**Lset(i),x), f(x))]" apply (simp (no_asm_use) only: is_lambda_def) diff -r 0a9228532106 -r c7cf8fa66534 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Fri Nov 08 10:28:29 2002 +0100 +++ b/src/ZF/Constructible/Relative.thy Fri Nov 08 10:34:40 2002 +0100 @@ -493,7 +493,9 @@ by (blast intro: transM) text{*Simplifies proofs of equalities when there's an iff-equality - available for rewriting, universally quantified over M. *} + available for rewriting, universally quantified over M. + But it's not the only way to prove such equalities: its + premises @{term "M(A)"} and @{term "M(B)"} can be too strong.*} lemma (in M_trivial) M_equalityI: "[| !!x. M(x) ==> x\A <-> x\B; M(A); M(B) |] ==> A=B" by (blast intro!: equalityI dest: transM) @@ -669,15 +671,17 @@ done lemma (in M_trivial) Replace_abs: - "[| M(A); M(z); univalent(M,A,P); strong_replacement(M, P); + "[| M(A); M(z); univalent(M,A,P); !!x y. [| x\A; P(x,y) |] ==> M(y) |] ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)" apply (simp add: is_Replace_def) apply (rule iffI) -apply (rule M_equalityI) -apply (simp_all add: univalent_Replace_iff, blast, blast) + apply (rule equality_iffI) + apply (simp_all add: univalent_Replace_iff) + apply (blast dest: transM)+ done + (*The first premise can't simply be assumed as a schema. It is essential to take care when asserting instances of Replacement. Let K be a nonconstructible subset of nat and define @@ -727,16 +731,17 @@ apply (blast intro: RepFun_closed2 dest: transM) done -lemma (in M_trivial) lambda_abs2 [simp]: - "[| strong_replacement(M, \x y. x\A & y = \x, b(x)\); - Relation1(M,A,is_b,b); M(A); \m[M]. m\A --> M(b(m)); M(z) |] +lemma (in M_trivial) lambda_abs2: + "[| 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: Relation1_def is_lambda_def) apply (rule iffI) prefer 2 apply (simp add: lam_def) -apply (rule M_equalityI) - apply (simp add: lam_def) - apply (simp add: lam_closed2)+ +apply (rule equality_iffI) +apply (simp add: lam_def) +apply (rule iffI) + apply (blast dest: transM) +apply (auto simp add: transM [of _ A]) done lemma is_lambda_cong [cong]: @@ -1159,8 +1164,7 @@ done lemma (in M_basic) composition_abs [simp]: - "[| M(r); M(s); M(t) |] - ==> composition(M,r,s,t) <-> t = r O s" + "[| M(r); M(s); M(t) |] ==> composition(M,r,s,t) <-> t = r O s" apply safe txt{*Proving @{term "composition(M, r, s, r O s)"}*} prefer 2 diff -r 0a9228532106 -r c7cf8fa66534 src/ZF/Constructible/Satisfies_absolute.thy --- a/src/ZF/Constructible/Satisfies_absolute.thy Fri Nov 08 10:28:29 2002 +0100 +++ b/src/ZF/Constructible/Satisfies_absolute.thy Fri Nov 08 10:34:40 2002 +0100 @@ -369,7 +369,7 @@ lemma (in M_satisfies) a_rel: "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) +apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) done lemma (in M_satisfies) b_closed: @@ -381,7 +381,7 @@ lemma (in M_satisfies) b_rel: "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) +apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) done lemma (in M_satisfies) c_closed: @@ -400,8 +400,8 @@ \u v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))" 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) +apply (auto del: iffI intro!: lambda_abs2 + simp add: Relation1_def formula_into_M) done lemma (in M_satisfies) d_closed: @@ -418,8 +418,7 @@ \u. satisfies_d(A, u, f ` succ(depth(u)) ` u))" apply (simp del: rall_abs add: Relation1_def satisfies_is_d_def satisfies_d_def) -apply (simp add: lambda_abs2 [OF Forall_replacement' triv_Relation1] - formula_into_M) +apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) done