Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/ZF/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 19 kB

Quelle Zorn.thy Sprache: Isabelle

(*  Title:      ZF/Zorn.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge
*)

section\<open>Zorn's Lemma\<close>

theory Zorn imports OrderArith AC Inductive begin

text\<open>Based upon the unpublished article ``Towards the Mechanization of the
Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.\<close>

definition
  Subset_rel :: "i\i" where
   "Subset_rel(A) \ {z \ A*A . \x y. z=\x,y\ \ x<=y \ x\y}"

definition
  chain      :: "i\i" where
   "chain(A) \ {F \ Pow(A). \X\F. \Y\F. X<=Y | Y<=X}"

definition
  super      :: "[i,i]\i" where
   "super(A,c) \ {d \ chain(A). c<=d \ c\d}"

definition
  maxchain   :: "i\i" where
   "maxchain(A) \ {c \ chain(A). super(A,c)=0}"

definition
  increasing :: "i\i" where
    "increasing(A) \ {f \ Pow(A)->Pow(A). \x. x<=A \ x<=f`x}"

text\<open>Lemma for the inductive definition below\<close>
lemma Union_in_Pow: "Y \ Pow(Pow(A)) \ \(Y) \ Pow(A)"
by blast

text\<open>We could make the inductive definition conditional on
    \<^term>\<open>next \<in> increasing(S)\<close>
    but instead we make this a side-condition of an introduction rule.  Thus
    the induction rule lets us assume that condition!  Many inductive proofs
    are therefore unconditional.\<close>
consts
  "TFin" :: "[i,i]\i"

inductive
  domains       "TFin(S,next)" \<subseteq> "Pow(S)"
  intros
    nextI:       "\x \ TFin(S,next); next \ increasing(S)\
                  \<Longrightarrow> next`x \<in> TFin(S,next)"

    Pow_UnionI: "Y \ Pow(TFin(S,next)) \ \(Y) \ TFin(S,next)"

  monos         Pow_mono
  con_defs      increasing_def
  type_intros   CollectD1 [THEN apply_funtype] Union_in_Pow

subsection\<open>Mathematical Preamble\<close>

lemma Union_lemma0: "(\x\C. x<=A | B<=x) \ \(C)<=A | B<=\(C)"
by blast

lemma Inter_lemma0:
     "\c \ C; \x\C. A<=x | x<=B\ \ A \ \(C) | \(C) \ B"
by blast

subsection\<open>The Transfinite Construction\<close>

lemma increasingD1: "f \ increasing(A) \ f \ Pow(A)->Pow(A)"
  unfolding increasing_def
apply (erule CollectD1)
done

lemma increasingD2: "\f \ increasing(A); x<=A\ \ x \ f`x"
by (unfold increasing_def, blast)

lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI]

lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD]

text\<open>Structural induction on \<^term>\<open>TFin(S,next)\<close>\<close>
lemma TFin_induct:
  "\n \ TFin(S,next);
      \<And>x. \<lbrakk>x \<in> TFin(S,next);  P(x);  next \<in> increasing(S)\<rbrakk> \<Longrightarrow> P(next`x);
      \<And>Y. \<lbrakk>Y \<subseteq> TFin(S,next);  \<forall>y\<in>Y. P(y)\<rbrakk> \<Longrightarrow> P(\<Union>(Y))
\<rbrakk> \<Longrightarrow> P(n)"
by (erule TFin.induct, blast+)

subsection\<open>Some Properties of the Transfinite Construction\<close>

lemmas increasing_trans = subset_trans [OF _ increasingD2,
                                        OF _ _ TFin_is_subset]

text\<open>Lemma 1 of section 3.1\<close>
lemma TFin_linear_lemma1:
     "\n \ TFin(S,next); m \ TFin(S,next);
         \<forall>x \<in> TFin(S,next) . x<=m \<longrightarrow> x=m | next`x<=m\<rbrakk>
      \<Longrightarrow> n<=m | next`m<=n"
apply (erule TFin_induct)
apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*)
(*downgrade subsetI from intro! to intro*)
apply (blast dest: increasing_trans)
done

text\<open>Lemma 2 of section 3.2.  Interesting in its own right!
  Requires \<^term>\<open>next \<in> increasing(S)\<close> in the second induction step.\<close>
lemma TFin_linear_lemma2:
    "\m \ TFin(S,next); next \ increasing(S)\
     \<Longrightarrow> \<forall>n \<in> TFin(S,next). n<=m \<longrightarrow> n=m | next`n \<subseteq> m"
apply (erule TFin_induct)
apply (rule impI [THEN ballI])
txt\<open>case split using \<open>TFin_linear_lemma1\<close>\<close>
apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
       assumption+)
apply (blast del: subsetI
             intro: increasing_trans subsetI, blast)
txt\<open>second induction step\<close>
apply (rule impI [THEN ballI])
apply (rule Union_lemma0 [THEN disjE])
apply (erule_tac [3] disjI2)
prefer 2 apply blast
apply (rule ballI)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
       assumption+, blast)
apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
apply (blast dest: TFin_is_subset)+
done

text\<open>a more convenient form for Lemma 2\<close>
lemma TFin_subsetD:
     "\n<=m; m \ TFin(S,next); n \ TFin(S,next); next \ increasing(S)\
      \<Longrightarrow> n=m | next`n \<subseteq> m"
by (blast dest: TFin_linear_lemma2 [rule_format])

text\<open>Consequences from section 3.3 -- Property 3.2, the ordering is total\<close>
lemma TFin_subset_linear:
     "\m \ TFin(S,next); n \ TFin(S,next); next \ increasing(S)\
      \<Longrightarrow> n \<subseteq> m | m<=n"
apply (rule disjE)
apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
apply (assumption+, erule disjI2)
apply (blast del: subsetI
             intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset)
done

text\<open>Lemma 3 of section 3.3\<close>
lemma equal_next_upper:
     "\n \ TFin(S,next); m \ TFin(S,next); m = next`m\ \ n \ m"
apply (erule TFin_induct)
apply (drule TFin_subsetD)
apply (assumption+, force, blast)
done

text\<open>Property 3.3 of section 3.3\<close>
lemma equal_next_Union:
     "\m \ TFin(S,next); next \ increasing(S)\
      \<Longrightarrow> m = next`m <-> m = \<Union>(TFin(S,next))"
apply (rule iffI)
apply (rule Union_upper [THEN equalityI])
apply (rule_tac [2] equal_next_upper [THEN Union_least])
apply (assumption+)
apply (erule ssubst)
apply (rule increasingD2 [THEN equalityI], assumption)
apply (blast del: subsetI
             intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+
done

subsection\<open>Hausdorff's Theorem: Every Set Contains a Maximal Chain\<close>

text\<open>NOTE: We assume the partial ordering is \<open>\<subseteq>\<close>, the subset
relation!\<close>

text\<open>* Defining the "next" operation for Hausdorff's Theorem *\<close>

lemma chain_subset_Pow: "chain(A) \ Pow(A)"
  unfolding chain_def
apply (rule Collect_subset)
done

lemma super_subset_chain: "super(A,c) \ chain(A)"
  unfolding super_def
apply (rule Collect_subset)
done

lemma maxchain_subset_chain: "maxchain(A) \ chain(A)"
  unfolding maxchain_def
apply (rule Collect_subset)
done

lemma choice_super:
     "\ch \ (\X \ Pow(chain(S)) - {0}. X); X \ chain(S); X \ maxchain(S)\
      \<Longrightarrow> ch ` super(S,X) \<in> super(S,X)"
apply (erule apply_type)
apply (unfold super_def maxchain_def, blast)
done

lemma choice_not_equals:
     "\ch \ (\X \ Pow(chain(S)) - {0}. X); X \ chain(S); X \ maxchain(S)\
      \<Longrightarrow> ch ` super(S,X) \<noteq> X"
apply (rule notI)
apply (drule choice_super, assumption, assumption)
apply (simp add: super_def)
done

text\<open>This justifies Definition 4.4\<close>
lemma Hausdorff_next_exists:
     "ch \ (\X \ Pow(chain(S))-{0}. X) \
      \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
                   next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)"
apply (rule_tac x="\X\Pow(S).
                   if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X"
       in bexI)
apply force
  unfolding increasing_def
apply (rule CollectI)
apply (rule lam_type)
apply (simp (no_asm_simp))
apply (blast dest: super_subset_chain [THEN subsetD]
                   chain_subset_Pow [THEN subsetD] choice_super)
txt\<open>Now, verify that it increases\<close>
apply (simp (no_asm_simp) add: Pow_iff subset_refl)
apply safe
apply (drule choice_super)
apply (assumption+)
apply (simp add: super_def, blast)
done

text\<open>Lemma 4\<close>
lemma TFin_chain_lemma4:
     "\c \ TFin(S,next);
         ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X);
         next \<in> increasing(S);
         \<forall>X \<in> Pow(S). next`X =
                          if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)\<rbrakk>
     \<Longrightarrow> c \<in> chain(S)"
apply (erule TFin_induct)
apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD]
            choice_super [THEN super_subset_chain [THEN subsetD]])
  unfolding chain_def
apply (rule CollectI, blast, safe)
apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+)
      txt\<open>\<open>Blast_tac's\<close> slow\<close>
done

theorem Hausdorff: "\c. c \ maxchain(S)"
apply (rule AC_Pi_Pow [THEN exE])
apply (rule Hausdorff_next_exists [THEN bexE], assumption)
apply (rename_tac ch "next")
apply (subgoal_tac "\(TFin (S,next)) \ chain (S) ")
prefer 2
apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI])
apply (rule_tac x = "\(TFin (S,next))" in exI)
apply (rule classical)
apply (subgoal_tac "next ` Union(TFin (S,next)) = \(TFin (S,next))")
apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric])
apply (rule_tac [2] subset_refl [THEN TFin_UnionI])
prefer 2 apply assumption
apply (rule_tac [2] refl)
apply (simp add: subset_refl [THEN TFin_UnionI,
                              THEN TFin.dom_subset [THEN subsetD, THEN PowD]])
apply (erule choice_not_equals [THEN notE])
apply (assumption+)
done

subsection\<open>Zorn's Lemma: If All Chains in S Have Upper Bounds In S,
       then S contains a Maximal Element\<close>

text\<open>Used in the proof of Zorn's Lemma\<close>
lemma chain_extend:
    "\c \ chain(A); z \ A; \x \ c. x<=z\ \ cons(z,c) \ chain(A)"
by (unfold chain_def, blast)

lemma Zorn: "\c \ chain(S). \(c) \ S \ \y \ S. \z \ S. y<=z \ y=z"
apply (rule Hausdorff [THEN exE])
apply (simp add: maxchain_def)
apply (rename_tac c)
apply (rule_tac x = "\(c)" in bexI)
prefer 2 apply blast
apply safe
apply (rename_tac z)
apply (rule classical)
apply (subgoal_tac "cons (z,c) \ super (S,c) ")
apply (blast elim: equalityE)
apply (unfold super_def, safe)
apply (fast elim: chain_extend)
apply (fast elim: equalityE)
done

text \<open>Alternative version of Zorn's Lemma\<close>

theorem Zorn2:
  "\c \ chain(S). \y \ S. \x \ c. x \ y \ \y \ S. \z \ S. y<=z \ y=z"
apply (cut_tac Hausdorff maxchain_subset_chain)
apply (erule exE)
apply (drule subsetD, assumption)
apply (drule bspec, assumption, erule bexE)
apply (rule_tac x = y in bexI)
  prefer 2 apply assumption
apply clarify
apply rule apply assumption
apply rule
apply (rule ccontr)
apply (frule_tac z=z in chain_extend)
  apply (assumption, blast)
  unfolding maxchain_def super_def
apply (blast elim!: equalityCE)
done

subsection\<open>Zermelo's Theorem: Every Set can be Well-Ordered\<close>

text\<open>Lemma 5\<close>
lemma TFin_well_lemma5:
     "\n \ TFin(S,next); Z \ TFin(S,next); z:Z; \ \(Z) \ Z\
      \<Longrightarrow> \<forall>m \<in> Z. n \<subseteq> m"
apply (erule TFin_induct)
prefer 2 apply blast txt\<open>second induction step is easy\<close>
apply (rule ballI)
apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto)
apply (subgoal_tac "m = \(Z) ")
apply blast+
done

text\<open>Well-ordering of \<^term>\<open>TFin(S,next)\<close>\<close>
lemma well_ord_TFin_lemma: "\Z \ TFin(S,next); z \ Z\ \ \(Z) \ Z"
apply (rule classical)
apply (subgoal_tac "Z = {\(TFin (S,next))}")
apply (simp (no_asm_simp) add: Inter_singleton)
apply (erule equal_singleton)
apply (rule Union_upper [THEN equalityI])
apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+)
done

text\<open>This theorem just packages the previous result\<close>
lemma well_ord_TFin:
     "next \ increasing(S)
      \<Longrightarrow> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
apply (rule well_ordI)
  unfolding Subset_rel_def linear_def
txt\<open>Prove the well-foundedness goal\<close>
apply (rule wf_onI)
apply (frule well_ord_TFin_lemma, assumption)
apply (drule_tac x = "\(Z) " in bspec, assumption)
apply blast
txt\<open>Now prove the linearity goal\<close>
apply (intro ballI)
apply (case_tac "x=y")
apply blast
txt\<open>The \<^term>\<open>x\<noteq>y\<close> case remains\<close>
apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
       assumption+, blast+)
done

text\<open>* Defining the "next" operation for Zermelo's Theorem *\<close>

lemma choice_Diff:
     "\ch \ (\X \ Pow(S) - {0}. X); X \ S; X\S\ \ ch ` (S-X) \ S-X"
apply (erule apply_type)
apply (blast elim!: equalityE)
done

text\<open>This justifies Definition 6.1\<close>
lemma Zermelo_next_exists:
     "ch \ (\X \ Pow(S)-{0}. X) \
           \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
                      next`X = (if X=S then S else cons(ch`(S-X), X))"
apply (rule_tac x="\X\Pow(S). if X=S then S else cons(ch`(S-X), X)"
       in bexI)
apply force
  unfolding increasing_def
apply (rule CollectI)
apply (rule lam_type)
txt\<open>Type checking is surprisingly hard!\<close>
apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl)
apply (blast intro!: choice_Diff [THEN DiffD1])
txt\<open>Verify that it increases\<close>
apply (intro allI impI)
apply (simp add: Pow_iff subset_consI subset_refl)
done

text\<open>The construction of the injection\<close>
lemma choice_imp_injection:
     "\ch \ (\X \ Pow(S)-{0}. X);
         next \<in> increasing(S);
         \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X))\<rbrakk>
      \<Longrightarrow> (\<lambda> x \<in> S. \<Union>({y \<in> TFin(S,next). x \<notin> y}))
               \<in> inj(S, TFin(S,next) - {S})"
apply (rule_tac d = "\y. ch` (S-y) " in lam_injective)
apply (rule DiffI)
apply (rule Collect_subset [THEN TFin_UnionI])
apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE)
apply (subgoal_tac "x \ \({y \ TFin (S,next) . x \ y}) ")
prefer 2 apply (blast elim: equalityE)
apply (subgoal_tac "\({y \ TFin (S,next) . x \ y}) \ S")
prefer 2 apply (blast elim: equalityE)
txt\<open>For proving \<open>x \<in> next`\<Union>(...)\<close>.
  Abrial and Laffitte's justification appears to be faulty.\
apply (subgoal_tac "\ next ` Union({y \ TFin (S,next) . x \ y})
                    \<subseteq> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ")
prefer 2
apply (simp del: Union_iff
             add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]
             Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2])
apply (subgoal_tac "x \ next ` Union({y \ TFin (S,next) . x \ y}) ")
prefer 2
apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI)
txt\<open>End of the lemmas!\<close>
apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset])
done

text\<open>The wellordering theorem\<close>
theorem AC_well_ord: "\r. well_ord(S,r)"
apply (rule AC_Pi_Pow [THEN exE])
apply (rule Zermelo_next_exists [THEN bexE], assumption)
apply (rule exI)
apply (rule well_ord_rvimage)
apply (erule_tac [2] well_ord_TFin)
apply (rule choice_imp_injection [THEN inj_weaken_type], blast+)
done

subsection \<open>Zorn's Lemma for Partial Orders\<close>

text \<open>Reimported from HOL by Clemens Ballarin.\<close>

definition Chain :: "i \ i" where
  "Chain(r) = {A \ Pow(field(r)). \a\A. \b\A. \a, b\ \ r | \b, a\ \ r}"

lemma mono_Chain:
  "r \ s \ Chain(r) \ Chain(s)"
  unfolding Chain_def
  by blast

theorem Zorn_po:
  assumes po: "Partial_order(r)"
    and u: "\C\Chain(r). \u\field(r). \a\C. \a, u\ \ r"
  shows "\m\field(r). \a\field(r). \m, a\ \ r \ a = m"
proof -
  have "Preorder(r)" using po by (simp add: partial_order_on_def)
  \<comment> \<open>Mirror r in the set of subsets below (wrt r) elements of A (?).\<close>
  let ?B = "\x\field(r). r -`` {x}" let ?S = "?B `` field(r)"
  have "\C\chain(?S). \U\?S. \A\C. A \ U"
  proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp)
    fix C
    assume 1: "C \ ?S" and 2: "\A\C. \B\C. A \ B | B \ A"
    let ?A = "{x \ field(r). \M\C. M = ?B`x}"
    have "C = ?B `` ?A" using 1
      apply (auto simp: image_def)
      apply rule
      apply rule
      apply (drule subsetD) apply assumption
      apply (erule CollectE)
      apply rule apply assumption
      apply (erule bexE)
      apply rule prefer 2 apply assumption
      apply rule
      apply (erule lamE) apply simp
      apply assumption

      apply (thin_tac "C \ X" for X)
      apply (fast elim: lamE)
      done
    have "?A \ Chain(r)"
    proof (simp add: Chain_def subsetI, intro conjI ballI impI)
      fix a b
      assume "a \ field(r)" "r -`` {a} \ C" "b \ field(r)" "r -`` {b} \ C"
      hence "r -`` {a} \ r -`` {b} | r -`` {b} \ r -`` {a}" using 2 by auto
      then show "\a, b\ \ r | \b, a\ \ r"
        using \<open>Preorder(r)\<close> \<open>a \<in> field(r)\<close> \<open>b \<in> field(r)\<close>
        by (simp add: subset_vimage1_vimage1_iff)
    qed
    then obtain u where uA: "u \ field(r)" "\a\?A. \a, u\ \ r"
      using u
      apply auto
      apply (drule bspec) apply assumption
      apply auto
      done
    have "\A\C. A \ r -`` {u}"
    proof (auto intro!: vimageI)
      fix a B
      assume aB: "B \ C" "a \ B"
      with 1 obtain x where "x \ field(r)" "B = r -`` {x}"
        apply -
        apply (drule subsetD) apply assumption
        apply (erule imageE)
        apply (erule lamE)
        apply simp
        done
      then show "\a, u\ \ r" using uA aB \Preorder(r)\
        by (auto simp: preorder_on_def refl_def) (blast dest: trans_onD)+
    qed
    then show "\U\field(r). \A\C. A \ r -`` {U}"
      using \<open>u \<in> field(r)\<close> ..
  qed
  from Zorn2 [OF this]
  obtain m B where "m \ field(r)" "B = r -`` {m}"
    "\x\field(r). B \ r -`` {x} \ B = r -`` {x}"
    by (auto elim!: lamE simp: ball_image_simp)
  then have "\a\field(r). \m, a\ \ r \ a = m"
    using po \<open>Preorder(r)\<close> \<open>m \<in> field(r)\<close>
    by (auto simp: subset_vimage1_vimage1_iff Partial_order_eq_vimage1_vimage1_iff)
  then show ?thesis using \<open>m \<in> field(r)\<close> by blast
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.