Theory LatticeProperties.Lattice_Ordered_Group

section‹Lattice Orderd Groups›

(*
    Author: Viorel Preoteasa
*)

theory Lattice_Ordered_Group
imports Modular_Distrib_Lattice
begin

text‹
This theory introduces lattice ordered groups \<^cite>‹"birkhoff:1942"› 
and proves some results about them. The most important result is 
that a lattice ordered group is also a distributive lattice.
›

class lgroup = group_add + lattice +
assumes add_order_preserving: "a ≤ b ⟹ u + a + v ≤ u + b + v"
begin

lemma add_order_preserving_left: "a ≤ b ⟹ u + a ≤ u + b"
  apply (cut_tac a = a and b = b and u = u and v = 0 in add_order_preserving)
  by simp_all

lemma add_order_preserving_right: "a ≤ b ⟹ a + v ≤ b + v"
  apply (cut_tac a = a and b = b and u = 0 and v = v in add_order_preserving)
  by simp_all


lemma minus_order: "-a ≤ -b ⟹ b ≤ a"
  apply (cut_tac a = "-a" and b = "-b" and u = a and v = b in add_order_preserving)
  by simp_all


lemma right_move_to_left: "a + - c ≤ b ⟹ a ≤ b + c"  
  apply (drule_tac v = "c" in add_order_preserving_right)
  by (simp add: add.assoc)
 
lemma right_move_to_right: "a ≤ b + -c ⟹ a + c ≤ b"  
  apply (drule_tac v = "c" in add_order_preserving_right)
  by (simp add: add.assoc)
 

lemma [simp]: "(a ⊓ b) + c = (a + c) ⊓ (b + c)"
  apply (rule order.antisym)
  apply simp
  apply safe
  apply (rule add_order_preserving_right)
  apply simp
  apply (rule add_order_preserving_right)
  apply simp
  apply (rule right_move_to_left)
  apply simp
  apply safe
  apply (simp_all only: diff_conv_add_uminus)
  apply (rule right_move_to_right)
  apply simp
  apply (rule right_move_to_right)
  by simp

lemma [simp]: "(a ⊓ b) - c = (a - c) ⊓ (b - c)"
  by (simp add: diff_conv_add_uminus del: add_uminus_conv_diff)


lemma left_move_to_left: "-c + a ≤ b ⟹ a ≤ c + b"  
  apply (drule_tac u = "c" in add_order_preserving_left)
  by (simp add: add.assoc [THEN sym])
 
lemma left_move_to_right: "a ≤ - c + b ⟹ c + a ≤ b"  
  apply (drule_tac u = "c" in add_order_preserving_left)
  by (simp add: add.assoc [THEN sym])

lemma [simp]: "c + (a ⊓ b) = (c + a) ⊓ (c + b)"
  apply (rule order.antisym)
  apply simp
  apply safe
  apply (rule add_order_preserving_left)
  apply simp
  apply (rule add_order_preserving_left)
  apply simp
  apply (rule left_move_to_left)
  apply simp
  apply safe
  apply (rule left_move_to_right)
  apply simp
  apply (rule left_move_to_right)
  by simp

lemma [simp]: "- (a ⊓ b) = (- a) ⊔ (- b)"
  apply (rule order.antisym)
  apply (rule minus_order)
  apply simp
  apply safe
  apply (rule minus_order)
  apply simp
  apply (rule minus_order)
  apply simp
  apply simp
  apply safe
  apply (rule minus_order)
  apply simp
  apply (rule minus_order)
  by simp

lemma [simp]: "(a ⊔ b) + c = (a + c) ⊔ (b + c)"
  apply (rule order.antisym)
  apply (rule right_move_to_right)
  apply simp
  apply safe
  apply (simp_all only: diff_conv_add_uminus)
  apply (rule right_move_to_left)
  apply simp
  apply (rule right_move_to_left)
  apply simp
  apply simp
  apply safe
  apply (rule add_order_preserving_right)
  apply simp
  apply (rule add_order_preserving_right)
  by simp
  
lemma [simp]: "c + (a ⊔ b) = (c + a) ⊔ (c + b)"
  apply (rule order.antisym)
  apply (rule left_move_to_right)
  apply simp
  apply safe
  apply (rule left_move_to_left)
  apply simp
  apply (rule left_move_to_left)
  apply simp
  apply simp
  apply safe
  apply (rule add_order_preserving_left)
  apply simp
  apply (rule add_order_preserving_left)
  by simp

lemma [simp]: "c - (a ⊓ b) = (c - a) ⊔ (c - b)"
  by (simp add: diff_conv_add_uminus del: add_uminus_conv_diff)

lemma [simp]: "(a ⊔ b) - c = (a - c) ⊔  (b - c)"
  by (simp add: diff_conv_add_uminus del: add_uminus_conv_diff)

lemma [simp]: "- (a ⊔ b) = (- a) ⊓ (- b)"
  apply (rule order.antisym)
  apply simp
  apply safe
  apply (rule minus_order)
  apply simp
  apply (rule minus_order)
  apply simp
  apply (rule minus_order)
  by simp
  
lemma [simp]: "c - (a ⊔ b) = (c - a) ⊓ (c - b)"
  by (simp add: diff_conv_add_uminus del: add_uminus_conv_diff)
  
lemma add_pos: "0 ≤ a ⟹ b ≤ b + a"
  apply (cut_tac a = 0 and b = a and u = b and v = 0 in add_order_preserving)
  by simp_all

lemma add_pos_left: "0 ≤ a ⟹ b ≤ a + b"
  apply (rule right_move_to_left)
  by simp

lemma inf_sup: "a - (a ⊓ b) + b = a ⊔ b"
  by (simp add: add.assoc sup_commute)

lemma inf_sup_2: "b = (a ⊓ b) - a + (a ⊔ b)"
  apply (unfold inf_sup [THEN sym])
  proof -
    fix a b:: 'a
    have "b = (a ⊓ b) + (- a + a) + - (a ⊓ b) + b" by (simp only: right_minus left_minus add_0_right add_0_left)
    also have "… = (a ⊓ b) + - a + (a + - (a ⊓ b) + b)" by (unfold add.assoc, simp) 
    also have "… = (a ⊓ b) - a + (a - (a ⊓ b) + b)" by simp
    finally show "b = (a ⊓ b) - a + (a - (a ⊓ b) + b)" .
  qed


subclass inf_sup_eq_lattice
  proof
    fix x y z:: 'a
    assume A: "x ⊓ z = y ⊓ z"
    assume B: "x ⊔ z = y ⊔ z"
    have "x = (z ⊓ x) - z + (z ⊔ x)" by (rule inf_sup_2)
    also have "… = (z ⊓ y) - z + (z ⊔ y)" by (simp add: sup_commute inf_commute A B)
    also have "… = y" by (simp only: inf_sup_2 [THEN sym])
    finally show "x = y" .
  qed
end

end