# HG changeset patch
# User haftmann
# Date 1364055066 -3600
# Node ID f4bfdee993045e99b1061f83b9b9eed7bb0f63dc
# Parent  0a0c9a45d294459c6c60fb3f4dfd7c71a8bf753e
locales for abstract orders

diff -r 0a0c9a45d294 -r f4bfdee99304 CONTRIBUTORS
--- a/CONTRIBUTORS	Sat Mar 23 07:30:53 2013 +0100
+++ b/CONTRIBUTORS	Sat Mar 23 17:11:06 2013 +0100
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* March 2013: Florian Haftmann, TUM
+  Algebraic locale hierarchy for orderings and (semi)lattices.
+
 * Feb. 2013: Florian Haftmann, TUM
   Reworking and consolidation of code generation for target
   language numerals.
diff -r 0a0c9a45d294 -r f4bfdee99304 NEWS
--- a/NEWS	Sat Mar 23 07:30:53 2013 +0100
+++ b/NEWS	Sat Mar 23 17:11:06 2013 +0100
@@ -33,6 +33,8 @@
 
 *** HOL ***
 
+* Locale hierarchy for abstract orderings and (semi)lattices.
+
 * Discontinued theory src/HOL/Library/Eval_Witness.
 INCOMPATIBILITY.
 
diff -r 0a0c9a45d294 -r f4bfdee99304 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Mar 23 07:30:53 2013 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Mar 23 17:11:06 2013 +0100
@@ -1280,8 +1280,16 @@
 
 end
 
+class ab_semigroup_idem_mult = ab_semigroup_mult +
+  assumes mult_idem: "x * x = x"
+
+sublocale ab_semigroup_idem_mult < times!: semilattice times proof
+qed (fact mult_idem)
+
 context ab_semigroup_idem_mult
 begin
+ 
+lemmas mult_left_idem = times.left_idem
 
 lemma comp_fun_idem: "comp_fun_idem (op *)"
   by default (simp_all add: fun_eq_iff mult_left_commute)
diff -r 0a0c9a45d294 -r f4bfdee99304 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat Mar 23 07:30:53 2013 +0100
+++ b/src/HOL/Lattices.thy	Sat Mar 23 17:11:06 2013 +0100
@@ -11,39 +11,134 @@
 subsection {* Abstract semilattice *}
 
 text {*
-  This locales provide a basic structure for interpretation into
+  These locales provide a basic structure for interpretation into
   bigger structures;  extensions require careful thinking, otherwise
   undesired effects may occur due to interpretation.
 *}
 
+no_notation times (infixl "*" 70)
+no_notation Groups.one ("1")
+
 locale semilattice = abel_semigroup +
-  assumes idem [simp]: "f a a = a"
+  assumes idem [simp]: "a * a = a"
 begin
 
-lemma left_idem [simp]: "f a (f a b) = f a b"
+lemma left_idem [simp]: "a * (a * b) = a * b"
 by (simp add: assoc [symmetric])
 
-lemma right_idem [simp]: "f (f a b) b = f a b"
+lemma right_idem [simp]: "(a * b) * b = a * b"
 by (simp add: assoc)
 
 end
 
+locale semilattice_neutr = semilattice + comm_monoid
 
-subsection {* Idempotent semigroup *}
+locale semilattice_order = semilattice +
+  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
+    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
+  assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
+    and semilattice_strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
+begin
+
+lemma orderI:
+  "a = a * b \<Longrightarrow> a \<preceq> b"
+  by (simp add: order_iff)
+
+lemma orderE:
+  assumes "a \<preceq> b"
+  obtains "a = a * b"
+  using assms by (unfold order_iff)
+
+end
 
-class ab_semigroup_idem_mult = ab_semigroup_mult +
-  assumes mult_idem: "x * x = x"
+sublocale semilattice_order < ordering less_eq less
+proof
+  fix a b
+  show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
+    by (fact semilattice_strict_iff_order)
+next
+  fix a
+  show "a \<preceq> a"
+    by (simp add: order_iff)
+next
+  fix a b
+  assume "a \<preceq> b" "b \<preceq> a"
+  then have "a = a * b" "a * b = b"
+    by (simp_all add: order_iff commute)
+  then show "a = b" by simp
+next
+  fix a b c
+  assume "a \<preceq> b" "b \<preceq> c"
+  then have "a = a * b" "b = b * c"
+    by (simp_all add: order_iff commute)
+  then have "a = a * (b * c)"
+    by simp
+  then have "a = (a * b) * c"
+    by (simp add: assoc)
+  with `a = a * b` [symmetric] have "a = a * c" by simp
+  then show "a \<preceq> c" by (rule orderI)
+qed
 
-sublocale ab_semigroup_idem_mult < times!: semilattice times proof
-qed (fact mult_idem)
-
-context ab_semigroup_idem_mult
+context semilattice_order
 begin
 
-lemmas mult_left_idem = times.left_idem
+lemma cobounded1 [simp]:
+  "a * b \<preceq> a"
+  by (simp add: order_iff commute)  
+
+lemma cobounded2 [simp]:
+  "a * b \<preceq> b"
+  by (simp add: order_iff)
+
+lemma boundedI:
+  assumes "a \<preceq> b" and "a \<preceq> c"
+  shows "a \<preceq> b * c"
+proof (rule orderI)
+  from assms obtain "a * b = a" and "a * c = a" by (auto elim!: orderE)
+  then show "a = a * (b * c)" by (simp add: assoc [symmetric])
+qed
+
+lemma boundedE:
+  assumes "a \<preceq> b * c"
+  obtains "a \<preceq> b" and "a \<preceq> c"
+  using assms by (blast intro: trans cobounded1 cobounded2)
+
+lemma bounded_iff:
+  "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c"
+  by (blast intro: boundedI elim: boundedE)
+
+lemma strict_boundedE:
+  assumes "a \<prec> b * c"
+  obtains "a \<prec> b" and "a \<prec> c"
+  using assms by (auto simp add: commute strict_iff_order bounded_iff elim: orderE intro!: that)+
+
+lemma coboundedI1:
+  "a \<preceq> c \<Longrightarrow> a * b \<preceq> c"
+  by (rule trans) auto
+
+lemma coboundedI2:
+  "b \<preceq> c \<Longrightarrow> a * b \<preceq> c"
+  by (rule trans) auto
+
+lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d"
+  by (blast intro: boundedI coboundedI1 coboundedI2)
+
+lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a"
+  by (rule antisym) (auto simp add: refl bounded_iff)
+
+lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b"
+  by (rule antisym) (auto simp add: refl bounded_iff)
 
 end
 
+locale semilattice_neutr_order = semilattice_neutr + semilattice_order
+
+sublocale semilattice_neutr_order < ordering_top less_eq less 1
+  by default (simp add: order_iff)
+
+notation times (infixl "*" 70)
+notation Groups.one ("1")
+
 
 subsection {* Syntactic infimum and supremum operations *}
 
@@ -171,6 +266,23 @@
     by (rule antisym) auto
 qed
 
+sublocale semilattice_sup < sup!: semilattice sup
+proof
+  fix a b c
+  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
+    by (rule antisym) (auto intro: le_supI1 le_supI2)
+  show "a \<squnion> b = b \<squnion> a"
+    by (rule antisym) auto
+  show "a \<squnion> a = a"
+    by (rule antisym) auto
+qed
+
+sublocale semilattice_inf < inf!: semilattice_order inf less_eq less
+  by default (auto simp add: le_iff_inf less_le)
+
+sublocale semilattice_sup < sup!: semilattice_order sup greater_eq greater
+  by default (auto simp add: le_iff_sup sup.commute less_le)
+
 context semilattice_inf
 begin
 
@@ -202,17 +314,6 @@
 
 end
 
-sublocale semilattice_sup < sup!: semilattice sup
-proof
-  fix a b c
-  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
-    by (rule antisym) (auto intro: le_supI1 le_supI2)
-  show "a \<squnion> b = b \<squnion> a"
-    by (rule antisym) auto
-  show "a \<squnion> a = a"
-    by (rule antisym) auto
-qed
-
 context semilattice_sup
 begin
 
@@ -367,9 +468,33 @@
 
 subsection {* Bounded lattices and boolean algebras *}
 
+class bounded_semilattice_inf_top = semilattice_inf + top
+
+sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
+proof
+  fix x
+  show "x \<sqinter> \<top> = x"
+    by (rule inf_absorb1) simp
+qed
+
+sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr_order inf top less_eq less ..
+
+class bounded_semilattice_sup_bot = semilattice_sup + bot
+
+sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
+proof
+  fix x
+  show "x \<squnion> \<bottom> = x"
+    by (rule sup_absorb1) simp
+qed
+
+sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr_order sup bot greater_eq greater ..
+
 class bounded_lattice_bot = lattice + bot
 begin
 
+subclass bounded_semilattice_sup_bot ..
+
 lemma inf_bot_left [simp]:
   "\<bottom> \<sqinter> x = \<bottom>"
   by (rule inf_absorb1) simp
@@ -378,13 +503,13 @@
   "x \<sqinter> \<bottom> = \<bottom>"
   by (rule inf_absorb2) simp
 
-lemma sup_bot_left [simp]:
+lemma sup_bot_left:
   "\<bottom> \<squnion> x = x"
-  by (rule sup_absorb2) simp
+  by (fact sup_bot.left_neutral)
 
-lemma sup_bot_right [simp]:
+lemma sup_bot_right:
   "x \<squnion> \<bottom> = x"
-  by (rule sup_absorb1) simp
+  by (fact sup_bot.right_neutral)
 
 lemma sup_eq_bot_iff [simp]:
   "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
@@ -395,6 +520,8 @@
 class bounded_lattice_top = lattice + top
 begin
 
+subclass bounded_semilattice_inf_top ..
+
 lemma sup_top_left [simp]:
   "\<top> \<squnion> x = \<top>"
   by (rule sup_absorb1) simp
@@ -403,13 +530,13 @@
   "x \<squnion> \<top> = \<top>"
   by (rule sup_absorb2) simp
 
-lemma inf_top_left [simp]:
+lemma inf_top_left:
   "\<top> \<sqinter> x = x"
-  by (rule inf_absorb2) simp
+  by (fact inf_top.left_neutral)
 
-lemma inf_top_right [simp]:
+lemma inf_top_right:
   "x \<sqinter> \<top> = x"
-  by (rule inf_absorb1) simp
+  by (fact inf_top.right_neutral)
 
 lemma inf_eq_top_iff [simp]:
   "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
@@ -417,9 +544,12 @@
 
 end
 
-class bounded_lattice = bounded_lattice_bot + bounded_lattice_top
+class bounded_lattice = lattice + bot + top
 begin
 
+subclass bounded_lattice_bot ..
+subclass bounded_lattice_top ..
+
 lemma dual_bounded_lattice:
   "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
   by unfold_locales (auto simp add: less_le_not_le)
diff -r 0a0c9a45d294 -r f4bfdee99304 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Mar 23 07:30:53 2013 +0100
+++ b/src/HOL/Orderings.thy	Sat Mar 23 17:11:06 2013 +0100
@@ -12,6 +12,79 @@
 ML_file "~~/src/Provers/order.ML"
 ML_file "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
 
+subsection {* Abstract ordering *}
+
+locale ordering =
+  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
+   and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
+  assumes strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
+  assumes refl: "a \<preceq> a" -- {* not @{text iff}: makes problems due to multiple (dual) interpretations *}
+    and antisym: "a \<preceq> b \<Longrightarrow> b \<preceq> a \<Longrightarrow> a = b"
+    and trans: "a \<preceq> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<preceq> c"
+begin
+
+lemma strict_implies_order:
+  "a \<prec> b \<Longrightarrow> a \<preceq> b"
+  by (simp add: strict_iff_order)
+
+lemma strict_implies_not_eq:
+  "a \<prec> b \<Longrightarrow> a \<noteq> b"
+  by (simp add: strict_iff_order)
+
+lemma not_eq_order_implies_strict:
+  "a \<noteq> b \<Longrightarrow> a \<preceq> b \<Longrightarrow> a \<prec> b"
+  by (simp add: strict_iff_order)
+
+lemma order_iff_strict:
+  "a \<preceq> b \<longleftrightarrow> a \<prec> b \<or> a = b"
+  by (auto simp add: strict_iff_order refl)
+
+lemma irrefl: -- {* not @{text iff}: makes problems due to multiple (dual) interpretations *}
+  "\<not> a \<prec> a"
+  by (simp add: strict_iff_order)
+
+lemma asym:
+  "a \<prec> b \<Longrightarrow> b \<prec> a \<Longrightarrow> False"
+  by (auto simp add: strict_iff_order intro: antisym)
+
+lemma strict_trans1:
+  "a \<preceq> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
+  by (auto simp add: strict_iff_order intro: trans antisym)
+
+lemma strict_trans2:
+  "a \<prec> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<prec> c"
+  by (auto simp add: strict_iff_order intro: trans antisym)
+
+lemma strict_trans:
+  "a \<prec> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
+  by (auto intro: strict_trans1 strict_implies_order)
+
+end
+
+locale ordering_top = ordering +
+  fixes top :: "'a"
+  assumes extremum [simp]: "a \<preceq> top"
+begin
+
+lemma extremum_uniqueI:
+  "top \<preceq> a \<Longrightarrow> a = top"
+  by (rule antisym) auto
+
+lemma extremum_unique:
+  "top \<preceq> a \<longleftrightarrow> a = top"
+  by (auto intro: antisym)
+
+lemma extremum_strict [simp]:
+  "\<not> (top \<prec> a)"
+  using extremum [of a] by (auto simp add: order_iff_strict intro: asym irrefl)
+
+lemma not_eq_extremum:
+  "a \<noteq> top \<longleftrightarrow> a \<prec> top"
+  by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum)
+
+end  
+
+
 subsection {* Syntactic orders *}
 
 class ord =
@@ -119,10 +192,21 @@
   assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
 begin
 
-text {* Reflexivity. *}
+lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
+  by (auto simp add: less_le_not_le intro: antisym)
+
+end
+
+sublocale order < order!: ordering less_eq less
+  by default (auto intro: antisym order_trans simp add: less_le)
 
-lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
-by (auto simp add: less_le_not_le intro: antisym)
+sublocale order < dual_order!: ordering greater_eq greater
+  by default (auto intro: antisym order_trans simp add: less_le)
+
+context order
+begin
+
+text {* Reflexivity. *}
 
 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
     -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
@@ -1089,46 +1173,59 @@
 
 class bot = order +
   fixes bot :: 'a ("\<bottom>")
-  assumes bot_least [simp]: "\<bottom> \<le> a"
+  assumes bot_least: "\<bottom> \<le> a"
+
+sublocale bot < bot!: ordering_top greater_eq greater bot
+proof
+qed (fact bot_least)
+
+context bot
 begin
 
 lemma le_bot:
   "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
-  by (auto intro: antisym)
+  by (fact bot.extremum_uniqueI)
 
 lemma bot_unique:
   "a \<le> \<bottom> \<longleftrightarrow> a = \<bottom>"
-  by (auto intro: antisym)
+  by (fact bot.extremum_unique)
 
-lemma not_less_bot [simp]:
-  "\<not> (a < \<bottom>)"
-  using bot_least [of a] by (auto simp: le_less)
+lemma not_less_bot:
+  "\<not> a < \<bottom>"
+  by (fact bot.extremum_strict)
 
 lemma bot_less:
   "a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a"
-  by (auto simp add: less_le_not_le intro!: antisym)
+  by (fact bot.not_eq_extremum)
 
 end
 
 class top = order +
   fixes top :: 'a ("\<top>")
-  assumes top_greatest [simp]: "a \<le> \<top>"
+  assumes top_greatest: "a \<le> \<top>"
+
+sublocale top < top!: ordering_top less_eq less top
+proof
+qed (fact top_greatest)
+
+context top
 begin
 
 lemma top_le:
   "\<top> \<le> a \<Longrightarrow> a = \<top>"
-  by (rule antisym) auto
+  by (fact top.extremum_uniqueI)
 
 lemma top_unique:
   "\<top> \<le> a \<longleftrightarrow> a = \<top>"
-  by (auto intro: antisym)
+  by (fact top.extremum_unique)
 
-lemma not_top_less [simp]: "\<not> (\<top> < a)"
-  using top_greatest [of a] by (auto simp: le_less)
+lemma not_top_less:
+  "\<not> \<top> < a"
+  by (fact top.extremum_strict)
 
 lemma less_top:
   "a \<noteq> \<top> \<longleftrightarrow> a < \<top>"
-  by (auto simp add: less_le_not_le intro!: antisym)
+  by (fact top.not_eq_extremum)
 
 end
 
@@ -1489,3 +1586,4 @@
 lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
 
 end
+