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 19 kB

Quelle Order_Relation_More.thy Sprache: Isabelle

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

Basics on order-like relations.
*)

section \<open>Basics on Order-Like Relations\<close>

theory Order_Relation_More
  imports Main
begin

subsection \<open>The upper and lower bounds operators\<close>

lemma aboveS_subset_above: "aboveS r a \ above r a"
  by(auto simp add: aboveS_def above_def)

lemma AboveS_subset_Above: "AboveS r A \ Above r A"
  by(auto simp add: AboveS_def Above_def)

lemma UnderS_disjoint: "A Int (UnderS r A) = {}"
  by(auto simp add: UnderS_def)

lemma aboveS_notIn: "a \ aboveS r a"
  by(auto simp add: aboveS_def)

lemma Refl_above_in: "\Refl r; a \ Field r\ \ a \ above r a"
  by(auto simp add: refl_on_def above_def)

lemma in_Above_under: "a \ Field r \ a \ Above r (under r a)"
  by(auto simp add: Above_def under_def)

lemma in_Under_above: "a \ Field r \ a \ Under r (above r a)"
  by(auto simp add: Under_def above_def)

lemma in_UnderS_aboveS: "a \ Field r \ a \ UnderS r (aboveS r a)"
  by(auto simp add: UnderS_def aboveS_def)

lemma UnderS_subset_Under: "UnderS r A \ Under r A"
  by(auto simp add: UnderS_def Under_def)

lemma subset_Above_Under: "B \ Field r \ B \ Above r (Under r B)"
  by(auto simp add: Above_def Under_def)

lemma subset_Under_Above: "B \ Field r \ B \ Under r (Above r B)"
  by(auto simp add: Under_def Above_def)

lemma subset_AboveS_UnderS: "B \ Field r \ B \ AboveS r (UnderS r B)"
  by(auto simp add: AboveS_def UnderS_def)

lemma subset_UnderS_AboveS: "B \ Field r \ B \ UnderS r (AboveS r B)"
  by(auto simp add: UnderS_def AboveS_def)

lemma Under_Above_Galois:
  "\B \ Field r; C \ Field r\ \ (B \ Above r C) = (C \ Under r B)"
  by(unfold Above_def Under_def, blast)

lemma UnderS_AboveS_Galois:
  "\B \ Field r; C \ Field r\ \ (B \ AboveS r C) = (C \ UnderS r B)"
  by(unfold AboveS_def UnderS_def, blast)

lemma Refl_above_aboveS:
  assumes REFL: "Refl r" and IN: "a \ Field r"
  shows "above r a = aboveS r a \ {a}"
proof(unfold above_def aboveS_def, auto)
  show "(a,a) \ r" using REFL IN refl_on_def[of _ r] by blast
qed

lemma Linear_order_under_aboveS_Field:
  assumes LIN: "Linear_order r" and IN: "a \ Field r"
  shows "Field r = under r a \ aboveS r a"
proof(unfold under_def aboveS_def, auto)
  assume "a \ Field r" "(a, a) \ r"
  with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
  show False by auto
next
  fix b assume "b \ Field r" "(b, a) \ r"
  with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
  have "(a,b) \ r \ a = b" by blast
  thus "(a,b) \ r"
    using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
next
  fix b assume "(b, a) \ r"
  thus "b \ Field r"
    using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
next
  fix b assume "b \ a" "(a, b) \ r"
  thus "b \ Field r"
    using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
qed

lemma Linear_order_underS_above_Field:
  assumes LIN: "Linear_order r" and IN: "a \ Field r"
  shows "Field r = underS r a \ above r a"
proof(unfold underS_def above_def, auto)
  assume "a \ Field r" "(a, a) \ r"
  with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
  show False by metis
next
  fix b assume "b \ Field r" "(a, b) \ r"
  with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
  have "(b,a) \ r \ b = a" by blast
  thus "(b,a) \ r"
    using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto
next
  fix b assume "b \ a" "(b, a) \ r"
  thus "b \ Field r"
    using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast
next
  fix b assume "(a, b) \ r"
  thus "b \ Field r"
    using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
qed

lemma under_empty: "a \ Field r \ under r a = {}"
  unfolding Field_def under_def by auto

lemma Under_Field: "Under r A \ Field r"
  by(unfold Under_def Field_def, auto)

lemma UnderS_Field: "UnderS r A \ Field r"
  by(unfold UnderS_def Field_def, auto)

lemma above_Field: "above r a \ Field r"
  by(unfold above_def Field_def, auto)

lemma aboveS_Field: "aboveS r a \ Field r"
  by(unfold aboveS_def Field_def, auto)

lemma Above_Field: "Above r A \ Field r"
  by(unfold Above_def Field_def, auto)

lemma Refl_under_Under:
  assumes REFL: "Refl r" and NE: "A \ {}"
  shows "Under r A = (\a \ A. under r a)"
proof
  show "Under r A \ (\a \ A. under r a)"
    by(unfold Under_def under_def, auto)
next
  show "(\a \ A. under r a) \ Under r A"
  proof(auto)
    fix x
    assume *: "\xa \ A. x \ under r xa"
    hence "\xa \ A. (x,xa) \ r"
      by (simp add: under_def)
    moreover
    {from NE obtain a where "a \ A" by blast
      with * have "x \ under r a" by simp
      hence "x \ Field r"
        using under_Field[of r a] by auto
    }
    ultimately show "x \ Under r A"
      unfolding Under_def by auto
  qed
qed

lemma Refl_underS_UnderS:
  assumes REFL: "Refl r" and NE: "A \ {}"
  shows "UnderS r A = (\a \ A. underS r a)"
proof
  show "UnderS r A \ (\a \ A. underS r a)"
    by(unfold UnderS_def underS_def, auto)
next
  show "(\a \ A. underS r a) \ UnderS r A"
  proof(auto)
    fix x
    assume *: "\xa \ A. x \ underS r xa"
    hence "\xa \ A. x \ xa \ (x,xa) \ r"
      by (auto simp add: underS_def)
    moreover
    {from NE obtain a where "a \ A" by blast
      with * have "x \ underS r a" by simp
      hence "x \ Field r"
        using underS_Field[of _ r a] by auto
    }
    ultimately show "x \ UnderS r A"
      unfolding UnderS_def by auto
  qed
qed

lemma Refl_above_Above:
  assumes REFL: "Refl r" and NE: "A \ {}"
  shows "Above r A = (\a \ A. above r a)"
proof
  show "Above r A \ (\a \ A. above r a)"
    by(unfold Above_def above_def, auto)
next
  show "(\a \ A. above r a) \ Above r A"
  proof(auto)
    fix x
    assume *: "\xa \ A. x \ above r xa"
    hence "\xa \ A. (xa,x) \ r"
      by (simp add: above_def)
    moreover
    {from NE obtain a where "a \ A" by blast
      with * have "x \ above r a" by simp
      hence "x \ Field r"
        using above_Field[of r a] by auto
    }
    ultimately show "x \ Above r A"
      unfolding Above_def by auto
  qed
qed

lemma Refl_aboveS_AboveS:
  assumes REFL: "Refl r" and NE: "A \ {}"
  shows "AboveS r A = (\a \ A. aboveS r a)"
proof
  show "AboveS r A \ (\a \ A. aboveS r a)"
    by(unfold AboveS_def aboveS_def, auto)
next
  show "(\a \ A. aboveS r a) \ AboveS r A"
  proof(auto)
    fix x
    assume *: "\xa \ A. x \ aboveS r xa"
    hence "\xa \ A. xa \ x \ (xa,x) \ r"
      by (auto simp add: aboveS_def)
    moreover
    {from NE obtain a where "a \ A" by blast
      with * have "x \ aboveS r a" by simp
      hence "x \ Field r"
        using aboveS_Field[of r a] by auto
    }
    ultimately show "x \ AboveS r A"
      unfolding AboveS_def by auto
  qed
qed

lemma under_Under_singl: "under r a = Under r {a}"
  by(unfold Under_def under_def, auto simp add: Field_def)

lemma underS_UnderS_singl: "underS r a = UnderS r {a}"
  by(unfold UnderS_def underS_def, auto simp add: Field_def)

lemma above_Above_singl: "above r a = Above r {a}"
  by(unfold Above_def above_def, auto simp add: Field_def)

lemma aboveS_AboveS_singl: "aboveS r a = AboveS r {a}"
  by(unfold AboveS_def aboveS_def, auto simp add: Field_def)

lemma Under_decr: "A \ B \ Under r B \ Under r A"
  by(unfold Under_def, auto)

lemma UnderS_decr: "A \ B \ UnderS r B \ UnderS r A"
  by(unfold UnderS_def, auto)

lemma Above_decr: "A \ B \ Above r B \ Above r A"
  by(unfold Above_def, auto)

lemma AboveS_decr: "A \ B \ AboveS r B \ AboveS r A"
  by(unfold AboveS_def, auto)

lemma under_incl_iff:
  assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a \ Field r"
  shows "(under r a \ under r b) = ((a,b) \ r)"
proof
  assume "(a,b) \ r"
  thus "under r a \ under r b" using TRANS
    by (auto simp add: under_incr)
next
  assume "under r a \ under r b"
  moreover
  have "a \ under r a" using REFL IN
    by (auto simp add: Refl_under_in)
  ultimately show "(a,b) \ r"
    by (auto simp add: under_def)
qed

lemma above_decr:
  assumes TRANS: "trans r" and REL: "(a,b) \ r"
  shows "above r b \ above r a"
proof(unfold above_def, auto)
  fix x assume "(b,x) \ r"
  with REL TRANS trans_def[of r]
  show "(a,x) \ r" by blast
qed

lemma aboveS_decr:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    REL: "(a,b) \ r"
  shows "aboveS r b \ aboveS r a"
proof(unfold aboveS_def, auto)
  assume *: "a \ b" and **: "(b,a) \ r"
  with ANTISYM antisym_def[of r] REL
  show False by auto
next
  fix x assume "x \ b" "(b,x) \ r"
  with REL TRANS trans_def[of r]
  show "(a,x) \ r" by blast
qed

lemma under_trans:
  assumes TRANS: "trans r" and
    IN1: "a \ under r b" and IN2: "b \ under r c"
  shows "a \ under r c"
proof-
  have "(a,b) \ r \ (b,c) \ r"
    using IN1 IN2 under_def by fastforce
  hence "(a,c) \ r"
    using TRANS trans_def[of r] by blast
  thus ?thesis unfolding under_def by simp
qed

lemma under_underS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a \ under r b" and IN2: "b \ underS r c"
  shows "a \ underS r c"
proof-
  have 0: "(a,b) \ r \ (b,c) \ r"
    using IN1 IN2 under_def underS_def by fastforce
  hence 1: "(a,c) \ r"
    using TRANS trans_def[of r] by blast
  have 2: "b \ c" using IN2 underS_def by force
  have 3: "a \ c"
  proof
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
    show False by auto
  qed
  from 1 3 show ?thesis unfolding underS_def by simp
qed

lemma underS_under_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a \ underS r b" and IN2: "b \ under r c"
  shows "a \ underS r c"
proof-
  have 0: "(a,b) \ r \ (b,c) \ r"
    using IN1 IN2 under_def underS_def by fast
  hence 1: "(a,c) \ r"
    using TRANS trans_def[of r] by fast
  have 2: "a \ b" using IN1 underS_def by force
  have 3: "a \ c"
  proof
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
    show False by auto
  qed
  from 1 3 show ?thesis unfolding underS_def by simp
qed

lemma underS_underS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a \ underS r b" and IN2: "b \ underS r c"
  shows "a \ underS r c"
proof-
  have "a \ under r b"
    using IN1 underS_subset_under by fast
  with assms under_underS_trans show ?thesis by fast
qed

lemma above_trans:
  assumes TRANS: "trans r" and
    IN1: "b \<in> above r a" and IN2: "c \<in> above r b"
  shows "c \<in> above r a"
proof-
  have "(a,b) \<in> r \<and> (b,c) \<in> r"
    using IN1 IN2 above_def by fast
  hence "(a,c) \<in> r"
    using TRANS trans_def[of r] by blast
  thus ?thesis unfolding above_def by simp
qed

lemma above_aboveS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "b \<in> above r a" and IN2: "c \<in> aboveS r b"
  shows "c \<in> aboveS r a"
proof-
  have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
    using IN1 IN2 above_def aboveS_def by fast
  hence 1: "(a,c) \<in> r"
    using TRANS trans_def[of r] by blast
  have 2: "b \<noteq> c" using IN2 aboveS_def by force
  have 3: "a \<noteq> c"
  proof
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
    show False by auto
  qed
  from 1 3 show ?thesis unfolding aboveS_def by simp
qed

lemma aboveS_above_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "b \<in> aboveS r a" and IN2: "c \<in> above r b"
  shows "c \<in> aboveS r a"
proof-
  have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
    using IN1 IN2 above_def aboveS_def by fast
  hence 1: "(a,c) \<in> r"
    using TRANS trans_def[of r] by blast
  have 2: "a \<noteq> b" using IN1 aboveS_def by force
  have 3: "a \<noteq> c"
  proof
    assume "a = c" with 0 2 ANTISYM antisym_def[of r]
    show False by auto
  qed
  from 1 3 show ?thesis unfolding aboveS_def by simp
qed

lemma aboveS_aboveS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "b \<in> aboveS r a" and IN2: "c \<in> aboveS r b"
  shows "c \<in> aboveS r a"
proof-
  have "b \<in> above r a"
    using IN1 aboveS_subset_above by fast
  with assms above_aboveS_trans show ?thesis by fast
qed

lemma under_Under_trans:
  assumes TRANS: "trans r" and
    IN1: "a \<in> under r b" and IN2: "b \<in> Under r C"
  shows "a \<in> Under r C"
proof-
  have "b \<in> {u \<in> Field r. \<forall>x. x \<in> C \<longrightarrow> (u, x) \<in> r}"
    using IN2 Under_def by force
  hence "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
    using IN1 under_def by fast
  hence "\<forall>c \<in> C. (a,c) \<in> r"
    using TRANS trans_def[of r] by blast
  moreover
  have "a \<in> Field r" using IN1 unfolding Field_def under_def by blast
  ultimately
  show ?thesis unfolding Under_def by blast
qed

lemma underS_Under_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a \<in> underS r b" and IN2: "b \<in> Under r C"
  shows "a \<in> UnderS r C"
proof-
  from IN1 have "a \<in> under r b"
    using underS_subset_under[of r b] by fast
  with assms under_Under_trans
  have "a \<in> Under r C" by fast
      (*  *)
  moreover
  have "a \<notin> C"
  proof
    assume *: "a \<in> C"
    have 1: "b \<noteq> a \<and> (a,b) \<in> r"
      using IN1 underS_def[of r b] by auto
    have "\<forall>c \<in> C. (b,c) \<in> r"
      using IN2 Under_def[of r C] by auto
    with * have "(b,a) \<in> r" by simp
    with 1 ANTISYM antisym_def[of r]
    show False by blast
  qed
    (*  *)
  ultimately
  show ?thesis unfolding UnderS_def
    using Under_def by force
qed

lemma underS_UnderS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a \<in> underS r b" and IN2: "b \<in> UnderS r C"
  shows "a \<in> UnderS r C"
proof-
  from IN2 have "b \<in> Under r C"
    using UnderS_subset_Under[of r C] by blast
  with underS_Under_trans assms
  show ?thesis by force
qed

lemma above_Above_trans:
  assumes TRANS: "trans r" and
    IN1: "a \<in> above r b" and IN2: "b \<in> Above r C"
  shows "a \<in> Above r C"
proof-
  have "(b,a) \<in> r \<and> (\<forall>c \<in> C. (c,b) \<in> r)"
    using IN1[unfolded above_def] IN2[unfolded Above_def] by simp
  hence "\<forall>c \<in> C. (c,a) \<in> r"
    using TRANS trans_def[of r] by blast
  moreover
  have "a \<in> Field r" using IN1[unfolded above_def] Field_def by fast
  ultimately
  show ?thesis unfolding Above_def by auto
qed

lemma aboveS_Above_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a \<in> aboveS r b" and IN2: "b \<in> Above r C"
  shows "a \<in> AboveS r C"
proof-
  from IN1 have "a \<in> above r b"
    using aboveS_subset_above[of r b] by blast
  with assms above_Above_trans
  have "a \<in> Above r C" by fast
      (*  *)
  moreover
  have "a \<notin> C"
  proof
    assume *: "a \<in> C"
    have 1: "b \<noteq> a \<and> (b,a) \<in> r"
      using IN1 aboveS_def[of r b] by auto
    have "\<forall>c \<in> C. (c,b) \<in> r"
      using IN2 Above_def[of r C] by auto
    with * have "(a,b) \<in> r" by simp
    with 1 ANTISYM antisym_def[of r]
    show False by blast
  qed
    (*  *)
  ultimately
  show ?thesis unfolding AboveS_def
    using Above_def by force
qed

lemma above_AboveS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a \<in> above r b" and IN2: "b \<in> AboveS r C"
  shows "a \<in> AboveS r C"
proof-
  from IN2 have "b \<in> Above r C"
    using AboveS_subset_Above[of r C] by blast
  with assms above_Above_trans
  have "a \<in> Above r C" by force
      (*  *)
  moreover
  have "a \<notin> C"
  proof
    assume *: "a \<in> C"
    have 1: "(b,a) \<in> r"
      using IN1 above_def[of r b] by auto
    have "\<forall>c \<in> C. b \<noteq> c \<and> (c,b) \<in> r"
      using IN2 AboveS_def[of r C] by auto
    with * have "b \<noteq> a \<and> (a,b) \<in> r" by simp
    with 1 ANTISYM antisym_def[of r]
    show False by blast
  qed
    (*  *)
  ultimately
  show ?thesis unfolding AboveS_def
    using Above_def by force
qed

lemma aboveS_AboveS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a \<in> aboveS r b" and IN2: "b \<in> AboveS r C"
  shows "a \<in> AboveS r C"
proof-
  from IN2 have "b \<in> Above r C"
    using AboveS_subset_Above[of r C] by blast
  with aboveS_Above_trans assms
  show ?thesis by force
qed

lemma under_UnderS_trans:
  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
    IN1: "a \<in> under r b" and IN2: "b \<in> UnderS r C"
  shows "a \<in> UnderS r C"
proof-
  from IN2 have "b \<in> Under r C"
    using UnderS_subset_Under[of r C] by blast
  with assms under_Under_trans
  have "a \<in> Under r C" by force
      (*  *)
  moreover
  have "a \<notin> C"
  proof
    assume *: "a \<in> C"
    have 1: "(a,b) \<in> r"
      using IN1 under_def[of r b] by auto
    have "\<forall>c \<in> C. b \<noteq> c \<and> (b,c) \<in> r"
      using IN2 UnderS_def[of r C] by blast
    with * have "b \<noteq> a \<and> (b,a) \<in> r" by blast
    with 1 ANTISYM antisym_def[of r]
    show False by blast
  qed
    (*  *)
  ultimately
  show ?thesis unfolding UnderS_def Under_def by fast
qed

subsection \<open>Properties depending on more than one relation\<close>

lemma under_incr2:
  "r \<le> r' \<Longrightarrow> under r a \<le> under r' a"
  unfolding under_def by blast

lemma underS_incr2:
  "r \<le> r' \<Longrightarrow> underS r a \<le> underS r' a"
  unfolding underS_def by blast

(* FIXME: r \<leadsto> r'
lemma Under_incr:
"r \<le> r' \<Longrightarrow> Under r A \<le> Under r A"
unfolding Under_def by blast

lemma UnderS_incr:
"r \<le> r' \<Longrightarrow> UnderS r A \<le> UnderS r A"
unfolding UnderS_def by blast

lemma Under_incr_decr:
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> Under r A \<le> Under r A'"
unfolding Under_def by blast

lemma UnderS_incr_decr:
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> UnderS r A \<le> UnderS r A'"
unfolding UnderS_def by blast
*)

lemma above_incr2:
  "r \<le> r' \<Longrightarrow> above r a \<le> above r' a"
  unfolding above_def by blast

lemma aboveS_incr2:
  "r \<le> r' \<Longrightarrow> aboveS r a \<le> aboveS r' a"
  unfolding aboveS_def by blast

(* FIXME
lemma Above_incr:
"r \<le> r' \<Longrightarrow> Above r A \<le> Above r A"
unfolding Above_def by blast

lemma AboveS_incr:
"r \<le> r' \<Longrightarrow> AboveS r A \<le> AboveS r A"
unfolding AboveS_def by blast

lemma Above_incr_decr:
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> Above r A \<le> Above r A'"
unfolding Above_def by blast

lemma AboveS_incr_decr:
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> AboveS r A \<le> AboveS r A'"
unfolding AboveS_def by blast
*)

end

quality100%

¤ Dauer der Verarbeitung: 0.32 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.