separate library theory for type classes combining lattices with various algebraic structures
authorhaftmann
Mon Feb 08 14:06:41 2010 +0100 (2010-02-08)
changeset 350327efe662e41b4
parent 35028 108662d50512
child 35033 e47934673b74
separate library theory for type classes combining lattices with various algebraic structures
NEWS
src/HOL/Int.thy
src/HOL/IsaMakefile
src/HOL/Library/Float.thy
src/HOL/Library/Library.thy
src/HOL/Matrix/ComputeFloat.thy
src/HOL/Matrix/LP.thy
src/HOL/Matrix/Matrix.thy
src/HOL/RealDef.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/NEWS	Fri Feb 05 14:33:50 2010 +0100
     1.2 +++ b/NEWS	Mon Feb 08 14:06:41 2010 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* more consistent naming of type classes involving orderings (and lattices):
     1.8 +* More consistent naming of type classes involving orderings (and lattices):
     1.9  
    1.10      lower_semilattice                   ~> semilattice_inf
    1.11      upper_semilattice                   ~> semilattice_sup
    1.12 @@ -33,12 +33,6 @@
    1.13      pordered_ring_abs                   ~> ordered_ring_abs
    1.14      pordered_semiring                   ~> ordered_semiring
    1.15  
    1.16 -    lordered_ab_group_add               ~> lattice_ab_group_add
    1.17 -    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
    1.18 -    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
    1.19 -    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
    1.20 -    lordered_ring                       ~> lattice_ring
    1.21 -
    1.22      ordered_ab_group_add                ~> linordered_ab_group_add
    1.23      ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add
    1.24      ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add
    1.25 @@ -58,6 +52,15 @@
    1.26      ordered_semiring_1_strict           ~> linordered_semiring_1_strict
    1.27      ordered_semiring_strict             ~> linordered_semiring_strict
    1.28  
    1.29 +  The following slightly odd type classes have been moved to
    1.30 +  a separate theory Library/Lattice_Algebras.thy:
    1.31 +
    1.32 +    lordered_ab_group_add               ~> lattice_ab_group_add
    1.33 +    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
    1.34 +    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
    1.35 +    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
    1.36 +    lordered_ring                       ~> lattice_ring
    1.37 +
    1.38  INCOMPATIBILITY.
    1.39  
    1.40  * new theory Algebras.thy contains generic algebraic structures and
     2.1 --- a/src/HOL/Int.thy	Fri Feb 05 14:33:50 2010 +0100
     2.2 +++ b/src/HOL/Int.thy	Mon Feb 08 14:06:41 2010 +0100
     2.3 @@ -256,13 +256,6 @@
     2.4      by (simp only: zsgn_def)
     2.5  qed
     2.6  
     2.7 -instance int :: lattice_ring
     2.8 -proof  
     2.9 -  fix k :: int
    2.10 -  show "abs k = sup k (- k)"
    2.11 -    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
    2.12 -qed
    2.13 -
    2.14  lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
    2.15  apply (cases w, cases z) 
    2.16  apply (simp add: less le add One_int_def)
     3.1 --- a/src/HOL/IsaMakefile	Fri Feb 05 14:33:50 2010 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Mon Feb 08 14:06:41 2010 +0100
     3.3 @@ -384,6 +384,7 @@
     3.4    Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy	\
     3.5    Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy	\
     3.6    Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
     3.7 +  Library/Lattice_Algebras.thy						\
     3.8    Library/Lattice_Syntax.thy Library/Library.thy			\
     3.9    Library/List_Prefix.thy Library/List_Set.thy Library/State_Monad.thy	\
    3.10    Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy	\
     4.1 --- a/src/HOL/Library/Float.thy	Fri Feb 05 14:33:50 2010 +0100
     4.2 +++ b/src/HOL/Library/Float.thy	Mon Feb 08 14:06:41 2010 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Floating-Point Numbers *}
     4.5  
     4.6  theory Float
     4.7 -imports Complex_Main
     4.8 +imports Complex_Main Lattice_Algebras
     4.9  begin
    4.10  
    4.11  definition
     5.1 --- a/src/HOL/Library/Library.thy	Fri Feb 05 14:33:50 2010 +0100
     5.2 +++ b/src/HOL/Library/Library.thy	Mon Feb 08 14:06:41 2010 +0100
     5.3 @@ -28,6 +28,7 @@
     5.4    Fundamental_Theorem_Algebra
     5.5    Infinite_Set
     5.6    Inner_Product
     5.7 +  Lattice_Algebras
     5.8    Lattice_Syntax
     5.9    ListVector
    5.10    Kleene_Algebra
     6.1 --- a/src/HOL/Matrix/ComputeFloat.thy	Fri Feb 05 14:33:50 2010 +0100
     6.2 +++ b/src/HOL/Matrix/ComputeFloat.thy	Mon Feb 08 14:06:41 2010 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Floating Point Representation of the Reals *}
     6.5  
     6.6  theory ComputeFloat
     6.7 -imports Complex_Main
     6.8 +imports Complex_Main Lattice_Algebras
     6.9  uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
    6.10  begin
    6.11  
     7.1 --- a/src/HOL/Matrix/LP.thy	Fri Feb 05 14:33:50 2010 +0100
     7.2 +++ b/src/HOL/Matrix/LP.thy	Mon Feb 08 14:06:41 2010 +0100
     7.3 @@ -3,7 +3,7 @@
     7.4  *)
     7.5  
     7.6  theory LP 
     7.7 -imports Main
     7.8 +imports Main Lattice_Algebras
     7.9  begin
    7.10  
    7.11  lemma linprog_dual_estimate:
     8.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Feb 05 14:33:50 2010 +0100
     8.2 +++ b/src/HOL/Matrix/Matrix.thy	Mon Feb 08 14:06:41 2010 +0100
     8.3 @@ -3,7 +3,7 @@
     8.4  *)
     8.5  
     8.6  theory Matrix
     8.7 -imports Main
     8.8 +imports Main Lattice_Algebras
     8.9  begin
    8.10  
    8.11  types 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
     9.1 --- a/src/HOL/RealDef.thy	Fri Feb 05 14:33:50 2010 +0100
     9.2 +++ b/src/HOL/RealDef.thy	Mon Feb 08 14:06:41 2010 +0100
     9.3 @@ -426,8 +426,6 @@
     9.4      by (simp only: real_sgn_def)
     9.5  qed
     9.6  
     9.7 -instance real :: lattice_ab_group_add ..
     9.8 -
     9.9  text{*The function @{term real_of_preal} requires many proofs, but it seems
    9.10  to be essential for proving completeness of the reals from that of the
    9.11  positive reals.*}
    9.12 @@ -1046,13 +1044,6 @@
    9.13  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
    9.14  by simp
    9.15  
    9.16 -instance real :: lattice_ring
    9.17 -proof
    9.18 -  fix a::real
    9.19 -  show "abs a = sup a (-a)"
    9.20 -    by (auto simp add: real_abs_def sup_real_def)
    9.21 -qed
    9.22 -
    9.23  
    9.24  subsection {* Implementation of rational real numbers *}
    9.25  
    10.1 --- a/src/HOL/Ring_and_Field.thy	Fri Feb 05 14:33:50 2010 +0100
    10.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Feb 08 14:06:41 2010 +0100
    10.3 @@ -2143,100 +2143,6 @@
    10.4    assumes abs_eq_mult:
    10.5      "(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>"
    10.6  
    10.7 -
    10.8 -class lattice_ring = ordered_ring + lattice_ab_group_add_abs
    10.9 -begin
   10.10 -
   10.11 -subclass semilattice_inf_ab_group_add ..
   10.12 -subclass semilattice_sup_ab_group_add ..
   10.13 -
   10.14 -end
   10.15 -
   10.16 -lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lattice_ring))" 
   10.17 -proof -
   10.18 -  let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
   10.19 -  let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
   10.20 -  have a: "(abs a) * (abs b) = ?x"
   10.21 -    by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
   10.22 -  {
   10.23 -    fix u v :: 'a
   10.24 -    have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> 
   10.25 -              u * v = pprt a * pprt b + pprt a * nprt b + 
   10.26 -                      nprt a * pprt b + nprt a * nprt b"
   10.27 -      apply (subst prts[of u], subst prts[of v])
   10.28 -      apply (simp add: algebra_simps) 
   10.29 -      done
   10.30 -  }
   10.31 -  note b = this[OF refl[of a] refl[of b]]
   10.32 -  note addm = add_mono[of "0::'a" _ "0::'a", simplified]
   10.33 -  note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
   10.34 -  have xy: "- ?x <= ?y"
   10.35 -    apply (simp)
   10.36 -    apply (rule_tac y="0::'a" in order_trans)
   10.37 -    apply (rule addm2)
   10.38 -    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
   10.39 -    apply (rule addm)
   10.40 -    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
   10.41 -    done
   10.42 -  have yx: "?y <= ?x"
   10.43 -    apply (simp add:diff_def)
   10.44 -    apply (rule_tac y=0 in order_trans)
   10.45 -    apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
   10.46 -    apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
   10.47 -    done
   10.48 -  have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
   10.49 -  have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
   10.50 -  show ?thesis
   10.51 -    apply (rule abs_leI)
   10.52 -    apply (simp add: i1)
   10.53 -    apply (simp add: i2[simplified minus_le_iff])
   10.54 -    done
   10.55 -qed
   10.56 -
   10.57 -instance lattice_ring \<subseteq> ordered_ring_abs
   10.58 -proof
   10.59 -  fix a b :: "'a\<Colon> lattice_ring"
   10.60 -  assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
   10.61 -  show "abs (a*b) = abs a * abs b"
   10.62 -proof -
   10.63 -  have s: "(0 <= a*b) | (a*b <= 0)"
   10.64 -    apply (auto)    
   10.65 -    apply (rule_tac split_mult_pos_le)
   10.66 -    apply (rule_tac contrapos_np[of "a*b <= 0"])
   10.67 -    apply (simp)
   10.68 -    apply (rule_tac split_mult_neg_le)
   10.69 -    apply (insert prems)
   10.70 -    apply (blast)
   10.71 -    done
   10.72 -  have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
   10.73 -    by (simp add: prts[symmetric])
   10.74 -  show ?thesis
   10.75 -  proof cases
   10.76 -    assume "0 <= a * b"
   10.77 -    then show ?thesis
   10.78 -      apply (simp_all add: mulprts abs_prts)
   10.79 -      apply (insert prems)
   10.80 -      apply (auto simp add: 
   10.81 -        algebra_simps 
   10.82 -        iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
   10.83 -        iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
   10.84 -        apply(drule (1) mult_nonneg_nonpos[of a b], simp)
   10.85 -        apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
   10.86 -      done
   10.87 -  next
   10.88 -    assume "~(0 <= a*b)"
   10.89 -    with s have "a*b <= 0" by simp
   10.90 -    then show ?thesis
   10.91 -      apply (simp_all add: mulprts abs_prts)
   10.92 -      apply (insert prems)
   10.93 -      apply (auto simp add: algebra_simps)
   10.94 -      apply(drule (1) mult_nonneg_nonneg[of a b],simp)
   10.95 -      apply(drule (1) mult_nonpos_nonpos[of a b],simp)
   10.96 -      done
   10.97 -  qed
   10.98 -qed
   10.99 -qed
  10.100 -
  10.101  context linordered_idom
  10.102  begin
  10.103  
  10.104 @@ -2308,76 +2214,6 @@
  10.105    apply (simp add: order_less_imp_le)
  10.106  done
  10.107  
  10.108 -
  10.109 -subsection {* Bounds of products via negative and positive Part *}
  10.110 -
  10.111 -lemma mult_le_prts:
  10.112 -  assumes
  10.113 -  "a1 <= (a::'a::lattice_ring)"
  10.114 -  "a <= a2"
  10.115 -  "b1 <= b"
  10.116 -  "b <= b2"
  10.117 -  shows
  10.118 -  "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
  10.119 -proof - 
  10.120 -  have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" 
  10.121 -    apply (subst prts[symmetric])+
  10.122 -    apply simp
  10.123 -    done
  10.124 -  then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  10.125 -    by (simp add: algebra_simps)
  10.126 -  moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
  10.127 -    by (simp_all add: prems mult_mono)
  10.128 -  moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
  10.129 -  proof -
  10.130 -    have "pprt a * nprt b <= pprt a * nprt b2"
  10.131 -      by (simp add: mult_left_mono prems)
  10.132 -    moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
  10.133 -      by (simp add: mult_right_mono_neg prems)
  10.134 -    ultimately show ?thesis
  10.135 -      by simp
  10.136 -  qed
  10.137 -  moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
  10.138 -  proof - 
  10.139 -    have "nprt a * pprt b <= nprt a2 * pprt b"
  10.140 -      by (simp add: mult_right_mono prems)
  10.141 -    moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
  10.142 -      by (simp add: mult_left_mono_neg prems)
  10.143 -    ultimately show ?thesis
  10.144 -      by simp
  10.145 -  qed
  10.146 -  moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
  10.147 -  proof -
  10.148 -    have "nprt a * nprt b <= nprt a * nprt b1"
  10.149 -      by (simp add: mult_left_mono_neg prems)
  10.150 -    moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
  10.151 -      by (simp add: mult_right_mono_neg prems)
  10.152 -    ultimately show ?thesis
  10.153 -      by simp
  10.154 -  qed
  10.155 -  ultimately show ?thesis
  10.156 -    by - (rule add_mono | simp)+
  10.157 -qed
  10.158 -
  10.159 -lemma mult_ge_prts:
  10.160 -  assumes
  10.161 -  "a1 <= (a::'a::lattice_ring)"
  10.162 -  "a <= a2"
  10.163 -  "b1 <= b"
  10.164 -  "b <= b2"
  10.165 -  shows
  10.166 -  "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
  10.167 -proof - 
  10.168 -  from prems have a1:"- a2 <= -a" by auto
  10.169 -  from prems have a2: "-a <= -a1" by auto
  10.170 -  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
  10.171 -  have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp  
  10.172 -  then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
  10.173 -    by (simp only: minus_le_iff)
  10.174 -  then show ?thesis by simp
  10.175 -qed
  10.176 -
  10.177 -
  10.178  code_modulename SML
  10.179    Ring_and_Field Arith
  10.180