--- 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.
--- 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.
--- 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)
--- 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)
--- 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
+