# HG changeset patch
# User haftmann
# Date 1265634401 -3600
# Node ID 7efe662e41b46b51477ffa5352c872664be24bb2
# Parent  108662d5051240fec0a5cceef30fd0b06fc1a565
separate library theory for type classes combining lattices with various algebraic structures

diff -r 108662d50512 -r 7efe662e41b4 NEWS
--- a/NEWS	Fri Feb 05 14:33:50 2010 +0100
+++ b/NEWS	Mon Feb 08 14:06:41 2010 +0100
@@ -12,7 +12,7 @@
 
 *** HOL ***
 
-* more consistent naming of type classes involving orderings (and lattices):
+* More consistent naming of type classes involving orderings (and lattices):
 
     lower_semilattice                   ~> semilattice_inf
     upper_semilattice                   ~> semilattice_sup
@@ -33,12 +33,6 @@
     pordered_ring_abs                   ~> ordered_ring_abs
     pordered_semiring                   ~> ordered_semiring
 
-    lordered_ab_group_add               ~> lattice_ab_group_add
-    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
-    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
-    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
-    lordered_ring                       ~> lattice_ring
-
     ordered_ab_group_add                ~> linordered_ab_group_add
     ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add
     ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add
@@ -58,6 +52,15 @@
     ordered_semiring_1_strict           ~> linordered_semiring_1_strict
     ordered_semiring_strict             ~> linordered_semiring_strict
 
+  The following slightly odd type classes have been moved to
+  a separate theory Library/Lattice_Algebras.thy:
+
+    lordered_ab_group_add               ~> lattice_ab_group_add
+    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
+    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
+    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
+    lordered_ring                       ~> lattice_ring
+
 INCOMPATIBILITY.
 
 * new theory Algebras.thy contains generic algebraic structures and
diff -r 108662d50512 -r 7efe662e41b4 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/Int.thy	Mon Feb 08 14:06:41 2010 +0100
@@ -256,13 +256,6 @@
     by (simp only: zsgn_def)
 qed
 
-instance int :: lattice_ring
-proof  
-  fix k :: int
-  show "abs k = sup k (- k)"
-    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
-qed
-
 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
 apply (cases w, cases z) 
 apply (simp add: less le add One_int_def)
diff -r 108662d50512 -r 7efe662e41b4 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/IsaMakefile	Mon Feb 08 14:06:41 2010 +0100
@@ -384,6 +384,7 @@
   Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy	\
   Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy	\
   Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
+  Library/Lattice_Algebras.thy						\
   Library/Lattice_Syntax.thy Library/Library.thy			\
   Library/List_Prefix.thy Library/List_Set.thy Library/State_Monad.thy	\
   Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy	\
diff -r 108662d50512 -r 7efe662e41b4 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/Library/Float.thy	Mon Feb 08 14:06:41 2010 +0100
@@ -6,7 +6,7 @@
 header {* Floating-Point Numbers *}
 
 theory Float
-imports Complex_Main
+imports Complex_Main Lattice_Algebras
 begin
 
 definition
diff -r 108662d50512 -r 7efe662e41b4 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/Library/Library.thy	Mon Feb 08 14:06:41 2010 +0100
@@ -28,6 +28,7 @@
   Fundamental_Theorem_Algebra
   Infinite_Set
   Inner_Product
+  Lattice_Algebras
   Lattice_Syntax
   ListVector
   Kleene_Algebra
diff -r 108662d50512 -r 7efe662e41b4 src/HOL/Matrix/ComputeFloat.thy
--- a/src/HOL/Matrix/ComputeFloat.thy	Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/Matrix/ComputeFloat.thy	Mon Feb 08 14:06:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Floating Point Representation of the Reals *}
 
 theory ComputeFloat
-imports Complex_Main
+imports Complex_Main Lattice_Algebras
 uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
 begin
 
diff -r 108662d50512 -r 7efe662e41b4 src/HOL/Matrix/LP.thy
--- a/src/HOL/Matrix/LP.thy	Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/Matrix/LP.thy	Mon Feb 08 14:06:41 2010 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory LP 
-imports Main
+imports Main Lattice_Algebras
 begin
 
 lemma linprog_dual_estimate:
diff -r 108662d50512 -r 7efe662e41b4 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/Matrix/Matrix.thy	Mon Feb 08 14:06:41 2010 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory Matrix
-imports Main
+imports Main Lattice_Algebras
 begin
 
 types 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
diff -r 108662d50512 -r 7efe662e41b4 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/RealDef.thy	Mon Feb 08 14:06:41 2010 +0100
@@ -426,8 +426,6 @@
     by (simp only: real_sgn_def)
 qed
 
-instance real :: lattice_ab_group_add ..
-
 text{*The function @{term real_of_preal} requires many proofs, but it seems
 to be essential for proving completeness of the reals from that of the
 positive reals.*}
@@ -1046,13 +1044,6 @@
 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
 by simp
 
-instance real :: lattice_ring
-proof
-  fix a::real
-  show "abs a = sup a (-a)"
-    by (auto simp add: real_abs_def sup_real_def)
-qed
-
 
 subsection {* Implementation of rational real numbers *}
 
diff -r 108662d50512 -r 7efe662e41b4 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/Ring_and_Field.thy	Mon Feb 08 14:06:41 2010 +0100
@@ -2143,100 +2143,6 @@
   assumes abs_eq_mult:
     "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
 
-
-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: "abs (a * b) \<le> (abs a) * (abs (b::'a::lattice_ring))" 
-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: "(abs a) * (abs b) = ?x"
-    by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
-  {
-    fix u v :: 'a
-    have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> 
-              u * v = pprt a * pprt b + pprt a * nprt b + 
-                      nprt a * pprt b + nprt a * nprt b"
-      apply (subst prts[of u], subst prts[of v])
-      apply (simp add: algebra_simps) 
-      done
-  }
-  note b = this[OF refl[of a] refl[of b]]
-  note addm = add_mono[of "0::'a" _ "0::'a", simplified]
-  note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
-  have xy: "- ?x <= ?y"
-    apply (simp)
-    apply (rule_tac y="0::'a" in order_trans)
-    apply (rule addm2)
-    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
-    apply (rule addm)
-    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
-    done
-  have yx: "?y <= ?x"
-    apply (simp add:diff_def)
-    apply (rule_tac y=0 in order_trans)
-    apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
-    apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
-    done
-  have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
-  have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
-  show ?thesis
-    apply (rule abs_leI)
-    apply (simp add: i1)
-    apply (simp add: i2[simplified minus_le_iff])
-    done
-qed
-
-instance lattice_ring \<subseteq> ordered_ring_abs
-proof
-  fix a b :: "'a\<Colon> lattice_ring"
-  assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
-  show "abs (a*b) = abs a * abs b"
-proof -
-  have s: "(0 <= a*b) | (a*b <= 0)"
-    apply (auto)    
-    apply (rule_tac split_mult_pos_le)
-    apply (rule_tac contrapos_np[of "a*b <= 0"])
-    apply (simp)
-    apply (rule_tac split_mult_neg_le)
-    apply (insert prems)
-    apply (blast)
-    done
-  have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
-    by (simp add: prts[symmetric])
-  show ?thesis
-  proof cases
-    assume "0 <= a * b"
-    then show ?thesis
-      apply (simp_all add: mulprts abs_prts)
-      apply (insert prems)
-      apply (auto simp add: 
-        algebra_simps 
-        iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
-        iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
-        apply(drule (1) mult_nonneg_nonpos[of a b], simp)
-        apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
-      done
-  next
-    assume "~(0 <= a*b)"
-    with s have "a*b <= 0" by simp
-    then show ?thesis
-      apply (simp_all add: mulprts abs_prts)
-      apply (insert prems)
-      apply (auto simp add: algebra_simps)
-      apply(drule (1) mult_nonneg_nonneg[of a b],simp)
-      apply(drule (1) mult_nonpos_nonpos[of a b],simp)
-      done
-  qed
-qed
-qed
-
 context linordered_idom
 begin
 
@@ -2308,76 +2214,6 @@
   apply (simp add: order_less_imp_le)
 done
 
-
-subsection {* Bounds of products via negative and positive Part *}
-
-lemma mult_le_prts:
-  assumes
-  "a1 <= (a::'a::lattice_ring)"
-  "a <= a2"
-  "b1 <= b"
-  "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)" 
-    apply (subst prts[symmetric])+
-    apply simp
-    done
-  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: prems 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 prems)
-    moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
-      by (simp add: mult_right_mono_neg prems)
-    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 prems)
-    moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
-      by (simp add: mult_left_mono_neg prems)
-    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 prems)
-    moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
-      by (simp add: mult_right_mono_neg prems)
-    ultimately show ?thesis
-      by simp
-  qed
-  ultimately show ?thesis
-    by - (rule add_mono | simp)+
-qed
-
-lemma mult_ge_prts:
-  assumes
-  "a1 <= (a::'a::lattice_ring)"
-  "a <= a2"
-  "b1 <= b"
-  "b <= b2"
-  shows
-  "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
-proof - 
-  from prems have a1:"- a2 <= -a" by auto
-  from prems have a2: "-a <= -a1" by auto
-  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(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) <= a * b"
-    by (simp only: minus_le_iff)
-  then show ?thesis by simp
-qed
-
-
 code_modulename SML
   Ring_and_Field Arith