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

Quelle Lattice_Algebras.thy Sprache: Isabelle

(*  Author:     Steven Obua, TU Muenchen *)

section \<open>Various algebraic structures combined with a lattice\<close>

theory Lattice_Algebras
  imports Complex_Main
begin

class semilattice_inf_ab_group_add = ordered_ab_group_add + semilattice_inf
begin

lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + c)" (is "?L=?R")
proof (intro order.antisym)
  show "?R \ ?L"
  by (metis add_commute diff_le_eq inf_greatest inf_le1 inf_le2)
qed simp

lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)"
  using add_commute add_inf_distrib_left by presburger

end

class semilattice_sup_ab_group_add = ordered_ab_group_add + semilattice_sup
begin

lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)" (is "?L = ?R")
proof (rule order.antisym)
  show "?L \ ?R"
    by (metis add_commute le_diff_eq sup.bounded_iff sup_ge1 sup_ge2)
qed simp

lemma add_sup_distrib_right: "sup a b + c = sup (a + c) (b + c)"
proof -
  have "c + sup a b = sup (c+a) (c+b)"
    by (simp add: add_sup_distrib_left)
  then show ?thesis
    by (simp add: add.commute)
qed

end

class lattice_ab_group_add = ordered_ab_group_add + lattice
begin

subclass semilattice_inf_ab_group_add ..
subclass semilattice_sup_ab_group_add ..

lemmas add_sup_inf_distribs =
  add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left

lemma inf_eq_neg_sup: "inf a b = - sup (- a) (- b)"
proof (rule inf_unique)
  fix a b c :: 'a
  show "- sup (- a) (- b) \ a"
    by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
      (simp, simp add: add_sup_distrib_left)
  show "- sup (-a) (-b) \ b"
    by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
      (simp, simp add: add_sup_distrib_left)
  assume "a \ b" "a \ c"
  then show "a \ - sup (-b) (-c)"
    by (subst neg_le_iff_le [symmetric]) (simp add: le_supI)
qed

lemma sup_eq_neg_inf: "sup a b = - inf (- a) (- b)"
proof (rule sup_unique)
  fix a b c :: 'a
  show "a \ - inf (- a) (- b)"
    by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
      (simp, simp add: add_inf_distrib_left)
  show "b \ - inf (- a) (- b)"
    by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
      (simp, simp add: add_inf_distrib_left)
  show "- inf (- a) (- b) \ c" if "a \ c" "b \ c"
    using that by (subst neg_le_iff_le [symmetric]) (simp add: le_infI)
qed

lemma neg_inf_eq_sup: "- inf a b = sup (- a) (- b)"
  by (simp add: inf_eq_neg_sup)

lemma diff_inf_eq_sup: "a - inf b c = a + sup (- b) (- c)"
  using neg_inf_eq_sup [of b c, symmetric] by simp

lemma neg_sup_eq_inf: "- sup a b = inf (- a) (- b)"
  by (simp add: sup_eq_neg_inf)

lemma diff_sup_eq_inf: "a - sup b c = a + inf (- b) (- c)"
  using neg_sup_eq_inf [of b c, symmetric] by simp

lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
proof -
  have "0 = - inf 0 (a - b) + inf (a - b) 0"
    by (simp add: inf_commute)
  then have "0 = sup 0 (b - a) + inf (a - b) 0"
    by (simp add: inf_eq_neg_sup)
  then have "0 = (- a + sup a b) + (inf a b + (- b))"
    by (simp only: add_sup_distrib_left add_inf_distrib_right) simp
  then show ?thesis
    by (simp add: algebra_simps)
qed

subsection \<open>Positive Part, Negative Part, Absolute Value\<close>

definition nprt :: "'a \ 'a"
  where "nprt x = inf x 0"

definition pprt :: "'a \ 'a"
  where "pprt x = sup x 0"

lemma pprt_neg: "pprt (- x) = - nprt x"
proof -
  have "sup (- x) 0 = sup (- x) (- 0)"
    by (simp only: minus_zero)
  also have "\ = - inf x 0"
    by (simp only: neg_inf_eq_sup)
  finally have "sup (- x) 0 = - inf x 0" .
  then show ?thesis
    by (simp only: pprt_def nprt_def)
qed

lemma nprt_neg: "nprt (- x) = - pprt x"
proof -
  from pprt_neg have "pprt (- (- x)) = - nprt (- x)" .
  then have "pprt x = - nprt (- x)" by simp
  then show ?thesis by simp
qed

lemma prts: "a = pprt a + nprt a"
  by (simp add: pprt_def nprt_def flip: add_eq_inf_sup)

lemma zero_le_pprt[simp]: "0 \ pprt a"
  by (simp add: pprt_def)

lemma nprt_le_zero[simp]: "nprt a \ 0"
  by (simp add: nprt_def)

lemma le_eq_neg: "a \ - b \ a + b \ 0"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  show ?rhs
    by (rule add_le_imp_le_right[of _ "uminus b" _]) (simp add: add.assoc \<open>?lhs\<close>)
next
  assume ?rhs
  show ?lhs
    by (rule add_le_imp_le_right[of _ "b" _]) (simp add: \<open>?rhs\<close>)
qed

lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)

lemma pprt_eq_id [simp, no_atp]: "0 \ x \ pprt x = x"
  by (simp add: pprt_def sup_absorb1)

lemma nprt_eq_id [simp, no_atp]: "x \ 0 \ nprt x = x"
  by (simp add: nprt_def inf_absorb1)

lemma pprt_eq_0 [simp, no_atp]: "x \ 0 \ pprt x = 0"
  by (simp add: pprt_def sup_absorb2)

lemma nprt_eq_0 [simp, no_atp]: "0 \ x \ nprt x = 0"
  by (simp add: nprt_def inf_absorb2)

lemma sup_0_imp_0:
  assumes "sup a (- a) = 0"
  shows "a = 0"
proof -
  have pos: "0 \ a" if "sup a (- a) = 0" for a :: 'a
  proof -
    from that have "sup a (- a) + a = a"
      by simp
    then have "sup (a + a) 0 = a"
      by (simp add: add_sup_distrib_right)
    then have "sup (a + a) 0 \ a"
      by simp
    then show ?thesis
      by (blast intro: order_trans inf_sup_ord)
  qed
  from assms have **: "sup (-a) (-(-a)) = 0"
    by (simp add: sup_commute)
  from pos[OF assms] pos[OF **] show "a = 0"
    by simp
qed

lemma inf_0_imp_0: "inf a (- a) = 0 \ a = 0"
  by (metis local.neg_0_equal_iff_equal neg_inf_eq_sup sup_0_imp_0)

lemma inf_0_eq_0 [simp]: "inf a (- a) = 0 \ a = 0"
  by (metis inf_0_imp_0 inf.idem minus_zero)

lemma sup_0_eq_0 [simp]: "sup a (- a) = 0 \ a = 0"
  by (metis minus_zero sup.idem sup_0_imp_0)

lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \ a + a \ 0 \ a"
  (is "?lhs \ ?rhs")
proof
  show ?rhs if ?lhs
  proof -
    from that have a: "inf (a + a) 0 = 0"
      by (simp add: inf_commute inf_absorb1)
    have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l = _")
      by (simp add: add_sup_inf_distribs inf_aci)
    then have "?l = 0 + inf a 0"
      by (simp add: a, simp add: inf_commute)
    then have "inf a 0 = 0"
      by (simp only: add_right_cancel)
    then show ?thesis
      unfolding le_iff_inf by (simp add: inf_commute)
  qed
  show ?lhs if ?rhs
    by (simp add: add_mono[OF that that, simplified])
qed

lemma double_zero [simp]: "a + a = 0 \ a = 0"
  using add_nonneg_eq_0_iff order.eq_iff by auto

lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \ 0 < a"
  by (meson le_less_trans less_add_same_cancel2 less_le_not_le
      zero_le_double_add_iff_zero_le_single_add)

lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a \ 0 \ a \ 0"
proof -
  have "a + a \ 0 \ 0 \ - (a + a)"
    by (subst le_minus_iff) simp
  moreover have "\ \ a \ 0"
    by (simp only: minus_add_distrib zero_le_double_add_iff_zero_le_single_add) simp
  ultimately show ?thesis
    by blast
qed

lemma double_add_less_zero_iff_single_less_zero [simp]: "a + a < 0 \ a < 0"
proof -
  have "a + a < 0 \ 0 < - (a + a)"
    by (subst less_minus_iff) simp
  moreover have "\ \ a < 0"
    by (simp only: minus_add_distrib zero_less_double_add_iff_zero_less_single_add) simp
  ultimately show ?thesis
    by blast
qed

declare neg_inf_eq_sup [simp]
  and neg_sup_eq_inf [simp]
  and diff_inf_eq_sup [simp]
  and diff_sup_eq_inf [simp]

lemma le_minus_self_iff: "a \ - a \ a \ 0"
proof -
  from add_le_cancel_left [of "uminus a" "plus a a" zero]
  have "a \ - a \ a + a \ 0"
    by (simp flip: add.assoc)
  then show ?thesis
    by simp
qed

lemma minus_le_self_iff: "- a \ a \ 0 \ a"
proof -
  have "- a \ a \ 0 \ a + a"
    using add_le_cancel_left [of "uminus a" zero "plus a a"]
    by (simp flip: add.assoc)
  then show ?thesis
    by simp
qed

lemma zero_le_iff_zero_nprt: "0 \ a \ nprt a = 0"
  unfolding le_iff_inf by (simp add: nprt_def inf_commute)

lemma le_zero_iff_zero_pprt: "a \ 0 \ pprt a = 0"
  unfolding le_iff_sup by (simp add: pprt_def sup_commute)

lemma le_zero_iff_pprt_id: "0 \ a \ pprt a = a"
  unfolding le_iff_sup by (simp add: pprt_def sup_commute)

lemma zero_le_iff_nprt_id: "a \ 0 \ nprt a = a"
  unfolding le_iff_inf by (simp add: nprt_def inf_commute)

lemma pprt_mono [simp, no_atp]: "a \ b \ pprt a \ pprt b"
  unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a])

lemma nprt_mono [simp, no_atp]: "a \ b \ nprt a \ nprt b"
  unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a])

end

lemmas add_sup_inf_distribs =
  add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left

class lattice_ab_group_add_abs = lattice_ab_group_add + abs +
  assumes abs_lattice: "\a\ = sup a (- a)"
begin

lemma abs_prts: "\a\ = pprt a - nprt a"
proof -
  have "0 \ \a\"
  proof -
    have a: "a \ \a\" and b: "- a \ \a\"
      by (auto simp add: abs_lattice)
    show ?thesis
      by (rule add_mono [OF a b, simplified])
  qed
  then have "0 \ sup a (- a)"
    unfolding abs_lattice .
  then have "sup (sup a (- a)) 0 = sup a (- a)"
    by (rule sup_absorb1)
  then show ?thesis
    by (simp add: add_sup_inf_distribs ac_simps pprt_def nprt_def abs_lattice)
qed

subclass ordered_ab_group_add_abs
proof
  have abs_ge_zero [simp]: "0 \ \a\" for a
  proof -
    have a: "a \ \a\" and b: "- a \ \a\"
      by (auto simp add: abs_lattice)
    show "0 \ \a\"
      by (rule add_mono [OF a b, simplified])
  qed
  have abs_leI: "a \ b \ - a \ b \ \a\ \ b" for a b
    by (simp add: abs_lattice le_supI)
  fix a b
  show "0 \ \a\"
    by simp
  show "a \ \a\"
    by (auto simp add: abs_lattice)
  show "\-a\ = \a\"
    by (simp add: abs_lattice sup_commute)
  show "- a \ b \ \a\ \ b" if "a \ b"
    using that by (rule abs_leI)
  show "\a + b\ \ \a\ + \b\"
  proof -
    have g: "\a\ + \b\ = sup (a + b) (sup (- a - b) (sup (- a + b) (a + (- b))))"
      (is "_ = sup ?m ?n")
      by (simp add: abs_lattice add_sup_inf_distribs ac_simps)
    have a: "a + b \ sup ?m ?n"
      by simp
    have b: "- a - b \ ?n"
      by simp
    have c: "?n \ sup ?m ?n"
      by simp
    from b c have d: "- a - b \ sup ?m ?n"
      by (rule order_trans)
    have e: "- a - b = - (a + b)"
      by simp
    from a d e have "\a + b\ \ sup ?m ?n"
      by (metis abs_leI)
    with g[symmetric] show ?thesis by simp
  qed
qed

end

lemma sup_eq_if:
  fixes a :: "'a::{lattice_ab_group_add,linorder}"
  shows "sup a (- a) = (if a < 0 then - a else a)"
  using add_le_cancel_right [of a a "- a", symmetric, simplified]
    and add_le_cancel_right [of "-a" a a, symmetric, simplified]
  by (auto simp: sup_max max.absorb1 max.absorb2)

lemma abs_if_lattice:
  fixes a :: "'a::{lattice_ab_group_add_abs,linorder}"
  shows "\a\ = (if a < 0 then - a else a)"
  by auto

lemma estimate_by_abs:
  fixes a b c :: "'a::lattice_ab_group_add_abs"
  assumes "a + b \ c"
  shows "a \ c + \b\"
proof -
  from assms have "a \ c + (- b)"
    by (simp add: algebra_simps)
  have "- b \ \b\"
    by (rule abs_ge_minus_self)
  then have "c + (- b) \ c + \b\"
    by (rule add_left_mono)
  with \<open>a \<le> c + (- b)\<close> show ?thesis
    by (rule order_trans)
qed

class lattice_ring = ordered_ring + lattice_ab_group_add_abs
begin

subclass semilattice_inf_ab_group_add ..
subclass semilattice_sup_ab_group_add ..

end

lemma abs_le_mult:
  fixes a b :: "'a::lattice_ring"
  shows "\a * b\ \ \a\ * \b\"
proof -
  let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
  let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  have a: "\a\ * \b\ = ?x"
    by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
  have bh: "u = a \ v = b \
            u * v = pprt a * pprt b + pprt a * nprt b +
                    nprt a * pprt b + nprt a * nprt b" for u v :: 'a
    by (metis add.commute combine_common_factor distrib_left prts)
  note b = this[OF refl[of a] refl[of b]]
  have xy: "- ?x \ ?y"
    apply simp
    by (meson add_increasing2 diff_le_eq neg_le_0_iff_le nprt_le_zero order.trans split_mult_pos_le zero_le_pprt)
  have yx: "?y \ ?x"
    apply simp
    by (metis add_decreasing2 diff_0 diff_mono diff_zero mult_nonpos_nonneg mult_right_mono_neg mult_zero_left nprt_le_zero zero_le_pprt)
  show ?thesis
  proof (rule abs_leI)
    show "a * b \ \a\ * \b\"
      by (simp only: a b yx)
    show "- (a * b) \ \a\ * \b\"
      by (metis a bh minus_le_iff xy)
  qed
qed

instance lattice_ring \<subseteq> ordered_ring_abs
proof
  fix a b :: "'a::lattice_ring"
  assume a: "(0 \ a \ a \ 0) \ (0 \ b \ b \ 0)"
  show "\a * b\ = \a\ * \b\"
  proof -
    have s: "(0 \ a * b) \ (a * b \ 0)"
      by (metis a split_mult_neg_le split_mult_pos_le)
    have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
      by (simp flip: prts)
    show ?thesis
    proof (cases "0 \ a * b")
      case True
      then show ?thesis
        using a split_mult_neg_le by fastforce
    next
      case False
      with s have "a * b \ 0"
        by simp
      then show ?thesis
        using a split_mult_pos_le by fastforce
    qed
  qed
qed

lemma mult_le_prts:
  fixes a b :: "'a::lattice_ring"
  assumes "a1 \ a"
    and "a \ a2"
    and "b1 \ b"
    and "b \ b2"
  shows "a * b \
    pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
proof -
  have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
    by (subst prts[symmetric])+ simp
  then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
    by (simp add: algebra_simps)
  moreover have "pprt a * pprt b \ pprt a2 * pprt b2"
    by (simp_all add: assms mult_mono)
  moreover have "pprt a * nprt b \ pprt a1 * nprt b2"
  proof -
    have "pprt a * nprt b \ pprt a * nprt b2"
      by (simp add: mult_left_mono assms)
    moreover have "pprt a * nprt b2 \ pprt a1 * nprt b2"
      by (simp add: mult_right_mono_neg assms)
    ultimately show ?thesis
      by simp
  qed
  moreover have "nprt a * pprt b \ nprt a2 * pprt b1"
  proof -
    have "nprt a * pprt b \ nprt a2 * pprt b"
      by (simp add: mult_right_mono assms)
    moreover have "nprt a2 * pprt b \ nprt a2 * pprt b1"
      by (simp add: mult_left_mono_neg assms)
    ultimately show ?thesis
      by simp
  qed
  moreover have "nprt a * nprt b \ nprt a1 * nprt b1"
  proof -
    have "nprt a * nprt b \ nprt a * nprt b1"
      by (simp add: mult_left_mono_neg assms)
    moreover have "nprt a * nprt b1 \ nprt a1 * nprt b1"
      by (simp add: mult_right_mono_neg assms)
    ultimately show ?thesis
      by simp
  qed
  ultimately show ?thesis
    by - (rule add_mono | simp)+
qed

lemma mult_ge_prts:
  fixes a b :: "'a::lattice_ring"
  assumes "a1 \ a"
    and "a \ a2"
    and "b1 \ b"
    and "b \ b2"
  shows "a * b \
    nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
proof -
  from assms have a1: "- a2 \ -a"
    by auto
  from assms have a2: "- a \ -a1"
    by auto
  from mult_le_prts[of "- a2" "- a" "- a1" "b1" b "b2",
    OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg]
  have le: "- (a * b) \
    - nprt a1 * pprt b2 + - nprt a2 * nprt b2 +
    - pprt a1 * pprt b1 + - pprt a2 * nprt b1"
    by simp
  then have "- (- nprt a1 * pprt b2 + - nprt a2 * nprt b2 +
      - pprt a1 * pprt b1 + - pprt a2 * nprt b1) \<le> a * b"
    by (simp only: minus_le_iff)
  then show ?thesis
    by (simp add: algebra_simps)
qed

instance int :: lattice_ring
proof
  show "\k\ = sup k (- k)" for k :: int
    by (auto simp add: sup_int_def)
qed

instance real :: lattice_ring
proof
  show "\a\ = sup a (- a)" for a :: real
    by (auto simp add: sup_real_def)
qed

end

quality98%

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