abolished slightly odd global lattice interpretation for min/max
authorhaftmann
Wed Dec 25 17:39:07 2013 +0100 (2013-12-25)
changeset 54864a064732223ad
parent 54863 82acc20ded73
child 54865 82bfac35f16f
abolished slightly odd global lattice interpretation for min/max
NEWS
src/HOL/IMP/Sec_Typing.thy
src/HOL/IMP/Sec_TypingT.thy
src/HOL/Lattices_Big.thy
src/HOL/Matrix_LP/Matrix.thy
src/HOL/Metis_Examples/Binary_Tree.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
     1.1 --- a/NEWS	Wed Dec 25 17:39:06 2013 +0100
     1.2 +++ b/NEWS	Wed Dec 25 17:39:07 2013 +0100
     1.3 @@ -28,6 +28,61 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Abolished slightly odd global lattice interpretation for min/max.
     1.8 +
     1.9 +Fact consolidations:
    1.10 +    min_max.inf_assoc ~> min.assoc
    1.11 +    min_max.inf_commute ~> min.commute
    1.12 +    min_max.inf_left_commute ~> min.left_commute
    1.13 +    min_max.inf_idem ~> min.idem
    1.14 +    min_max.inf_left_idem ~> min.left_idem
    1.15 +    min_max.inf_right_idem ~> min.right_idem
    1.16 +    min_max.sup_assoc ~> max.assoc
    1.17 +    min_max.sup_commute ~> max.commute
    1.18 +    min_max.sup_left_commute ~> max.left_commute
    1.19 +    min_max.sup_idem ~> max.idem
    1.20 +    min_max.sup_left_idem ~> max.left_idem
    1.21 +    min_max.sup_inf_distrib1 ~> max_min_distrib2
    1.22 +    min_max.sup_inf_distrib2 ~> max_min_distrib1
    1.23 +    min_max.inf_sup_distrib1 ~> min_max_distrib2
    1.24 +    min_max.inf_sup_distrib2 ~> min_max_distrib1
    1.25 +    min_max.distrib ~> min_max_distribs
    1.26 +    min_max.inf_absorb1 ~> min.absorb1
    1.27 +    min_max.inf_absorb2 ~> min.absorb2
    1.28 +    min_max.sup_absorb1 ~> max.absorb1
    1.29 +    min_max.sup_absorb2 ~> max.absorb2
    1.30 +    min_max.le_iff_inf ~> min.absorb_iff1
    1.31 +    min_max.le_iff_sup ~> max.absorb_iff2
    1.32 +    min_max.inf_le1 ~> min.cobounded1
    1.33 +    min_max.inf_le2 ~> min.cobounded2
    1.34 +    le_maxI1, min_max.sup_ge1 ~> max.cobounded1
    1.35 +    le_maxI2, min_max.sup_ge2 ~> max.cobounded2
    1.36 +    min_max.le_infI1 ~> min.coboundedI1
    1.37 +    min_max.le_infI2 ~> min.coboundedI2
    1.38 +    min_max.le_supI1 ~> max.coboundedI1
    1.39 +    min_max.le_supI2 ~> max.coboundedI2
    1.40 +    min_max.less_infI1 ~> min.strict_coboundedI1
    1.41 +    min_max.less_infI2 ~> min.strict_coboundedI2
    1.42 +    min_max.less_supI1 ~> max.strict_coboundedI1
    1.43 +    min_max.less_supI2 ~> max.strict_coboundedI2
    1.44 +    min_max.inf_mono ~> min.mono
    1.45 +    min_max.sup_mono ~> max.mono
    1.46 +    min_max.le_infI, min_max.inf_greatest ~> min.boundedI
    1.47 +    min_max.le_supI, min_max.sup_least ~> max.boundedI
    1.48 +    min_max.le_inf_iff ~> min.bounded_iff
    1.49 +    min_max.le_sup_iff ~> max.bounded_iff
    1.50 +
    1.51 +For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc,
    1.52 +min.left_commute, min.left_idem, max.commute, max.assoc,
    1.53 +max.left_commute, max.left_idem directly.
    1.54 +
    1.55 +For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2,
    1.56 +max.cobounded1m max.cobounded2 directly.
    1.57 +
    1.58 +For min_ac or max_ac, prefor more general collection ac_simps.
    1.59 +
    1.60 +INCOMPATBILITY. 
    1.61 +
    1.62  * Word library: bit representations prefer type bool over type bit.
    1.63  INCOMPATIBILITY.
    1.64  
     2.1 --- a/src/HOL/IMP/Sec_Typing.thy	Wed Dec 25 17:39:06 2013 +0100
     2.2 +++ b/src/HOL/IMP/Sec_Typing.thy	Wed Dec 25 17:39:07 2013 +0100
     2.3 @@ -200,7 +200,7 @@
     2.4  apply (metis Skip')
     2.5  apply (metis Assign')
     2.6  apply (metis Seq')
     2.7 -apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
     2.8 +apply (metis max.commute max.absorb_iff2 nat_le_linear If' anti_mono')
     2.9  by (metis less_or_eq_imp_le max.absorb1 max.absorb2 nat_le_linear While' anti_mono')
    2.10  
    2.11  
     3.1 --- a/src/HOL/IMP/Sec_TypingT.thy	Wed Dec 25 17:39:06 2013 +0100
     3.2 +++ b/src/HOL/IMP/Sec_TypingT.thy	Wed Dec 25 17:39:07 2013 +0100
     3.3 @@ -190,7 +190,7 @@
     3.4  apply (metis Skip')
     3.5  apply (metis Assign')
     3.6  apply (metis Seq')
     3.7 -apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
     3.8 +apply (metis max.commute max.absorb_iff2 nat_le_linear If' anti_mono')
     3.9  by (metis While')
    3.10  
    3.11  
     4.1 --- a/src/HOL/Lattices_Big.thy	Wed Dec 25 17:39:06 2013 +0100
     4.2 +++ b/src/HOL/Lattices_Big.thy	Wed Dec 25 17:39:07 2013 +0100
     4.3 @@ -308,15 +308,6 @@
     4.4  
     4.5  subsection {* Lattice operations on finite sets *}
     4.6  
     4.7 -text {*
     4.8 -  For historic reasons, there is the sublocale dependency from @{class distrib_lattice}
     4.9 -  to @{class linorder}.  This is badly designed: both should depend on a common abstract
    4.10 -  distributive lattice rather than having this non-subclass dependecy between two
    4.11 -  classes.  But for the moment we have to live with it.  This forces us to setup
    4.12 -  this sublocale dependency simultaneously with the lattice operations on finite
    4.13 -  sets, to avoid garbage.
    4.14 -*}
    4.15 -
    4.16  definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
    4.17  where
    4.18    "Inf_fin = semilattice_set.F inf"
    4.19 @@ -325,62 +316,6 @@
    4.20  where
    4.21    "Sup_fin = semilattice_set.F sup"
    4.22  
    4.23 -context linorder
    4.24 -begin
    4.25 -
    4.26 -definition Min :: "'a set \<Rightarrow> 'a"
    4.27 -where
    4.28 -  "Min = semilattice_set.F min"
    4.29 -
    4.30 -definition Max :: "'a set \<Rightarrow> 'a"
    4.31 -where
    4.32 -  "Max = semilattice_set.F max"
    4.33 -
    4.34 -sublocale Min!: semilattice_order_set min less_eq less
    4.35 -  + Max!: semilattice_order_set max greater_eq greater
    4.36 -where
    4.37 -  "semilattice_set.F min = Min"
    4.38 -  and "semilattice_set.F max = Max"
    4.39 -proof -
    4.40 -  show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
    4.41 -  then interpret Min!: semilattice_order_set min less_eq less .
    4.42 -  show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
    4.43 -  then interpret Max!: semilattice_order_set max greater_eq greater .
    4.44 -  from Min_def show "semilattice_set.F min = Min" by rule
    4.45 -  from Max_def show "semilattice_set.F max = Max" by rule
    4.46 -qed
    4.47 -
    4.48 -
    4.49 -text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
    4.50 -
    4.51 -sublocale min_max!: distrib_lattice min less_eq less max
    4.52 -where
    4.53 -  "semilattice_inf.Inf_fin min = Min"
    4.54 -  and "semilattice_sup.Sup_fin max = Max"
    4.55 -proof -
    4.56 -  show "class.distrib_lattice min less_eq less max"
    4.57 -  proof
    4.58 -    fix x y z
    4.59 -    show "max x (min y z) = min (max x y) (max x z)"
    4.60 -      by (auto simp add: min_def max_def)
    4.61 -  qed (auto simp add: min_def max_def not_le less_imp_le)
    4.62 -  then interpret min_max!: distrib_lattice min less_eq less max .
    4.63 -  show "semilattice_inf.Inf_fin min = Min"
    4.64 -    by (simp only: min_max.Inf_fin_def Min_def)
    4.65 -  show "semilattice_sup.Sup_fin max = Max"
    4.66 -    by (simp only: min_max.Sup_fin_def Max_def)
    4.67 -qed
    4.68 -
    4.69 -lemmas le_maxI1 = max.cobounded1
    4.70 -lemmas le_maxI2 = max.cobounded2
    4.71 -lemmas min_ac = min.assoc min.commute min.left_commute
    4.72 -lemmas max_ac = max.assoc max.commute max.left_commute
    4.73 -
    4.74 -end
    4.75 -
    4.76 -
    4.77 -text {* Lattice operations proper *}
    4.78 -
    4.79  sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
    4.80  where
    4.81    "semilattice_set.F inf = Inf_fin"
    4.82 @@ -400,18 +335,6 @@
    4.83  qed
    4.84  
    4.85  
    4.86 -text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
    4.87 -
    4.88 -lemma Inf_fin_Min:
    4.89 -  "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
    4.90 -  by (simp add: Inf_fin_def Min_def inf_min)
    4.91 -
    4.92 -lemma Sup_fin_Max:
    4.93 -  "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
    4.94 -  by (simp add: Sup_fin_def Max_def sup_max)
    4.95 -
    4.96 -
    4.97 -
    4.98  subsection {* Infimum and Supremum over non-empty sets *}
    4.99  
   4.100  text {*
   4.101 @@ -550,6 +473,43 @@
   4.102  context linorder
   4.103  begin
   4.104  
   4.105 +definition Min :: "'a set \<Rightarrow> 'a"
   4.106 +where
   4.107 +  "Min = semilattice_set.F min"
   4.108 +
   4.109 +definition Max :: "'a set \<Rightarrow> 'a"
   4.110 +where
   4.111 +  "Max = semilattice_set.F max"
   4.112 +
   4.113 +sublocale Min!: semilattice_order_set min less_eq less
   4.114 +  + Max!: semilattice_order_set max greater_eq greater
   4.115 +where
   4.116 +  "semilattice_set.F min = Min"
   4.117 +  and "semilattice_set.F max = Max"
   4.118 +proof -
   4.119 +  show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
   4.120 +  then interpret Min!: semilattice_order_set min less_eq less .
   4.121 +  show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
   4.122 +  then interpret Max!: semilattice_order_set max greater_eq greater .
   4.123 +  from Min_def show "semilattice_set.F min = Min" by rule
   4.124 +  from Max_def show "semilattice_set.F max = Max" by rule
   4.125 +qed
   4.126 +
   4.127 +end
   4.128 +
   4.129 +text {* An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
   4.130 +
   4.131 +lemma Inf_fin_Min:
   4.132 +  "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
   4.133 +  by (simp add: Inf_fin_def Min_def inf_min)
   4.134 +
   4.135 +lemma Sup_fin_Max:
   4.136 +  "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
   4.137 +  by (simp add: Sup_fin_def Max_def sup_max)
   4.138 +
   4.139 +context linorder
   4.140 +begin
   4.141 +
   4.142  lemma dual_min:
   4.143    "ord.min greater_eq = max"
   4.144    by (auto simp add: ord.min_def max_def fun_eq_iff)
   4.145 @@ -826,3 +786,4 @@
   4.146  end
   4.147  
   4.148  end
   4.149 +
     5.1 --- a/src/HOL/Matrix_LP/Matrix.thy	Wed Dec 25 17:39:06 2013 +0100
     5.2 +++ b/src/HOL/Matrix_LP/Matrix.thy	Wed Dec 25 17:39:07 2013 +0100
     5.3 @@ -1270,7 +1270,7 @@
     5.4    apply (simp add: Rep_matrix_inject[THEN sym])
     5.5    apply (rule ext)+
     5.6    using assms
     5.7 -  apply (simp add: Rep_mult_matrix max_ac)
     5.8 +  apply (simp add: Rep_mult_matrix ac_simps)
     5.9    done
    5.10  
    5.11  lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"
     6.1 --- a/src/HOL/Metis_Examples/Binary_Tree.thy	Wed Dec 25 17:39:06 2013 +0100
     6.2 +++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Wed Dec 25 17:39:07 2013 +0100
     6.3 @@ -80,7 +80,7 @@
     6.4  lemma depth_reflect: "depth (reflect t) = depth t"
     6.5  apply (induct t)
     6.6   apply (metis depth.simps(1) reflect.simps(1))
     6.7 -by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2))
     6.8 +by (metis depth.simps(2) max.commute reflect.simps(2))
     6.9  
    6.10  text {*
    6.11  The famous relationship between the numbers of leaves and nodes.
     7.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Dec 25 17:39:06 2013 +0100
     7.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Dec 25 17:39:07 2013 +0100
     7.3 @@ -944,7 +944,7 @@
     7.4    apply assumption+ apply (rule HOL.refl)
     7.5    apply (simp (no_asm_simp))
     7.6    apply (simp (no_asm_simp) add: max_ssize_def)
     7.7 -  apply (simp add: max_of_list_def max_ac)
     7.8 +  apply (simp add: max_of_list_def ac_simps)
     7.9    apply arith
    7.10    apply (simp (no_asm_simp))+
    7.11  
    7.12 @@ -961,7 +961,7 @@
    7.13  apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
    7.14  apply (simp only:)
    7.15  apply (rule check_type_mono) apply assumption
    7.16 -apply (simp (no_asm_simp) add: max_ssize_def max_ac)
    7.17 +apply (simp (no_asm_simp) add: max_ssize_def ac_simps)
    7.18  apply (simp add: nth_append)
    7.19  
    7.20  apply (erule conjE)+