# HG changeset patch
# User haftmann
# Date 1174077128 -3600
# Node ID 8a86fd2a1bf039dc05c6a08895ae5304eb387a3b
# Parent  989182f660e0b0f29ab7bf5e7b17938aa4cdbc53
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy

diff -r 989182f660e0 -r 8a86fd2a1bf0 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/FixedPoint.thy	Fri Mar 16 21:32:08 2007 +0100
@@ -5,37 +5,35 @@
     Copyright   1992  University of Cambridge
 *)
 
-header{* Fixed Points and the Knaster-Tarski Theorem*}
+header {* Fixed Points and the Knaster-Tarski Theorem*}
 
 theory FixedPoint
-imports Product_Type LOrder
+imports Product_Type
 begin
 
 subsection {* Complete lattices *}
 
-consts
-  Inf :: "'a::order set \<Rightarrow> 'a"
-
-definition
-  Sup :: "'a::order set \<Rightarrow> 'a" where
-  "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
-
-class comp_lat = order +
+class complete_lattice = lattice +
+  fixes Inf :: "'a set \<Rightarrow> 'a"
   assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x"
   assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A"
 
-theorem Sup_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Sup A"
+definition
+  Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a" where
+  "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
+
+theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x <= Sup A"
   by (auto simp: Sup_def intro: Inf_greatest)
 
-theorem Sup_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
+theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
   by (auto simp: Sup_def intro: Inf_lower)
 
 definition
-  SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
+  SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where
   "SUPR A f == Sup (f ` A)"
 
 definition
-  INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
+  INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where
   "INFI A f == Inf (f ` A)"
 
 syntax
@@ -80,17 +78,6 @@
 
 text {* A complete lattice is a lattice *}
 
-lemma is_meet_Inf: "is_meet (\<lambda>(x::'a::comp_lat) y. Inf {x, y})"
-  by (auto simp: is_meet_def intro: Inf_lower Inf_greatest)
-
-lemma is_join_Sup: "is_join (\<lambda>(x::'a::comp_lat) y. Sup {x, y})"
-  by (auto simp: is_join_def intro: Sup_upper Sup_least)
-
-instance comp_lat < lorder
-proof
-  from is_meet_Inf show "\<exists>m::'a\<Rightarrow>'a\<Rightarrow>'a. is_meet m" by iprover
-  from is_join_Sup show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
-qed
 
 subsubsection {* Properties *}
 
@@ -100,7 +87,7 @@
 lemma mono_sup: "mono f \<Longrightarrow> sup (f A) (f B) <= f (sup A B)"
   by (auto simp add: mono_def)
 
-lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = sup a (Sup A)"
+lemma Sup_insert[simp]: "Sup (insert (a::'a::complete_lattice) A) = sup a (Sup A)"
   apply (rule order_antisym)
   apply (rule Sup_least)
   apply (erule insertE)
@@ -116,7 +103,7 @@
   apply simp
   done
 
-lemma Inf_insert[simp]: "Inf (insert (a::'a::comp_lat) A) = inf a (Inf A)"
+lemma Inf_insert[simp]: "Inf (insert (a::'a::complete_lattice) A) = inf a (Inf A)"
   apply (rule order_antisym)
   apply (rule le_infI)
   apply (rule Inf_lower)
@@ -132,10 +119,10 @@
   apply (erule Inf_lower)
   done
 
-lemma bot_least[simp]: "Sup{} \<le> (x::'a::comp_lat)"
+lemma bot_least[simp]: "Sup{} \<le> (x::'a::complete_lattice)"
   by (rule Sup_least) simp
 
-lemma top_greatest[simp]: "(x::'a::comp_lat) \<le> Inf{}"
+lemma top_greatest[simp]: "(x::'a::complete_lattice) \<le> Inf{}"
   by (rule Inf_greatest) simp
 
 lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
@@ -149,51 +136,15 @@
 
 subsubsection {* Booleans *}
 
-defs
-  Inf_bool_def: "Inf A == ALL x:A. x"
-
-instance bool :: comp_lat
+instance bool :: complete_lattice
+  Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>A. x"
   apply intro_classes
   apply (unfold Inf_bool_def)
   apply (iprover intro!: le_boolI elim: ballE)
   apply (iprover intro!: ballI le_boolI elim: ballE le_boolE)
   done
 
-theorem inf_bool_eq: "inf P Q \<longleftrightarrow> P \<and> Q"
-  apply (rule order_antisym)
-  apply (rule le_boolI)
-  apply (rule conjI)
-  apply (rule le_boolE)
-  apply (rule inf_le1)
-  apply assumption+
-  apply (rule le_boolE)
-  apply (rule inf_le2)
-  apply assumption+
-  apply (rule le_infI)
-  apply (rule le_boolI)
-  apply (erule conjunct1)
-  apply (rule le_boolI)
-  apply (erule conjunct2)
-  done
-
-theorem sup_bool_eq: "sup P Q \<longleftrightarrow> P \<or> Q"
-  apply (rule order_antisym)
-  apply (rule le_supI)
-  apply (rule le_boolI)
-  apply (erule disjI1)
-  apply (rule le_boolI)
-  apply (erule disjI2)
-  apply (rule le_boolI)
-  apply (erule disjE)
-  apply (rule le_boolE)
-  apply (rule sup_ge1)
-  apply assumption+
-  apply (rule le_boolE)
-  apply (rule sup_ge2)
-  apply assumption+
-  done
-
-theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x \<in> A. x)"
+theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
   apply (rule order_antisym)
   apply (rule Sup_least)
   apply (rule le_boolI)
@@ -208,51 +159,8 @@
 
 subsubsection {* Functions *}
 
-text {*
-  Handy introduction and elimination rules for @{text "\<le>"}
-  on unary and binary predicates
-*}
-
-lemma predicate1I [Pure.intro!, intro!]:
-  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
-  shows "P \<le> Q"
-  apply (rule le_funI)
-  apply (rule le_boolI)
-  apply (rule PQ)
-  apply assumption
-  done
-
-lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
-  apply (erule le_funE)
-  apply (erule le_boolE)
-  apply assumption+
-  done
-
-lemma predicate2I [Pure.intro!, intro!]:
-  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
-  shows "P \<le> Q"
-  apply (rule le_funI)+
-  apply (rule le_boolI)
-  apply (rule PQ)
-  apply assumption
-  done
-
-lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
-  apply (erule le_funE)+
-  apply (erule le_boolE)
-  apply assumption+
-  done
-
-lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
-  by (rule predicate1D)
-
-lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
-  by (rule predicate2D)
-
-defs
-  Inf_fun_def: "Inf A == (\<lambda>x. Inf {y. EX f:A. y = f x})"
-
-instance "fun" :: (type, comp_lat) comp_lat
+instance "fun" :: (type, complete_lattice) complete_lattice
+  Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})"
   apply intro_classes
   apply (unfold Inf_fun_def)
   apply (rule le_funI)
@@ -268,33 +176,7 @@
   apply (iprover elim: le_funE)
   done
 
-theorem inf_fun_eq: "inf f g = (\<lambda>x. inf (f x) (g x))"
-  apply (rule order_antisym)
-  apply (rule le_funI)
-  apply (rule le_infI)
-  apply (rule le_funD [OF inf_le1])
-  apply (rule le_funD [OF inf_le2])
-  apply (rule le_infI)
-  apply (rule le_funI)
-  apply (rule inf_le1)
-  apply (rule le_funI)
-  apply (rule inf_le2)
-  done
-
-theorem sup_fun_eq: "sup f g = (\<lambda>x. sup (f x) (g x))"
-  apply (rule order_antisym)
-  apply (rule le_supI)
-  apply (rule le_funI)
-  apply (rule sup_ge1)
-  apply (rule le_funI)
-  apply (rule sup_ge2)
-  apply (rule le_funI)
-  apply (rule le_supI)
-  apply (rule le_funD [OF sup_ge1])
-  apply (rule le_funD [OF sup_ge2])
-  done
-
-theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y::'a::comp_lat. EX f:A. y = f x})"
+theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
   apply (rule order_antisym)
   apply (rule Sup_least)
   apply (rule le_funI)
@@ -308,34 +190,13 @@
   apply simp
   done
 
+
 subsubsection {* Sets *}
 
-defs
-  Inf_set_def: "Inf S == \<Inter>S"
-
-instance set :: (type) comp_lat
+instance set :: (type) complete_lattice
+  Inf_set_def: "Inf S \<equiv> \<Inter>S"
   by intro_classes (auto simp add: Inf_set_def)
 
-theorem inf_set_eq: "inf A B = A \<inter> B"
-  apply (rule subset_antisym)
-  apply (rule Int_greatest)
-  apply (rule inf_le1)
-  apply (rule inf_le2)
-  apply (rule le_infI)
-  apply (rule Int_lower1)
-  apply (rule Int_lower2)
-  done
-
-theorem sup_set_eq: "sup A B = A \<union> B"
-  apply (rule subset_antisym)
-  apply (rule le_supI)
-  apply (rule Un_upper1)
-  apply (rule Un_upper2)
-  apply (rule Un_least)
-  apply (rule sup_ge1)
-  apply (rule sup_ge2)
-  done
-
 theorem Sup_set_eq: "Sup S = \<Union>S"
   apply (rule subset_antisym)
   apply (rule Sup_least)
@@ -348,11 +209,11 @@
 subsection {* Least and greatest fixed points *}
 
 definition
-  lfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
+  lfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "lfp f = Inf {u. f u \<le> u}"    --{*least fixed point*}
 
 definition
-  gfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
+  gfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "gfp f = Sup {u. u \<le> f u}"    --{*greatest fixed point*}
 
 
@@ -403,10 +264,8 @@
   by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
     (auto simp: inf_set_eq intro: indhyp)
 
-
-text{*Version of induction for binary relations*}
-lemmas lfp_induct2 =  lfp_induct_set [of "(a,b)", split_format (complete)]
-
+text {* Version of induction for binary relations *}
+lemmas lfp_induct2 =  lfp_induct_set [of "(a, b)", split_format (complete)]
 
 lemma lfp_ordinal_induct: 
   assumes mono: "mono f"
@@ -563,8 +422,6 @@
 lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
   by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
 
-
-
 ML
 {*
 val lfp_def = thm "lfp_def";
diff -r 989182f660e0 -r 8a86fd2a1bf0 src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy	Fri Mar 16 21:32:08 2007 +0100
@@ -11,10 +11,6 @@
 
 subsection {* Syntactic classes *}
 
-instance star :: (ord) ord
-  star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
-  star_less_def:    "(op <) \<equiv> *p2* (op <)" ..
-
 instance star :: (zero) zero
   star_zero_def:    "0 \<equiv> star_of 0" ..
 
@@ -24,7 +20,6 @@
 instance star :: (plus) plus
   star_add_def:     "(op +) \<equiv> *f2* (op +)" ..
 
-
 instance star :: (times) times
   star_mult_def:    "(op *) \<equiv> *f2* (op *)" ..
 
@@ -47,6 +42,10 @@
 instance star :: (power) power
   star_power_def:   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" ..
 
+instance star :: (ord) ord
+  star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
+  star_less_def:    "(op <) \<equiv> *p2* (op <)" ..
+
 lemmas star_class_defs [transfer_unfold] =
   star_zero_def     star_one_def      star_number_def
   star_add_def      star_diff_def     star_minus_def
@@ -206,7 +205,7 @@
   star_of_number_less star_of_number_le star_of_number_eq
   star_of_less_number star_of_le_number star_of_eq_number
 
-subsection {* Ordering classes *}
+subsection {* Ordering and lattice classes *}
 
 instance star :: (order) order
 apply (intro_classes)
@@ -216,6 +215,33 @@
 apply (transfer, erule (1) order_antisym)
 done
 
+instance star :: (lower_semilattice) lower_semilattice
+  star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
+  by default (transfer star_inf_def, auto)+
+
+instance star :: (upper_semilattice) upper_semilattice
+  star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
+  by default (transfer star_sup_def, auto)+
+
+instance star :: (lattice) lattice ..
+
+instance star :: (distrib_lattice) distrib_lattice
+  by default (transfer, auto simp add: sup_inf_distrib1)
+
+lemma Standard_inf [simp]:
+  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
+by (simp add: star_inf_def)
+
+lemma Standard_sup [simp]:
+  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
+by (simp add: star_sup_def)
+
+lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
+by transfer (rule refl)
+
+lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
+by transfer (rule refl)
+
 instance star :: (linorder) linorder
 by (intro_classes, transfer, rule linorder_linear)
 
@@ -245,63 +271,6 @@
 lemma star_of_min [simp]: "star_of (min x y) = min (star_of x) (star_of y)"
 by transfer (rule refl)
 
-subsection {* Lattice ordering classes *}
-
-text {*
-  Some extra trouble is necessary because the class axioms 
-  for @{term inf} and @{term sup} use quantification over
-  function spaces.
-*}
-
-lemma ex_star_fun:
-  "\<exists>f::('a \<Rightarrow> 'b) star. P (\<lambda>x. f \<star> x)
-   \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star. P f"
-by (erule exE, erule exI)
-
-lemma ex_star_fun2:
-  "\<exists>f::('a \<Rightarrow> 'b \<Rightarrow> 'c) star. P (\<lambda>x y. f \<star> x \<star> y)
-   \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star \<Rightarrow> 'c star. P f"
-by (erule exE, erule exI)
-
-instance star :: (join_semilorder) join_semilorder
-apply (intro_classes)
-apply (rule ex_star_fun2)
-apply (transfer is_join_def)
-apply (rule join_exists)
-done
-
-instance star :: (meet_semilorder) meet_semilorder
-apply (intro_classes)
-apply (rule ex_star_fun2)
-apply (transfer is_meet_def)
-apply (rule meet_exists)
-done
-
-instance star :: (lorder) lorder ..
-
-lemma star_inf_def [transfer_unfold]: "inf = *f2* inf"
-apply (rule is_meet_unique [OF is_meet_meet])
-apply (transfer is_meet_def, rule is_meet_meet)
-done
-
-lemma star_sup_def [transfer_unfold]: "sup = *f2* sup"
-apply (rule is_join_unique [OF is_join_join])
-apply (transfer is_join_def, rule is_join_join)
-done
-
-lemma Standard_inf [simp]:
-  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
-by (simp add: star_inf_def)
-
-lemma Standard_sup [simp]:
-  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
-by (simp add: star_sup_def)
-
-lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
-by transfer (rule refl)
-
-lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
-by transfer (rule refl)
 
 subsection {* Ordered group classes *}
 
diff -r 989182f660e0 -r 8a86fd2a1bf0 src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Library/Continuity.thy	Fri Mar 16 21:32:08 2007 +0100
@@ -12,15 +12,15 @@
 subsection {* Continuity for complete lattices *}
 
 definition
-  chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
+  chain :: "(nat \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
   "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
 
 definition
-  continuous :: "('a::comp_lat \<Rightarrow> 'a::comp_lat) \<Rightarrow> bool" where
+  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
   "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
 
 abbreviation
-  bot :: "'a::order" where
+  bot :: "'a::complete_lattice" where
   "bot \<equiv> Sup {}"
 
 lemma SUP_nat_conv:
@@ -34,7 +34,7 @@
 apply (blast intro:SUP_leI le_SUPI)
 done
 
-lemma continuous_mono: fixes F :: "'a::comp_lat \<Rightarrow> 'a::comp_lat"
+lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
   assumes "continuous F" shows "mono F"
 proof
   fix A B :: "'a" assume "A <= B"
diff -r 989182f660e0 -r 8a86fd2a1bf0 src/HOL/Library/Graphs.thy
--- a/src/HOL/Library/Graphs.thy	Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Library/Graphs.thy	Fri Mar 16 21:32:08 2007 +0100
@@ -20,6 +20,19 @@
   "Graph (dest_graph G) = G"
   by (cases G) simp
 
+lemma split_graph_all:
+  "(\<And>gr. PROP P gr) \<equiv> (\<And>set. PROP P (Graph set))"
+proof
+  fix set
+  assume "\<And>gr. PROP P gr"
+  then show "PROP P (Graph set)" .
+next
+  fix gr
+  assume "\<And>set. PROP P (Graph set)"
+  then have "PROP P (Graph (dest_graph gr))" .
+  then show "PROP P gr" by simp
+qed
+
 definition 
   has_edge :: "('n,'e) graph \<Rightarrow> 'n \<Rightarrow> 'e \<Rightarrow> 'n \<Rightarrow> bool"
 ("_ \<turnstile> _ \<leadsto>\<^bsup>_\<^esup> _")
@@ -132,11 +145,9 @@
 
 subsection {* Order on Graphs *}
 
-instance graph :: (type, type) ord 
-  graph_leq_def: "G \<le> H == dest_graph G \<subseteq> dest_graph H"
-  graph_less_def: "G < H == dest_graph G \<subset> dest_graph H" ..
-
 instance graph :: (type, type) order
+  graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
+  graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
 proof
   fix x y z :: "('a,'b) graph"
 
@@ -153,27 +164,14 @@
     by (cases x, cases y) auto
 qed
 
-
-defs (overloaded)
-  Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
-
-instance graph :: (type, type) comp_lat
-  by default (auto simp: Inf_graph_def is_join_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
+instance graph :: (type, type) distrib_lattice
+  "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
+  "sup G H \<equiv> G + H"
+  by default (auto simp add: split_graph_all graph_plus_def inf_graph_def sup_graph_def graph_leq_def graph_less_def)
 
-lemma plus_graph_is_join: "is_join ((op +)::('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
-  unfolding is_join_def 
-proof (intro allI conjI impI)
-  fix a b x :: "('a, 'b) graph"
-
-  show "a \<le> a + b" "b \<le> a + b" "a \<le> x \<and> b \<le> x \<Longrightarrow> a + b \<le> x"
-    unfolding graph_leq_def graph_plus_def
-    by (cases a, cases b) auto
-qed
-
-lemma plus_is_join:
-  "(op +) =
-  (sup :: ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
-  using plus_graph_is_join by (simp add:join_unique)
+instance graph :: (type, type) complete_lattice
+  Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
+  by default (auto simp: Inf_graph_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
 
 instance graph :: (type, monoid_mult) semiring_1
 proof
@@ -199,11 +197,10 @@
     by simp
 qed
 
-
 instance graph :: (type, monoid_mult) idem_add
 proof
   fix a :: "('a, 'b) graph"
-  show "a + a = a" unfolding plus_is_join by simp
+  show "a + a = a" unfolding graph_plus_def by simp
 qed
 
 
@@ -270,7 +267,7 @@
   unfolding Sup_graph_eq2 has_edge_leq graph_leq_def
   by simp
 
-instance graph :: (type, monoid_mult) kleene_by_comp_lat
+instance graph :: (type, monoid_mult) kleene_by_complete_lattice
 proof
   fix a b c :: "('a, 'b) graph"
 
diff -r 989182f660e0 -r 8a86fd2a1bf0 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Matrix/Matrix.thy	Fri Mar 16 21:32:08 2007 +0100
@@ -7,6 +7,11 @@
 imports MatrixGeneral
 begin
 
+instance matrix :: ("{zero, lattice}") lattice
+  "inf \<equiv> combine_matrix inf"
+  "sup \<equiv> combine_matrix sup"
+  by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
+
 instance matrix :: ("{plus, zero}") plus
   plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" ..
 
@@ -17,13 +22,8 @@
 instance matrix :: ("{plus, times, zero}") times
   times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
 
-lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix inf)"
-  by (simp_all add: is_meet_def le_matrix_def inf_le1 inf_le2 le_infI)
-
-lemma is_join_combine_matrix_join: "is_join (combine_matrix sup)"
-  by (simp_all add: is_join_def le_matrix_def sup_ge1 sup_ge2 le_supI)
-
 instance matrix :: (lordered_ab_group) lordered_ab_group_meet
+  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
 proof 
   fix A B C :: "('a::lordered_ab_group) matrix"
   show "A + B + C = A + (B + C)"    
@@ -45,8 +45,6 @@
     by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
   show "A - B = A + - B" 
     by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
-  show "\<exists>m\<Colon>'a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix. is_meet m"
-    by (auto intro: is_meet_combine_matrix_meet)
   assume "A <= B"
   then show "C + A <= C + B"
     apply (simp add: plus_matrix_def)
@@ -55,9 +53,6 @@
     done
 qed
 
-defs (overloaded)
-  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
-
 instance matrix :: (lordered_ring) lordered_ring
 proof
   fix A B C :: "('a :: lordered_ring) matrix"
@@ -90,7 +85,7 @@
     apply (rule le_right_mult)
     apply (simp_all add: add_mono mult_right_mono)
     done
-qed
+qed 
 
 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)"
 by (simp add: plus_matrix_def)
@@ -286,17 +281,7 @@
 lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
   by (simp add: minus_matrix_def)
 
-lemma join_matrix: "sup (A::('a::lordered_ring) matrix) B = combine_matrix sup A B"  
-  apply (insert join_unique[of "(combine_matrix sup)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join])
-  apply (simp)
-  done
-
-lemma meet_matrix: "inf (A::('a::lordered_ring) matrix) B = combine_matrix inf A B"
-  apply (insert meet_unique[of "(combine_matrix inf)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet])
-  apply (simp)
-  done
-
 lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
-  by (simp add: abs_lattice join_matrix)
+  by (simp add: abs_lattice sup_matrix_def)
 
 end
diff -r 989182f660e0 -r 8a86fd2a1bf0 src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Mar 16 21:32:08 2007 +0100
@@ -922,7 +922,7 @@
 
 
 lemma pprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B"
-  apply (simp add: pprt_def join_matrix)
+  apply (simp add: pprt_def sup_matrix_def)
   apply (simp add: Rep_matrix_inject[symmetric])
   apply (rule ext)+
   apply simp
@@ -931,7 +931,7 @@
   done
 
 lemma nprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> nprt (A+B) = nprt A + nprt B"
-  apply (simp add: nprt_def meet_matrix)
+  apply (simp add: nprt_def inf_matrix_def)
   apply (simp add: Rep_matrix_inject[symmetric])
   apply (rule ext)+
   apply simp
@@ -940,14 +940,14 @@
   done
 
 lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (pprt x)"
-  apply (simp add: pprt_def join_matrix)
+  apply (simp add: pprt_def sup_matrix_def)
   apply (simp add: Rep_matrix_inject[symmetric])
   apply (rule ext)+
   apply simp
   done
 
 lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (nprt x)"
-  apply (simp add: nprt_def meet_matrix)
+  apply (simp add: nprt_def inf_matrix_def)
   apply (simp add: Rep_matrix_inject[symmetric])
   apply (rule ext)+
   apply simp
@@ -978,7 +978,7 @@
   
 lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (pprt A) j i"
   apply (simp add: pprt_def)
-  apply (simp add: join_matrix)
+  apply (simp add: sup_matrix_def)
   apply (simp add: Rep_matrix_inject[symmetric])
   apply (rule ext)+
   apply (simp)
@@ -986,7 +986,7 @@
 
 lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (nprt A) j i"
   apply (simp add: nprt_def)
-  apply (simp add: meet_matrix)
+  apply (simp add: inf_matrix_def)
   apply (simp add: Rep_matrix_inject[symmetric])
   apply (rule ext)+
   apply (simp)
diff -r 989182f660e0 -r 8a86fd2a1bf0 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/OrderedGroup.thy	Fri Mar 16 21:32:08 2007 +0100
@@ -1,4 +1,3 @@
-
 (*  Title:   HOL/OrderedGroup.thy
     ID:      $Id$
     Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
@@ -8,7 +7,7 @@
 header {* Ordered Groups *}
 
 theory OrderedGroup
-imports LOrder
+imports Lattices
 uses "~~/src/Provers/Arith/abel_cancel.ML"
 begin
 
@@ -204,7 +203,7 @@
 instance pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add ..
 
 class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +
-  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c + b \<Longrightarrow> a \<sqsubseteq> b"
+  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b \<Longrightarrow> a \<sqsubseteq> b"
 
 class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add
 
@@ -565,13 +564,19 @@
 lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::pordered_ab_group_add))"
 by (simp add: compare_rls)
 
+
 subsection {* Lattice Ordered (Abelian) Groups *}
 
-axclass lordered_ab_group_meet < pordered_ab_group_add, meet_semilorder
+class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice
+
+class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice
 
-axclass lordered_ab_group_join < pordered_ab_group_add, join_semilorder
+class lordered_ab_group = pordered_ab_group_add + lattice
 
-lemma add_inf_distrib_left: "a + (inf b c) = inf (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
+instance lordered_ab_group \<subseteq> lordered_ab_group_meet by default
+instance lordered_ab_group \<subseteq> lordered_ab_group_join by default
+
+lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + (c::'a::{pordered_ab_group_add, lower_semilattice}))"
 apply (rule order_antisym)
 apply (simp_all add: le_infI)
 apply (rule add_le_imp_le_left [of "-a"])
@@ -580,7 +585,7 @@
 apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
 done
 
-lemma add_sup_distrib_left: "a + (sup b c) = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))" 
+lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, upper_semilattice}))" 
 apply (rule order_antisym)
 apply (rule add_le_imp_le_left [of "-a"])
 apply (simp only: add_assoc[symmetric], simp)
@@ -590,55 +595,53 @@
 apply (simp_all)
 done
 
-lemma is_join_neg_inf: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (inf (-a) (-b)))"
-apply (auto simp add: is_join_def)
-apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
-apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
-apply (subst neg_le_iff_le[symmetric]) 
-apply (simp add: le_infI)
-done
-
-lemma is_meet_neg_sup: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (sup (-a) (-b)))"
-apply (auto simp add: is_meet_def)
-apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
-apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
-apply (subst neg_le_iff_le[symmetric]) 
-apply (simp add: le_supI)
-done
-
-axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
-
-instance lordered_ab_group_join \<subseteq> lordered_ab_group
-proof
-  show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_sup)
-qed
-
-instance lordered_ab_group_meet \<subseteq> lordered_ab_group
-proof 
-  show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_inf)
-qed
-
-lemma add_inf_distrib_right: "(inf a b) + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
+lemma add_inf_distrib_right: "inf a b + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
 proof -
-  have "c + (inf a b) = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
+  have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
   thus ?thesis by (simp add: add_commute)
 qed
 
-lemma add_sup_distrib_right: "(sup a b) + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
+lemma add_sup_distrib_right: "sup a b + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
 proof -
-  have "c + (sup a b) = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
+  have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
   thus ?thesis by (simp add: add_commute)
 qed
 
 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
 
-lemma sup_eq_neg_inf: "sup a (b::'a::lordered_ab_group) = - inf (-a) (-b)"
-by (simp add: is_join_unique[OF is_join_join is_join_neg_inf])
+lemma inf_eq_neg_sup: "inf a (b\<Colon>'a\<Colon>lordered_ab_group) = - sup (-a) (-b)"
+proof (rule inf_unique)
+  fix a b :: 'a
+  show "- sup (-a) (-b) \<le> a" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
+    (simp, simp add: add_sup_distrib_left)
+next
+  fix a b :: 'a
+  show "- sup (-a) (-b) \<le> b" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
+    (simp, simp add: add_sup_distrib_left)
+next
+  fix a b c :: 'a
+  assume "a \<le> b" "a \<le> c"
+  then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric])
+    (simp add: le_supI)
+qed
+  
+lemma sup_eq_neg_inf: "sup a (b\<Colon>'a\<Colon>lordered_ab_group) = - inf (-a) (-b)"
+proof (rule sup_unique)
+  fix a b :: 'a
+  show "a \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
+    (simp, simp add: add_inf_distrib_left)
+next
+  fix a b :: 'a
+  show "b \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
+    (simp, simp add: add_inf_distrib_left)
+next
+  fix a b c :: 'a
+  assume "a \<le> c" "b \<le> c"
+  then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric])
+    (simp add: le_infI)
+qed
 
-lemma inf_eq_neg_sup: "inf a (b::'a::lordered_ab_group) = - sup (-a) (-b)"
-by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_sup])
-
-lemma add_eq_inf_sup: "a + b = (sup a b) + (inf a (b::'a::lordered_ab_group))"
+lemma add_eq_inf_sup: "a + b = sup a b + inf a (b\<Colon>'a\<Colon>lordered_ab_group)"
 proof -
   have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
   hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
@@ -761,8 +764,8 @@
   with a show ?thesis by simp 
 qed
 
-axclass lordered_ab_group_abs \<subseteq> lordered_ab_group
-  abs_lattice: "abs x = sup x (-x)"
+class lordered_ab_group_abs = lordered_ab_group +
+  assumes abs_lattice: "abs x = sup x (uminus x)"
 
 lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
 by (simp add: abs_lattice)
@@ -786,7 +789,7 @@
 proof -
   note b = add_le_cancel_right[of a a "-a",symmetric,simplified]
   have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)
-  show ?thesis by (auto simp add: max_def b linorder_not_less join_max)
+  show ?thesis by (auto simp add: max_def b linorder_not_less sup_max)
 qed
 
 lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"
@@ -1131,8 +1134,6 @@
 val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
 val add_inf_distrib_left = thm "add_inf_distrib_left";
 val add_sup_distrib_left = thm "add_sup_distrib_left";
-val is_join_neg_inf = thm "is_join_neg_inf";
-val is_meet_neg_sup = thm "is_meet_neg_sup";
 val add_sup_distrib_right = thm "add_sup_distrib_right";
 val add_inf_distrib_right = thm "add_inf_distrib_right";
 val add_sup_inf_distribs = thms "add_sup_inf_distribs";
diff -r 989182f660e0 -r 8a86fd2a1bf0 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Ring_and_Field.thy	Fri Mar 16 21:32:08 2007 +0100
@@ -265,7 +265,7 @@
 
 instance pordered_ring \<subseteq> pordered_ab_group_add ..
 
-axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
+class lordered_ring = pordered_ring + lordered_ab_group_abs
 
 instance lordered_ring \<subseteq> lordered_ab_group_meet ..
 
@@ -274,9 +274,7 @@
 class abs_if = minus + ord + zero +
   assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
 
-class ordered_ring_strict = ring + ordered_semiring_strict + abs_if
-
-instance ordered_ring_strict \<subseteq> lordered_ab_group ..
+class ordered_ring_strict = ring + ordered_semiring_strict + abs_if + lordered_ab_group
 
 instance ordered_ring_strict \<subseteq> lordered_ring
   by intro_classes (simp add: abs_if sup_eq_if)
@@ -287,7 +285,7 @@
   (*previously ordered_semiring*)
   assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
 
-class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if
+class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if + lordered_ab_group
   (*previously ordered_ring*)
 
 instance ordered_idom \<subseteq> ordered_ring_strict ..