Theory 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