adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
authorhaftmann
Fri Mar 16 21:32:08 2007 +0100 (2007-03-16)
changeset 224528a86fd2a1bf0
parent 22451 989182f660e0
child 22453 530db8c36f53
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
src/HOL/FixedPoint.thy
src/HOL/Hyperreal/StarClasses.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Graphs.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/SparseMatrix.thy
src/HOL/OrderedGroup.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/FixedPoint.thy	Fri Mar 16 21:32:07 2007 +0100
     1.2 +++ b/src/HOL/FixedPoint.thy	Fri Mar 16 21:32:08 2007 +0100
     1.3 @@ -5,37 +5,35 @@
     1.4      Copyright   1992  University of Cambridge
     1.5  *)
     1.6  
     1.7 -header{* Fixed Points and the Knaster-Tarski Theorem*}
     1.8 +header {* Fixed Points and the Knaster-Tarski Theorem*}
     1.9  
    1.10  theory FixedPoint
    1.11 -imports Product_Type LOrder
    1.12 +imports Product_Type
    1.13  begin
    1.14  
    1.15  subsection {* Complete lattices *}
    1.16  
    1.17 -consts
    1.18 -  Inf :: "'a::order set \<Rightarrow> 'a"
    1.19 -
    1.20 -definition
    1.21 -  Sup :: "'a::order set \<Rightarrow> 'a" where
    1.22 -  "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
    1.23 -
    1.24 -class comp_lat = order +
    1.25 +class complete_lattice = lattice +
    1.26 +  fixes Inf :: "'a set \<Rightarrow> 'a"
    1.27    assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x"
    1.28    assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A"
    1.29  
    1.30 -theorem Sup_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Sup A"
    1.31 +definition
    1.32 +  Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a" where
    1.33 +  "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
    1.34 +
    1.35 +theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x <= Sup A"
    1.36    by (auto simp: Sup_def intro: Inf_greatest)
    1.37  
    1.38 -theorem Sup_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
    1.39 +theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
    1.40    by (auto simp: Sup_def intro: Inf_lower)
    1.41  
    1.42  definition
    1.43 -  SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
    1.44 +  SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where
    1.45    "SUPR A f == Sup (f ` A)"
    1.46  
    1.47  definition
    1.48 -  INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
    1.49 +  INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where
    1.50    "INFI A f == Inf (f ` A)"
    1.51  
    1.52  syntax
    1.53 @@ -80,17 +78,6 @@
    1.54  
    1.55  text {* A complete lattice is a lattice *}
    1.56  
    1.57 -lemma is_meet_Inf: "is_meet (\<lambda>(x::'a::comp_lat) y. Inf {x, y})"
    1.58 -  by (auto simp: is_meet_def intro: Inf_lower Inf_greatest)
    1.59 -
    1.60 -lemma is_join_Sup: "is_join (\<lambda>(x::'a::comp_lat) y. Sup {x, y})"
    1.61 -  by (auto simp: is_join_def intro: Sup_upper Sup_least)
    1.62 -
    1.63 -instance comp_lat < lorder
    1.64 -proof
    1.65 -  from is_meet_Inf show "\<exists>m::'a\<Rightarrow>'a\<Rightarrow>'a. is_meet m" by iprover
    1.66 -  from is_join_Sup show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
    1.67 -qed
    1.68  
    1.69  subsubsection {* Properties *}
    1.70  
    1.71 @@ -100,7 +87,7 @@
    1.72  lemma mono_sup: "mono f \<Longrightarrow> sup (f A) (f B) <= f (sup A B)"
    1.73    by (auto simp add: mono_def)
    1.74  
    1.75 -lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = sup a (Sup A)"
    1.76 +lemma Sup_insert[simp]: "Sup (insert (a::'a::complete_lattice) A) = sup a (Sup A)"
    1.77    apply (rule order_antisym)
    1.78    apply (rule Sup_least)
    1.79    apply (erule insertE)
    1.80 @@ -116,7 +103,7 @@
    1.81    apply simp
    1.82    done
    1.83  
    1.84 -lemma Inf_insert[simp]: "Inf (insert (a::'a::comp_lat) A) = inf a (Inf A)"
    1.85 +lemma Inf_insert[simp]: "Inf (insert (a::'a::complete_lattice) A) = inf a (Inf A)"
    1.86    apply (rule order_antisym)
    1.87    apply (rule le_infI)
    1.88    apply (rule Inf_lower)
    1.89 @@ -132,10 +119,10 @@
    1.90    apply (erule Inf_lower)
    1.91    done
    1.92  
    1.93 -lemma bot_least[simp]: "Sup{} \<le> (x::'a::comp_lat)"
    1.94 +lemma bot_least[simp]: "Sup{} \<le> (x::'a::complete_lattice)"
    1.95    by (rule Sup_least) simp
    1.96  
    1.97 -lemma top_greatest[simp]: "(x::'a::comp_lat) \<le> Inf{}"
    1.98 +lemma top_greatest[simp]: "(x::'a::complete_lattice) \<le> Inf{}"
    1.99    by (rule Inf_greatest) simp
   1.100  
   1.101  lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
   1.102 @@ -149,51 +136,15 @@
   1.103  
   1.104  subsubsection {* Booleans *}
   1.105  
   1.106 -defs
   1.107 -  Inf_bool_def: "Inf A == ALL x:A. x"
   1.108 -
   1.109 -instance bool :: comp_lat
   1.110 +instance bool :: complete_lattice
   1.111 +  Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>A. x"
   1.112    apply intro_classes
   1.113    apply (unfold Inf_bool_def)
   1.114    apply (iprover intro!: le_boolI elim: ballE)
   1.115    apply (iprover intro!: ballI le_boolI elim: ballE le_boolE)
   1.116    done
   1.117  
   1.118 -theorem inf_bool_eq: "inf P Q \<longleftrightarrow> P \<and> Q"
   1.119 -  apply (rule order_antisym)
   1.120 -  apply (rule le_boolI)
   1.121 -  apply (rule conjI)
   1.122 -  apply (rule le_boolE)
   1.123 -  apply (rule inf_le1)
   1.124 -  apply assumption+
   1.125 -  apply (rule le_boolE)
   1.126 -  apply (rule inf_le2)
   1.127 -  apply assumption+
   1.128 -  apply (rule le_infI)
   1.129 -  apply (rule le_boolI)
   1.130 -  apply (erule conjunct1)
   1.131 -  apply (rule le_boolI)
   1.132 -  apply (erule conjunct2)
   1.133 -  done
   1.134 -
   1.135 -theorem sup_bool_eq: "sup P Q \<longleftrightarrow> P \<or> Q"
   1.136 -  apply (rule order_antisym)
   1.137 -  apply (rule le_supI)
   1.138 -  apply (rule le_boolI)
   1.139 -  apply (erule disjI1)
   1.140 -  apply (rule le_boolI)
   1.141 -  apply (erule disjI2)
   1.142 -  apply (rule le_boolI)
   1.143 -  apply (erule disjE)
   1.144 -  apply (rule le_boolE)
   1.145 -  apply (rule sup_ge1)
   1.146 -  apply assumption+
   1.147 -  apply (rule le_boolE)
   1.148 -  apply (rule sup_ge2)
   1.149 -  apply assumption+
   1.150 -  done
   1.151 -
   1.152 -theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x \<in> A. x)"
   1.153 +theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
   1.154    apply (rule order_antisym)
   1.155    apply (rule Sup_least)
   1.156    apply (rule le_boolI)
   1.157 @@ -208,51 +159,8 @@
   1.158  
   1.159  subsubsection {* Functions *}
   1.160  
   1.161 -text {*
   1.162 -  Handy introduction and elimination rules for @{text "\<le>"}
   1.163 -  on unary and binary predicates
   1.164 -*}
   1.165 -
   1.166 -lemma predicate1I [Pure.intro!, intro!]:
   1.167 -  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
   1.168 -  shows "P \<le> Q"
   1.169 -  apply (rule le_funI)
   1.170 -  apply (rule le_boolI)
   1.171 -  apply (rule PQ)
   1.172 -  apply assumption
   1.173 -  done
   1.174 -
   1.175 -lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
   1.176 -  apply (erule le_funE)
   1.177 -  apply (erule le_boolE)
   1.178 -  apply assumption+
   1.179 -  done
   1.180 -
   1.181 -lemma predicate2I [Pure.intro!, intro!]:
   1.182 -  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
   1.183 -  shows "P \<le> Q"
   1.184 -  apply (rule le_funI)+
   1.185 -  apply (rule le_boolI)
   1.186 -  apply (rule PQ)
   1.187 -  apply assumption
   1.188 -  done
   1.189 -
   1.190 -lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   1.191 -  apply (erule le_funE)+
   1.192 -  apply (erule le_boolE)
   1.193 -  apply assumption+
   1.194 -  done
   1.195 -
   1.196 -lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
   1.197 -  by (rule predicate1D)
   1.198 -
   1.199 -lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
   1.200 -  by (rule predicate2D)
   1.201 -
   1.202 -defs
   1.203 -  Inf_fun_def: "Inf A == (\<lambda>x. Inf {y. EX f:A. y = f x})"
   1.204 -
   1.205 -instance "fun" :: (type, comp_lat) comp_lat
   1.206 +instance "fun" :: (type, complete_lattice) complete_lattice
   1.207 +  Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})"
   1.208    apply intro_classes
   1.209    apply (unfold Inf_fun_def)
   1.210    apply (rule le_funI)
   1.211 @@ -268,33 +176,7 @@
   1.212    apply (iprover elim: le_funE)
   1.213    done
   1.214  
   1.215 -theorem inf_fun_eq: "inf f g = (\<lambda>x. inf (f x) (g x))"
   1.216 -  apply (rule order_antisym)
   1.217 -  apply (rule le_funI)
   1.218 -  apply (rule le_infI)
   1.219 -  apply (rule le_funD [OF inf_le1])
   1.220 -  apply (rule le_funD [OF inf_le2])
   1.221 -  apply (rule le_infI)
   1.222 -  apply (rule le_funI)
   1.223 -  apply (rule inf_le1)
   1.224 -  apply (rule le_funI)
   1.225 -  apply (rule inf_le2)
   1.226 -  done
   1.227 -
   1.228 -theorem sup_fun_eq: "sup f g = (\<lambda>x. sup (f x) (g x))"
   1.229 -  apply (rule order_antisym)
   1.230 -  apply (rule le_supI)
   1.231 -  apply (rule le_funI)
   1.232 -  apply (rule sup_ge1)
   1.233 -  apply (rule le_funI)
   1.234 -  apply (rule sup_ge2)
   1.235 -  apply (rule le_funI)
   1.236 -  apply (rule le_supI)
   1.237 -  apply (rule le_funD [OF sup_ge1])
   1.238 -  apply (rule le_funD [OF sup_ge2])
   1.239 -  done
   1.240 -
   1.241 -theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y::'a::comp_lat. EX f:A. y = f x})"
   1.242 +theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
   1.243    apply (rule order_antisym)
   1.244    apply (rule Sup_least)
   1.245    apply (rule le_funI)
   1.246 @@ -308,34 +190,13 @@
   1.247    apply simp
   1.248    done
   1.249  
   1.250 +
   1.251  subsubsection {* Sets *}
   1.252  
   1.253 -defs
   1.254 -  Inf_set_def: "Inf S == \<Inter>S"
   1.255 -
   1.256 -instance set :: (type) comp_lat
   1.257 +instance set :: (type) complete_lattice
   1.258 +  Inf_set_def: "Inf S \<equiv> \<Inter>S"
   1.259    by intro_classes (auto simp add: Inf_set_def)
   1.260  
   1.261 -theorem inf_set_eq: "inf A B = A \<inter> B"
   1.262 -  apply (rule subset_antisym)
   1.263 -  apply (rule Int_greatest)
   1.264 -  apply (rule inf_le1)
   1.265 -  apply (rule inf_le2)
   1.266 -  apply (rule le_infI)
   1.267 -  apply (rule Int_lower1)
   1.268 -  apply (rule Int_lower2)
   1.269 -  done
   1.270 -
   1.271 -theorem sup_set_eq: "sup A B = A \<union> B"
   1.272 -  apply (rule subset_antisym)
   1.273 -  apply (rule le_supI)
   1.274 -  apply (rule Un_upper1)
   1.275 -  apply (rule Un_upper2)
   1.276 -  apply (rule Un_least)
   1.277 -  apply (rule sup_ge1)
   1.278 -  apply (rule sup_ge2)
   1.279 -  done
   1.280 -
   1.281  theorem Sup_set_eq: "Sup S = \<Union>S"
   1.282    apply (rule subset_antisym)
   1.283    apply (rule Sup_least)
   1.284 @@ -348,11 +209,11 @@
   1.285  subsection {* Least and greatest fixed points *}
   1.286  
   1.287  definition
   1.288 -  lfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
   1.289 +  lfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
   1.290    "lfp f = Inf {u. f u \<le> u}"    --{*least fixed point*}
   1.291  
   1.292  definition
   1.293 -  gfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
   1.294 +  gfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
   1.295    "gfp f = Sup {u. u \<le> f u}"    --{*greatest fixed point*}
   1.296  
   1.297  
   1.298 @@ -403,10 +264,8 @@
   1.299    by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
   1.300      (auto simp: inf_set_eq intro: indhyp)
   1.301  
   1.302 -
   1.303 -text{*Version of induction for binary relations*}
   1.304 -lemmas lfp_induct2 =  lfp_induct_set [of "(a,b)", split_format (complete)]
   1.305 -
   1.306 +text {* Version of induction for binary relations *}
   1.307 +lemmas lfp_induct2 =  lfp_induct_set [of "(a, b)", split_format (complete)]
   1.308  
   1.309  lemma lfp_ordinal_induct: 
   1.310    assumes mono: "mono f"
   1.311 @@ -563,8 +422,6 @@
   1.312  lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
   1.313    by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
   1.314  
   1.315 -
   1.316 -
   1.317  ML
   1.318  {*
   1.319  val lfp_def = thm "lfp_def";
     2.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Fri Mar 16 21:32:07 2007 +0100
     2.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Fri Mar 16 21:32:08 2007 +0100
     2.3 @@ -11,10 +11,6 @@
     2.4  
     2.5  subsection {* Syntactic classes *}
     2.6  
     2.7 -instance star :: (ord) ord
     2.8 -  star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
     2.9 -  star_less_def:    "(op <) \<equiv> *p2* (op <)" ..
    2.10 -
    2.11  instance star :: (zero) zero
    2.12    star_zero_def:    "0 \<equiv> star_of 0" ..
    2.13  
    2.14 @@ -24,7 +20,6 @@
    2.15  instance star :: (plus) plus
    2.16    star_add_def:     "(op +) \<equiv> *f2* (op +)" ..
    2.17  
    2.18 -
    2.19  instance star :: (times) times
    2.20    star_mult_def:    "(op *) \<equiv> *f2* (op *)" ..
    2.21  
    2.22 @@ -47,6 +42,10 @@
    2.23  instance star :: (power) power
    2.24    star_power_def:   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" ..
    2.25  
    2.26 +instance star :: (ord) ord
    2.27 +  star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
    2.28 +  star_less_def:    "(op <) \<equiv> *p2* (op <)" ..
    2.29 +
    2.30  lemmas star_class_defs [transfer_unfold] =
    2.31    star_zero_def     star_one_def      star_number_def
    2.32    star_add_def      star_diff_def     star_minus_def
    2.33 @@ -206,7 +205,7 @@
    2.34    star_of_number_less star_of_number_le star_of_number_eq
    2.35    star_of_less_number star_of_le_number star_of_eq_number
    2.36  
    2.37 -subsection {* Ordering classes *}
    2.38 +subsection {* Ordering and lattice classes *}
    2.39  
    2.40  instance star :: (order) order
    2.41  apply (intro_classes)
    2.42 @@ -216,6 +215,33 @@
    2.43  apply (transfer, erule (1) order_antisym)
    2.44  done
    2.45  
    2.46 +instance star :: (lower_semilattice) lower_semilattice
    2.47 +  star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
    2.48 +  by default (transfer star_inf_def, auto)+
    2.49 +
    2.50 +instance star :: (upper_semilattice) upper_semilattice
    2.51 +  star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
    2.52 +  by default (transfer star_sup_def, auto)+
    2.53 +
    2.54 +instance star :: (lattice) lattice ..
    2.55 +
    2.56 +instance star :: (distrib_lattice) distrib_lattice
    2.57 +  by default (transfer, auto simp add: sup_inf_distrib1)
    2.58 +
    2.59 +lemma Standard_inf [simp]:
    2.60 +  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
    2.61 +by (simp add: star_inf_def)
    2.62 +
    2.63 +lemma Standard_sup [simp]:
    2.64 +  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
    2.65 +by (simp add: star_sup_def)
    2.66 +
    2.67 +lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
    2.68 +by transfer (rule refl)
    2.69 +
    2.70 +lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
    2.71 +by transfer (rule refl)
    2.72 +
    2.73  instance star :: (linorder) linorder
    2.74  by (intro_classes, transfer, rule linorder_linear)
    2.75  
    2.76 @@ -245,63 +271,6 @@
    2.77  lemma star_of_min [simp]: "star_of (min x y) = min (star_of x) (star_of y)"
    2.78  by transfer (rule refl)
    2.79  
    2.80 -subsection {* Lattice ordering classes *}
    2.81 -
    2.82 -text {*
    2.83 -  Some extra trouble is necessary because the class axioms 
    2.84 -  for @{term inf} and @{term sup} use quantification over
    2.85 -  function spaces.
    2.86 -*}
    2.87 -
    2.88 -lemma ex_star_fun:
    2.89 -  "\<exists>f::('a \<Rightarrow> 'b) star. P (\<lambda>x. f \<star> x)
    2.90 -   \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star. P f"
    2.91 -by (erule exE, erule exI)
    2.92 -
    2.93 -lemma ex_star_fun2:
    2.94 -  "\<exists>f::('a \<Rightarrow> 'b \<Rightarrow> 'c) star. P (\<lambda>x y. f \<star> x \<star> y)
    2.95 -   \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star \<Rightarrow> 'c star. P f"
    2.96 -by (erule exE, erule exI)
    2.97 -
    2.98 -instance star :: (join_semilorder) join_semilorder
    2.99 -apply (intro_classes)
   2.100 -apply (rule ex_star_fun2)
   2.101 -apply (transfer is_join_def)
   2.102 -apply (rule join_exists)
   2.103 -done
   2.104 -
   2.105 -instance star :: (meet_semilorder) meet_semilorder
   2.106 -apply (intro_classes)
   2.107 -apply (rule ex_star_fun2)
   2.108 -apply (transfer is_meet_def)
   2.109 -apply (rule meet_exists)
   2.110 -done
   2.111 -
   2.112 -instance star :: (lorder) lorder ..
   2.113 -
   2.114 -lemma star_inf_def [transfer_unfold]: "inf = *f2* inf"
   2.115 -apply (rule is_meet_unique [OF is_meet_meet])
   2.116 -apply (transfer is_meet_def, rule is_meet_meet)
   2.117 -done
   2.118 -
   2.119 -lemma star_sup_def [transfer_unfold]: "sup = *f2* sup"
   2.120 -apply (rule is_join_unique [OF is_join_join])
   2.121 -apply (transfer is_join_def, rule is_join_join)
   2.122 -done
   2.123 -
   2.124 -lemma Standard_inf [simp]:
   2.125 -  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
   2.126 -by (simp add: star_inf_def)
   2.127 -
   2.128 -lemma Standard_sup [simp]:
   2.129 -  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
   2.130 -by (simp add: star_sup_def)
   2.131 -
   2.132 -lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
   2.133 -by transfer (rule refl)
   2.134 -
   2.135 -lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
   2.136 -by transfer (rule refl)
   2.137  
   2.138  subsection {* Ordered group classes *}
   2.139  
     3.1 --- a/src/HOL/Library/Continuity.thy	Fri Mar 16 21:32:07 2007 +0100
     3.2 +++ b/src/HOL/Library/Continuity.thy	Fri Mar 16 21:32:08 2007 +0100
     3.3 @@ -12,15 +12,15 @@
     3.4  subsection {* Continuity for complete lattices *}
     3.5  
     3.6  definition
     3.7 -  chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
     3.8 +  chain :: "(nat \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
     3.9    "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
    3.10  
    3.11  definition
    3.12 -  continuous :: "('a::comp_lat \<Rightarrow> 'a::comp_lat) \<Rightarrow> bool" where
    3.13 +  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    3.14    "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    3.15  
    3.16  abbreviation
    3.17 -  bot :: "'a::order" where
    3.18 +  bot :: "'a::complete_lattice" where
    3.19    "bot \<equiv> Sup {}"
    3.20  
    3.21  lemma SUP_nat_conv:
    3.22 @@ -34,7 +34,7 @@
    3.23  apply (blast intro:SUP_leI le_SUPI)
    3.24  done
    3.25  
    3.26 -lemma continuous_mono: fixes F :: "'a::comp_lat \<Rightarrow> 'a::comp_lat"
    3.27 +lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    3.28    assumes "continuous F" shows "mono F"
    3.29  proof
    3.30    fix A B :: "'a" assume "A <= B"
     4.1 --- a/src/HOL/Library/Graphs.thy	Fri Mar 16 21:32:07 2007 +0100
     4.2 +++ b/src/HOL/Library/Graphs.thy	Fri Mar 16 21:32:08 2007 +0100
     4.3 @@ -20,6 +20,19 @@
     4.4    "Graph (dest_graph G) = G"
     4.5    by (cases G) simp
     4.6  
     4.7 +lemma split_graph_all:
     4.8 +  "(\<And>gr. PROP P gr) \<equiv> (\<And>set. PROP P (Graph set))"
     4.9 +proof
    4.10 +  fix set
    4.11 +  assume "\<And>gr. PROP P gr"
    4.12 +  then show "PROP P (Graph set)" .
    4.13 +next
    4.14 +  fix gr
    4.15 +  assume "\<And>set. PROP P (Graph set)"
    4.16 +  then have "PROP P (Graph (dest_graph gr))" .
    4.17 +  then show "PROP P gr" by simp
    4.18 +qed
    4.19 +
    4.20  definition 
    4.21    has_edge :: "('n,'e) graph \<Rightarrow> 'n \<Rightarrow> 'e \<Rightarrow> 'n \<Rightarrow> bool"
    4.22  ("_ \<turnstile> _ \<leadsto>\<^bsup>_\<^esup> _")
    4.23 @@ -132,11 +145,9 @@
    4.24  
    4.25  subsection {* Order on Graphs *}
    4.26  
    4.27 -instance graph :: (type, type) ord 
    4.28 -  graph_leq_def: "G \<le> H == dest_graph G \<subseteq> dest_graph H"
    4.29 -  graph_less_def: "G < H == dest_graph G \<subset> dest_graph H" ..
    4.30 -
    4.31  instance graph :: (type, type) order
    4.32 +  graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
    4.33 +  graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
    4.34  proof
    4.35    fix x y z :: "('a,'b) graph"
    4.36  
    4.37 @@ -153,27 +164,14 @@
    4.38      by (cases x, cases y) auto
    4.39  qed
    4.40  
    4.41 -
    4.42 -defs (overloaded)
    4.43 -  Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
    4.44 -
    4.45 -instance graph :: (type, type) comp_lat
    4.46 -  by default (auto simp: Inf_graph_def is_join_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
    4.47 +instance graph :: (type, type) distrib_lattice
    4.48 +  "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
    4.49 +  "sup G H \<equiv> G + H"
    4.50 +  by default (auto simp add: split_graph_all graph_plus_def inf_graph_def sup_graph_def graph_leq_def graph_less_def)
    4.51  
    4.52 -lemma plus_graph_is_join: "is_join ((op +)::('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
    4.53 -  unfolding is_join_def 
    4.54 -proof (intro allI conjI impI)
    4.55 -  fix a b x :: "('a, 'b) graph"
    4.56 -
    4.57 -  show "a \<le> a + b" "b \<le> a + b" "a \<le> x \<and> b \<le> x \<Longrightarrow> a + b \<le> x"
    4.58 -    unfolding graph_leq_def graph_plus_def
    4.59 -    by (cases a, cases b) auto
    4.60 -qed
    4.61 -
    4.62 -lemma plus_is_join:
    4.63 -  "(op +) =
    4.64 -  (sup :: ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
    4.65 -  using plus_graph_is_join by (simp add:join_unique)
    4.66 +instance graph :: (type, type) complete_lattice
    4.67 +  Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
    4.68 +  by default (auto simp: Inf_graph_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
    4.69  
    4.70  instance graph :: (type, monoid_mult) semiring_1
    4.71  proof
    4.72 @@ -199,11 +197,10 @@
    4.73      by simp
    4.74  qed
    4.75  
    4.76 -
    4.77  instance graph :: (type, monoid_mult) idem_add
    4.78  proof
    4.79    fix a :: "('a, 'b) graph"
    4.80 -  show "a + a = a" unfolding plus_is_join by simp
    4.81 +  show "a + a = a" unfolding graph_plus_def by simp
    4.82  qed
    4.83  
    4.84  
    4.85 @@ -270,7 +267,7 @@
    4.86    unfolding Sup_graph_eq2 has_edge_leq graph_leq_def
    4.87    by simp
    4.88  
    4.89 -instance graph :: (type, monoid_mult) kleene_by_comp_lat
    4.90 +instance graph :: (type, monoid_mult) kleene_by_complete_lattice
    4.91  proof
    4.92    fix a b c :: "('a, 'b) graph"
    4.93  
     5.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Mar 16 21:32:07 2007 +0100
     5.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Mar 16 21:32:08 2007 +0100
     5.3 @@ -7,6 +7,11 @@
     5.4  imports MatrixGeneral
     5.5  begin
     5.6  
     5.7 +instance matrix :: ("{zero, lattice}") lattice
     5.8 +  "inf \<equiv> combine_matrix inf"
     5.9 +  "sup \<equiv> combine_matrix sup"
    5.10 +  by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
    5.11 +
    5.12  instance matrix :: ("{plus, zero}") plus
    5.13    plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" ..
    5.14  
    5.15 @@ -17,13 +22,8 @@
    5.16  instance matrix :: ("{plus, times, zero}") times
    5.17    times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
    5.18  
    5.19 -lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix inf)"
    5.20 -  by (simp_all add: is_meet_def le_matrix_def inf_le1 inf_le2 le_infI)
    5.21 -
    5.22 -lemma is_join_combine_matrix_join: "is_join (combine_matrix sup)"
    5.23 -  by (simp_all add: is_join_def le_matrix_def sup_ge1 sup_ge2 le_supI)
    5.24 -
    5.25  instance matrix :: (lordered_ab_group) lordered_ab_group_meet
    5.26 +  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
    5.27  proof 
    5.28    fix A B C :: "('a::lordered_ab_group) matrix"
    5.29    show "A + B + C = A + (B + C)"    
    5.30 @@ -45,8 +45,6 @@
    5.31      by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    5.32    show "A - B = A + - B" 
    5.33      by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    5.34 -  show "\<exists>m\<Colon>'a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix. is_meet m"
    5.35 -    by (auto intro: is_meet_combine_matrix_meet)
    5.36    assume "A <= B"
    5.37    then show "C + A <= C + B"
    5.38      apply (simp add: plus_matrix_def)
    5.39 @@ -55,9 +53,6 @@
    5.40      done
    5.41  qed
    5.42  
    5.43 -defs (overloaded)
    5.44 -  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
    5.45 -
    5.46  instance matrix :: (lordered_ring) lordered_ring
    5.47  proof
    5.48    fix A B C :: "('a :: lordered_ring) matrix"
    5.49 @@ -90,7 +85,7 @@
    5.50      apply (rule le_right_mult)
    5.51      apply (simp_all add: add_mono mult_right_mono)
    5.52      done
    5.53 -qed
    5.54 +qed 
    5.55  
    5.56  lemma Rep_matrix_add[simp]: "Rep_matrix ((a::('a::lordered_ab_group)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
    5.57  by (simp add: plus_matrix_def)
    5.58 @@ -286,17 +281,7 @@
    5.59  lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
    5.60    by (simp add: minus_matrix_def)
    5.61  
    5.62 -lemma join_matrix: "sup (A::('a::lordered_ring) matrix) B = combine_matrix sup A B"  
    5.63 -  apply (insert join_unique[of "(combine_matrix sup)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join])
    5.64 -  apply (simp)
    5.65 -  done
    5.66 -
    5.67 -lemma meet_matrix: "inf (A::('a::lordered_ring) matrix) B = combine_matrix inf A B"
    5.68 -  apply (insert meet_unique[of "(combine_matrix inf)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet])
    5.69 -  apply (simp)
    5.70 -  done
    5.71 -
    5.72  lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
    5.73 -  by (simp add: abs_lattice join_matrix)
    5.74 +  by (simp add: abs_lattice sup_matrix_def)
    5.75  
    5.76  end
     6.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Fri Mar 16 21:32:07 2007 +0100
     6.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Mar 16 21:32:08 2007 +0100
     6.3 @@ -922,7 +922,7 @@
     6.4  
     6.5  
     6.6  lemma pprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B"
     6.7 -  apply (simp add: pprt_def join_matrix)
     6.8 +  apply (simp add: pprt_def sup_matrix_def)
     6.9    apply (simp add: Rep_matrix_inject[symmetric])
    6.10    apply (rule ext)+
    6.11    apply simp
    6.12 @@ -931,7 +931,7 @@
    6.13    done
    6.14  
    6.15  lemma nprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> nprt (A+B) = nprt A + nprt B"
    6.16 -  apply (simp add: nprt_def meet_matrix)
    6.17 +  apply (simp add: nprt_def inf_matrix_def)
    6.18    apply (simp add: Rep_matrix_inject[symmetric])
    6.19    apply (rule ext)+
    6.20    apply simp
    6.21 @@ -940,14 +940,14 @@
    6.22    done
    6.23  
    6.24  lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (pprt x)"
    6.25 -  apply (simp add: pprt_def join_matrix)
    6.26 +  apply (simp add: pprt_def sup_matrix_def)
    6.27    apply (simp add: Rep_matrix_inject[symmetric])
    6.28    apply (rule ext)+
    6.29    apply simp
    6.30    done
    6.31  
    6.32  lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (nprt x)"
    6.33 -  apply (simp add: nprt_def meet_matrix)
    6.34 +  apply (simp add: nprt_def inf_matrix_def)
    6.35    apply (simp add: Rep_matrix_inject[symmetric])
    6.36    apply (rule ext)+
    6.37    apply simp
    6.38 @@ -978,7 +978,7 @@
    6.39    
    6.40  lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (pprt A) j i"
    6.41    apply (simp add: pprt_def)
    6.42 -  apply (simp add: join_matrix)
    6.43 +  apply (simp add: sup_matrix_def)
    6.44    apply (simp add: Rep_matrix_inject[symmetric])
    6.45    apply (rule ext)+
    6.46    apply (simp)
    6.47 @@ -986,7 +986,7 @@
    6.48  
    6.49  lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (nprt A) j i"
    6.50    apply (simp add: nprt_def)
    6.51 -  apply (simp add: meet_matrix)
    6.52 +  apply (simp add: inf_matrix_def)
    6.53    apply (simp add: Rep_matrix_inject[symmetric])
    6.54    apply (rule ext)+
    6.55    apply (simp)
     7.1 --- a/src/HOL/OrderedGroup.thy	Fri Mar 16 21:32:07 2007 +0100
     7.2 +++ b/src/HOL/OrderedGroup.thy	Fri Mar 16 21:32:08 2007 +0100
     7.3 @@ -1,4 +1,3 @@
     7.4 -
     7.5  (*  Title:   HOL/OrderedGroup.thy
     7.6      ID:      $Id$
     7.7      Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
     7.8 @@ -8,7 +7,7 @@
     7.9  header {* Ordered Groups *}
    7.10  
    7.11  theory OrderedGroup
    7.12 -imports LOrder
    7.13 +imports Lattices
    7.14  uses "~~/src/Provers/Arith/abel_cancel.ML"
    7.15  begin
    7.16  
    7.17 @@ -204,7 +203,7 @@
    7.18  instance pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add ..
    7.19  
    7.20  class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +
    7.21 -  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c + b \<Longrightarrow> a \<sqsubseteq> b"
    7.22 +  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b \<Longrightarrow> a \<sqsubseteq> b"
    7.23  
    7.24  class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add
    7.25  
    7.26 @@ -565,13 +564,19 @@
    7.27  lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::pordered_ab_group_add))"
    7.28  by (simp add: compare_rls)
    7.29  
    7.30 +
    7.31  subsection {* Lattice Ordered (Abelian) Groups *}
    7.32  
    7.33 -axclass lordered_ab_group_meet < pordered_ab_group_add, meet_semilorder
    7.34 +class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice
    7.35 +
    7.36 +class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice
    7.37  
    7.38 -axclass lordered_ab_group_join < pordered_ab_group_add, join_semilorder
    7.39 +class lordered_ab_group = pordered_ab_group_add + lattice
    7.40  
    7.41 -lemma add_inf_distrib_left: "a + (inf b c) = inf (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
    7.42 +instance lordered_ab_group \<subseteq> lordered_ab_group_meet by default
    7.43 +instance lordered_ab_group \<subseteq> lordered_ab_group_join by default
    7.44 +
    7.45 +lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + (c::'a::{pordered_ab_group_add, lower_semilattice}))"
    7.46  apply (rule order_antisym)
    7.47  apply (simp_all add: le_infI)
    7.48  apply (rule add_le_imp_le_left [of "-a"])
    7.49 @@ -580,7 +585,7 @@
    7.50  apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
    7.51  done
    7.52  
    7.53 -lemma add_sup_distrib_left: "a + (sup b c) = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))" 
    7.54 +lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, upper_semilattice}))" 
    7.55  apply (rule order_antisym)
    7.56  apply (rule add_le_imp_le_left [of "-a"])
    7.57  apply (simp only: add_assoc[symmetric], simp)
    7.58 @@ -590,55 +595,53 @@
    7.59  apply (simp_all)
    7.60  done
    7.61  
    7.62 -lemma is_join_neg_inf: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (inf (-a) (-b)))"
    7.63 -apply (auto simp add: is_join_def)
    7.64 -apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
    7.65 -apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
    7.66 -apply (subst neg_le_iff_le[symmetric]) 
    7.67 -apply (simp add: le_infI)
    7.68 -done
    7.69 -
    7.70 -lemma is_meet_neg_sup: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (sup (-a) (-b)))"
    7.71 -apply (auto simp add: is_meet_def)
    7.72 -apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
    7.73 -apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
    7.74 -apply (subst neg_le_iff_le[symmetric]) 
    7.75 -apply (simp add: le_supI)
    7.76 -done
    7.77 -
    7.78 -axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
    7.79 -
    7.80 -instance lordered_ab_group_join \<subseteq> lordered_ab_group
    7.81 -proof
    7.82 -  show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_sup)
    7.83 -qed
    7.84 -
    7.85 -instance lordered_ab_group_meet \<subseteq> lordered_ab_group
    7.86 -proof 
    7.87 -  show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_inf)
    7.88 -qed
    7.89 -
    7.90 -lemma add_inf_distrib_right: "(inf a b) + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
    7.91 +lemma add_inf_distrib_right: "inf a b + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
    7.92  proof -
    7.93 -  have "c + (inf a b) = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
    7.94 +  have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
    7.95    thus ?thesis by (simp add: add_commute)
    7.96  qed
    7.97  
    7.98 -lemma add_sup_distrib_right: "(sup a b) + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
    7.99 +lemma add_sup_distrib_right: "sup a b + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
   7.100  proof -
   7.101 -  have "c + (sup a b) = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
   7.102 +  have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
   7.103    thus ?thesis by (simp add: add_commute)
   7.104  qed
   7.105  
   7.106  lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
   7.107  
   7.108 -lemma sup_eq_neg_inf: "sup a (b::'a::lordered_ab_group) = - inf (-a) (-b)"
   7.109 -by (simp add: is_join_unique[OF is_join_join is_join_neg_inf])
   7.110 +lemma inf_eq_neg_sup: "inf a (b\<Colon>'a\<Colon>lordered_ab_group) = - sup (-a) (-b)"
   7.111 +proof (rule inf_unique)
   7.112 +  fix a b :: 'a
   7.113 +  show "- sup (-a) (-b) \<le> a" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
   7.114 +    (simp, simp add: add_sup_distrib_left)
   7.115 +next
   7.116 +  fix a b :: 'a
   7.117 +  show "- sup (-a) (-b) \<le> b" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
   7.118 +    (simp, simp add: add_sup_distrib_left)
   7.119 +next
   7.120 +  fix a b c :: 'a
   7.121 +  assume "a \<le> b" "a \<le> c"
   7.122 +  then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric])
   7.123 +    (simp add: le_supI)
   7.124 +qed
   7.125 +  
   7.126 +lemma sup_eq_neg_inf: "sup a (b\<Colon>'a\<Colon>lordered_ab_group) = - inf (-a) (-b)"
   7.127 +proof (rule sup_unique)
   7.128 +  fix a b :: 'a
   7.129 +  show "a \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
   7.130 +    (simp, simp add: add_inf_distrib_left)
   7.131 +next
   7.132 +  fix a b :: 'a
   7.133 +  show "b \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
   7.134 +    (simp, simp add: add_inf_distrib_left)
   7.135 +next
   7.136 +  fix a b c :: 'a
   7.137 +  assume "a \<le> c" "b \<le> c"
   7.138 +  then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric])
   7.139 +    (simp add: le_infI)
   7.140 +qed
   7.141  
   7.142 -lemma inf_eq_neg_sup: "inf a (b::'a::lordered_ab_group) = - sup (-a) (-b)"
   7.143 -by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_sup])
   7.144 -
   7.145 -lemma add_eq_inf_sup: "a + b = (sup a b) + (inf a (b::'a::lordered_ab_group))"
   7.146 +lemma add_eq_inf_sup: "a + b = sup a b + inf a (b\<Colon>'a\<Colon>lordered_ab_group)"
   7.147  proof -
   7.148    have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
   7.149    hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
   7.150 @@ -761,8 +764,8 @@
   7.151    with a show ?thesis by simp 
   7.152  qed
   7.153  
   7.154 -axclass lordered_ab_group_abs \<subseteq> lordered_ab_group
   7.155 -  abs_lattice: "abs x = sup x (-x)"
   7.156 +class lordered_ab_group_abs = lordered_ab_group +
   7.157 +  assumes abs_lattice: "abs x = sup x (uminus x)"
   7.158  
   7.159  lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
   7.160  by (simp add: abs_lattice)
   7.161 @@ -786,7 +789,7 @@
   7.162  proof -
   7.163    note b = add_le_cancel_right[of a a "-a",symmetric,simplified]
   7.164    have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)
   7.165 -  show ?thesis by (auto simp add: max_def b linorder_not_less join_max)
   7.166 +  show ?thesis by (auto simp add: max_def b linorder_not_less sup_max)
   7.167  qed
   7.168  
   7.169  lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"
   7.170 @@ -1131,8 +1134,6 @@
   7.171  val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
   7.172  val add_inf_distrib_left = thm "add_inf_distrib_left";
   7.173  val add_sup_distrib_left = thm "add_sup_distrib_left";
   7.174 -val is_join_neg_inf = thm "is_join_neg_inf";
   7.175 -val is_meet_neg_sup = thm "is_meet_neg_sup";
   7.176  val add_sup_distrib_right = thm "add_sup_distrib_right";
   7.177  val add_inf_distrib_right = thm "add_inf_distrib_right";
   7.178  val add_sup_inf_distribs = thms "add_sup_inf_distribs";
     8.1 --- a/src/HOL/Ring_and_Field.thy	Fri Mar 16 21:32:07 2007 +0100
     8.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Mar 16 21:32:08 2007 +0100
     8.3 @@ -265,7 +265,7 @@
     8.4  
     8.5  instance pordered_ring \<subseteq> pordered_ab_group_add ..
     8.6  
     8.7 -axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
     8.8 +class lordered_ring = pordered_ring + lordered_ab_group_abs
     8.9  
    8.10  instance lordered_ring \<subseteq> lordered_ab_group_meet ..
    8.11  
    8.12 @@ -274,9 +274,7 @@
    8.13  class abs_if = minus + ord + zero +
    8.14    assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
    8.15  
    8.16 -class ordered_ring_strict = ring + ordered_semiring_strict + abs_if
    8.17 -
    8.18 -instance ordered_ring_strict \<subseteq> lordered_ab_group ..
    8.19 +class ordered_ring_strict = ring + ordered_semiring_strict + abs_if + lordered_ab_group
    8.20  
    8.21  instance ordered_ring_strict \<subseteq> lordered_ring
    8.22    by intro_classes (simp add: abs_if sup_eq_if)
    8.23 @@ -287,7 +285,7 @@
    8.24    (*previously ordered_semiring*)
    8.25    assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
    8.26  
    8.27 -class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if
    8.28 +class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if + lordered_ab_group
    8.29    (*previously ordered_ring*)
    8.30  
    8.31  instance ordered_idom \<subseteq> ordered_ring_strict ..