prefer more canonical names for lemmas on min/max
authorhaftmann
Wed Dec 25 17:39:06 2013 +0100 (2013-12-25)
changeset 5486382acc20ded73
parent 54862 c65e5cbdbc97
child 54864 a064732223ad
prefer more canonical names for lemmas on min/max
src/HOL/Algebra/UnivPoly.thy
src/HOL/Bali/Evaln.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/HOLCF/Completion.thy
src/HOL/HOLCF/Library/List_Cpo.thy
src/HOL/HOLCF/Pcpo.thy
src/HOL/HOLCF/Universal.thy
src/HOL/Hoare_Parallel/Graph.thy
src/HOL/IMP/Sec_Typing.thy
src/HOL/IMP/Sec_TypingT.thy
src/HOL/Import/HOL_Light_Maps.thy
src/HOL/Int.thy
src/HOL/Lattices_Big.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Lattice_Algebras.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Product_Lexorder.thy
src/HOL/Library/Saturated.thy
src/HOL/Limits.thy
src/HOL/List.thy
src/HOL/Metis_Examples/Big_O.thy
src/HOL/MicroJava/BV/Effect.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/MicroJava/DFA/LBVSpec.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NanoJava/OpSem.thy
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/UNITY/Simple/Common.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Bool_List_Representation.thy
src/HOL/Word/Misc_Numeric.thy
src/HOL/Word/Word.thy
src/HOL/ex/Dedekind_Real.thy
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Wed Dec 25 17:39:06 2013 +0100
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Dec 25 17:39:06 2013 +0100
     1.3 @@ -1252,7 +1252,7 @@
     1.4            h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
     1.5          (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q} \<union> {deg R q<..max (deg R p) (deg R q)}.
     1.6            h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
     1.7 -      by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
     1.8 +      by (simp only: ivl_disj_un_one max.cobounded1 max.cobounded2)
     1.9      also from R S have "... =
    1.10        (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
    1.11        (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
     2.1 --- a/src/HOL/Bali/Evaln.thy	Wed Dec 25 17:39:06 2013 +0100
     2.2 +++ b/src/HOL/Bali/Evaln.thy	Wed Dec 25 17:39:06 2013 +0100
     2.3 @@ -459,7 +459,7 @@
     2.4  
     2.5  lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2')\<rbrakk> \<Longrightarrow> 
     2.6               G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1') \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2')"
     2.7 -by (fast intro: le_maxI1 le_maxI2)
     2.8 +by (fast intro: max.cobounded1 max.cobounded2)
     2.9  
    2.10  corollary evaln_max2E [consumes 2]:
    2.11    "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); 
    2.12 @@ -473,7 +473,7 @@
    2.13   G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2') \<and> 
    2.14   G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')"
    2.15  apply (drule (1) evaln_max2, erule thin_rl)
    2.16 -apply (fast intro!: le_maxI1 le_maxI2)
    2.17 +apply (fast intro!: max.cobounded1 max.cobounded2)
    2.18  done
    2.19  
    2.20  corollary evaln_max3E: 
    2.21 @@ -489,10 +489,10 @@
    2.22  lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
    2.23  proof -
    2.24    have "n2 \<le> max n2 n3"
    2.25 -    by (rule le_maxI1)
    2.26 +    by (rule max.cobounded1)
    2.27    also
    2.28    have "max n2 n3 \<le> max n1 (max n2 n3)"
    2.29 -    by (rule le_maxI2)
    2.30 +    by (rule max.cobounded2)
    2.31    finally
    2.32    show ?thesis .
    2.33  qed
    2.34 @@ -500,10 +500,10 @@
    2.35  lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
    2.36  proof -
    2.37    have "n3 \<le> max n2 n3"
    2.38 -    by (rule le_maxI2)
    2.39 +    by (rule max.cobounded2)
    2.40    also
    2.41    have "max n2 n3 \<le> max n1 (max n2 n3)"
    2.42 -    by (rule le_maxI2)
    2.43 +    by (rule max.cobounded2)
    2.44    finally
    2.45    show ?thesis .
    2.46  qed
    2.47 @@ -568,13 +568,13 @@
    2.48          then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
    2.49                G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
    2.50          else s3 = s1"
    2.51 -    by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
    2.52 +    by simp (iprover intro: evaln_nonstrict max.cobounded1 max.cobounded2)
    2.53    ultimately
    2.54    have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
    2.55      apply -
    2.56      apply (rule evaln.Loop)
    2.57 -    apply   (iprover intro: evaln_nonstrict intro: le_maxI1)
    2.58 -    apply   (auto intro: evaln_nonstrict intro: le_maxI2)
    2.59 +    apply   (iprover intro: evaln_nonstrict intro: max.cobounded1)
    2.60 +    apply   (auto intro: evaln_nonstrict intro: max.cobounded2)
    2.61      done
    2.62    then show ?case ..
    2.63  next
    2.64 @@ -603,7 +603,7 @@
    2.65      by fastforce 
    2.66    ultimately
    2.67    have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
    2.68 -    by (auto intro!: evaln.Try le_maxI1 le_maxI2)
    2.69 +    by (auto intro!: evaln.Try max.cobounded1 max.cobounded2)
    2.70    then show ?case ..
    2.71  next
    2.72    case (Fin s0 c1 x1 s1 c2 s2 s3)
    2.73 @@ -629,7 +629,7 @@
    2.74                \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
    2.75                     G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
    2.76                     s3 = restore_lvars s1 s2)"
    2.77 -    by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
    2.78 +    by (auto intro: evaln_nonstrict max.cobounded1 max.cobounded2)
    2.79    ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
    2.80      by (rule evaln.Init)
    2.81    then show ?case ..
    2.82 @@ -755,7 +755,7 @@
    2.83    ultimately
    2.84    have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
    2.85              (set_lvars (locals (store s2))) s4"
    2.86 -    by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
    2.87 +    by (auto intro!: evaln.Call max.cobounded1 le_max3I1 le_max3I2)
    2.88    thus ?case ..
    2.89  next
    2.90    case (Methd s0 D sig v s1)
     3.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Dec 25 17:39:06 2013 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Dec 25 17:39:06 2013 +0100
     3.3 @@ -444,7 +444,7 @@
     3.4    assumes g0: "numgcd t = 0"
     3.5    shows "Inum bs t = 0"
     3.6    using g0[simplified numgcd_def] 
     3.7 -  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos min_max.sup_absorb2)
     3.8 +  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos max.absorb2)
     3.9  
    3.10  lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
    3.11    using gp
     4.1 --- a/src/HOL/HOLCF/Completion.thy	Wed Dec 25 17:39:06 2013 +0100
     4.2 +++ b/src/HOL/HOLCF/Completion.thy	Wed Dec 25 17:39:06 2013 +0100
     4.3 @@ -62,8 +62,8 @@
     4.4   apply (rule idealI)
     4.5     apply (cut_tac idealD1 [OF ideal_A], fast)
     4.6    apply (clarify, rename_tac i j)
     4.7 -  apply (drule subsetD [OF chain_A [OF le_maxI1]])
     4.8 -  apply (drule subsetD [OF chain_A [OF le_maxI2]])
     4.9 +  apply (drule subsetD [OF chain_A [OF max.cobounded1]])
    4.10 +  apply (drule subsetD [OF chain_A [OF max.cobounded2]])
    4.11    apply (drule (1) idealD2 [OF ideal_A])
    4.12    apply blast
    4.13   apply clarify
     5.1 --- a/src/HOL/HOLCF/Library/List_Cpo.thy	Wed Dec 25 17:39:06 2013 +0100
     5.2 +++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Wed Dec 25 17:39:06 2013 +0100
     5.3 @@ -273,8 +273,8 @@
     5.4  apply (erule list_chain_cases)
     5.5  apply (auto simp add: lub_Cons dest!: compactD2)
     5.6  apply (rename_tac i j, rule_tac x="max i j" in exI)
     5.7 -apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI1]])
     5.8 -apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI2]])
     5.9 +apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded1]])
    5.10 +apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded2]])
    5.11  apply (erule (1) conjI)
    5.12  done
    5.13  
     6.1 --- a/src/HOL/HOLCF/Pcpo.thy	Wed Dec 25 17:39:06 2013 +0100
     6.2 +++ b/src/HOL/HOLCF/Pcpo.thy	Wed Dec 25 17:39:06 2013 +0100
     6.3 @@ -118,8 +118,8 @@
     6.4      apply (rule lub_below [OF 2])
     6.5      apply (rule below_lub [OF 3])
     6.6      apply (rule below_trans)
     6.7 -    apply (rule chain_mono [OF 1 le_maxI1])
     6.8 -    apply (rule chain_mono [OF 2 le_maxI2])
     6.9 +    apply (rule chain_mono [OF 1 max.cobounded1])
    6.10 +    apply (rule chain_mono [OF 2 max.cobounded2])
    6.11      done
    6.12    show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
    6.13      apply (rule lub_mono [OF 3 4])
     7.1 --- a/src/HOL/HOLCF/Universal.thy	Wed Dec 25 17:39:06 2013 +0100
     7.2 +++ b/src/HOL/HOLCF/Universal.thy	Wed Dec 25 17:39:06 2013 +0100
     7.3 @@ -802,7 +802,7 @@
     7.4        by (simp add: approximants_def approx_below)
     7.5      moreover from x y have "x \<sqsubseteq> ?z \<and> y \<sqsubseteq> ?z"
     7.6        by (simp add: approximants_def compact_le_def)
     7.7 -         (metis i j monofun_cfun chain_mono chain_approx le_maxI1 le_maxI2)
     7.8 +         (metis i j monofun_cfun chain_mono chain_approx max.cobounded1 max.cobounded2)
     7.9      ultimately show "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" ..
    7.10    next
    7.11      fix x y :: "'a compact_basis"
     8.1 --- a/src/HOL/Hoare_Parallel/Graph.thy	Wed Dec 25 17:39:06 2013 +0100
     8.2 +++ b/src/HOL/Hoare_Parallel/Graph.thy	Wed Dec 25 17:39:06 2013 +0100
     8.3 @@ -182,7 +182,7 @@
     8.4  
     8.5  subsubsection{* Graph 3 *}
     8.6  
     8.7 -declare min_max.inf_absorb1 [simp] min_max.inf_absorb2 [simp]
     8.8 +declare min.absorb1 [simp] min.absorb2 [simp]
     8.9  
    8.10  lemma Graph3: 
    8.11    "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
    8.12 @@ -304,7 +304,7 @@
    8.13  apply force
    8.14  done
    8.15  
    8.16 -declare min_max.inf_absorb1 [simp del] min_max.inf_absorb2 [simp del]
    8.17 +declare min.absorb1 [simp del] min.absorb2 [simp del]
    8.18  
    8.19  subsubsection {* Graph 5 *}
    8.20  
     9.1 --- a/src/HOL/IMP/Sec_Typing.thy	Wed Dec 25 17:39:06 2013 +0100
     9.2 +++ b/src/HOL/IMP/Sec_Typing.thy	Wed Dec 25 17:39:06 2013 +0100
     9.3 @@ -48,19 +48,19 @@
     9.4  next
     9.5    case (IfTrue b s c1)
     9.6    hence "max (sec b) l \<turnstile> c1" by auto
     9.7 -  hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
     9.8 +  hence "l \<turnstile> c1" by (metis max.cobounded2 anti_mono)
     9.9    thus ?case using IfTrue.IH by metis
    9.10  next
    9.11    case (IfFalse b s c2)
    9.12    hence "max (sec b) l \<turnstile> c2" by auto
    9.13 -  hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
    9.14 +  hence "l \<turnstile> c2" by (metis max.cobounded2 anti_mono)
    9.15    thus ?case using IfFalse.IH by metis
    9.16  next
    9.17    case WhileFalse thus ?case by auto
    9.18  next
    9.19    case (WhileTrue b s1 c)
    9.20    hence "max (sec b) l \<turnstile> c" by auto
    9.21 -  hence "l \<turnstile> c" by (metis le_maxI2 anti_mono)
    9.22 +  hence "l \<turnstile> c" by (metis max.cobounded2 anti_mono)
    9.23    thus ?case using WhileTrue by metis
    9.24  qed
    9.25  
    9.26 @@ -200,8 +200,8 @@
    9.27  apply (metis Skip')
    9.28  apply (metis Assign')
    9.29  apply (metis Seq')
    9.30 -apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
    9.31 -by (metis less_or_eq_imp_le min_max.sup_absorb1 min_max.sup_absorb2 nat_le_linear While' anti_mono')
    9.32 +apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
    9.33 +by (metis less_or_eq_imp_le max.absorb1 max.absorb2 nat_le_linear While' anti_mono')
    9.34  
    9.35  
    9.36  lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
    9.37 @@ -209,8 +209,8 @@
    9.38  apply (metis Skip)
    9.39  apply (metis Assign)
    9.40  apply (metis Seq)
    9.41 -apply (metis min_max.sup_absorb2 If)
    9.42 -apply (metis min_max.sup_absorb2 While)
    9.43 +apply (metis max.absorb2 If)
    9.44 +apply (metis max.absorb2 While)
    9.45  by (metis anti_mono)
    9.46  
    9.47  subsection "A Bottom-Up Typing System"
    9.48 @@ -233,15 +233,15 @@
    9.49  apply(induction rule: sec_type2.induct)
    9.50  apply (metis Skip')
    9.51  apply (metis Assign' eq_imp_le)
    9.52 -apply (metis Seq' anti_mono' min_max.inf_le1 min_max.inf_le2)
    9.53 -apply (metis If' anti_mono' min_max.inf_absorb2 min_max.le_iff_inf nat_le_linear)
    9.54 +apply (metis Seq' anti_mono' min.cobounded1 min.cobounded2)
    9.55 +apply (metis If' anti_mono' min.absorb2 min.absorb_iff1 nat_le_linear)
    9.56  by (metis While')
    9.57  
    9.58  lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
    9.59  apply(induction rule: sec_type'.induct)
    9.60  apply (metis Skip2 le_refl)
    9.61  apply (metis Assign2)
    9.62 -apply (metis Seq2 min_max.inf_greatest)
    9.63 +apply (metis Seq2 min.boundedI)
    9.64  apply (metis If2 inf_greatest inf_nat_def le_trans)
    9.65  apply (metis While2 le_trans)
    9.66  by (metis le_trans)
    10.1 --- a/src/HOL/IMP/Sec_TypingT.thy	Wed Dec 25 17:39:06 2013 +0100
    10.2 +++ b/src/HOL/IMP/Sec_TypingT.thy	Wed Dec 25 17:39:06 2013 +0100
    10.3 @@ -41,12 +41,12 @@
    10.4  next
    10.5    case (IfTrue b s c1)
    10.6    hence "max (sec b) l \<turnstile> c1" by auto
    10.7 -  hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
    10.8 +  hence "l \<turnstile> c1" by (metis max.cobounded2 anti_mono)
    10.9    thus ?case using IfTrue.IH by metis
   10.10  next
   10.11    case (IfFalse b s c2)
   10.12    hence "max (sec b) l \<turnstile> c2" by auto
   10.13 -  hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
   10.14 +  hence "l \<turnstile> c2" by (metis max.cobounded2 anti_mono)
   10.15    thus ?case using IfFalse.IH by metis
   10.16  next
   10.17    case WhileFalse thus ?case by auto
   10.18 @@ -61,7 +61,7 @@
   10.19  apply (metis big_step.Skip)
   10.20  apply (metis big_step.Assign)
   10.21  apply (metis big_step.Seq)
   10.22 -apply (metis IfFalse IfTrue le0 le_antisym le_maxI2)
   10.23 +apply (metis IfFalse IfTrue le0 le_antisym max.cobounded2)
   10.24  apply simp
   10.25  done
   10.26  
   10.27 @@ -190,7 +190,7 @@
   10.28  apply (metis Skip')
   10.29  apply (metis Assign')
   10.30  apply (metis Seq')
   10.31 -apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
   10.32 +apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
   10.33  by (metis While')
   10.34  
   10.35  
   10.36 @@ -200,7 +200,7 @@
   10.37  apply (metis Skip)
   10.38  apply (metis Assign)
   10.39  apply (metis Seq)
   10.40 -apply (metis min_max.sup_absorb2 If)
   10.41 +apply (metis max.absorb2 If)
   10.42  apply (metis While)
   10.43  by (metis anti_mono)
   10.44  
    11.1 --- a/src/HOL/Import/HOL_Light_Maps.thy	Wed Dec 25 17:39:06 2013 +0100
    11.2 +++ b/src/HOL/Import/HOL_Light_Maps.thy	Wed Dec 25 17:39:06 2013 +0100
    11.3 @@ -175,11 +175,11 @@
    11.4  
    11.5  lemma DEF_MAX[import_const "MAX"]:
    11.6    "max = (\<lambda>x y :: nat. if x \<le> y then y else x)"
    11.7 -  by (auto simp add: min_max.le_iff_sup fun_eq_iff)
    11.8 +  by (auto simp add: max.absorb_iff2 fun_eq_iff)
    11.9  
   11.10  lemma DEF_MIN[import_const "MIN"]:
   11.11    "min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
   11.12 -  by (auto simp add: min_max.le_iff_inf fun_eq_iff)
   11.13 +  by (auto simp add: min.absorb_iff1 fun_eq_iff)
   11.14  
   11.15  lemma EVEN[import_const "EVEN" : "Parity.even_odd_class.even"]:
   11.16    "even (id 0\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
    12.1 --- a/src/HOL/Int.thy	Wed Dec 25 17:39:06 2013 +0100
    12.2 +++ b/src/HOL/Int.thy	Wed Dec 25 17:39:06 2013 +0100
    12.3 @@ -114,7 +114,7 @@
    12.4  
    12.5  instance
    12.6    by intro_classes
    12.7 -    (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
    12.8 +    (auto simp add: inf_int_def sup_int_def max_min_distrib2)
    12.9  
   12.10  end
   12.11  
    13.1 --- a/src/HOL/Lattices_Big.thy	Wed Dec 25 17:39:06 2013 +0100
    13.2 +++ b/src/HOL/Lattices_Big.thy	Wed Dec 25 17:39:06 2013 +0100
    13.3 @@ -371,10 +371,10 @@
    13.4      by (simp only: min_max.Sup_fin_def Max_def)
    13.5  qed
    13.6  
    13.7 -lemmas le_maxI1 = min_max.sup_ge1
    13.8 -lemmas le_maxI2 = min_max.sup_ge2
    13.9 -lemmas min_ac = min.assoc min_max.inf_commute min.left_commute
   13.10 -lemmas max_ac = min_max.sup_assoc min_max.sup_commute max.left_commute
   13.11 +lemmas le_maxI1 = max.cobounded1
   13.12 +lemmas le_maxI2 = max.cobounded2
   13.13 +lemmas min_ac = min.assoc min.commute min.left_commute
   13.14 +lemmas max_ac = max.assoc max.commute max.left_commute
   13.15  
   13.16  end
   13.17  
    14.1 --- a/src/HOL/Library/BigO.thy	Wed Dec 25 17:39:06 2013 +0100
    14.2 +++ b/src/HOL/Library/BigO.thy	Wed Dec 25 17:39:06 2013 +0100
    14.3 @@ -171,7 +171,7 @@
    14.4    apply (subgoal_tac "c <= max c ca")
    14.5    apply (erule order_less_le_trans)
    14.6    apply assumption
    14.7 -  apply (rule le_maxI1)
    14.8 +  apply (rule max.cobounded1)
    14.9    apply clarify
   14.10    apply (drule_tac x = "xa" in spec)+
   14.11    apply (subgoal_tac "0 <= f xa + g xa")
   14.12 @@ -184,12 +184,12 @@
   14.13    apply (subgoal_tac "c * f xa <= max c ca * f xa")
   14.14    apply (force)
   14.15    apply (rule mult_right_mono)
   14.16 -  apply (rule le_maxI1)
   14.17 +  apply (rule max.cobounded1)
   14.18    apply assumption
   14.19    apply (subgoal_tac "ca * g xa <= max c ca * g xa")
   14.20    apply (force)
   14.21    apply (rule mult_right_mono)
   14.22 -  apply (rule le_maxI2)
   14.23 +  apply (rule max.cobounded2)
   14.24    apply assumption
   14.25    apply (rule abs_triangle_ineq)
   14.26    apply (rule add_nonneg_nonneg)
   14.27 @@ -770,7 +770,7 @@
   14.28    apply (rule bigo_lesseq4)
   14.29    apply (erule set_plus_imp_minus)
   14.30    apply (rule allI)
   14.31 -  apply (rule le_maxI2)
   14.32 +  apply (rule max.cobounded2)
   14.33    apply (rule allI)
   14.34    apply (subst fun_diff_def)
   14.35    apply (case_tac "0 <= k x - g x")
   14.36 @@ -794,7 +794,7 @@
   14.37    apply (rule bigo_lesseq4)
   14.38    apply (erule set_plus_imp_minus)
   14.39    apply (rule allI)
   14.40 -  apply (rule le_maxI2)
   14.41 +  apply (rule max.cobounded2)
   14.42    apply (rule allI)
   14.43    apply (subst fun_diff_def)
   14.44    apply (case_tac "0 <= f x - k x")
   14.45 @@ -836,7 +836,7 @@
   14.46    apply (subgoal_tac "abs(max (f x - g x) 0) = max (f x - g x) 0")
   14.47    apply (clarsimp simp add: algebra_simps) 
   14.48    apply (rule abs_of_nonneg)
   14.49 -  apply (rule le_maxI2)
   14.50 +  apply (rule max.cobounded2)
   14.51    done
   14.52  
   14.53  lemma lesso_add: "f <o g =o O(h) ==>
    15.1 --- a/src/HOL/Library/Char_ord.thy	Wed Dec 25 17:39:06 2013 +0100
    15.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Dec 25 17:39:06 2013 +0100
    15.3 @@ -32,7 +32,7 @@
    15.4    "(sup \<Colon> nibble \<Rightarrow> _) = max"
    15.5  
    15.6  instance proof
    15.7 -qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    15.8 +qed (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
    15.9  
   15.10  end
   15.11  
   15.12 @@ -90,7 +90,7 @@
   15.13    "(sup \<Colon> char \<Rightarrow> _) = max"
   15.14  
   15.15  instance proof
   15.16 -qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
   15.17 +qed (auto simp add: inf_char_def sup_char_def max_min_distrib2)
   15.18  
   15.19  end
   15.20  
    16.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Dec 25 17:39:06 2013 +0100
    16.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Dec 25 17:39:06 2013 +0100
    16.3 @@ -1622,7 +1622,7 @@
    16.4          then have "range f = {0}"
    16.5            by auto
    16.6          with True show "c * SUPR UNIV f \<le> y"
    16.7 -          using * by (auto simp: SUP_def min_max.sup_absorb1)
    16.8 +          using * by (auto simp: SUP_def max.absorb1)
    16.9        next
   16.10          case False
   16.11          then obtain i where "f i \<noteq> 0"
   16.12 @@ -1779,7 +1779,7 @@
   16.13    proof (cases a)
   16.14      case PInf with `A \<noteq> {}`
   16.15      show ?thesis
   16.16 -      by (auto simp: image_constant min_max.sup_absorb1)
   16.17 +      by (auto simp: image_constant max.absorb1)
   16.18    next
   16.19      case (real r)
   16.20      then have **: "op + (- a) ` op + a ` A = A"
    17.1 --- a/src/HOL/Library/Fraction_Field.thy	Wed Dec 25 17:39:06 2013 +0100
    17.2 +++ b/src/HOL/Library/Fraction_Field.thy	Wed Dec 25 17:39:06 2013 +0100
    17.3 @@ -424,7 +424,7 @@
    17.4  instance
    17.5    by intro_classes
    17.6      (auto simp add: abs_fract_def sgn_fract_def
    17.7 -      min_max.sup_inf_distrib1 inf_fract_def sup_fract_def)
    17.8 +      max_min_distrib2 inf_fract_def sup_fract_def)
    17.9  
   17.10  end
   17.11  
    18.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Wed Dec 25 17:39:06 2013 +0100
    18.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Wed Dec 25 17:39:06 2013 +0100
    18.3 @@ -384,7 +384,7 @@
    18.4  proof -
    18.5    note add_le_cancel_right [of a a "- a", symmetric, simplified]
    18.6    moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
    18.7 -  then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2)
    18.8 +  then show ?thesis by (auto simp: sup_max max.absorb1 max.absorb2)
    18.9  qed
   18.10  
   18.11  lemma abs_if_lattice:
    19.1 --- a/src/HOL/Library/List_lexord.thy	Wed Dec 25 17:39:06 2013 +0100
    19.2 +++ b/src/HOL/Library/List_lexord.thy	Wed Dec 25 17:39:06 2013 +0100
    19.3 @@ -74,7 +74,7 @@
    19.4  definition "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    19.5  
    19.6  instance
    19.7 -  by default (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
    19.8 +  by default (auto simp add: inf_list_def sup_list_def max_min_distrib2)
    19.9  
   19.10  end
   19.11  
    20.1 --- a/src/HOL/Library/Product_Lexorder.thy	Wed Dec 25 17:39:06 2013 +0100
    20.2 +++ b/src/HOL/Library/Product_Lexorder.thy	Wed Dec 25 17:39:06 2013 +0100
    20.3 @@ -55,7 +55,7 @@
    20.4    "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
    20.5  
    20.6  instance
    20.7 -  by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
    20.8 +  by default (auto simp add: inf_prod_def sup_prod_def max_min_distrib2)
    20.9  
   20.10  end
   20.11  
    21.1 --- a/src/HOL/Library/Saturated.thy	Wed Dec 25 17:39:06 2013 +0100
    21.2 +++ b/src/HOL/Library/Saturated.thy	Wed Dec 25 17:39:06 2013 +0100
    21.3 @@ -41,7 +41,7 @@
    21.4  
    21.5  lemma min_len_of_nat_of [simp]:
    21.6    "min (len_of TYPE('a)) (nat_of (n::('a::len) sat)) = nat_of n"
    21.7 -  by (rule min_max.inf_absorb2 [OF nat_of_le_len_of])
    21.8 +  by (rule min.absorb2 [OF nat_of_le_len_of])
    21.9  
   21.10  lemma min_nat_of_len_of [simp]:
   21.11    "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
   21.12 @@ -61,7 +61,7 @@
   21.13    less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
   21.14  
   21.15  instance
   21.16 -by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
   21.17 +by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 nat_mult_commute)
   21.18  
   21.19  end
   21.20  
   21.21 @@ -117,14 +117,14 @@
   21.22        case True thus ?thesis by (simp add: sat_eq_iff)
   21.23      next
   21.24        case False with `a \<noteq> 0` show ?thesis
   21.25 -        by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min_max.inf_assoc min_max.inf_absorb2)
   21.26 +        by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min.assoc min.absorb2)
   21.27      qed
   21.28    qed
   21.29  next
   21.30    fix a :: "('a::len) sat"
   21.31    show "1 * a = a"
   21.32      apply (simp add: sat_eq_iff)
   21.33 -    apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min_max.le_iff_inf min_nat_of_len_of nat_mult_1_right nat_mult_commute)
   21.34 +    apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min.absorb_iff1 min_nat_of_len_of nat_mult_1_right nat_mult_commute)
   21.35      done
   21.36  next
   21.37    fix a b c :: "('a::len) sat"
   21.38 @@ -133,7 +133,7 @@
   21.39      case True thus ?thesis by (simp add: sat_eq_iff)
   21.40    next
   21.41      case False thus ?thesis
   21.42 -      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min_max.inf_assoc min_max.inf_absorb2)
   21.43 +      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min.assoc min.absorb2)
   21.44    qed
   21.45  qed (simp_all add: sat_eq_iff mult.commute)
   21.46  
   21.47 @@ -143,7 +143,7 @@
   21.48  begin
   21.49  
   21.50  instance
   21.51 -by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
   21.52 +by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 nat_mult_commute)
   21.53  
   21.54  end
   21.55  
   21.56 @@ -202,7 +202,7 @@
   21.57    "top = Sat (len_of TYPE('a))"
   21.58  
   21.59  instance proof
   21.60 -qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def min_max.sup_inf_distrib1,
   21.61 +qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
   21.62    simp_all add: less_eq_sat_def)
   21.63  
   21.64  end
   21.65 @@ -243,7 +243,7 @@
   21.66    note finite
   21.67    moreover assume "x \<in> A"
   21.68    ultimately show "Inf A \<le> x"
   21.69 -    by (induct A) (auto intro: min_max.le_infI2)
   21.70 +    by (induct A) (auto intro: min.coboundedI2)
   21.71  next
   21.72    fix z :: "'a sat"
   21.73    fix A :: "'a sat set"
   21.74 @@ -256,7 +256,7 @@
   21.75    note finite
   21.76    moreover assume "x \<in> A"
   21.77    ultimately show "x \<le> Sup A"
   21.78 -    by (induct A) (auto intro: min_max.le_supI2)
   21.79 +    by (induct A) (auto intro: max.coboundedI2)
   21.80  next
   21.81    fix z :: "'a sat"
   21.82    fix A :: "'a sat set"
    22.1 --- a/src/HOL/Limits.thy	Wed Dec 25 17:39:06 2013 +0100
    22.2 +++ b/src/HOL/Limits.thy	Wed Dec 25 17:39:06 2013 +0100
    22.3 @@ -125,7 +125,7 @@
    22.4  proof safe
    22.5    fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
    22.6    then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
    22.7 -    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
    22.8 +    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2)
    22.9         (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
   22.10  qed auto
   22.11  
    23.1 --- a/src/HOL/List.thy	Wed Dec 25 17:39:06 2013 +0100
    23.2 +++ b/src/HOL/List.thy	Wed Dec 25 17:39:06 2013 +0100
    23.3 @@ -2065,13 +2065,13 @@
    23.4  
    23.5  lemma butlast_take:
    23.6    "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
    23.7 -by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
    23.8 +by (simp add: butlast_conv_take min.absorb1 min.absorb2)
    23.9  
   23.10  lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
   23.11  by (simp add: butlast_conv_take drop_take add_ac)
   23.12  
   23.13  lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
   23.14 -by (simp add: butlast_conv_take min_max.inf_absorb1)
   23.15 +by (simp add: butlast_conv_take min.absorb1)
   23.16  
   23.17  lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
   23.18  by (simp add: butlast_conv_take drop_take add_ac)
    24.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Wed Dec 25 17:39:06 2013 +0100
    24.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Wed Dec 25 17:39:06 2013 +0100
    24.3 @@ -212,8 +212,8 @@
    24.4    apply (metis abs_triangle_ineq)
    24.5   apply (metis add_nonneg_nonneg)
    24.6  apply (rule add_mono)
    24.7 - apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
    24.8 -by (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
    24.9 + apply (metis max.cobounded2 linorder_linear max.absorb1 mult_right_mono xt1(6))
   24.10 +by (metis max.cobounded2 linorder_not_le mult_le_cancel_right order_trans)
   24.11  
   24.12  lemma bigo_bounded_alt: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)"
   24.13  apply (auto simp add: bigo_def)
   24.14 @@ -658,7 +658,7 @@
   24.15  apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")
   24.16   apply (metis bigo_zero)
   24.17  by (metis (lifting, no_types) func_zero le_fun_def le_iff_diff_le_0
   24.18 -      min_max.sup_absorb2 order_eq_iff)
   24.19 +      max.absorb2 order_eq_iff)
   24.20  
   24.21  lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>
   24.22      \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. k x <= f x \<Longrightarrow>
   24.23 @@ -667,15 +667,15 @@
   24.24    apply (rule bigo_lesseq4)
   24.25    apply (erule set_plus_imp_minus)
   24.26    apply (rule allI)
   24.27 -  apply (rule le_maxI2)
   24.28 +  apply (rule max.cobounded2)
   24.29    apply (rule allI)
   24.30    apply (subst fun_diff_def)
   24.31  apply (erule thin_rl)
   24.32  (* sledgehammer *)
   24.33  apply (case_tac "0 <= k x - g x")
   24.34   apply (metis (lifting) abs_le_D1 linorder_linear min_diff_distrib_left
   24.35 -          min_max.inf_absorb1 min_max.inf_absorb2 min_max.sup_absorb1)
   24.36 -by (metis abs_ge_zero le_cases min_max.sup_absorb2)
   24.37 +          min.absorb1 min.absorb2 max.absorb1)
   24.38 +by (metis abs_ge_zero le_cases max.absorb2)
   24.39  
   24.40  lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>
   24.41      \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. g x <= k x \<Longrightarrow>
   24.42 @@ -684,7 +684,7 @@
   24.43  apply (rule bigo_lesseq4)
   24.44    apply (erule set_plus_imp_minus)
   24.45   apply (rule allI)
   24.46 - apply (rule le_maxI2)
   24.47 + apply (rule max.cobounded2)
   24.48  apply (rule allI)
   24.49  apply (subst fun_diff_def)
   24.50  apply (erule thin_rl)
   24.51 @@ -695,7 +695,7 @@
   24.52    apply (drule_tac x = x in spec) back
   24.53    apply (metis diff_less_0_iff_less linorder_not_le not_leE xt1(12) xt1(6))
   24.54   apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
   24.55 -by (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
   24.56 +by (metis abs_ge_zero linorder_linear max.absorb1 max.commute)
   24.57  
   24.58  lemma bigo_lesso4:
   24.59    "f <o g =o O(k\<Colon>'a=>'b\<Colon>{linordered_field}) \<Longrightarrow>
    25.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Wed Dec 25 17:39:06 2013 +0100
    25.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Dec 25 17:39:06 2013 +0100
    25.3 @@ -379,7 +379,7 @@
    25.4    with Pair 
    25.5    have "?app s \<Longrightarrow> ?P s" by (simp only:)
    25.6    moreover
    25.7 -  have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min_max.inf_absorb2)
    25.8 +  have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min.absorb2)
    25.9    ultimately
   25.10    show ?thesis by (rule iffI) 
   25.11  qed 
    26.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Dec 25 17:39:06 2013 +0100
    26.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Dec 25 17:39:06 2013 +0100
    26.3 @@ -442,7 +442,7 @@
    26.4  (********************************************************************************)
    26.5  
    26.6  lemma max_of_list_elem: "x \<in> set xs \<Longrightarrow> x \<le> (max_of_list xs)"
    26.7 -by (induct xs, auto intro: le_maxI1 simp: le_max_iff_disj max_of_list_def)
    26.8 +by (induct xs, auto intro: max.cobounded1 simp: le_max_iff_disj max_of_list_def)
    26.9  
   26.10  lemma max_of_list_sublist: "set xs \<subseteq> set ys 
   26.11    \<Longrightarrow> (max_of_list xs) \<le> (max_of_list ys)"
   26.12 @@ -1053,7 +1053,7 @@
   26.13  lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
   26.14    \<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
   26.15  apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   26.16 -    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   26.17 +    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   26.18  apply (intro strip)
   26.19  apply (rule conjI)
   26.20  apply (rule check_type_mono, assumption, simp)
   26.21 @@ -1064,7 +1064,7 @@
   26.22    bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   26.23    apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   26.24    apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) 
   26.25 -  apply (simp add: check_type_simps min_max.sup_absorb1)
   26.26 +  apply (simp add: check_type_simps max.absorb1)
   26.27    apply clarify
   26.28    apply (rule_tac x="(length ST)" in exI)
   26.29    apply simp+
   26.30 @@ -1087,7 +1087,7 @@
   26.31    \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
   26.32  apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   26.33    apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   26.34 -              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   26.35 +              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   26.36    apply (intro strip)
   26.37    apply (rule conjI)
   26.38    apply (rule check_type_mono, assumption, simp)
   26.39 @@ -1106,7 +1106,7 @@
   26.40    \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
   26.41  apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   26.42    apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   26.43 -              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   26.44 +              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   26.45    apply (intro strip)
   26.46    apply (rule conjI)
   26.47    apply (rule check_type_mono, assumption, simp)
   26.48 @@ -1124,7 +1124,7 @@
   26.49    \<Longrightarrow> bc_mt_corresp [Load i] 
   26.50           (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
   26.51  apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   26.52 -            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   26.53 +            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   26.54    apply (intro strip)
   26.55    apply (rule conjI)
   26.56    apply (rule check_type_mono, assumption, simp)
   26.57 @@ -1148,7 +1148,7 @@
   26.58    apply (simp add: max_ssize_def  max_of_list_def)
   26.59    apply (simp add: ssize_sto_def)
   26.60    apply (intro strip)
   26.61 -apply (simp add: check_type_simps min_max.sup_absorb1)
   26.62 +apply (simp add: check_type_simps max.absorb1)
   26.63  apply clarify
   26.64  apply (rule conjI)
   26.65  apply (rule_tac x="(length ST)" in exI)
   26.66 @@ -1162,7 +1162,7 @@
   26.67    apply (simp add: sup_state_conv)
   26.68    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
   26.69   apply (intro strip)
   26.70 -apply (simp add: check_type_simps min_max.sup_absorb1)
   26.71 +apply (simp add: check_type_simps max.absorb1)
   26.72  apply clarify
   26.73  apply (rule_tac x="(length ST)" in exI)
   26.74  apply simp+
   26.75 @@ -1172,7 +1172,7 @@
   26.76  lemma bc_mt_corresp_Dup: "
   26.77    bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
   26.78   apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
   26.79 -             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   26.80 +             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   26.81    apply (intro strip)
   26.82    apply (rule conjI)
   26.83    apply (rule check_type_mono, assumption, simp)
   26.84 @@ -1185,7 +1185,7 @@
   26.85  lemma bc_mt_corresp_Dup_x1: "
   26.86    bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
   26.87    apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
   26.88 -              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   26.89 +              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   26.90    apply (intro strip)
   26.91    apply (rule conjI)
   26.92    apply (rule check_type_mono, assumption, simp)
   26.93 @@ -1202,7 +1202,7 @@
   26.94           (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
   26.95    apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
   26.96    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
   26.97 -  apply (simp add: check_type_simps min_max.sup_absorb1)
   26.98 +  apply (simp add: check_type_simps max.absorb1)
   26.99    apply clarify
  26.100    apply (rule_tac x="Suc (length ST)" in exI)
  26.101    apply simp+
  26.102 @@ -1245,7 +1245,7 @@
  26.103    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  26.104  
  26.105    apply (intro strip)
  26.106 -apply (simp add: check_type_simps min_max.sup_absorb1)
  26.107 +apply (simp add: check_type_simps max.absorb1)
  26.108  apply clarify
  26.109  apply (rule_tac x="Suc (length ST)" in exI)
  26.110  apply simp+
    27.1 --- a/src/HOL/MicroJava/DFA/LBVSpec.thy	Wed Dec 25 17:39:06 2013 +0100
    27.2 +++ b/src/HOL/MicroJava/DFA/LBVSpec.thy	Wed Dec 25 17:39:06 2013 +0100
    27.3 @@ -283,7 +283,7 @@
    27.4    shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
    27.5  proof -
    27.6    from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
    27.7 -  with suc wtl show ?thesis by (simp add: min_max.inf_absorb2)
    27.8 +  with suc wtl show ?thesis by (simp add: min.absorb2)
    27.9  qed
   27.10  
   27.11  lemma (in lbv) wtl_all:
   27.12 @@ -298,7 +298,7 @@
   27.13    with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp 
   27.14    from pc have "is!pc = drop pc is ! 0" by simp
   27.15    with Cons have "is!pc = i" by simp
   27.16 -  with take pc show ?thesis by (auto simp add: min_max.inf_absorb2)
   27.17 +  with take pc show ?thesis by (auto simp add: min.absorb2)
   27.18  qed
   27.19  
   27.20  section "preserves-type"
    28.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Dec 25 17:39:06 2013 +0100
    28.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Dec 25 17:39:06 2013 +0100
    28.3 @@ -2723,7 +2723,7 @@
    28.4      show ?case
    28.5        apply (rule_tac x="max B1 B2" in exI)
    28.6        apply rule
    28.7 -      apply (rule min_max.less_supI1)
    28.8 +      apply (rule max.strict_coboundedI1)
    28.9        apply (rule B1)
   28.10        apply rule
   28.11        apply rule
   28.12 @@ -9576,7 +9576,7 @@
   28.13      show ?case
   28.14        apply (rule_tac x="max B1 B2" in exI)
   28.15        apply safe
   28.16 -      apply (rule min_max.less_supI1)
   28.17 +      apply (rule max.strict_coboundedI1)
   28.18        apply (rule B1)
   28.19      proof -
   28.20        fix a b c d :: 'n
    29.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 25 17:39:06 2013 +0100
    29.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 25 17:39:06 2013 +0100
    29.3 @@ -2527,7 +2527,7 @@
    29.4    apply (drule (1) bspec)
    29.5    apply simp
    29.6    apply (drule (1) bspec)
    29.7 -  apply (rule min_max.le_supI2)
    29.8 +  apply (rule max.coboundedI2)
    29.9    apply (erule order_trans [OF dist_triangle add_left_mono])
   29.10    done
   29.11  
    30.1 --- a/src/HOL/NanoJava/OpSem.thy	Wed Dec 25 17:39:06 2013 +0100
    30.2 +++ b/src/HOL/NanoJava/OpSem.thy	Wed Dec 25 17:39:06 2013 +0100
    30.3 @@ -86,15 +86,15 @@
    30.4  
    30.5  lemma exec_exec_max: "\<lbrakk>s1 -c1-    n1   \<rightarrow> t1 ; s2 -c2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
    30.6                         s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
    30.7 -by (fast intro: exec_mono le_maxI1 le_maxI2)
    30.8 +by (fast intro: exec_mono max.cobounded1 max.cobounded2)
    30.9  
   30.10  lemma eval_exec_max: "\<lbrakk>s1 -c-    n1   \<rightarrow> t1 ; s2 -e\<succ>v-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
   30.11                         s1 -c-max n1 n2\<rightarrow> t1 \<and> s2 -e\<succ>v-max n1 n2\<rightarrow> t2"
   30.12 -by (fast intro: eval_mono exec_mono le_maxI1 le_maxI2)
   30.13 +by (fast intro: eval_mono exec_mono max.cobounded1 max.cobounded2)
   30.14  
   30.15  lemma eval_eval_max: "\<lbrakk>s1 -e1\<succ>v1-    n1   \<rightarrow> t1 ; s2 -e2\<succ>v2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
   30.16                         s1 -e1\<succ>v1-max n1 n2\<rightarrow> t1 \<and> s2 -e2\<succ>v2-max n1 n2\<rightarrow> t2"
   30.17 -by (fast intro: eval_mono le_maxI1 le_maxI2)
   30.18 +by (fast intro: eval_mono max.cobounded1 max.cobounded2)
   30.19  
   30.20  lemma eval_eval_exec_max: 
   30.21   "\<lbrakk>s1 -e1\<succ>v1-n1\<rightarrow> t1; s2 -e2\<succ>v2-n2\<rightarrow> t2; s3 -c-n3\<rightarrow> t3\<rbrakk> \<Longrightarrow> 
   30.22 @@ -102,7 +102,7 @@
   30.23     s2 -e2\<succ>v2-max (max n1 n2) n3\<rightarrow> t2 \<and> 
   30.24     s3 -c    -max (max n1 n2) n3\<rightarrow> t3"
   30.25  apply (drule (1) eval_eval_max, erule thin_rl)
   30.26 -by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2)
   30.27 +by (fast intro: exec_mono eval_mono max.cobounded1 max.cobounded2)
   30.28  
   30.29  lemma Impl_body_eq: "(\<lambda>t. \<exists>n. Z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. Z -body M-n\<rightarrow> t)"
   30.30  apply (rule ext)
    31.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Dec 25 17:39:06 2013 +0100
    31.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Wed Dec 25 17:39:06 2013 +0100
    31.3 @@ -324,7 +324,7 @@
    31.4          using `incseq F1` `incseq F2` unfolding incseq_def
    31.5          by (force split: split_max)+
    31.6        then have "(fst x, snd x) \<in> F1 (max i j) \<times> F2 (max i j)"
    31.7 -        by (intro SigmaI) (auto simp add: min_max.sup_commute)
    31.8 +        by (intro SigmaI) (auto simp add: max.commute)
    31.9        then show "x \<in> (\<Union>i. ?F i)" by auto
   31.10      qed
   31.11      then show "(\<Union>i. ?F i) = space M1 \<times> space M2"
    32.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 25 17:39:06 2013 +0100
    32.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 25 17:39:06 2013 +0100
    32.3 @@ -795,7 +795,7 @@
    32.4  
    32.5      { fix z
    32.6        from F(4)[of z] have "F i z \<le> ereal (f z)"
    32.7 -        by (metis SUP_upper UNIV_I ereal_max_0 min_max.sup_absorb2 nonneg)
    32.8 +        by (metis SUP_upper UNIV_I ereal_max_0 max.absorb2 nonneg)
    32.9        with F(5)[of i z] have "real (F i z) \<le> f z"
   32.10          by (cases "F i z") simp_all }
   32.11      note F_bound = this
    33.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Dec 25 17:39:06 2013 +0100
    33.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Dec 25 17:39:06 2013 +0100
    33.3 @@ -187,7 +187,7 @@
    33.4  
    33.5  instance
    33.6    by default
    33.7 -     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
    33.8 +     (auto simp add: inf_int_def sup_int_def max_min_distrib2)
    33.9  
   33.10  end
   33.11  
    34.1 --- a/src/HOL/Rat.thy	Wed Dec 25 17:39:06 2013 +0100
    34.2 +++ b/src/HOL/Rat.thy	Wed Dec 25 17:39:06 2013 +0100
    34.3 @@ -494,7 +494,7 @@
    34.4    "(sup :: rat \<Rightarrow> rat \<Rightarrow> rat) = max"
    34.5  
    34.6  instance proof
    34.7 -qed (auto simp add: inf_rat_def sup_rat_def min_max.sup_inf_distrib1)
    34.8 +qed (auto simp add: inf_rat_def sup_rat_def max_min_distrib2)
    34.9  
   34.10  end
   34.11  
    35.1 --- a/src/HOL/Real.thy	Wed Dec 25 17:39:06 2013 +0100
    35.2 +++ b/src/HOL/Real.thy	Wed Dec 25 17:39:06 2013 +0100
    35.3 @@ -632,7 +632,7 @@
    35.4    "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
    35.5  
    35.6  instance proof
    35.7 -qed (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
    35.8 +qed (auto simp add: inf_real_def sup_real_def max_min_distrib2)
    35.9  
   35.10  end
   35.11  
    36.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Dec 25 17:39:06 2013 +0100
    36.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Dec 25 17:39:06 2013 +0100
    36.3 @@ -1097,12 +1097,12 @@
    36.4    show ?thesis
    36.5    proof (intro exI impI conjI allI)
    36.6      show "0 < max 1 K"
    36.7 -      by (rule order_less_le_trans [OF zero_less_one le_maxI1])
    36.8 +      by (rule order_less_le_trans [OF zero_less_one max.cobounded1])
    36.9    next
   36.10      fix x
   36.11      have "norm (f x) \<le> norm x * K" using K .
   36.12      also have "\<dots> \<le> norm x * max 1 K"
   36.13 -      by (rule mult_left_mono [OF le_maxI2 norm_ge_zero])
   36.14 +      by (rule mult_left_mono [OF max.cobounded2 norm_ge_zero])
   36.15      finally show "norm (f x) \<le> norm x * max 1 K" .
   36.16    qed
   36.17  qed
   36.18 @@ -1138,9 +1138,9 @@
   36.19    "\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
   36.20  apply (cut_tac bounded, erule exE)
   36.21  apply (rule_tac x="max 1 K" in exI, safe)
   36.22 -apply (rule order_less_le_trans [OF zero_less_one le_maxI1])
   36.23 +apply (rule order_less_le_trans [OF zero_less_one max.cobounded1])
   36.24  apply (drule spec, drule spec, erule order_trans)
   36.25 -apply (rule mult_left_mono [OF le_maxI2])
   36.26 +apply (rule mult_left_mono [OF max.cobounded2])
   36.27  apply (intro mult_nonneg_nonneg norm_ge_zero)
   36.28  done
   36.29  
    37.1 --- a/src/HOL/UNITY/Simple/Common.thy	Wed Dec 25 17:39:06 2013 +0100
    37.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Wed Dec 25 17:39:06 2013 +0100
    37.3 @@ -65,7 +65,7 @@
    37.4  lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
    37.5         \<in> {m} co (maxfg m)"
    37.6  apply (simp add: mk_total_program_def) 
    37.7 -apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
    37.8 +apply (simp add: constrains_def maxfg_def gasc max.absorb2)
    37.9  done
   37.10  
   37.11  (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
   37.12 @@ -73,7 +73,7 @@
   37.13            (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
   37.14         \<in> {m} co (maxfg m)"
   37.15  apply (simp add: mk_total_program_def) 
   37.16 -apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
   37.17 +apply (simp add: constrains_def maxfg_def gasc max.absorb2)
   37.18  done
   37.19  
   37.20  
    38.1 --- a/src/HOL/Word/Bit_Representation.thy	Wed Dec 25 17:39:06 2013 +0100
    38.2 +++ b/src/HOL/Word/Bit_Representation.thy	Wed Dec 25 17:39:06 2013 +0100
    38.3 @@ -420,7 +420,7 @@
    38.4  lemma sbintrunc_sbintrunc_min [simp]:
    38.5    "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
    38.6    apply (rule bin_eqI)
    38.7 -  apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2)
    38.8 +  apply (auto simp: nth_sbintr min.absorb1 min.absorb2)
    38.9    done
   38.10  
   38.11  lemmas bintrunc_Pls = 
    39.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Wed Dec 25 17:39:06 2013 +0100
    39.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Wed Dec 25 17:39:06 2013 +0100
    39.3 @@ -906,7 +906,7 @@
    39.4    apply (drule meta_spec)
    39.5    apply (erule trans)
    39.6    apply (drule_tac x = "bin_cat y n a" in meta_spec)
    39.7 -  apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
    39.8 +  apply (simp add : bin_cat_assoc_sym min.absorb2)
    39.9    done
   39.10  
   39.11  lemma bin_rcat_bl:
    40.1 --- a/src/HOL/Word/Misc_Numeric.thy	Wed Dec 25 17:39:06 2013 +0100
    40.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Wed Dec 25 17:39:06 2013 +0100
    40.3 @@ -20,7 +20,7 @@
    40.4  
    40.5  lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith
    40.6    
    40.7 -lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus]
    40.8 +lemmas min_minus' [simp] = trans [OF min.commute min_minus]
    40.9  
   40.10  lemma mod_2_neq_1_eq_eq_0:
   40.11    fixes k :: int
    41.1 --- a/src/HOL/Word/Word.thy	Wed Dec 25 17:39:06 2013 +0100
    41.2 +++ b/src/HOL/Word/Word.thy	Wed Dec 25 17:39:06 2013 +0100
    41.3 @@ -569,13 +569,13 @@
    41.4    shows "len_of TYPE('a) \<le> n \<Longrightarrow> bintrunc n (uint w) = uint w"
    41.5    apply (subst word_ubin.norm_Rep [symmetric]) 
    41.6    apply (simp only: bintrunc_bintrunc_min word_size)
    41.7 -  apply (simp add: min_max.inf_absorb2)
    41.8 +  apply (simp add: min.absorb2)
    41.9    done
   41.10  
   41.11  lemma wi_bintr:
   41.12    "len_of TYPE('a::len0) \<le> n \<Longrightarrow>
   41.13      word_of_int (bintrunc n w) = (word_of_int w :: 'a word)"
   41.14 -  by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
   41.15 +  by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min.absorb1)
   41.16  
   41.17  lemma td_ext_sbin: 
   41.18    "td_ext (sint :: 'a word => int) word_of_int (sints (len_of TYPE('a::len))) 
   41.19 @@ -3692,7 +3692,7 @@
   41.20    word_of_int (bin_cat w (size b) (uint b))"
   41.21    apply (unfold word_cat_def word_size) 
   41.22    apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
   41.23 -      word_ubin.eq_norm bintr_cat min_max.inf_absorb1)
   41.24 +      word_ubin.eq_norm bintr_cat min.absorb1)
   41.25    done
   41.26  
   41.27  lemma word_cat_split_alt:
    42.1 --- a/src/HOL/ex/Dedekind_Real.thy	Wed Dec 25 17:39:06 2013 +0100
    42.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Wed Dec 25 17:39:06 2013 +0100
    42.3 @@ -220,7 +220,7 @@
    42.4  
    42.5  instance
    42.6    by intro_classes
    42.7 -    (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
    42.8 +    (auto simp add: inf_preal_def sup_preal_def max_min_distrib2)
    42.9  
   42.10  end
   42.11  
   42.12 @@ -1555,7 +1555,7 @@
   42.13    "(sup \<Colon> real \<Rightarrow> real \<Rightarrow> real) = max"
   42.14  
   42.15  instance
   42.16 -  by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
   42.17 +  by default (auto simp add: inf_real_def sup_real_def max_min_distrib2)
   42.18  
   42.19  end
   42.20