--- a/src/HOL/Algebra/UnivPoly.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Dec 25 17:39:06 2013 +0100
@@ -1252,7 +1252,7 @@
h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q} \<union> {deg R q<..max (deg R p) (deg R q)}.
h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
- by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
+ by (simp only: ivl_disj_un_one max.cobounded1 max.cobounded2)
also from R S have "... =
(\<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>
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
--- a/src/HOL/Bali/Evaln.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Bali/Evaln.thy Wed Dec 25 17:39:06 2013 +0100
@@ -459,7 +459,7 @@
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>
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')"
-by (fast intro: le_maxI1 le_maxI2)
+by (fast intro: max.cobounded1 max.cobounded2)
corollary evaln_max2E [consumes 2]:
"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2');
@@ -473,7 +473,7 @@
G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2') \<and>
G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')"
apply (drule (1) evaln_max2, erule thin_rl)
-apply (fast intro!: le_maxI1 le_maxI2)
+apply (fast intro!: max.cobounded1 max.cobounded2)
done
corollary evaln_max3E:
@@ -489,10 +489,10 @@
lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
proof -
have "n2 \<le> max n2 n3"
- by (rule le_maxI1)
+ by (rule max.cobounded1)
also
have "max n2 n3 \<le> max n1 (max n2 n3)"
- by (rule le_maxI2)
+ by (rule max.cobounded2)
finally
show ?thesis .
qed
@@ -500,10 +500,10 @@
lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
proof -
have "n3 \<le> max n2 n3"
- by (rule le_maxI2)
+ by (rule max.cobounded2)
also
have "max n2 n3 \<le> max n1 (max n2 n3)"
- by (rule le_maxI2)
+ by (rule max.cobounded2)
finally
show ?thesis .
qed
@@ -568,13 +568,13 @@
then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and>
G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
else s3 = s1"
- by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
+ by simp (iprover intro: evaln_nonstrict max.cobounded1 max.cobounded2)
ultimately
have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
apply -
apply (rule evaln.Loop)
- apply (iprover intro: evaln_nonstrict intro: le_maxI1)
- apply (auto intro: evaln_nonstrict intro: le_maxI2)
+ apply (iprover intro: evaln_nonstrict intro: max.cobounded1)
+ apply (auto intro: evaln_nonstrict intro: max.cobounded2)
done
then show ?case ..
next
@@ -603,7 +603,7 @@
by fastforce
ultimately
have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
- by (auto intro!: evaln.Try le_maxI1 le_maxI2)
+ by (auto intro!: evaln.Try max.cobounded1 max.cobounded2)
then show ?case ..
next
case (Fin s0 c1 x1 s1 c2 s2 s3)
@@ -629,7 +629,7 @@
\<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and>
s3 = restore_lvars s1 s2)"
- by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
+ by (auto intro: evaln_nonstrict max.cobounded1 max.cobounded2)
ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
by (rule evaln.Init)
then show ?case ..
@@ -755,7 +755,7 @@
ultimately
have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow>
(set_lvars (locals (store s2))) s4"
- by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
+ by (auto intro!: evaln.Call max.cobounded1 le_max3I1 le_max3I2)
thus ?case ..
next
case (Methd s0 D sig v s1)
--- a/src/HOL/Decision_Procs/Ferrack.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Dec 25 17:39:06 2013 +0100
@@ -444,7 +444,7 @@
assumes g0: "numgcd t = 0"
shows "Inum bs t = 0"
using g0[simplified numgcd_def]
- by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos min_max.sup_absorb2)
+ by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos max.absorb2)
lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
using gp
--- a/src/HOL/HOLCF/Completion.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/HOLCF/Completion.thy Wed Dec 25 17:39:06 2013 +0100
@@ -62,8 +62,8 @@
apply (rule idealI)
apply (cut_tac idealD1 [OF ideal_A], fast)
apply (clarify, rename_tac i j)
- apply (drule subsetD [OF chain_A [OF le_maxI1]])
- apply (drule subsetD [OF chain_A [OF le_maxI2]])
+ apply (drule subsetD [OF chain_A [OF max.cobounded1]])
+ apply (drule subsetD [OF chain_A [OF max.cobounded2]])
apply (drule (1) idealD2 [OF ideal_A])
apply blast
apply clarify
--- a/src/HOL/HOLCF/Library/List_Cpo.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy Wed Dec 25 17:39:06 2013 +0100
@@ -273,8 +273,8 @@
apply (erule list_chain_cases)
apply (auto simp add: lub_Cons dest!: compactD2)
apply (rename_tac i j, rule_tac x="max i j" in exI)
-apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI1]])
-apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI2]])
+apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded1]])
+apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded2]])
apply (erule (1) conjI)
done
--- a/src/HOL/HOLCF/Pcpo.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/HOLCF/Pcpo.thy Wed Dec 25 17:39:06 2013 +0100
@@ -118,8 +118,8 @@
apply (rule lub_below [OF 2])
apply (rule below_lub [OF 3])
apply (rule below_trans)
- apply (rule chain_mono [OF 1 le_maxI1])
- apply (rule chain_mono [OF 2 le_maxI2])
+ apply (rule chain_mono [OF 1 max.cobounded1])
+ apply (rule chain_mono [OF 2 max.cobounded2])
done
show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
apply (rule lub_mono [OF 3 4])
--- a/src/HOL/HOLCF/Universal.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/HOLCF/Universal.thy Wed Dec 25 17:39:06 2013 +0100
@@ -802,7 +802,7 @@
by (simp add: approximants_def approx_below)
moreover from x y have "x \<sqsubseteq> ?z \<and> y \<sqsubseteq> ?z"
by (simp add: approximants_def compact_le_def)
- (metis i j monofun_cfun chain_mono chain_approx le_maxI1 le_maxI2)
+ (metis i j monofun_cfun chain_mono chain_approx max.cobounded1 max.cobounded2)
ultimately show "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" ..
next
fix x y :: "'a compact_basis"
--- a/src/HOL/Hoare_Parallel/Graph.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Hoare_Parallel/Graph.thy Wed Dec 25 17:39:06 2013 +0100
@@ -182,7 +182,7 @@
subsubsection{* Graph 3 *}
-declare min_max.inf_absorb1 [simp] min_max.inf_absorb2 [simp]
+declare min.absorb1 [simp] min.absorb2 [simp]
lemma Graph3:
"\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
@@ -304,7 +304,7 @@
apply force
done
-declare min_max.inf_absorb1 [simp del] min_max.inf_absorb2 [simp del]
+declare min.absorb1 [simp del] min.absorb2 [simp del]
subsubsection {* Graph 5 *}
--- 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:06 2013 +0100
@@ -48,19 +48,19 @@
next
case (IfTrue b s c1)
hence "max (sec b) l \<turnstile> c1" by auto
- hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
+ hence "l \<turnstile> c1" by (metis max.cobounded2 anti_mono)
thus ?case using IfTrue.IH by metis
next
case (IfFalse b s c2)
hence "max (sec b) l \<turnstile> c2" by auto
- hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
+ hence "l \<turnstile> c2" by (metis max.cobounded2 anti_mono)
thus ?case using IfFalse.IH by metis
next
case WhileFalse thus ?case by auto
next
case (WhileTrue b s1 c)
hence "max (sec b) l \<turnstile> c" by auto
- hence "l \<turnstile> c" by (metis le_maxI2 anti_mono)
+ hence "l \<turnstile> c" by (metis max.cobounded2 anti_mono)
thus ?case using WhileTrue by metis
qed
@@ -200,8 +200,8 @@
apply (metis Skip')
apply (metis Assign')
apply (metis Seq')
-apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
-by (metis less_or_eq_imp_le min_max.sup_absorb1 min_max.sup_absorb2 nat_le_linear While' anti_mono')
+apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
+by (metis less_or_eq_imp_le max.absorb1 max.absorb2 nat_le_linear While' anti_mono')
lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
@@ -209,8 +209,8 @@
apply (metis Skip)
apply (metis Assign)
apply (metis Seq)
-apply (metis min_max.sup_absorb2 If)
-apply (metis min_max.sup_absorb2 While)
+apply (metis max.absorb2 If)
+apply (metis max.absorb2 While)
by (metis anti_mono)
subsection "A Bottom-Up Typing System"
@@ -233,15 +233,15 @@
apply(induction rule: sec_type2.induct)
apply (metis Skip')
apply (metis Assign' eq_imp_le)
-apply (metis Seq' anti_mono' min_max.inf_le1 min_max.inf_le2)
-apply (metis If' anti_mono' min_max.inf_absorb2 min_max.le_iff_inf nat_le_linear)
+apply (metis Seq' anti_mono' min.cobounded1 min.cobounded2)
+apply (metis If' anti_mono' min.absorb2 min.absorb_iff1 nat_le_linear)
by (metis While')
lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
apply(induction rule: sec_type'.induct)
apply (metis Skip2 le_refl)
apply (metis Assign2)
-apply (metis Seq2 min_max.inf_greatest)
+apply (metis Seq2 min.boundedI)
apply (metis If2 inf_greatest inf_nat_def le_trans)
apply (metis While2 le_trans)
by (metis le_trans)
--- 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:06 2013 +0100
@@ -41,12 +41,12 @@
next
case (IfTrue b s c1)
hence "max (sec b) l \<turnstile> c1" by auto
- hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
+ hence "l \<turnstile> c1" by (metis max.cobounded2 anti_mono)
thus ?case using IfTrue.IH by metis
next
case (IfFalse b s c2)
hence "max (sec b) l \<turnstile> c2" by auto
- hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
+ hence "l \<turnstile> c2" by (metis max.cobounded2 anti_mono)
thus ?case using IfFalse.IH by metis
next
case WhileFalse thus ?case by auto
@@ -61,7 +61,7 @@
apply (metis big_step.Skip)
apply (metis big_step.Assign)
apply (metis big_step.Seq)
-apply (metis IfFalse IfTrue le0 le_antisym le_maxI2)
+apply (metis IfFalse IfTrue le0 le_antisym max.cobounded2)
apply simp
done
@@ -190,7 +190,7 @@
apply (metis Skip')
apply (metis Assign')
apply (metis Seq')
-apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
+apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
by (metis While')
@@ -200,7 +200,7 @@
apply (metis Skip)
apply (metis Assign)
apply (metis Seq)
-apply (metis min_max.sup_absorb2 If)
+apply (metis max.absorb2 If)
apply (metis While)
by (metis anti_mono)
--- a/src/HOL/Import/HOL_Light_Maps.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy Wed Dec 25 17:39:06 2013 +0100
@@ -175,11 +175,11 @@
lemma DEF_MAX[import_const "MAX"]:
"max = (\<lambda>x y :: nat. if x \<le> y then y else x)"
- by (auto simp add: min_max.le_iff_sup fun_eq_iff)
+ by (auto simp add: max.absorb_iff2 fun_eq_iff)
lemma DEF_MIN[import_const "MIN"]:
"min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
- by (auto simp add: min_max.le_iff_inf fun_eq_iff)
+ by (auto simp add: min.absorb_iff1 fun_eq_iff)
lemma EVEN[import_const "EVEN" : "Parity.even_odd_class.even"]:
"even (id 0\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
--- a/src/HOL/Int.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Int.thy Wed Dec 25 17:39:06 2013 +0100
@@ -114,7 +114,7 @@
instance
by intro_classes
- (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+ (auto simp add: inf_int_def sup_int_def max_min_distrib2)
end
--- 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:06 2013 +0100
@@ -371,10 +371,10 @@
by (simp only: min_max.Sup_fin_def Max_def)
qed
-lemmas le_maxI1 = min_max.sup_ge1
-lemmas le_maxI2 = min_max.sup_ge2
-lemmas min_ac = min.assoc min_max.inf_commute min.left_commute
-lemmas max_ac = min_max.sup_assoc min_max.sup_commute max.left_commute
+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
--- a/src/HOL/Library/BigO.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/BigO.thy Wed Dec 25 17:39:06 2013 +0100
@@ -171,7 +171,7 @@
apply (subgoal_tac "c <= max c ca")
apply (erule order_less_le_trans)
apply assumption
- apply (rule le_maxI1)
+ apply (rule max.cobounded1)
apply clarify
apply (drule_tac x = "xa" in spec)+
apply (subgoal_tac "0 <= f xa + g xa")
@@ -184,12 +184,12 @@
apply (subgoal_tac "c * f xa <= max c ca * f xa")
apply (force)
apply (rule mult_right_mono)
- apply (rule le_maxI1)
+ apply (rule max.cobounded1)
apply assumption
apply (subgoal_tac "ca * g xa <= max c ca * g xa")
apply (force)
apply (rule mult_right_mono)
- apply (rule le_maxI2)
+ apply (rule max.cobounded2)
apply assumption
apply (rule abs_triangle_ineq)
apply (rule add_nonneg_nonneg)
@@ -770,7 +770,7 @@
apply (rule bigo_lesseq4)
apply (erule set_plus_imp_minus)
apply (rule allI)
- apply (rule le_maxI2)
+ apply (rule max.cobounded2)
apply (rule allI)
apply (subst fun_diff_def)
apply (case_tac "0 <= k x - g x")
@@ -794,7 +794,7 @@
apply (rule bigo_lesseq4)
apply (erule set_plus_imp_minus)
apply (rule allI)
- apply (rule le_maxI2)
+ apply (rule max.cobounded2)
apply (rule allI)
apply (subst fun_diff_def)
apply (case_tac "0 <= f x - k x")
@@ -836,7 +836,7 @@
apply (subgoal_tac "abs(max (f x - g x) 0) = max (f x - g x) 0")
apply (clarsimp simp add: algebra_simps)
apply (rule abs_of_nonneg)
- apply (rule le_maxI2)
+ apply (rule max.cobounded2)
done
lemma lesso_add: "f <o g =o O(h) ==>
--- a/src/HOL/Library/Char_ord.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Char_ord.thy Wed Dec 25 17:39:06 2013 +0100
@@ -32,7 +32,7 @@
"(sup \<Colon> nibble \<Rightarrow> _) = max"
instance proof
-qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
+qed (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
end
@@ -90,7 +90,7 @@
"(sup \<Colon> char \<Rightarrow> _) = max"
instance proof
-qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
+qed (auto simp add: inf_char_def sup_char_def max_min_distrib2)
end
--- a/src/HOL/Library/Extended_Real.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy Wed Dec 25 17:39:06 2013 +0100
@@ -1622,7 +1622,7 @@
then have "range f = {0}"
by auto
with True show "c * SUPR UNIV f \<le> y"
- using * by (auto simp: SUP_def min_max.sup_absorb1)
+ using * by (auto simp: SUP_def max.absorb1)
next
case False
then obtain i where "f i \<noteq> 0"
@@ -1779,7 +1779,7 @@
proof (cases a)
case PInf with `A \<noteq> {}`
show ?thesis
- by (auto simp: image_constant min_max.sup_absorb1)
+ by (auto simp: image_constant max.absorb1)
next
case (real r)
then have **: "op + (- a) ` op + a ` A = A"
--- a/src/HOL/Library/Fraction_Field.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Fraction_Field.thy Wed Dec 25 17:39:06 2013 +0100
@@ -424,7 +424,7 @@
instance
by intro_classes
(auto simp add: abs_fract_def sgn_fract_def
- min_max.sup_inf_distrib1 inf_fract_def sup_fract_def)
+ max_min_distrib2 inf_fract_def sup_fract_def)
end
--- a/src/HOL/Library/Lattice_Algebras.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy Wed Dec 25 17:39:06 2013 +0100
@@ -384,7 +384,7 @@
proof -
note add_le_cancel_right [of a a "- a", symmetric, simplified]
moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
- then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2)
+ then show ?thesis by (auto simp: sup_max max.absorb1 max.absorb2)
qed
lemma abs_if_lattice:
--- a/src/HOL/Library/List_lexord.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/List_lexord.thy Wed Dec 25 17:39:06 2013 +0100
@@ -74,7 +74,7 @@
definition "(sup \<Colon> 'a list \<Rightarrow> _) = max"
instance
- by default (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
+ by default (auto simp add: inf_list_def sup_list_def max_min_distrib2)
end
--- a/src/HOL/Library/Product_Lexorder.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Product_Lexorder.thy Wed Dec 25 17:39:06 2013 +0100
@@ -55,7 +55,7 @@
"(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
instance
- by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
+ by default (auto simp add: inf_prod_def sup_prod_def max_min_distrib2)
end
--- a/src/HOL/Library/Saturated.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Library/Saturated.thy Wed Dec 25 17:39:06 2013 +0100
@@ -41,7 +41,7 @@
lemma min_len_of_nat_of [simp]:
"min (len_of TYPE('a)) (nat_of (n::('a::len) sat)) = nat_of n"
- by (rule min_max.inf_absorb2 [OF nat_of_le_len_of])
+ by (rule min.absorb2 [OF nat_of_le_len_of])
lemma min_nat_of_len_of [simp]:
"min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
@@ -61,7 +61,7 @@
less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
instance
-by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
+by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 nat_mult_commute)
end
@@ -117,14 +117,14 @@
case True thus ?thesis by (simp add: sat_eq_iff)
next
case False with `a \<noteq> 0` show ?thesis
- by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min_max.inf_assoc min_max.inf_absorb2)
+ by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min.assoc min.absorb2)
qed
qed
next
fix a :: "('a::len) sat"
show "1 * a = a"
apply (simp add: sat_eq_iff)
- 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)
+ 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)
done
next
fix a b c :: "('a::len) sat"
@@ -133,7 +133,7 @@
case True thus ?thesis by (simp add: sat_eq_iff)
next
case False thus ?thesis
- 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)
+ 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)
qed
qed (simp_all add: sat_eq_iff mult.commute)
@@ -143,7 +143,7 @@
begin
instance
-by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
+by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 nat_mult_commute)
end
@@ -202,7 +202,7 @@
"top = Sat (len_of TYPE('a))"
instance proof
-qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def min_max.sup_inf_distrib1,
+qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
simp_all add: less_eq_sat_def)
end
@@ -243,7 +243,7 @@
note finite
moreover assume "x \<in> A"
ultimately show "Inf A \<le> x"
- by (induct A) (auto intro: min_max.le_infI2)
+ by (induct A) (auto intro: min.coboundedI2)
next
fix z :: "'a sat"
fix A :: "'a sat set"
@@ -256,7 +256,7 @@
note finite
moreover assume "x \<in> A"
ultimately show "x \<le> Sup A"
- by (induct A) (auto intro: min_max.le_supI2)
+ by (induct A) (auto intro: max.coboundedI2)
next
fix z :: "'a sat"
fix A :: "'a sat set"
--- a/src/HOL/Limits.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Limits.thy Wed Dec 25 17:39:06 2013 +0100
@@ -125,7 +125,7 @@
proof safe
fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
- by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
+ by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2)
(auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
qed auto
--- a/src/HOL/List.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/List.thy Wed Dec 25 17:39:06 2013 +0100
@@ -2065,13 +2065,13 @@
lemma butlast_take:
"n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
-by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
+by (simp add: butlast_conv_take min.absorb1 min.absorb2)
lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
by (simp add: butlast_conv_take drop_take add_ac)
lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
-by (simp add: butlast_conv_take min_max.inf_absorb1)
+by (simp add: butlast_conv_take min.absorb1)
lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
by (simp add: butlast_conv_take drop_take add_ac)
--- a/src/HOL/Metis_Examples/Big_O.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Wed Dec 25 17:39:06 2013 +0100
@@ -212,8 +212,8 @@
apply (metis abs_triangle_ineq)
apply (metis add_nonneg_nonneg)
apply (rule add_mono)
- apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
-by (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
+ apply (metis max.cobounded2 linorder_linear max.absorb1 mult_right_mono xt1(6))
+by (metis max.cobounded2 linorder_not_le mult_le_cancel_right order_trans)
lemma bigo_bounded_alt: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)"
apply (auto simp add: bigo_def)
@@ -658,7 +658,7 @@
apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")
apply (metis bigo_zero)
by (metis (lifting, no_types) func_zero le_fun_def le_iff_diff_le_0
- min_max.sup_absorb2 order_eq_iff)
+ max.absorb2 order_eq_iff)
lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>
\<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. k x <= f x \<Longrightarrow>
@@ -667,15 +667,15 @@
apply (rule bigo_lesseq4)
apply (erule set_plus_imp_minus)
apply (rule allI)
- apply (rule le_maxI2)
+ apply (rule max.cobounded2)
apply (rule allI)
apply (subst fun_diff_def)
apply (erule thin_rl)
(* sledgehammer *)
apply (case_tac "0 <= k x - g x")
apply (metis (lifting) abs_le_D1 linorder_linear min_diff_distrib_left
- min_max.inf_absorb1 min_max.inf_absorb2 min_max.sup_absorb1)
-by (metis abs_ge_zero le_cases min_max.sup_absorb2)
+ min.absorb1 min.absorb2 max.absorb1)
+by (metis abs_ge_zero le_cases max.absorb2)
lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>
\<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. g x <= k x \<Longrightarrow>
@@ -684,7 +684,7 @@
apply (rule bigo_lesseq4)
apply (erule set_plus_imp_minus)
apply (rule allI)
- apply (rule le_maxI2)
+ apply (rule max.cobounded2)
apply (rule allI)
apply (subst fun_diff_def)
apply (erule thin_rl)
@@ -695,7 +695,7 @@
apply (drule_tac x = x in spec) back
apply (metis diff_less_0_iff_less linorder_not_le not_leE xt1(12) xt1(6))
apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
-by (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
+by (metis abs_ge_zero linorder_linear max.absorb1 max.commute)
lemma bigo_lesso4:
"f <o g =o O(k\<Colon>'a=>'b\<Colon>{linordered_field}) \<Longrightarrow>
--- a/src/HOL/MicroJava/BV/Effect.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Wed Dec 25 17:39:06 2013 +0100
@@ -379,7 +379,7 @@
with Pair
have "?app s \<Longrightarrow> ?P s" by (simp only:)
moreover
- have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min_max.inf_absorb2)
+ have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min.absorb2)
ultimately
show ?thesis by (rule iffI)
qed
--- 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:06 2013 +0100
@@ -442,7 +442,7 @@
(********************************************************************************)
lemma max_of_list_elem: "x \<in> set xs \<Longrightarrow> x \<le> (max_of_list xs)"
-by (induct xs, auto intro: le_maxI1 simp: le_max_iff_disj max_of_list_def)
+by (induct xs, auto intro: max.cobounded1 simp: le_max_iff_disj max_of_list_def)
lemma max_of_list_sublist: "set xs \<subseteq> set ys
\<Longrightarrow> (max_of_list xs) \<le> (max_of_list ys)"
@@ -1053,7 +1053,7 @@
lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
\<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1064,7 +1064,7 @@
bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def ssize_sto_def max_of_list_def)
- apply (simp add: check_type_simps min_max.sup_absorb1)
+ apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="(length ST)" in exI)
apply simp+
@@ -1087,7 +1087,7 @@
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1106,7 +1106,7 @@
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1124,7 +1124,7 @@
\<Longrightarrow> bc_mt_corresp [Load i]
(\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1148,7 +1148,7 @@
apply (simp add: max_ssize_def max_of_list_def)
apply (simp add: ssize_sto_def)
apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule conjI)
apply (rule_tac x="(length ST)" in exI)
@@ -1162,7 +1162,7 @@
apply (simp add: sup_state_conv)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="(length ST)" in exI)
apply simp+
@@ -1172,7 +1172,7 @@
lemma bc_mt_corresp_Dup: "
bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1185,7 +1185,7 @@
lemma bc_mt_corresp_Dup_x1: "
bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1202,7 +1202,7 @@
(PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
- apply (simp add: check_type_simps min_max.sup_absorb1)
+ apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+
@@ -1245,7 +1245,7 @@
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Dec 25 17:39:06 2013 +0100
@@ -283,7 +283,7 @@
shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
proof -
from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
- with suc wtl show ?thesis by (simp add: min_max.inf_absorb2)
+ with suc wtl show ?thesis by (simp add: min.absorb2)
qed
lemma (in lbv) wtl_all:
@@ -298,7 +298,7 @@
with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp
from pc have "is!pc = drop pc is ! 0" by simp
with Cons have "is!pc = i" by simp
- with take pc show ?thesis by (auto simp add: min_max.inf_absorb2)
+ with take pc show ?thesis by (auto simp add: min.absorb2)
qed
section "preserves-type"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Dec 25 17:39:06 2013 +0100
@@ -2723,7 +2723,7 @@
show ?case
apply (rule_tac x="max B1 B2" in exI)
apply rule
- apply (rule min_max.less_supI1)
+ apply (rule max.strict_coboundedI1)
apply (rule B1)
apply rule
apply rule
@@ -9576,7 +9576,7 @@
show ?case
apply (rule_tac x="max B1 B2" in exI)
apply safe
- apply (rule min_max.less_supI1)
+ apply (rule max.strict_coboundedI1)
apply (rule B1)
proof -
fix a b c d :: 'n
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Dec 25 17:39:06 2013 +0100
@@ -2527,7 +2527,7 @@
apply (drule (1) bspec)
apply simp
apply (drule (1) bspec)
- apply (rule min_max.le_supI2)
+ apply (rule max.coboundedI2)
apply (erule order_trans [OF dist_triangle add_left_mono])
done
--- a/src/HOL/NanoJava/OpSem.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/NanoJava/OpSem.thy Wed Dec 25 17:39:06 2013 +0100
@@ -86,15 +86,15 @@
lemma exec_exec_max: "\<lbrakk>s1 -c1- n1 \<rightarrow> t1 ; s2 -c2- n2\<rightarrow> t2\<rbrakk> \<Longrightarrow>
s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
-by (fast intro: exec_mono le_maxI1 le_maxI2)
+by (fast intro: exec_mono max.cobounded1 max.cobounded2)
lemma eval_exec_max: "\<lbrakk>s1 -c- n1 \<rightarrow> t1 ; s2 -e\<succ>v- n2\<rightarrow> t2\<rbrakk> \<Longrightarrow>
s1 -c-max n1 n2\<rightarrow> t1 \<and> s2 -e\<succ>v-max n1 n2\<rightarrow> t2"
-by (fast intro: eval_mono exec_mono le_maxI1 le_maxI2)
+by (fast intro: eval_mono exec_mono max.cobounded1 max.cobounded2)
lemma eval_eval_max: "\<lbrakk>s1 -e1\<succ>v1- n1 \<rightarrow> t1 ; s2 -e2\<succ>v2- n2\<rightarrow> t2\<rbrakk> \<Longrightarrow>
s1 -e1\<succ>v1-max n1 n2\<rightarrow> t1 \<and> s2 -e2\<succ>v2-max n1 n2\<rightarrow> t2"
-by (fast intro: eval_mono le_maxI1 le_maxI2)
+by (fast intro: eval_mono max.cobounded1 max.cobounded2)
lemma eval_eval_exec_max:
"\<lbrakk>s1 -e1\<succ>v1-n1\<rightarrow> t1; s2 -e2\<succ>v2-n2\<rightarrow> t2; s3 -c-n3\<rightarrow> t3\<rbrakk> \<Longrightarrow>
@@ -102,7 +102,7 @@
s2 -e2\<succ>v2-max (max n1 n2) n3\<rightarrow> t2 \<and>
s3 -c -max (max n1 n2) n3\<rightarrow> t3"
apply (drule (1) eval_eval_max, erule thin_rl)
-by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2)
+by (fast intro: exec_mono eval_mono max.cobounded1 max.cobounded2)
lemma Impl_body_eq: "(\<lambda>t. \<exists>n. Z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. Z -body M-n\<rightarrow> t)"
apply (rule ext)
--- a/src/HOL/Probability/Binary_Product_Measure.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Wed Dec 25 17:39:06 2013 +0100
@@ -324,7 +324,7 @@
using `incseq F1` `incseq F2` unfolding incseq_def
by (force split: split_max)+
then have "(fst x, snd x) \<in> F1 (max i j) \<times> F2 (max i j)"
- by (intro SigmaI) (auto simp add: min_max.sup_commute)
+ by (intro SigmaI) (auto simp add: max.commute)
then show "x \<in> (\<Union>i. ?F i)" by auto
qed
then show "(\<Union>i. ?F i) = space M1 \<times> space M2"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Dec 25 17:39:06 2013 +0100
@@ -795,7 +795,7 @@
{ fix z
from F(4)[of z] have "F i z \<le> ereal (f z)"
- by (metis SUP_upper UNIV_I ereal_max_0 min_max.sup_absorb2 nonneg)
+ by (metis SUP_upper UNIV_I ereal_max_0 max.absorb2 nonneg)
with F(5)[of i z] have "real (F i z) \<le> f z"
by (cases "F i z") simp_all }
note F_bound = this
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Dec 25 17:39:06 2013 +0100
@@ -187,7 +187,7 @@
instance
by default
- (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+ (auto simp add: inf_int_def sup_int_def max_min_distrib2)
end
--- a/src/HOL/Rat.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Rat.thy Wed Dec 25 17:39:06 2013 +0100
@@ -494,7 +494,7 @@
"(sup :: rat \<Rightarrow> rat \<Rightarrow> rat) = max"
instance proof
-qed (auto simp add: inf_rat_def sup_rat_def min_max.sup_inf_distrib1)
+qed (auto simp add: inf_rat_def sup_rat_def max_min_distrib2)
end
--- a/src/HOL/Real.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Real.thy Wed Dec 25 17:39:06 2013 +0100
@@ -632,7 +632,7 @@
"(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
instance proof
-qed (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
+qed (auto simp add: inf_real_def sup_real_def max_min_distrib2)
end
--- a/src/HOL/Real_Vector_Spaces.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Wed Dec 25 17:39:06 2013 +0100
@@ -1097,12 +1097,12 @@
show ?thesis
proof (intro exI impI conjI allI)
show "0 < max 1 K"
- by (rule order_less_le_trans [OF zero_less_one le_maxI1])
+ by (rule order_less_le_trans [OF zero_less_one max.cobounded1])
next
fix x
have "norm (f x) \<le> norm x * K" using K .
also have "\<dots> \<le> norm x * max 1 K"
- by (rule mult_left_mono [OF le_maxI2 norm_ge_zero])
+ by (rule mult_left_mono [OF max.cobounded2 norm_ge_zero])
finally show "norm (f x) \<le> norm x * max 1 K" .
qed
qed
@@ -1138,9 +1138,9 @@
"\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
apply (cut_tac bounded, erule exE)
apply (rule_tac x="max 1 K" in exI, safe)
-apply (rule order_less_le_trans [OF zero_less_one le_maxI1])
+apply (rule order_less_le_trans [OF zero_less_one max.cobounded1])
apply (drule spec, drule spec, erule order_trans)
-apply (rule mult_left_mono [OF le_maxI2])
+apply (rule mult_left_mono [OF max.cobounded2])
apply (intro mult_nonneg_nonneg norm_ge_zero)
done
--- a/src/HOL/UNITY/Simple/Common.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/UNITY/Simple/Common.thy Wed Dec 25 17:39:06 2013 +0100
@@ -65,7 +65,7 @@
lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
\<in> {m} co (maxfg m)"
apply (simp add: mk_total_program_def)
-apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
+apply (simp add: constrains_def maxfg_def gasc max.absorb2)
done
(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
@@ -73,7 +73,7 @@
(UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)
\<in> {m} co (maxfg m)"
apply (simp add: mk_total_program_def)
-apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
+apply (simp add: constrains_def maxfg_def gasc max.absorb2)
done
--- a/src/HOL/Word/Bit_Representation.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Wed Dec 25 17:39:06 2013 +0100
@@ -420,7 +420,7 @@
lemma sbintrunc_sbintrunc_min [simp]:
"sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
apply (rule bin_eqI)
- apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2)
+ apply (auto simp: nth_sbintr min.absorb1 min.absorb2)
done
lemmas bintrunc_Pls =
--- a/src/HOL/Word/Bool_List_Representation.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Wed Dec 25 17:39:06 2013 +0100
@@ -906,7 +906,7 @@
apply (drule meta_spec)
apply (erule trans)
apply (drule_tac x = "bin_cat y n a" in meta_spec)
- apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
+ apply (simp add : bin_cat_assoc_sym min.absorb2)
done
lemma bin_rcat_bl:
--- a/src/HOL/Word/Misc_Numeric.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy Wed Dec 25 17:39:06 2013 +0100
@@ -20,7 +20,7 @@
lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith
-lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus]
+lemmas min_minus' [simp] = trans [OF min.commute min_minus]
lemma mod_2_neq_1_eq_eq_0:
fixes k :: int
--- a/src/HOL/Word/Word.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Word/Word.thy Wed Dec 25 17:39:06 2013 +0100
@@ -569,13 +569,13 @@
shows "len_of TYPE('a) \<le> n \<Longrightarrow> bintrunc n (uint w) = uint w"
apply (subst word_ubin.norm_Rep [symmetric])
apply (simp only: bintrunc_bintrunc_min word_size)
- apply (simp add: min_max.inf_absorb2)
+ apply (simp add: min.absorb2)
done
lemma wi_bintr:
"len_of TYPE('a::len0) \<le> n \<Longrightarrow>
word_of_int (bintrunc n w) = (word_of_int w :: 'a word)"
- by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
+ by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min.absorb1)
lemma td_ext_sbin:
"td_ext (sint :: 'a word => int) word_of_int (sints (len_of TYPE('a::len)))
@@ -3692,7 +3692,7 @@
word_of_int (bin_cat w (size b) (uint b))"
apply (unfold word_cat_def word_size)
apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
- word_ubin.eq_norm bintr_cat min_max.inf_absorb1)
+ word_ubin.eq_norm bintr_cat min.absorb1)
done
lemma word_cat_split_alt:
--- a/src/HOL/ex/Dedekind_Real.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy Wed Dec 25 17:39:06 2013 +0100
@@ -220,7 +220,7 @@
instance
by intro_classes
- (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
+ (auto simp add: inf_preal_def sup_preal_def max_min_distrib2)
end
@@ -1555,7 +1555,7 @@
"(sup \<Colon> real \<Rightarrow> real \<Rightarrow> real) = max"
instance
- by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
+ by default (auto simp add: inf_real_def sup_real_def max_min_distrib2)
end