# HG changeset patch # User haftmann # Date 1387989547 -3600 # Node ID a064732223ad8d0db4f1c48f1d6b942c9dcfc00f # Parent 82acc20ded73cbb8386f71bc7a9f3072684aa86c abolished slightly odd global lattice interpretation for min/max diff -r 82acc20ded73 -r a064732223ad NEWS --- 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. diff -r 82acc20ded73 -r a064732223ad src/HOL/IMP/Sec_Typing.thy --- 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') diff -r 82acc20ded73 -r a064732223ad src/HOL/IMP/Sec_TypingT.thy --- 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') diff -r 82acc20ded73 -r a064732223ad src/HOL/Lattices_Big.thy --- 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 \ 'a" ("\\<^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 \ 'a" -where - "Min = semilattice_set.F min" - -definition Max :: "'a set \ '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 \ 'a)" - by (simp add: Inf_fin_def Min_def inf_min) - -lemma Sup_fin_Max: - "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \ '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 \ 'a" +where + "Min = semilattice_set.F min" + +definition Max :: "'a set \ '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 \ 'a)" + by (simp add: Inf_fin_def Min_def inf_min) + +lemma Sup_fin_Max: + "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \ '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 + diff -r 82acc20ded73 -r a064732223ad src/HOL/Matrix_LP/Matrix.thy --- 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)" diff -r 82acc20ded73 -r a064732223ad src/HOL/Metis_Examples/Binary_Tree.thy --- 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. diff -r 82acc20ded73 -r a064732223ad src/HOL/MicroJava/Comp/CorrCompTp.thy --- 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)+