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/HOL/Cardinals/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 10 kB

Quelle Wellorder_Relation.thy Sprache: Isabelle

(*  Title:      HOL/Cardinals/Wellorder_Relation.thy
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

Well-order relations.
*)

section \<open>Well-Order Relations\<close>

theory Wellorder_Relation
  imports Wellfounded_More
begin

context wo_rel
begin

subsection \<open>Auxiliaries\<close>

lemma PREORD: "Preorder r"
  using WELL order_on_defs[of _ r] by auto

lemma PARORD: "Partial_order r"
  using WELL order_on_defs[of _ r] by auto

lemma cases_Total2:
  "\ phi a b. \{a,b} \ Field r; ((a,b) \ r - Id \ phi a b);
              ((b,a) \<in> r - Id \<Longrightarrow> phi a b); (a = b \<Longrightarrow> phi a b)\<rbrakk>
             \<Longrightarrow> phi a b"
  using TOTALS by auto

subsection \<open>Well-founded induction and recursion adapted to non-strict well-order relations\<close>

lemma worec_unique_fixpoint:
  assumes ADM: "adm_wo H" and fp: "f = H f"
  shows "f = worec H"
proof-
  have "adm_wf (r - Id) H"
    unfolding adm_wf_def
    using ADM adm_wo_def[of H] underS_def[of r] by auto
  hence "f = wfrec (r - Id) H"
    using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp
  thus ?thesis unfolding worec_def .
qed

subsubsection \<open>Properties of max2\<close>

lemma max2_iff:
  assumes "a \ Field r" and "b \ Field r"
  shows "((max2 a b, c) \ r) = ((a,c) \ r \ (b,c) \ r)"
proof
  assume "(max2 a b, c) \ r"
  thus "(a,c) \ r \ (b,c) \ r"
    using assms max2_greater[of a b] TRANS trans_def[of r] by blast
next
  assume "(a,c) \ r \ (b,c) \ r"
  thus "(max2 a b, c) \ r"
    using assms max2_among[of a b] by auto
qed

subsubsection \<open>Properties of minim\<close>

lemma minim_Under:
  "\B \ Field r; B \ {}\ \ minim B \ Under B"
  by(auto simp add: Under_def minim_inField minim_least)

lemma equals_minim_Under:
  "\B \ Field r; a \ B; a \ Under B\
\<Longrightarrow> a = minim B"
  by(auto simp add: Under_def equals_minim)

lemma minim_iff_In_Under:
  assumes SUB: "B \ Field r" and NE: "B \ {}"
  shows "(a = minim B) = (a \ B \ a \ Under B)"
proof
  assume "a = minim B"
  thus "a \ B \ a \ Under B"
    using assms minim_in minim_Under by simp
next
  assume "a \ B \ a \ Under B"
  thus "a = minim B"
    using assms equals_minim_Under by simp
qed

lemma minim_Under_under:
  assumes NE: "A \ {}" and SUB: "A \ Field r"
  shows "Under A = under (minim A)"
proof-
  have "minim A \ A"
    using assms minim_in by auto
  then have "Under A \ under (minim A)"
    by (simp add: Under_decr under_Under_singl)
  moreover have "under (minim A) \ Under A"
    by (meson NE SUB TRANS minim_Under subset_eq under_Under_trans)
  ultimately show ?thesis by blast
qed

lemma minim_UnderS_underS:
  assumes NE: "A \ {}" and SUB: "A \ Field r"
  shows "UnderS A = underS (minim A)"
proof-
  have "minim A \ A"
    using assms minim_in by auto
  then have "UnderS A \ underS (minim A)"
    by (simp add: UnderS_decr underS_UnderS_singl)
  moreover have "underS (minim A) \ UnderS A"
    by (meson ANTISYM NE SUB TRANS minim_Under subset_eq underS_Under_trans)
  ultimately show ?thesis by blast
qed

subsubsection \<open>Properties of supr\<close>

lemma supr_Above:
  assumes "Above B \ {}"
  shows "supr B \ Above B"
  by (simp add: assms Above_Field minim_in supr_def)

lemma supr_greater:
  assumes "Above B \ {}" "b \ B"
  shows "(b, supr B) \ r"
  using assms Above_def supr_Above by fastforce

lemma supr_least_Above:
  assumes "a \ Above B"
  shows "(supr B, a) \ r"
  by (simp add: assms Above_Field minim_least supr_def)

lemma supr_least:
  "\B \ Field r; a \ Field r; (\ b. b \ B \ (b,a) \ r)\
\<Longrightarrow> (supr B, a) \<in> r"
  by(auto simp add: supr_least_Above Above_def)

lemma equals_supr_Above:
  assumes "a \ Above B" "\ a'. a' \ Above B \ (a,a') \ r"
  shows "a = supr B"
  by (simp add: assms Above_Field equals_minim supr_def)

lemma equals_supr:
  assumes SUB: "B \ Field r" and IN: "a \ Field r" and
    ABV: "\ b. b \ B \ (b,a) \ r" and
    MINIM: "\ a'. \ a' \ Field r; \ b. b \ B \ (b,a') \ r\ \ (a,a') \ r"
  shows "a = supr B"
proof-
  have "a \ Above B"
    unfolding Above_def using ABV IN by simp
  moreover
  have "\ a'. a' \ Above B \ (a,a') \ r"
    unfolding Above_def using MINIM by simp
  ultimately show ?thesis
    using equals_supr_Above SUB by auto
qed

lemma supr_inField:
  assumes "Above B \ {}"
  shows "supr B \ Field r"
  by (simp add: Above_Field assms minim_inField supr_def)

lemma supr_above_Above:
  assumes SUB: "B \ Field r" and ABOVE: "Above B \ {}"
  shows "Above B = above (supr B)"
  apply (clarsimp simp: Above_def above_def set_eq_iff)
  by (meson ABOVE FieldI2 SUB TRANS supr_greater supr_least transD)

lemma supr_under:
  assumes "a \ Field r"
  shows "a = supr (under a)"
proof-
  have "under a \ Field r"
    using under_Field[of r] by auto
  moreover
  have "under a \ {}"
    using assms Refl_under_in[of r] REFL by auto
  moreover
  have "a \ Above (under a)"
    using in_Above_under[of _ r] assms by auto
  moreover
  have "\a' \ Above (under a). (a,a') \ r"
    by (auto simp: Above_def above_def REFL Refl_under_in assms)
  ultimately show ?thesis
    using equals_supr_Above by auto
qed

subsubsection \<open>Properties of successor\<close>

lemma suc_least:
  "\B \ Field r; a \ Field r; (\ b. b \ B \ a \ b \ (b,a) \ r)\
\<Longrightarrow> (suc B, a) \<in> r"
  by(auto simp add: suc_least_AboveS AboveS_def)

lemma equals_suc:
  assumes SUB: "B \ Field r" and IN: "a \ Field r" and
    ABVS: "\ b. b \ B \ a \ b \ (b,a) \ r" and
    MINIM: "\ a'. \a' \ Field r; \ b. b \ B \ a' \ b \ (b,a') \ r\ \ (a,a') \ r"
  shows "a = suc B"
proof-
  have "a \ AboveS B"
    unfolding AboveS_def using ABVS IN by simp
  moreover
  have "\ a'. a' \ AboveS B \ (a,a') \ r"
    unfolding AboveS_def using MINIM by simp
  ultimately show ?thesis
    using equals_suc_AboveS SUB by auto
qed

lemma suc_above_AboveS:
  assumes SUB: "B \ Field r" and
    ABOVE: "AboveS B \ {}"
  shows "AboveS B = above (suc B)"
  using assms
proof(unfold AboveS_def above_def, auto)
  fix a assume "a \ Field r" "\b \ B. a \ b \ (b,a) \ r"
  with suc_least assms
  show "(suc B,a) \ r" by auto
next
  fix b assume "(suc B, b) \ r"
  thus "b \ Field r"
    by (simp add: FieldI2)
next
  fix a b
  assume 1: "(suc B, b) \ r" and 2: "a \ B"
  with assms suc_greater[of B a]
  have "(a,suc B) \ r" by auto
  thus "(a,b) \ r"
    using 1 TRANS trans_def[of r] by blast
next
  fix a
  assume "(suc B, a) \ r" and 2: "a \ B"
  thus False
    by (metis ABOVE ANTISYM SUB antisymD suc_greater)
qed

lemma suc_singl_pred:
  assumes IN: "a \ Field r" and ABOVE_NE: "aboveS a \ {}" and
    REL: "(a',suc {a}) \ r" and DIFF: "a' \ suc {a}"
  shows "a' = a \ (a',a) \ r"
proof-
  have *: "suc {a} \ Field r \ a' \ Field r"
    using WELL REL well_order_on_domain by metis
  {assume **: "a' \ a"
    hence "(a,a') \ r \ (a',a) \ r"
      using TOTAL IN * by (auto simp add: total_on_def)
    moreover
    {assume "(a,a') \ r"
      with ** * assms WELL suc_least[of "{a}" a']
      have "(suc {a},a') \ r" by auto
      with REL DIFF * ANTISYM antisym_def[of r]
      have False by simp
    }
    ultimately have "(a',a) \ r"
      by blast
  }
  thus ?thesis by blast
qed

lemma under_underS_suc:
  assumes IN: "a \ Field r" and ABV: "aboveS a \ {}"
  shows "underS (suc {a}) = under a"
proof -
  have "AboveS {a} \ {}"
    using ABV aboveS_AboveS_singl[of r] by auto
  then have 2: "a \ suc {a} \ (a,suc {a}) \ r"
    using suc_greater[of "{a}" a] IN  by auto
  have "underS (suc {a}) \ under a"
    using ABV IN REFL Refl_under_in underS_E under_def wo_rel.suc_singl_pred wo_rel_axioms by fastforce
  moreover
  have "under a \ underS (suc {a})"
    by (simp add: "2" ANTISYM TRANS subsetI underS_I under_underS_trans)
  ultimately show ?thesis by blast
qed

subsubsection \<open>Properties of order filters\<close>

lemma ofilter_Under[simp]:
  assumes "A \ Field r"
  shows "ofilter(Under A)"
  by (clarsimp simp: ofilter_def) (meson TRANS Under_Field subset_eq under_Under_trans)

lemma ofilter_UnderS[simp]:
  assumes "A \ Field r"
  shows "ofilter(UnderS A)"
  by (clarsimp simp: ofilter_def) (meson ANTISYM TRANS UnderS_Field subset_eq under_UnderS_trans)

lemma ofilter_Int[simp]: "\ofilter A; ofilter B\ \ ofilter(A Int B)"
  unfolding ofilter_def by blast

lemma ofilter_Un[simp]: "\ofilter A; ofilter B\ \ ofilter(A \ B)"
  unfolding ofilter_def by blast

lemma ofilter_INTER:
  "\I \ {}; \ i. i \ I \ ofilter(A i)\ \ ofilter (\i \ I. A i)"
  unfolding ofilter_def by blast

lemma ofilter_Inter:
  "\S \ {}; \ A. A \ S \ ofilter A\ \ ofilter (\S)"
  unfolding ofilter_def by blast

lemma ofilter_Union:
  "(\ A. A \ S \ ofilter A) \ ofilter (\S)"
  unfolding ofilter_def by blast

lemma ofilter_under_Union:
  "ofilter A \ A = \{under a| a. a \ A}"
  using ofilter_under_UNION [of A] by auto

subsubsection \<open>Other properties\<close>

lemma Trans_Under_regressive:
  assumes NE: "A \ {}" and SUB: "A \ Field r"
  shows "Under(Under A) \ Under A"
  by (metis INT_E NE REFL Refl_under_Under SUB empty_iff minim_Under minim_Under_under subsetI)

lemma ofilter_suc_Field:
  assumes OF: "ofilter A" and NE: "A \ Field r"
  shows "ofilter (A \ {suc A})"
  by (metis NE OF REFL Refl_under_underS ofilter_underS_Field suc_underS under_ofilter)

(* FIXME: needed? *)
declare
  minim_in[simp]
  minim_inField[simp]
  minim_least[simp]
  under_ofilter[simp]
  underS_ofilter[simp]
  Field_ofilter[simp]

end

abbreviation "worec \ wo_rel.worec"
abbreviation "adm_wo \ wo_rel.adm_wo"
abbreviation "isMinim \ wo_rel.isMinim"
abbreviation "minim \ wo_rel.minim"
abbreviation "max2 \ wo_rel.max2"
abbreviation "supr \ wo_rel.supr"
abbreviation "suc \ wo_rel.suc"

end

quality100%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

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.