subsection\<open>An Injection from Formulas into the Natural Numbers\<close>
text\<open>There is a well-known bijection between \<^term>\<open>nat*nat\<close> and \<^term>\<open>nat\<close> 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 toshow that f is a bijection. We already know that such a bijection exists by the theorem\<open>well_ord_InfCard_square_eq\<close>:
@{thm[display] well_ord_InfCard_square_eq[no_vars]}
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 istouse a locale.\<close>
text\<open>Locale for any arbitrary injection between \<^term>\<open>nat*nat\<close> and\<^term>\<open>nat\<close>\<close> locale Nat_Times_Nat = fixes fn assumes fn_inj: "fn \ inj(nat*nat, nat)"
consts enum :: "[i,i]\i" primrec "enum(f, Member(x,y)) = f ` <0, f ` \x,y\>" "enum(f, Equal(x,y)) = f ` <1, f ` \x,y\>" "enum(f, Nand(p,q)) = f ` <2, f ` >" "enum(f, Forall(p)) = f ` "
lemma (in Nat_Times_Nat) fn_type [TC,simp]: "\x \ nat; y \ nat\ \ fn`\x,y\ \ nat" 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\ \<Longrightarrow> (fn`\<langle>x,y\<rangle> = fn`\<langle>u,v\<rangle>) \<longleftrightarrow> (x=u \<and> y=v)" 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)
subsection\<open>Defining the Wellordering on \<^term>\<open>DPow(A)\<close>\<close>
text\<open>The objective is to build a wellordering on \<^term>\<open>DPow(A)\<close> from a
given one on \<^term>\<open>A\<close>. We first introduce wellorderings for environments,
which are lists built over \<^term>\<open>A\<close>. 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>\<open>DPow(A)\<close>, we take the minimum such ordinal.\<close>
definition
env_form_r :: "[i,i,i]\i" where \<comment> \<open>wellordering on (environment, formula) pairs\<close> "env_form_r(f,r,A) \
rmult(list(A), rlist(A, r),
formula, measure(formula, enum(f)))"
definition
env_form_map :: "[i,i,i,i]\i" where \<comment> \<open>map from (environment, formula) pairs to ordinals\<close> "env_form_map(f,r,A,z) \<equiv> ordermap(list(A) * formula, env_form_r(f,r,A)) ` z"
definition
DPow_ord :: "[i,i,i,i,i]\o" where \<comment> \<open>predicate that holds if \<^term>\<open>k\<close> is a valid index for \<^term>\<open>X\<close>\<close> "DPow_ord(f,r,A,X,k) \ \<exists>env \<in> list(A). \<exists>p \<in> formula.
arity(p) \<le> succ(length(env)) \<and>
X = {x\<in>A. sats(A, p, Cons(x,env))} \<and>
env_form_map(f,r,A,\<langle>env,p\<rangle>) = k"
definition
DPow_least :: "[i,i,i,i]\i" where \<comment> \<open>function yielding the smallest index for \<^term>\<open>X\<close>\<close> "DPow_least(f,r,A,X) \ \ k. DPow_ord(f,r,A,X,k)"
definition
DPow_r :: "[i,i,i]\i" where \<comment> \<open>a wellordering on \<^term>\<open>DPow(A)\<close>\<close> "DPow_r(f,r,A) \ measure(DPow(A), DPow_least(f,r,A))"
lemma (in Nat_Times_Nat) well_ord_env_form_r: "well_ord(A,r) \<Longrightarrow> 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\ \<Longrightarrow> Ord(env_form_map(fn,r,A,z))" by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r)
lemma (in Nat_Times_Nat) DPow_r_type: "DPow_r(fn,r,A) \ DPow(A) * DPow(A)" by (simp add: DPow_r_def measure_def, blast)
subsection\<open>Limit Construction for Well-Orderings\<close>
text\<open>Now we work towards the transfinite definition of wellorderings for \<^term>\<open>Lset(i)\<close>. We assume as an inductive hypothesis that there is a family
of wellorderings for smaller ordinals.\<close>
definition
rlimit :: "[i,i\i]\i" where \<comment> \<open>Expresses the wellordering at limit ordinals. The conditional
lets us remove the premise \<^term>\<open>Limit(i)\<close> from some theorems.\<close> "rlimit(i,r) \ if Limit(i) then
{z: Lset(i) * Lset(i). \<exists>x' x. z = <x',x> \<and>
(lrank(x') < lrank(x) |
(lrank(x') = lrank(x) \ \ r(succ(lrank(x)))))}
else 0"
definition
Lset_new :: "i\i" where \<comment> \<open>This constant denotes the set of elements introduced at level \<^term>\<open>succ(i)\<close>\<close> "Lset_new(i) \ {x \ Lset(succ(i)). lrank(x) = i}"
text\<open>The limit case is non-trivial because of the distinction between
object-level and meta-level abstraction.\<close> lemma [simp]: "Limit(i) \ L_r(f,i) = rlimit(i, L_r(f))" by (simp cong: rlimit_cong add: transrec3_Limit L_r_def ltD)
text\<open>Every constructible set is well-ordered! Therefore the Wellordering Theorem and
the Axiom of Choice hold in\<^term>\<open>L\<close>!\<close> theorem L_implies_AC: assumes x: "L(x)"shows"\r. well_ord(x,r)" using Transset_Lset x apply (simp add: Transset_def L_def) apply (blast dest!: well_ord_L_r intro: well_ord_subset) done
interpretation L: M_basic L by (rule M_basic_L)
theorem"\x[L]. \r. wellordered(L,x,r)" proof fix x assume"L(x)" thenobtain r where"well_ord(x,r)" by (blast dest: L_implies_AC) thus"\r. wellordered(L,x,r)" by (blast intro: L.well_ord_imp_relativized) qed
text\<open>In order to prove \<^term>\<open> \<exists>r[L]. wellordered(L,x,r)\<close>, it's necessary to know
that \<^term>\<open>r\<close> is actually constructible. It follows from the assumption ``\<^term>\<open>V\<close> equals \<^term>\<open>L''\<close>,
but this reasoning doesn't appear to work in Isabelle.\
end
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
