Lattice Proofs

A key part of mathematics is proofs, on this site I would like to include proofs in a consistant way across all the topics, I am therefore using a program called Isabelle which is a proof assistant. More about this program on this page.

This is taken from Isabelle code (from this site) but I have not put the complete code here, just an outline.

In mathematics, a join-semilattice (or upper semilattice) is a partially ordered set that has a join (a least upper bound) for any nonempty finite subset. Dually, a meet-semilattice (or lower semilattice) is a partially ordered set which has a meet (or greatest lower bound) for any nonempty finite subset. Every join-semilattice is a meet-semilattice in the inverse order and vice versa.

Semilattices can also be defined algebraically: join and meet are associative, commutative, idempotent binary operations, and any such operation induces a partial order (and the respective inverse order) such that the result of the operation for any two elements is the least upper bound (or greatest lower bound) of the elements with respect to this partial order.

A lattice is a partially ordered set that is both a meet- and join-semilattice with respect to the same partial order. Algebraically, a lattice is a set with two associative, commutative idempotent binary operations linked by corresponding absorption laws.

Abstract Semilattice

A lattice has both a join and a meet operation but a semilattice has only one of these operatiors.

Join and meet are associative, commutative, idempotent binary operations.

Idempotent means:

From which we can derive:

There is also a right-hand version of these.

Absorptive means:

This is represented in Isabelle code (from this site) by starting with an abelian group, which gives associative and commutitive binary operation (as discussed on this page) and adds the idempotent axiom like this:

So the 'f' can represent either '/\' or '\/' depending on wheter it is an infimum (meet) or supremum (join) semilattice.

A lattice is then built from one of each.

locale semilattice = abel_semigroup +
  assumes idem [simp]: "f a a = a"
begin

lemma left_idem [simp]: "f a (f a b) = f a b"
by (simp add: assoc [symmetric])

lemma right_idem [simp]: "f (f a b) b = f a b"
by (simp add: assoc)

end

Idempotent semigroup

class ab_semigroup_idem_mult = ab_semigroup_mult +
  assumes mult_idem: "x * x = x"

Semilattice

class inf =
  fixes inf :: "'a => 'a => 'a" (infixl "\" 70)

class sup = 
  fixes sup :: "'a => 'a => 'a" (infixl "\" 65)


subsection {* Concrete lattices *}

notation
  less_eq  (infix "\" 50) and
  less  (infix "\" 50)

class semilattice_inf =  order + inf +
  assumes inf_le1 [simp]: "x \ y \ x"
  and inf_le2 [simp]: "x \ y \ y"
  and inf_greatest: "x \ y ==> x \ z ==> x \ y \ z"

class semilattice_sup = order + sup +
  assumes sup_ge1 [simp]: "x \ x \ y"
  and sup_ge2 [simp]: "y \ x \ y"
  and sup_least: "y \ x ==> z \ x ==> y \ z \ x"
begin

Lattice

class lattice = semilattice_inf + semilattice_sup

Dual lattice

text {* Dual lattice *}

lemma dual_semilattice:
  "class.semilattice_inf sup greater_eq greater"
by (rule class.semilattice_inf.intro, rule dual_order)
  (unfold_locales, simp_all add: sup_least)

end

Introduction and Elimination Rules

infimum also known as meet (a /\ b) or greatest lower bound.

context semilattice_inf
begin

lemma le_infI1:
  "a \ x ==> a \ b \ x"
  by (rule order_trans) auto

lemma le_infI2:
  "b \ x ==> a \ b \ x"
  by (rule order_trans) auto

lemma le_infI: "x \ a ==> x \ b ==> x \ a \ b"
  by (rule inf_greatest) (* FIXME: duplicate lemma *)

lemma le_infE: "x \ a \ b ==> (x \ a ==> x \ b ==> P) ==> P"
  by (blast intro: order_trans inf_le1 inf_le2)

lemma le_inf_iff [simp]:
  "x \ y \ z <-> x \ y ∧ x \ z"
  by (blast intro: le_infI elim: le_infE)

lemma le_iff_inf:
  "x \ y <-> x \ y = x"
  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])

lemma inf_mono: "a \ c ==> b \ d ==> a \ b \ c \ d"
  by (fast intro: inf_greatest le_infI1 le_infI2)

lemma mono_inf:
  fixes f :: "'a => 'b::semilattice_inf"
  shows "mono f ==> f (A \ B) \ f A \ f B"
  by (auto simp add: mono_def intro: Lattices.inf_greatest)

end

supremum also known as the join (a \/ b) or least upper bound.

context semilattice_sup
begin

lemma le_supI1:
  "x \ a ==> x \ a \ b"
  by (rule order_trans) auto

lemma le_supI2:
  "x \ b ==> x \ a \ b"
  by (rule order_trans) auto 

lemma le_supI:
  "a \ x ==> b \ x ==> a \ b \ x"
  by (rule sup_least) (* FIXME: duplicate lemma *)

lemma le_supE:
  "a \ b \ x ==> (a \ x ==> b \ x ==> P) ==> P"
  by (blast intro: order_trans sup_ge1 sup_ge2)

lemma le_sup_iff [simp]:
  "x \ y \ z <-> x \ z ∧ y \ z"
  by (blast intro: le_supI elim: le_supE)

lemma le_iff_sup:
  "x \ y <-> x \ y = y"
  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])

lemma sup_mono: "a \ c ==> b \ d ==> a \ b \ c \ d"
  by (fast intro: sup_least le_supI1 le_supI2)

lemma mono_sup:
  fixes f :: "'a => 'b::semilattice_sup"
  shows "mono f ==> f A \ f B \ f (A \ B)"
  by (auto simp add: mono_def intro: Lattices.sup_least)

end

Equational laws

 











subsubsection {* Equational laws *}

sublocale semilattice_inf < inf!: semilattice inf
proof
  fix a b c
  show "(a \ b) \ c = a \ (b \ c)"
    by (rule antisym) (auto intro: le_infI1 le_infI2)
  show "a \ b = b \ a"
    by (rule antisym) auto
  show "a \ a = a"
    by (rule antisym) auto
qed

context semilattice_inf
begin

lemma inf_assoc: "(x \ y) \ z = x \ (y \ z)"
  by (fact inf.assoc)

lemma inf_commute: "(x \ y) = (y \ x)"
  by (fact inf.commute)

lemma inf_left_commute: "x \ (y \ z) = y \ (x \ z)"
  by (fact inf.left_commute)

lemma inf_idem: "x \ x = x"
  by (fact inf.idem) (* already simp *)

lemma inf_left_idem: "x \ (x \ y) = x \ y"
  by (fact inf.left_idem) (* already simp *)

lemma inf_right_idem: "(x \ y) \ y = x \ y"
  by (fact inf.right_idem) (* already simp *)

lemma inf_absorb1: "x \ y ==> x \ y = x"
  by (rule antisym) auto

lemma inf_absorb2: "y \ x ==> x \ y = y"
  by (rule antisym) auto
 
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem

end

sublocale semilattice_sup < sup!: semilattice sup
proof
  fix a b c
  show "(a \ b) \ c = a \ (b \ c)"
    by (rule antisym) (auto intro: le_supI1 le_supI2)
  show "a \ b = b \ a"
    by (rule antisym) auto
  show "a \ a = a"
    by (rule antisym) auto
qed

context semilattice_sup
begin

lemma sup_assoc: "(x \ y) \ z = x \ (y \ z)"
  by (fact sup.assoc)

lemma sup_commute: "(x \ y) = (y \ x)"
  by (fact sup.commute)

lemma sup_left_commute: "x \ (y \ z) = y \ (x \ z)"
  by (fact sup.left_commute)

lemma sup_idem: "x \ x = x"
  by (fact sup.idem) (* already simp *)

lemma sup_left_idem [simp]: "x \ (x \ y) = x \ y"
  by (fact sup.left_idem)

lemma sup_absorb1: "y \ x ==> x \ y = x"
  by (rule antisym) auto

lemma sup_absorb2: "x \ y ==> x \ y = y"
  by (rule antisym) auto

lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem

end

context lattice
begin

lemma dual_lattice:
  "class.lattice sup (op ≥) (op >) inf"
  by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
    (unfold_locales, auto)

lemma inf_sup_absorb [simp]: "x \ (x \ y) = x"
  by (blast intro: antisym inf_le1 inf_greatest sup_ge1)

lemma sup_inf_absorb [simp]: "x \ (x \ y) = x"
  by (blast intro: antisym sup_ge1 sup_least inf_le1)

lemmas inf_sup_aci = inf_aci sup_aci

lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2

text{* Towards distributivity *}

lemma distrib_sup_le: "x \ (y \ z) \ (x \ y) \ (x \ z)"
  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)

lemma distrib_inf_le: "(x \ y) \ (x \ z) \ x \ (y \ z)"
  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)

text{* If you have one of them, you have them all. *}

lemma distrib_imp1:
assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)"
shows "x \ (y \ z) = (x \ y) \ (x \ z)"
proof-
  have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" by simp
  also have "… = x \ (z \ (x \ y))"
    by (simp add: D inf_commute sup_assoc del: sup_inf_absorb)
  also have "… = ((x \ y) \ x) \ ((x \ y) \ z)"
    by(simp add: inf_commute)
  also have "… = (x \ y) \ (x \ z)" by(simp add:D)
  finally show ?thesis .
qed

lemma distrib_imp2:
assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)"
shows "x \ (y \ z) = (x \ y) \ (x \ z)"
proof-
  have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" by simp
  also have "… = x \ (z \ (x \ y))"
    by (simp add: D sup_commute inf_assoc del: inf_sup_absorb)
  also have "… = ((x \ y) \ x) \ ((x \ y) \ z)"
    by(simp add: sup_commute)
  also have "… = (x \ y) \ (x \ z)" by(simp add:D)
  finally show ?thesis .
qed

end

subsubsection {* Strict order *}

context semilattice_inf
begin

lemma less_infI1:
  "a \ x ==> a \ b \ x"
  by (auto simp add: less_le inf_absorb1 intro: le_infI1)

lemma less_infI2:
  "b \ x ==> a \ b \ x"
  by (auto simp add: less_le inf_absorb2 intro: le_infI2)

end

context semilattice_sup
begin

lemma less_supI1:
  "x \ a ==> x \ a \ b"
  using dual_semilattice
  by (rule semilattice_inf.less_infI1)

lemma less_supI2:
  "x \ b ==> x \ a \ b"
  using dual_semilattice
  by (rule semilattice_inf.less_infI2)

end


subsection {* Distributive lattices *}

class distrib_lattice = lattice +
  assumes sup_inf_distrib1: "x \ (y \ z) = (x \ y) \ (x \ z)"

context distrib_lattice
begin

lemma sup_inf_distrib2:
  "(y \ z) \ x = (y \ x) \ (z \ x)"
  by (simp add: sup_commute sup_inf_distrib1)

lemma inf_sup_distrib1:
  "x \ (y \ z) = (x \ y) \ (x \ z)"
  by (rule distrib_imp2 [OF sup_inf_distrib1])

lemma inf_sup_distrib2:
  "(y \ z) \ x = (y \ x) \ (z \ x)"
  by (simp add: inf_commute inf_sup_distrib1)

lemma dual_distrib_lattice:
  "class.distrib_lattice sup (op ≥) (op >) inf"
  by (rule class.distrib_lattice.intro, rule dual_lattice)
    (unfold_locales, fact inf_sup_distrib1)

lemmas sup_inf_distrib =
  sup_inf_distrib1 sup_inf_distrib2

lemmas inf_sup_distrib =
  inf_sup_distrib1 inf_sup_distrib2

lemmas distrib =
  sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2

end


subsection {* Bounded lattices and boolean algebras *}

class bounded_lattice_bot = lattice + bot
begin

lemma inf_bot_left [simp]:
  "⊥ \ x = ⊥"
  by (rule inf_absorb1) simp

lemma inf_bot_right [simp]:
  "x \ ⊥ = ⊥"
  by (rule inf_absorb2) simp

lemma sup_bot_left [simp]:
  "⊥ \ x = x"
  by (rule sup_absorb2) simp

lemma sup_bot_right [simp]:
  "x \ ⊥ = x"
  by (rule sup_absorb1) simp

lemma sup_eq_bot_iff [simp]:
  "x \ y = ⊥ <-> x = ⊥ ∧ y = ⊥"
  by (simp add: eq_iff)

end

class bounded_lattice_top = lattice + top
begin

lemma sup_top_left [simp]:
  "\ \ x = \"
  by (rule sup_absorb1) simp

lemma sup_top_right [simp]:
  "x \ \ = \"
  by (rule sup_absorb2) simp

lemma inf_top_left [simp]:
  "\ \ x = x"
  by (rule inf_absorb2) simp

lemma inf_top_right [simp]:
  "x \ \ = x"
  by (rule inf_absorb1) simp

lemma inf_eq_top_iff [simp]:
  "x \ y = \ <-> x = \ ∧ y = \"
  by (simp add: eq_iff)

end

class bounded_lattice = bounded_lattice_bot + bounded_lattice_top
begin

lemma dual_bounded_lattice:
  "class.bounded_lattice sup greater_eq greater inf \ ⊥"
  by unfold_locales (auto simp add: less_le_not_le)

end

class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
  assumes inf_compl_bot: "x \ - x = ⊥"
    and sup_compl_top: "x \ - x = \"
  assumes diff_eq: "x - y = x \ - y"
begin

lemma dual_boolean_algebra:
  "class.boolean_algebra (λx y. x \ - y) uminus sup greater_eq greater inf \ ⊥"
  by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)

lemma compl_inf_bot [simp]:
  "- x \ x = ⊥"
  by (simp add: inf_commute inf_compl_bot)

lemma compl_sup_top [simp]:
  "- x \ x = \"
  by (simp add: sup_commute sup_compl_top)

lemma compl_unique:
  assumes "x \ y = ⊥"
    and "x \ y = \"
  shows "- x = y"
proof -
  have "(x \ - x) \ (- x \ y) = (x \ y) \ (- x \ y)"
    using inf_compl_bot assms(1) by simp
  then have "(- x \ x) \ (- x \ y) = (y \ x) \ (y \ - x)"
    by (simp add: inf_commute)
  then have "- x \ (x \ y) = y \ (x \ - x)"
    by (simp add: inf_sup_distrib1)
  then have "- x \ \ = y \ \"
    using sup_compl_top assms(2) by simp
  then show "- x = y" by simp
qed

lemma double_compl [simp]:
  "- (- x) = x"
  using compl_inf_bot compl_sup_top by (rule compl_unique)

lemma compl_eq_compl_iff [simp]:
  "- x = - y <-> x = y"
proof
  assume "- x = - y"
  then have "- (- x) = - (- y)" by (rule arg_cong)
  then show "x = y" by simp
next
  assume "x = y"
  then show "- x = - y" by simp
qed

lemma compl_bot_eq [simp]:
  "- ⊥ = \"
proof -
  from sup_compl_top have "⊥ \ - ⊥ = \" .
  then show ?thesis by simp
qed

lemma compl_top_eq [simp]:
  "- \ = ⊥"
proof -
  from inf_compl_bot have "\ \ - \ = ⊥" .
  then show ?thesis by simp
qed

lemma compl_inf [simp]:
  "- (x \ y) = - x \ - y"
proof (rule compl_unique)
  have "(x \ y) \ (- x \ - y) = (y \ (x \ - x)) \ (x \ (y \ - y))"
    by (simp only: inf_sup_distrib inf_aci)
  then show "(x \ y) \ (- x \ - y) = ⊥"
    by (simp add: inf_compl_bot)
next
  have "(x \ y) \ (- x \ - y) = (- y \ (x \ - x)) \ (- x \ (y \ - y))"
    by (simp only: sup_inf_distrib sup_aci)
  then show "(x \ y) \ (- x \ - y) = \"
    by (simp add: sup_compl_top)
qed

lemma compl_sup [simp]:
  "- (x \ y) = - x \ - y"
  using dual_boolean_algebra
  by (rule boolean_algebra.compl_inf)

lemma compl_mono:
  "x \ y ==> - y \ - x"
proof -
  assume "x \ y"
  then have "x \ y = y" by (simp only: le_iff_sup)
  then have "- (x \ y) = - y" by simp
  then have "- x \ - y = - y" by simp
  then have "- y \ - x = - y" by (simp only: inf_commute)
  then show "- y \ - x" by (simp only: le_iff_inf)
qed

lemma compl_le_compl_iff [simp]:
  "- x \ - y <-> y \ x"
  by (auto dest: compl_mono)

lemma compl_le_swap1:
  assumes "y \ - x" shows "x \ -y"
proof -
  from assms have "- (- x) \ - y" by (simp only: compl_le_compl_iff)
  then show ?thesis by simp
qed

lemma compl_le_swap2:
  assumes "- y \ x" shows "- x \ y"
proof -
  from assms have "- x \ - (- y)" by (simp only: compl_le_compl_iff)
  then show ?thesis by simp
qed

lemma compl_less_compl_iff: (* TODO: declare [simp] ? *)
  "- x \ - y <-> y \ x"
  by (auto simp add: less_le)

lemma compl_less_swap1:
  assumes "y \ - x" shows "x \ - y"
proof -
  from assms have "- (- x) \ - y" by (simp only: compl_less_compl_iff)
  then show ?thesis by simp
qed

lemma compl_less_swap2:
  assumes "- y \ x" shows "- x \ y"
proof -
  from assms have "- x \ - (- y)" by (simp only: compl_less_compl_iff)
  then show ?thesis by simp
qed

end


subsection {* Uniqueness of inf and sup *}

lemma (in semilattice_inf) inf_unique:
  fixes f (infixl "\" 70)
  assumes le1: "!!x y. x \ y \ x" and le2: "!!x y. x \ y \ y"
  and greatest: "!!x y z. x \ y ==> x \ z ==> x \ y \ z"
  shows "x \ y = x \ y"
proof (rule antisym)
  show "x \ y \ x \ y" by (rule le_infI) (rule le1, rule le2)
next
  have leI: "!!x y z. x \ y ==> x \ z ==> x \ y \ z" by (blast intro: greatest)
  show "x \ y \ x \ y" by (rule leI) simp_all
qed

lemma (in semilattice_sup) sup_unique:
  fixes f (infixl "∇" 70)
  assumes ge1 [simp]: "!!x y. x \ x ∇ y" and ge2: "!!x y. y \ x ∇ y"
  and least: "!!x y z. y \ x ==> z \ x ==> y ∇ z \ x"
  shows "x \ y = x ∇ y"
proof (rule antisym)
  show "x \ y \ x ∇ y" by (rule le_supI) (rule ge1, rule ge2)
next
  have leI: "!!x y z. x \ z ==> y \ z ==> x ∇ y \ z" by (blast intro: least)
  show "x ∇ y \ x \ y" by (rule leI) simp_all
qed


subsection {* @{const min}/@{const max} on linear orders as
  special case of @{const inf}/@{const sup} *}

sublocale linorder < min_max!: distrib_lattice min less_eq less max
proof
  fix x y z
  show "max x (min y z) = min (max x y) (max x z)"
    by (auto simp add: min_def max_def)
qed (auto simp add: min_def max_def not_le less_imp_le)

lemma inf_min: "inf = (min :: 'a::{semilattice_inf, linorder} => 'a => 'a)"
  by (rule ext)+ (auto intro: antisym)

lemma sup_max: "sup = (max :: 'a::{semilattice_sup, linorder} => 'a => 'a)"
  by (rule ext)+ (auto intro: antisym)

lemmas le_maxI1 = min_max.sup_ge1
lemmas le_maxI2 = min_max.sup_ge2
 
lemmas min_ac = min_max.inf_assoc min_max.inf_commute
  min_max.inf.left_commute

lemmas max_ac = min_max.sup_assoc min_max.sup_commute
  min_max.sup.left_commute


subsection {* Lattice on @{typ bool} *}

instantiation bool :: boolean_algebra
begin

definition
  bool_Compl_def [simp]: "uminus = Not"

definition
  bool_diff_def [simp]: "A - B <-> A ∧ ¬ B"

definition
  [simp]: "P \ Q <-> P ∧ Q"

definition
  [simp]: "P \ Q <-> P ∨ Q"

instance proof
qed auto

end

lemma sup_boolI1:
  "P ==> P \ Q"
  by simp

lemma sup_boolI2:
  "Q ==> P \ Q"
  by simp

lemma sup_boolE:
  "P \ Q ==> (P ==> R) ==> (Q ==> R) ==> R"
  by auto


subsection {* Lattice on @{typ "_ => _"} *}

instantiation "fun" :: (type, lattice) lattice
begin

definition
  "f \ g = (λx. f x \ g x)"

lemma inf_apply [simp, code]:
  "(f \ g) x = f x \ g x"
  by (simp add: inf_fun_def)

definition
  "f \ g = (λx. f x \ g x)"

lemma sup_apply [simp, code]:
  "(f \ g) x = f x \ g x"
  by (simp add: sup_fun_def)

instance proof
qed (simp_all add: le_fun_def)

end

instance "fun" :: (type, distrib_lattice) distrib_lattice proof
qed (rule ext, simp add: sup_inf_distrib1)

instance "fun" :: (type, bounded_lattice) bounded_lattice ..

instantiation "fun" :: (type, uminus) uminus
begin

definition
  fun_Compl_def: "- A = (λx. - A x)"

lemma uminus_apply [simp, code]:
  "(- A) x = - (A x)"
  by (simp add: fun_Compl_def)

instance ..

end

instantiation "fun" :: (type, minus) minus
begin

definition
  fun_diff_def: "A - B = (λx. A x - B x)"

lemma minus_apply [simp, code]:
  "(A - B) x = A x - B x"
  by (simp add: fun_diff_def)

instance ..

end

instance "fun" :: (type, boolean_algebra) boolean_algebra proof
qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+


subsection {* Lattice on unary and binary predicates *}

lemma inf1I: "A x ==> B x ==> (A \ B) x"
  by (simp add: inf_fun_def)

lemma inf2I: "A x y ==> B x y ==> (A \ B) x y"
  by (simp add: inf_fun_def)

lemma inf1E: "(A \ B) x ==> (A x ==> B x ==> P) ==> P"
  by (simp add: inf_fun_def)

lemma inf2E: "(A \ B) x y ==> (A x y ==> B x y ==> P) ==> P"
  by (simp add: inf_fun_def)

lemma inf1D1: "(A \ B) x ==> A x"
  by (simp add: inf_fun_def)

lemma inf2D1: "(A \ B) x y ==> A x y"
  by (simp add: inf_fun_def)

lemma inf1D2: "(A \ B) x ==> B x"
  by (simp add: inf_fun_def)

lemma inf2D2: "(A \ B) x y ==> B x y"
  by (simp add: inf_fun_def)

lemma sup1I1: "A x ==> (A \ B) x"
  by (simp add: sup_fun_def)

lemma sup2I1: "A x y ==> (A \ B) x y"
  by (simp add: sup_fun_def)

lemma sup1I2: "B x ==> (A \ B) x"
  by (simp add: sup_fun_def)

lemma sup2I2: "B x y ==> (A \ B) x y"
  by (simp add: sup_fun_def)

lemma sup1E: "(A \ B) x ==> (A x ==> P) ==> (B x ==> P) ==> P"
  by (simp add: sup_fun_def) iprover

lemma sup2E: "(A \ B) x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
  by (simp add: sup_fun_def) iprover

text {*
  \medskip Classical introduction rule: no commitment to @{text A} vs
  @{text B}.
*}

lemma sup1CI: "(¬ B x ==> A x) ==> (A \ B) x"
  by (auto simp add: sup_fun_def)

lemma sup2CI: "(¬ B x y ==> A x y) ==> (A \ B) x y"
  by (auto simp add: sup_fun_def)


no_notation
  less_eq (infix "\" 50) and
  less (infix "\" 50)

end

 


metadata block
see also:

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

cover Modern Graph Theory (Graduate Texts in Mathematics, 184)

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2017 Martin John Baker - All rights reserved - privacy policy.