--- a/NEWS Wed Dec 25 17:39:06 2013 +0100
+++ b/NEWS Wed Dec 25 17:39:07 2013 +0100
@@ -28,6 +28,61 @@
*** HOL ***
+* Abolished slightly odd global lattice interpretation for min/max.
+
+Fact consolidations:
+ min_max.inf_assoc ~> min.assoc
+ min_max.inf_commute ~> min.commute
+ min_max.inf_left_commute ~> min.left_commute
+ min_max.inf_idem ~> min.idem
+ min_max.inf_left_idem ~> min.left_idem
+ min_max.inf_right_idem ~> min.right_idem
+ min_max.sup_assoc ~> max.assoc
+ min_max.sup_commute ~> max.commute
+ min_max.sup_left_commute ~> max.left_commute
+ min_max.sup_idem ~> max.idem
+ min_max.sup_left_idem ~> max.left_idem
+ min_max.sup_inf_distrib1 ~> max_min_distrib2
+ min_max.sup_inf_distrib2 ~> max_min_distrib1
+ min_max.inf_sup_distrib1 ~> min_max_distrib2
+ min_max.inf_sup_distrib2 ~> min_max_distrib1
+ min_max.distrib ~> min_max_distribs
+ min_max.inf_absorb1 ~> min.absorb1
+ min_max.inf_absorb2 ~> min.absorb2
+ min_max.sup_absorb1 ~> max.absorb1
+ min_max.sup_absorb2 ~> max.absorb2
+ min_max.le_iff_inf ~> min.absorb_iff1
+ min_max.le_iff_sup ~> max.absorb_iff2
+ min_max.inf_le1 ~> min.cobounded1
+ min_max.inf_le2 ~> min.cobounded2
+ le_maxI1, min_max.sup_ge1 ~> max.cobounded1
+ le_maxI2, min_max.sup_ge2 ~> max.cobounded2
+ min_max.le_infI1 ~> min.coboundedI1
+ min_max.le_infI2 ~> min.coboundedI2
+ min_max.le_supI1 ~> max.coboundedI1
+ min_max.le_supI2 ~> max.coboundedI2
+ min_max.less_infI1 ~> min.strict_coboundedI1
+ min_max.less_infI2 ~> min.strict_coboundedI2
+ min_max.less_supI1 ~> max.strict_coboundedI1
+ min_max.less_supI2 ~> max.strict_coboundedI2
+ min_max.inf_mono ~> min.mono
+ min_max.sup_mono ~> max.mono
+ min_max.le_infI, min_max.inf_greatest ~> min.boundedI
+ min_max.le_supI, min_max.sup_least ~> max.boundedI
+ min_max.le_inf_iff ~> min.bounded_iff
+ min_max.le_sup_iff ~> max.bounded_iff
+
+For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc,
+min.left_commute, min.left_idem, max.commute, max.assoc,
+max.left_commute, max.left_idem directly.
+
+For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2,
+max.cobounded1m max.cobounded2 directly.
+
+For min_ac or max_ac, prefor more general collection ac_simps.
+
+INCOMPATBILITY.
+
* Word library: bit representations prefer type bool over type bit.
INCOMPATIBILITY.
--- a/src/HOL/IMP/Sec_Typing.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/IMP/Sec_Typing.thy Wed Dec 25 17:39:07 2013 +0100
@@ -200,7 +200,7 @@
apply (metis Skip')
apply (metis Assign')
apply (metis Seq')
-apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
+apply (metis max.commute max.absorb_iff2 nat_le_linear If' anti_mono')
by (metis less_or_eq_imp_le max.absorb1 max.absorb2 nat_le_linear While' anti_mono')
--- a/src/HOL/IMP/Sec_TypingT.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/IMP/Sec_TypingT.thy Wed Dec 25 17:39:07 2013 +0100
@@ -190,7 +190,7 @@
apply (metis Skip')
apply (metis Assign')
apply (metis Seq')
-apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
+apply (metis max.commute max.absorb_iff2 nat_le_linear If' anti_mono')
by (metis While')
--- a/src/HOL/Lattices_Big.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Lattices_Big.thy Wed Dec 25 17:39:07 2013 +0100
@@ -308,15 +308,6 @@
subsection {* Lattice operations on finite sets *}
-text {*
- For historic reasons, there is the sublocale dependency from @{class distrib_lattice}
- to @{class linorder}. This is badly designed: both should depend on a common abstract
- distributive lattice rather than having this non-subclass dependecy between two
- classes. But for the moment we have to live with it. This forces us to setup
- this sublocale dependency simultaneously with the lattice operations on finite
- sets, to avoid garbage.
-*}
-
definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
where
"Inf_fin = semilattice_set.F inf"
@@ -325,62 +316,6 @@
where
"Sup_fin = semilattice_set.F sup"
-context linorder
-begin
-
-definition Min :: "'a set \<Rightarrow> 'a"
-where
- "Min = semilattice_set.F min"
-
-definition Max :: "'a set \<Rightarrow> 'a"
-where
- "Max = semilattice_set.F max"
-
-sublocale Min!: semilattice_order_set min less_eq less
- + Max!: semilattice_order_set max greater_eq greater
-where
- "semilattice_set.F min = Min"
- and "semilattice_set.F max = Max"
-proof -
- show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
- then interpret Min!: semilattice_order_set min less_eq less .
- show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
- then interpret Max!: semilattice_order_set max greater_eq greater .
- from Min_def show "semilattice_set.F min = Min" by rule
- from Max_def show "semilattice_set.F max = Max" by rule
-qed
-
-
-text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
-
-sublocale min_max!: distrib_lattice min less_eq less max
-where
- "semilattice_inf.Inf_fin min = Min"
- and "semilattice_sup.Sup_fin max = Max"
-proof -
- show "class.distrib_lattice min less_eq less max"
- proof
- fix x y z
- show "max x (min y z) = min (max x y) (max x z)"
- by (auto simp add: min_def max_def)
- qed (auto simp add: min_def max_def not_le less_imp_le)
- then interpret min_max!: distrib_lattice min less_eq less max .
- show "semilattice_inf.Inf_fin min = Min"
- by (simp only: min_max.Inf_fin_def Min_def)
- show "semilattice_sup.Sup_fin max = Max"
- by (simp only: min_max.Sup_fin_def Max_def)
-qed
-
-lemmas le_maxI1 = max.cobounded1
-lemmas le_maxI2 = max.cobounded2
-lemmas min_ac = min.assoc min.commute min.left_commute
-lemmas max_ac = max.assoc max.commute max.left_commute
-
-end
-
-
-text {* Lattice operations proper *}
-
sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
where
"semilattice_set.F inf = Inf_fin"
@@ -400,18 +335,6 @@
qed
-text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
-
-lemma Inf_fin_Min:
- "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
- by (simp add: Inf_fin_def Min_def inf_min)
-
-lemma Sup_fin_Max:
- "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
- by (simp add: Sup_fin_def Max_def sup_max)
-
-
-
subsection {* Infimum and Supremum over non-empty sets *}
text {*
@@ -550,6 +473,43 @@
context linorder
begin
+definition Min :: "'a set \<Rightarrow> 'a"
+where
+ "Min = semilattice_set.F min"
+
+definition Max :: "'a set \<Rightarrow> 'a"
+where
+ "Max = semilattice_set.F max"
+
+sublocale Min!: semilattice_order_set min less_eq less
+ + Max!: semilattice_order_set max greater_eq greater
+where
+ "semilattice_set.F min = Min"
+ and "semilattice_set.F max = Max"
+proof -
+ show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
+ then interpret Min!: semilattice_order_set min less_eq less .
+ show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
+ then interpret Max!: semilattice_order_set max greater_eq greater .
+ from Min_def show "semilattice_set.F min = Min" by rule
+ from Max_def show "semilattice_set.F max = Max" by rule
+qed
+
+end
+
+text {* An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
+
+lemma Inf_fin_Min:
+ "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
+ by (simp add: Inf_fin_def Min_def inf_min)
+
+lemma Sup_fin_Max:
+ "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
+ by (simp add: Sup_fin_def Max_def sup_max)
+
+context linorder
+begin
+
lemma dual_min:
"ord.min greater_eq = max"
by (auto simp add: ord.min_def max_def fun_eq_iff)
@@ -826,3 +786,4 @@
end
end
+
--- a/src/HOL/Matrix_LP/Matrix.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Matrix_LP/Matrix.thy Wed Dec 25 17:39:07 2013 +0100
@@ -1270,7 +1270,7 @@
apply (simp add: Rep_matrix_inject[THEN sym])
apply (rule ext)+
using assms
- apply (simp add: Rep_mult_matrix max_ac)
+ apply (simp add: Rep_mult_matrix ac_simps)
done
lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"
--- a/src/HOL/Metis_Examples/Binary_Tree.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy Wed Dec 25 17:39:07 2013 +0100
@@ -80,7 +80,7 @@
lemma depth_reflect: "depth (reflect t) = depth t"
apply (induct t)
apply (metis depth.simps(1) reflect.simps(1))
-by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2))
+by (metis depth.simps(2) max.commute reflect.simps(2))
text {*
The famous relationship between the numbers of leaves and nodes.
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Dec 25 17:39:07 2013 +0100
@@ -944,7 +944,7 @@
apply assumption+ apply (rule HOL.refl)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp) add: max_ssize_def)
- apply (simp add: max_of_list_def max_ac)
+ apply (simp add: max_of_list_def ac_simps)
apply arith
apply (simp (no_asm_simp))+
@@ -961,7 +961,7 @@
apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
apply (simp only:)
apply (rule check_type_mono) apply assumption
-apply (simp (no_asm_simp) add: max_ssize_def max_ac)
+apply (simp (no_asm_simp) add: max_ssize_def ac_simps)
apply (simp add: nth_append)
apply (erule conjE)+