# HG changeset patch # User paulson # Date 1036169066 -3600 # Node ID 27f3c83e2984249741188f1e44fc1e228217bcee # Parent a6bc3001106a5e61ebae1fbcba4822cf03fd2288 proof streamlining diff -r a6bc3001106a -r 27f3c83e2984 src/ZF/Constructible/AC_in_L.thy --- a/src/ZF/Constructible/AC_in_L.thy Fri Nov 01 17:43:54 2002 +0100 +++ b/src/ZF/Constructible/AC_in_L.thy Fri Nov 01 17:44:26 2002 +0100 @@ -18,16 +18,16 @@ domains "rlist(A,r)" \ "list(A) * list(A)" intros shorterI: - "[| length(l') < length(l); l' \ list(A); l \ list(A) |] + "[| length(l') < length(l); l' \ list(A); l \ list(A) |] ==> \ rlist(A,r)" sameI: - "[| \ rlist(A,r); a \ A |] + "[| \ rlist(A,r); a \ A |] ==> \ rlist(A,r)" diffI: - "[| length(l') = length(l); \ r; - l' \ list(A); l \ list(A); a' \ A; a \ A |] + "[| length(l') = length(l); \ r; + l' \ list(A); l \ list(A); a' \ A; a \ A |] ==> \ rlist(A,r)" type_intros list.intros @@ -42,24 +42,24 @@ lemma rlist_Nil_Cons [intro]: "[|a \ A; l \ list(A)|] ==> <[], Cons(a,l)> \ rlist(A, r)" -by (simp add: shorterI) +by (simp add: shorterI) lemma linear_rlist: "linear(A,r) ==> linear(list(A),rlist(A,r))" apply (simp (no_asm_simp) add: linear_def) -apply (rule ballI) -apply (induct_tac x) - apply (rule ballI) - apply (induct_tac y) - apply (simp_all add: shorterI) -apply (rule ballI) -apply (erule_tac a=y in list.cases) - apply (rename_tac [2] a2 l2) +apply (rule ballI) +apply (induct_tac x) + apply (rule ballI) + apply (induct_tac y) + apply (simp_all add: shorterI) +apply (rule ballI) +apply (erule_tac a=y in list.cases) + apply (rename_tac [2] a2 l2) apply (rule_tac [2] i = "length(l)" and j = "length(l2)" in Ord_linear_lt) - apply (simp_all add: shorterI) -apply (erule_tac x=a and y=a2 in linearE) - apply (simp_all add: diffI) -apply (blast intro: sameI) + apply (simp_all add: shorterI) +apply (erule_tac x=a and y=a2 in linearE) + apply (simp_all add: diffI) +apply (blast intro: sameI) done @@ -75,27 +75,27 @@ lemma rlist_imp_length_le: " \ rlist(A,r) ==> length(l') \ length(l)" apply (erule rlist.induct) -apply (simp_all add: leI) +apply (simp_all add: leI) done lemma wf_on_rlist_n: "[| n \ nat; wf[A](r) |] ==> wf[{l \ list(A). length(l) = n}](rlist(A,r))" -apply (induct_tac n) - apply (rule wf_onI2, simp) -apply (rule wf_onI2, clarify) -apply (erule_tac a=y in list.cases, clarify) +apply (induct_tac n) + apply (rule wf_onI2, simp) +apply (rule wf_onI2, clarify) +apply (erule_tac a=y in list.cases, clarify) apply (simp (no_asm_use)) -apply clarify +apply clarify apply (simp (no_asm_use)) apply (subgoal_tac "\l2 \ list(A). length(l2) = x --> Cons(a,l2) \ B", blast) apply (erule_tac a=a in wf_on_induct, assumption) apply (rule ballI) -apply (rule impI) +apply (rule impI) apply (erule_tac a=l2 in wf_on_induct, blast, clarify) -apply (rename_tac a' l2 l') -apply (drule_tac x="Cons(a',l')" in bspec, typecheck) -apply simp -apply (erule mp, clarify) +apply (rename_tac a' l2 l') +apply (drule_tac x="Cons(a',l')" in bspec, typecheck) +apply simp +apply (erule mp, clarify) apply (erule rlist_ConsE, auto) done @@ -104,22 +104,22 @@ lemma wf_on_rlist: "wf[A](r) ==> wf[list(A)](rlist(A,r))" -apply (subst list_eq_UN_length) -apply (rule wf_on_Union) +apply (subst list_eq_UN_length) +apply (rule wf_on_Union) apply (rule wf_imp_wf_on [OF wf_Memrel [of nat]]) apply (simp add: wf_on_rlist_n) -apply (frule rlist_type [THEN subsetD]) -apply (simp add: length_type) +apply (frule rlist_type [THEN subsetD]) +apply (simp add: length_type) apply (drule rlist_imp_length_le) -apply (erule leE) -apply (simp_all add: lt_def) +apply (erule leE) +apply (simp_all add: lt_def) done lemma wf_rlist: "wf(r) ==> wf(rlist(field(r),r))" apply (simp add: wf_iff_wf_on_field) apply (rule wf_on_subset_A [OF _ field_rlist]) -apply (blast intro: wf_on_rlist) +apply (blast intro: wf_on_rlist) done lemma well_ord_rlist: @@ -136,11 +136,15 @@ nat} given by the expression f(m,n) = triangle(m+n) + m, where triangle(k) enumerates the triangular numbers and can be defined by triangle(0)=0, triangle(succ(k)) = succ(k + triangle(k)). Some small amount of effort is -needed to show that f is a bijection. We already know (by the theorem @{text -InfCard_square_eqpoll}) that such a bijection exists, but as we have no direct -way to refer to it, we must use a locale.*} +needed to show that f is a bijection. We already know that such a bijection exists by the theorem @{text well_ord_InfCard_square_eq}: +@{thm[display] well_ord_InfCard_square_eq[no_vars]} -text{*Locale for any arbitrary injection between @{term "nat*nat"} +However, this result merely states that there is a bijection between the two +sets. It provides no means of naming a specific bijection. Therefore, we +conduct the proofs under the assumption that a bijection exists. The simplest +way to organize this is to use a locale.*} + +text{*Locale for any arbitrary injection between @{term "nat*nat"} and @{term nat}*} locale Nat_Times_Nat = fixes fn @@ -156,45 +160,45 @@ lemma (in Nat_Times_Nat) fn_type [TC,simp]: "[|x \ nat; y \ nat|] ==> fn` \ nat" -by (blast intro: inj_is_fun [OF fn_inj] apply_funtype) +by (blast intro: inj_is_fun [OF fn_inj] apply_funtype) lemma (in Nat_Times_Nat) fn_iff: - "[|x \ nat; y \ nat; u \ nat; v \ nat|] + "[|x \ nat; y \ nat; u \ nat; v \ nat|] ==> (fn` = fn`) <-> (x=u & y=v)" -by (blast dest: inj_apply_equality [OF fn_inj]) +by (blast dest: inj_apply_equality [OF fn_inj]) lemma (in Nat_Times_Nat) enum_type [TC,simp]: "p \ formula ==> enum(fn,p) \ nat" -by (induct_tac p, simp_all) +by (induct_tac p, simp_all) lemma (in Nat_Times_Nat) enum_inject [rule_format]: "p \ formula ==> \q\formula. enum(fn,p) = enum(fn,q) --> p=q" -apply (induct_tac p, simp_all) - apply (rule ballI) - apply (erule formula.cases) - apply (simp_all add: fn_iff) - apply (rule ballI) - apply (erule formula.cases) - apply (simp_all add: fn_iff) - apply (rule ballI) - apply (erule_tac a=qa in formula.cases) - apply (simp_all add: fn_iff) - apply blast -apply (rule ballI) -apply (erule_tac a=q in formula.cases) -apply (simp_all add: fn_iff, blast) +apply (induct_tac p, simp_all) + apply (rule ballI) + apply (erule formula.cases) + apply (simp_all add: fn_iff) + apply (rule ballI) + apply (erule formula.cases) + apply (simp_all add: fn_iff) + apply (rule ballI) + apply (erule_tac a=qa in formula.cases) + apply (simp_all add: fn_iff) + apply blast +apply (rule ballI) +apply (erule_tac a=q in formula.cases) +apply (simp_all add: fn_iff, blast) done lemma (in Nat_Times_Nat) inj_formula_nat: "(\p \ formula. enum(fn,p)) \ inj(formula, nat)" -apply (simp add: inj_def lam_type) -apply (blast intro: enum_inject) +apply (simp add: inj_def lam_type) +apply (blast intro: enum_inject) done lemma (in Nat_Times_Nat) well_ord_formula: "well_ord(formula, measure(formula, enum(fn)))" apply (rule well_ord_measure, simp) -apply (blast intro: enum_inject) +apply (blast intro: enum_inject) done lemmas nat_times_nat_lepoll_nat = @@ -205,9 +209,150 @@ theorem formula_lepoll_nat: "formula \ nat" apply (insert nat_times_nat_lepoll_nat) apply (unfold lepoll_def) -apply (blast intro: exI Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro) +apply (blast intro: Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro) +done + + +subsection{*Defining the Wellordering on @{term "DPow(A)"}*} + +text{*The objective is to build a wellordering on @{term "DPow(A)"} from a +given one on @{term A}. We first introduce wellorderings for environments, +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)"}.*} + +constdefs + env_form_r :: "[i,i,i]=>i" + --{*wellordering on (environment, formula) pairs*} + "env_form_r(f,r,A) == + rmult(list(A), rlist(A, r), + formula, measure(formula, enum(f)))" + + env_form_map :: "[i,i,i,i]=>i" + --{*map from (environment, formula) pairs to ordinals*} + "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" + --{*predicate that holds if @{term k} is a valid index for @{term X}*} + "DPow_new_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" + --{*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_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" + + +lemma (in Nat_Times_Nat) well_ord_env_form_r: + "well_ord(A,r) + ==> well_ord(list(A) * formula, env_form_r(fn,r,A))" +by (simp add: env_form_r_def well_ord_rmult well_ord_rlist well_ord_formula) + +lemma (in Nat_Times_Nat) Ord_env_form_map: + "[|well_ord(A,r); z \ list(A) * formula|] + ==> 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) +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) +apply (simp add: Ord_env_form_map) done +lemma (in Nat_Times_Nat) DPow_imp_DPow_new_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) +done + +lemma (in Nat_Times_Nat) env_form_map_inject: + "[|env_form_map(fn,r,A,u) = env_form_map(fn,r,A,v); well_ord(A,r); + u \ list(A) * formula; v \ list(A) * formula|] + ==> u=v" +apply (simp add: env_form_map_def) +apply (rule inj_apply_equality [OF bij_is_inj, OF ordermap_bij, + 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)|] + ==> X=Y" +apply (simp add: DPow_new_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) +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 +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) +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 + subsection{*Limit Construction for Well-Orderings*} @@ -215,299 +360,149 @@ @{term "Lset(i)"}. We assume as an inductive hypothesis that there is a family of wellorderings for smaller ordinals.*} -text{*This constant denotes the set of elements introduced at level -@{term "succ(i)"}*} constdefs + rlimit :: "[i,i=>i]=>i" + --{*expresses the wellordering at limit ordinals.*} + "rlimit(i,r) == + {z: Lset(i) * Lset(i). + \x' x. z = & + (lrank(x') < lrank(x) | + (lrank(x') = lrank(x) & \ r(succ(lrank(x)))))}" + 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) +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) +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) +apply (simp add: Limit_Lset_eq) apply (rule equalityI) apply safe apply (subgoal_tac "Ord(y)") prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord) - apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def - Ord_mem_iff_lt) - apply (blast intro: lt_trans) + apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def + Ord_mem_iff_lt) + apply (blast intro: lt_trans) apply (rule_tac x = "succ(lrank(x))" in bexI) - apply (simp add: Lset_succ_lrank_iff) -apply (blast intro: Limit_has_succ ltD) -done - -text{*This constant expresses the wellordering at limit ordinals.*} -constdefs - rlimit :: "[i,i=>i]=>i" - "rlimit(i,r) == - {z: Lset(i) * Lset(i). - \x' x. z = & - (lrank(x') < lrank(x) | - (lrank(x') = lrank(x) & \ r(succ(lrank(x)))))}" - -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) + apply (simp add: Lset_succ_lrank_iff) +apply (blast intro: Limit_has_succ ltD) done lemma wf_on_Lset: "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: wf_on_def Lset_new_def) +apply (erule wf_subset) +apply (force simp add: rlimit_def) done lemma wf_on_rlimit: "[|Limit(i); \j wf[Lset(i)](rlimit(i,r))" apply (simp add: Limit_Lset_eq2) apply (rule wf_on_Union) - apply (rule wf_imp_wf_on [OF wf_Memrel [of i]]) - apply (blast intro: wf_on_Lset Limit_has_succ Limit_is_Ord ltI) + apply (rule wf_imp_wf_on [OF wf_Memrel [of i]]) + apply (blast intro: wf_on_Lset Limit_has_succ Limit_is_Ord ltI) apply (force simp add: rlimit_def Limit_is_Ord Lset_iff_lrank_lt Lset_new_def Ord_mem_iff_lt) - done lemma linear_rlimit: "[|Limit(i); \j linear(Lset(i), rlimit(i,r))" -apply (frule Limit_is_Ord) -apply (simp add: Limit_Lset_eq2) -apply (simp add: linear_def Lset_new_def rlimit_def Ball_def) -apply (simp add: lt_Ord Lset_iff_lrank_lt) -apply (simp add: ltI, clarify) -apply (rename_tac u v) -apply (rule_tac i="lrank(u)" and j="lrank(v)" in Ord_linear_lt) -apply simp_all -apply (drule_tac x="succ(lrank(u) Un lrank(v))" in ospec) -apply (simp add: ltI) -apply (drule_tac x=u in spec, simp) -apply (drule_tac x=v in spec, simp) +apply (frule Limit_is_Ord) +apply (simp add: Limit_Lset_eq2 Lset_new_def) +apply (simp add: linear_def rlimit_def Ball_def lt_Ord Lset_iff_lrank_lt) +apply (simp add: ltI, clarify) +apply (rename_tac u v) +apply (rule_tac i="lrank(u)" and j="lrank(v)" in Ord_linear_lt, simp_all) +apply (drule_tac x="succ(lrank(u) Un lrank(v))" in ospec) + apply (simp add: ltI) +apply (drule_tac x=u in spec, simp) +apply (drule_tac x=v in spec, simp) done - lemma well_ord_rlimit: "[|Limit(i); \j well_ord(Lset(i), rlimit(i,r))" -by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf - linear_rlimit well_ord_is_linear) - - -subsection{*Defining the Wellordering on @{term "Lset(succ(i))"}*} - -text{*We introduce wellorderings for environments, which are lists built over -@{term "Lset(succ(i))"}. 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(Lset(i))"}, -we take the minimum such ordinal. This yields a wellordering of -@{term "DPow(Lset(i))"}, which we then extend to @{term "Lset(succ(i))"}*} - -constdefs - env_form_r :: "[i,i,i]=>i" - --{*wellordering on (environment, formula) pairs*} - "env_form_r(f,r,i) == - rmult(list(Lset(i)), rlist(Lset(i), r), - formula, measure(formula, enum(f)))" - - env_form_map :: "[i,i,i,i]=>i" - --{*map from (environment, formula) pairs to ordinals*} - "env_form_map(f,r,i,z) - == ordermap(list(Lset(i)) * formula, env_form_r(f,r,i)) ` z" - - L_new_ord :: "[i,i,i,i,i]=>o" - --{*predicate that holds if @{term k} is a valid index for @{term X}*} - "L_new_ord(f,r,i,X,k) == - \env \ list(Lset(i)). \p \ formula. - arity(p) \ succ(length(env)) & - X = {x\Lset(i). sats(Lset(i), p, Cons(x,env))} & - env_form_map(f,r,i,) = k" - - L_new_least :: "[i,i,i,i]=>i" - --{*function yielding the smallest index for @{term X}*} - "L_new_least(f,r,i,X) == \k. L_new_ord(f,r,i,X,k)" - - L_new_r :: "[i,i,i]=>i" - --{*a wellordering on @{term "DPow(Lset(i))"}*} - "L_new_r(f,r,i) == measure(Lset_new(i), L_new_least(f,r,i))" - - L_succ_r :: "[i,i,i]=>i" - --{*a wellordering on @{term "Lset(succ(i))"}*} - "L_succ_r(f,r,i) == (L_new_r(f,r,i) Un (Lset(i) * Lset_new(i))) Un r" - - -lemma (in Nat_Times_Nat) well_ord_env_form_r: - "well_ord(Lset(i), r) - ==> well_ord(list(Lset(i)) * formula, env_form_r(fn,r,i))" -by (simp add: env_form_r_def well_ord_rmult well_ord_rlist well_ord_formula) - -lemma (in Nat_Times_Nat) Ord_env_form_map: - "[|well_ord(Lset(i), r); z \ list(Lset(i)) * formula|] - ==> Ord(env_form_map(fn,r,i,z))" -by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r) - - -lemma DPow_imp_ex_L_new_ord: - "X \ DPow(Lset(i)) ==> \k. L_new_ord(fn,r,i,X,k)" -apply (simp add: L_new_ord_def) -apply (blast dest!: DPowD) -done - -lemma (in Nat_Times_Nat) L_new_ord_imp_Ord: - "[|L_new_ord(fn,r,i,X,k); well_ord(Lset(i), r)|] ==> Ord(k)" -apply (simp add: L_new_ord_def, clarify) -apply (simp add: Ord_env_form_map) -done - -lemma (in Nat_Times_Nat) DPow_imp_L_new_least: - "[|X \ DPow(Lset(i)); well_ord(Lset(i), r)|] - ==> L_new_ord(fn, r, i, X, L_new_least(fn,r,i,X))" -apply (simp add: L_new_least_def) -apply (blast dest!: DPow_imp_ex_L_new_ord intro: L_new_ord_imp_Ord LeastI) -done - -lemma (in Nat_Times_Nat) env_form_map_inject: - "[|env_form_map(fn,r,i,u) = env_form_map(fn,r,i,v); well_ord(Lset(i), r); - u \ list(Lset(i)) * formula; v \ list(Lset(i)) * formula|] - ==> u=v" -apply (simp add: env_form_map_def) -apply (rule inj_apply_equality [OF bij_is_inj, OF ordermap_bij, - OF well_ord_env_form_r], assumption+) -done - - -lemma (in Nat_Times_Nat) L_new_ord_unique: - "[|L_new_ord(fn,r,i,X,k); L_new_ord(fn,r,i,Y,k); well_ord(Lset(i), r)|] - ==> X=Y" -apply (simp add: L_new_ord_def, clarify) -apply (drule env_form_map_inject, auto) -done - -lemma (in Nat_Times_Nat) well_ord_L_new_r: - "[|Ord(i); well_ord(Lset(i), r)|] - ==> well_ord(Lset_new(i), L_new_r(fn,r,i))" -apply (simp add: L_new_r_def) -apply (rule well_ord_measure) - apply (simp add: L_new_least_def Ord_Least) -apply (simp add: Lset_new_eq Lset_succ, clarify) -apply (drule DPow_imp_L_new_least, assumption)+ -apply simp -apply (blast intro: L_new_ord_unique) -done - -lemma L_new_r_subset: "L_new_r(f,r,i) <= Lset_new(i) * Lset_new(i)" -by (simp add: L_new_r_def measure_type) - -lemma Lset_Lset_new_disjoint: "Ord(i) ==> Lset(i) \ Lset_new(i) = 0" -by (simp add: Lset_new_eq, blast) - -lemma (in Nat_Times_Nat) linear_L_succ_r: - "[|Ord(i); well_ord(Lset(i), r)|] - ==> linear(Lset(succ(i)), L_succ_r(fn, r, i))" -apply (frule well_ord_L_new_r, assumption) -apply (drule well_ord_is_linear)+ -apply (simp add: linear_def L_succ_r_def Lset_new_eq, auto) -done - - -lemma (in Nat_Times_Nat) wf_L_new_r: - "[|Ord(i); well_ord(Lset(i), r)|] ==> wf(L_new_r(fn,r,i))" -apply (rule well_ord_L_new_r [THEN well_ord_is_wf, THEN wf_on_imp_wf], - assumption+) -apply (rule L_new_r_subset) -done - - -lemma (in Nat_Times_Nat) well_ord_L_succ_r: - "[|Ord(i); well_ord(Lset(i), r); r \ Lset(i) * Lset(i)|] - ==> well_ord(Lset(succ(i)), L_succ_r(fn,r,i))" -apply (rule well_ordI [OF wf_imp_wf_on]) - prefer 2 apply (blast intro: linear_L_succ_r) -apply (simp add: L_succ_r_def) -apply (rule wf_Un) - apply (cut_tac L_new_r_subset [of fn r i], simp add: Lset_new_eq, blast) - apply (rule wf_Un) - apply (cut_tac L_new_r_subset [of fn r i], simp add: Lset_new_eq, blast) - apply (blast intro: wf_L_new_r) - apply (simp add: wf_times Lset_Lset_new_disjoint) -apply (blast intro: well_ord_is_wf wf_on_imp_wf) -done - - -lemma (in Nat_Times_Nat) L_succ_r_type: - "[|Ord(i); r \ Lset(i) * Lset(i)|] - ==> L_succ_r(fn,r,i) \ Lset(succ(i)) * Lset(succ(i))" -apply (simp add: L_succ_r_def L_new_r_def measure_def Lset_new_eq) -apply (blast intro: Lset_mono_mem [OF succI1, THEN subsetD] ) -done +by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf + linear_rlimit well_ord_is_linear) subsection{*Transfinite Definition of the Wellordering on @{term "L"}*} constdefs L_r :: "[i, i] => i" - "L_r(f,i) == - transrec(i, \x r. + "L_r(f,i) == + transrec(i, \x r. if x=0 then 0 else if Limit(x) then rlimit(x, \y. r`y) - else L_succ_r(f, r ` Arith.pred(x), Arith.pred(x)))" + else DPow_r(f, r ` Arith.pred(x), Lset(Arith.pred(x))))" subsubsection{*The Corresponding Recursion Equations*} lemma [simp]: "L_r(f,0) = 0" by (simp add: def_transrec [OF L_r_def]) -lemma [simp]: "Ord(i) ==> L_r(f, succ(i)) = L_succ_r(f, L_r(f,i), i)" +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]) text{*Needed to handle the limit case*} lemma L_r_eq: - "Ord(i) ==> + "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 L_succ_r (f, Lambda(i, L_r(f)) ` Arith.pred(i), Arith.pred(i)))" + 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.*} 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]) +apply (frule lt_Ord) +apply (simp only: beta ltD L_r_eq [symmetric]) done lemma (in Nat_Times_Nat) L_r_type: "Ord(i) ==> L_r(fn,i) \ Lset(i) * Lset(i)" apply (induct i rule: trans_induct3_rule) - apply (simp_all add: L_succ_r_type well_ord_L_succ_r rlimit_def, blast) + apply (simp_all add: Lset_succ DPow_r_type well_ord_DPow_r rlimit_def + Transset_subset_DPow [OF Transset_Lset], blast) done lemma (in Nat_Times_Nat) well_ord_L_r: "Ord(i) ==> well_ord(Lset(i), L_r(fn,i))" apply (induct i rule: trans_induct3_rule) -apply (simp_all add: well_ord0 L_r_type well_ord_L_succ_r well_ord_rlimit ltD) +apply (simp_all add: well_ord0 Lset_succ L_r_type well_ord_DPow_r + well_ord_rlimit ltD) done lemma well_ord_L_r: "Ord(i) ==> \r. well_ord(Lset(i), r)" apply (insert nat_times_nat_lepoll_nat) apply (unfold lepoll_def) -apply (blast intro: exI Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro) +apply (blast intro: Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro) done @@ -518,9 +513,9 @@ text{*The Axiom of Choice holds in @{term L}! Or, to be precise, the Wellordering Theorem.*} theorem (in V_equals_L) AC: "\r. well_ord(x,r)" -apply (insert Transset_Lset VL [of x]) +apply (insert Transset_Lset VL [of x]) apply (simp add: Transset_def L_def) -apply (blast dest!: well_ord_L_r intro: well_ord_subset) +apply (blast dest!: well_ord_L_r intro: well_ord_subset) done end diff -r a6bc3001106a -r 27f3c83e2984 src/ZF/Constructible/DPow_absolute.thy --- a/src/ZF/Constructible/DPow_absolute.thy Fri Nov 01 17:43:54 2002 +0100 +++ b/src/ZF/Constructible/DPow_absolute.thy Fri Nov 01 17:44:26 2002 +0100 @@ -111,71 +111,72 @@ subsection {*Relativization of the Operator @{term DPow'}*} lemma DPow'_eq: - "DPow'(A) = Replace(list(A) * formula, - %ep z. \env \ list(A). \p \ formula. - ep = & z = {x\A. sats(A, p, Cons(x,env))})" -apply (simp add: DPow'_def, blast) -done + "DPow'(A) = {z . ep \ list(A) * formula, + \env \ list(A). \p \ formula. + ep = & z = {x\A. sats(A, p, Cons(x,env))}}" +by (simp add: DPow'_def, blast) +text{*Relativize the use of @{term sats} within @{term DPow'} +(the comprehension).*} constdefs - is_DPow_body :: "[i=>o,i,i,i,i] => o" - "is_DPow_body(M,A,env,p,x) == + is_DPow_sats :: "[i=>o,i,i,i,i] => o" + "is_DPow_sats(M,A,env,p,x) == \n1[M]. \e[M]. \sp[M]. is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) --> fun_apply(M, sp, e, n1) --> number1(M, n1)" -lemma (in M_satisfies) DPow_body_abs: +lemma (in M_satisfies) DPow_sats_abs: "[| M(A); env \ list(A); p \ formula; M(x) |] - ==> is_DPow_body(M,A,env,p,x) <-> sats(A, p, Cons(x,env))" + ==> is_DPow_sats(M,A,env,p,x) <-> sats(A, p, Cons(x,env))" apply (subgoal_tac "M(env)") - apply (simp add: is_DPow_body_def satisfies_closed satisfies_abs) + apply (simp add: is_DPow_sats_def satisfies_closed satisfies_abs) apply (blast dest: transM) done -lemma (in M_satisfies) Collect_DPow_body_abs: +lemma (in M_satisfies) Collect_DPow_sats_abs: "[| M(A); env \ list(A); p \ formula |] - ==> Collect(A, is_DPow_body(M,A,env,p)) = + ==> Collect(A, is_DPow_sats(M,A,env,p)) = {x \ A. sats(A, p, Cons(x,env))}" -by (simp add: DPow_body_abs transM [of _ A]) +by (simp add: DPow_sats_abs transM [of _ A]) -subsubsection{*The Operator @{term is_DPow_body}, Internalized*} +subsubsection{*The Operator @{term is_DPow_sats}, Internalized*} -(* is_DPow_body(M,A,env,p,x) == +(* is_DPow_sats(M,A,env,p,x) == \n1[M]. \e[M]. \sp[M]. is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) --> fun_apply(M, sp, e, n1) --> number1(M, n1) *) -constdefs DPow_body_fm :: "[i,i,i,i]=>i" - "DPow_body_fm(A,env,p,x) == +constdefs DPow_sats_fm :: "[i,i,i,i]=>i" + "DPow_sats_fm(A,env,p,x) == Forall(Forall(Forall( Implies(satisfies_fm(A#+3,p#+3,0), Implies(Cons_fm(x#+3,env#+3,1), Implies(fun_apply_fm(0,1,2), number1_fm(2)))))))" -lemma is_DPow_body_type [TC]: +lemma is_DPow_sats_type [TC]: "[| A \ nat; x \ nat; y \ nat; z \ nat |] - ==> DPow_body_fm(A,x,y,z) \ formula" -by (simp add: DPow_body_fm_def) + ==> DPow_sats_fm(A,x,y,z) \ formula" +by (simp add: DPow_sats_fm_def) -lemma sats_DPow_body_fm [simp]: +lemma sats_DPow_sats_fm [simp]: "[| u \ nat; x \ nat; y \ nat; z \ nat; env \ list(A)|] - ==> sats(A, DPow_body_fm(u,x,y,z), env) <-> - is_DPow_body(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))" -by (simp add: DPow_body_fm_def is_DPow_body_def) + ==> sats(A, DPow_sats_fm(u,x,y,z), env) <-> + is_DPow_sats(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))" +by (simp add: DPow_sats_fm_def is_DPow_sats_def) -lemma DPow_body_iff_sats: +lemma DPow_sats_iff_sats: "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz; u \ nat; x \ nat; y \ nat; z \ nat; env \ list(A)|] - ==> is_DPow_body(**A,nu,nx,ny,nz) <-> - sats(A, DPow_body_fm(u,x,y,z), env)" + ==> is_DPow_sats(**A,nu,nx,ny,nz) <-> + sats(A, DPow_sats_fm(u,x,y,z), env)" by simp -theorem DPow_body_reflection: - "REFLECTS[\x. is_DPow_body(L,f(x),g(x),h(x),g'(x)), - \i x. is_DPow_body(**Lset(i),f(x),g(x),h(x),g'(x))]" -apply (unfold is_DPow_body_def) +theorem DPow_sats_reflection: + "REFLECTS[\x. is_DPow_sats(L,f(x),g(x),h(x),g'(x)), + \i x. is_DPow_sats(**Lset(i),f(x),g(x),h(x),g'(x))]" +apply (unfold is_DPow_sats_def) apply (intro FOL_reflections function_reflections extra_reflections satisfies_reflection) done @@ -186,25 +187,25 @@ locale M_DPow = M_satisfies + assumes sep: "[| M(A); env \ list(A); p \ formula |] - ==> separation(M, \x. is_DPow_body(M,A,env,p,x))" + ==> separation(M, \x. is_DPow_sats(M,A,env,p,x))" and rep: "M(A) ==> strong_replacement (M, \ep z. \env[M]. \p[M]. mem_formula(M,p) & mem_list(M,A,env) & pair(M,env,p,ep) & - is_Collect(M, A, \x. is_DPow_body(M,A,env,p,x), z))" + is_Collect(M, A, \x. is_DPow_sats(M,A,env,p,x), z))" lemma (in M_DPow) sep': "[| M(A); env \ list(A); p \ formula |] ==> separation(M, \x. sats(A, p, Cons(x,env)))" -by (insert sep [of A env p], simp add: DPow_body_abs) +by (insert sep [of A env p], simp add: DPow_sats_abs) lemma (in M_DPow) rep': "M(A) ==> strong_replacement (M, \ep z. \env\list(A). \p\formula. ep = & z = {x \ A . sats(A, p, Cons(x, env))})" -by (insert rep [of A], simp add: Collect_DPow_body_abs) +by (insert rep [of A], simp add: Collect_DPow_sats_abs) lemma univalent_pair_eq: @@ -223,14 +224,14 @@ \X[M]. X \ Z <-> subset(M,X,A) & (\env[M]. \p[M]. mem_formula(M,p) & mem_list(M,A,env) & - is_Collect(M, A, is_DPow_body(M,A,env,p), X))" + is_Collect(M, A, is_DPow_sats(M,A,env,p), X))" lemma (in M_DPow) DPow'_abs: "[|M(A); M(Z)|] ==> is_DPow'(M,A,Z) <-> Z = DPow'(A)" apply (rule iffI) - prefer 2 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_body_abs) + prefer 2 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs) apply (rule M_equalityI) -apply (simp add: is_DPow'_def DPow'_def Collect_DPow_body_abs, assumption) +apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs, assumption) apply (erule DPow'_closed) done @@ -241,11 +242,11 @@ lemma DPow_separation: "[| L(A); env \ list(A); p \ formula |] - ==> separation(L, \x. is_DPow_body(L,A,env,p,x))" -apply (rule gen_separation_multi [OF DPow_body_reflection, of "{A,env,p}"], + ==> separation(L, \x. is_DPow_sats(L,A,env,p,x))" +apply (rule gen_separation_multi [OF DPow_sats_reflection, of "{A,env,p}"], auto intro: transL) apply (rule_tac env="[A,env,p]" in DPow_LsetI) -apply (rule DPow_body_iff_sats sep_rules | simp)+ +apply (rule DPow_sats_iff_sats sep_rules | simp)+ done @@ -256,15 +257,15 @@ "REFLECTS [\x. \u[L]. u \ B & (\env[L]. \p[L]. mem_formula(L,p) & mem_list(L,A,env) & pair(L,env,p,u) & - is_Collect (L, A, is_DPow_body(L,A,env,p), x)), + is_Collect (L, A, is_DPow_sats(L,A,env,p), x)), \i x. \u \ Lset(i). u \ B & (\env \ Lset(i). \p \ Lset(i). mem_formula(**Lset(i),p) & mem_list(**Lset(i),A,env) & pair(**Lset(i),env,p,u) & - is_Collect (**Lset(i), A, is_DPow_body(**Lset(i),A,env,p), x))]" + is_Collect (**Lset(i), A, is_DPow_sats(**Lset(i),A,env,p), x))]" apply (unfold is_Collect_def) apply (intro FOL_reflections function_reflections mem_formula_reflection - mem_list_reflection DPow_body_reflection) + mem_list_reflection DPow_sats_reflection) done lemma DPow_replacement: @@ -272,7 +273,7 @@ ==> strong_replacement (L, \ep z. \env[L]. \p[L]. mem_formula(L,p) & mem_list(L,A,env) & pair(L,env,p,ep) & - is_Collect(L, A, \x. is_DPow_body(L,A,env,p,x), z))" + is_Collect(L, A, \x. is_DPow_sats(L,A,env,p,x), z))" apply (rule strong_replacementI) apply (rule_tac u="{A,B}" in gen_separation_multi [OF DPow_replacement_Reflects], @@ -280,7 +281,7 @@ apply (unfold is_Collect_def) apply (rule_tac env="[A,B]" in DPow_LsetI) apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats - DPow_body_iff_sats | simp)+ + DPow_sats_iff_sats | simp)+ done @@ -410,7 +411,7 @@ \X[M]. X \ Z <-> subset(M,X,A) & (\env[M]. \p[M]. mem_formula(M,p) & mem_list(M,A,env) & - is_Collect(M, A, is_DPow_body(M,A,env,p), X))" *) + is_Collect(M, A, is_DPow_sats(M,A,env,p), X))" *) constdefs DPow'_fm :: "[i,i]=>i" "DPow'_fm(A,Z) == @@ -421,7 +422,7 @@ And(mem_formula_fm(0), And(mem_list_fm(A#+3,1), Collect_fm(A#+3, - DPow_body_fm(A#+4, 2, 1, 0), 2))))))))" + DPow_sats_fm(A#+4, 2, 1, 0), 2))))))))" lemma is_DPow'_type [TC]: "[| x \ nat; y \ nat |] ==> DPow'_fm(x,y) \ formula" @@ -444,7 +445,7 @@ \i x. is_DPow'(**Lset(i),f(x),g(x))]" apply (simp only: is_DPow'_def) apply (intro FOL_reflections function_reflections mem_formula_reflection - mem_list_reflection Collect_reflection DPow_body_reflection) + mem_list_reflection Collect_reflection DPow_sats_reflection) done @@ -501,9 +502,12 @@ text{*Relativization of the Operator @{term Lset}*} + constdefs - is_Lset :: "[i=>o, i, i] => o" + --{*We can use the term language below because @{term is_Lset} will + not have to be internalized: it isn't used in any instance of + separation.*} "is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\y\x. DPow'(f`y)), a, z)" lemma (in M_Lset) Lset_abs: