--- a/NEWS Wed Jun 23 17:43:31 2021 +0000
+++ b/NEWS Wed Jun 23 17:43:31 2021 +0000
@@ -175,6 +175,10 @@
"setBit", "clearBit". See there further the changelog in theory Guide.
INCOMPATIBILITY.
+* New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3,
+min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor
+INCOMPATIBILITY.
+
*** ML ***
--- a/src/HOL/Analysis/Bochner_Integration.thy Wed Jun 23 17:43:31 2021 +0000
+++ b/src/HOL/Analysis/Bochner_Integration.thy Wed Jun 23 17:43:31 2021 +0000
@@ -1657,7 +1657,8 @@
have U_le: "x \<in> space M \<Longrightarrow> U i x \<le> max 0 (f x)" for x i
using seq by (intro incseq_le) (auto simp: incseq_def le_fun_def)
with seq nonneg show "(\<lambda>i. integral\<^sup>L M (U i)) \<longlonglongrightarrow> LINT x|M. max 0 (f x)"
- by (intro integral_dominated_convergence) auto
+ by (intro integral_dominated_convergence)
+ (simp_all, fastforce)
have "integrable M (U i)" for i
using seq.prems by (rule integrable_bound) (insert U_le seq, auto)
with seq show "\<exists>N. \<forall>n\<ge>N. 0 \<le> integral\<^sup>L M (U n)"
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Wed Jun 23 17:43:31 2021 +0000
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Wed Jun 23 17:43:31 2021 +0000
@@ -765,13 +765,7 @@
using LIMSEQ_ignore_initial_segment [where k=2, OF b] by simp
qed
also have "(\<Sum>i\<in>Basis. max (a \<bullet> i) (min (f x \<bullet> i) (b \<bullet> i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (f x \<bullet> i) *\<^sub>R i)"
- apply (rule sum.cong)
- using fab
- apply auto
- apply (intro order_antisym)
- apply (auto simp: mem_box)
- using less_imp_le apply blast
- by (metis (full_types) linear max_less_iff_conj min.bounded_iff not_le)
+ using fab by (auto simp add: mem_box intro: sum.cong)
also have "\<dots> = f x"
using euclidean_representation by blast
finally show "(\<lambda>n. \<theta> n x) \<longlonglongrightarrow> f x" .
--- a/src/HOL/Decision_Procs/Ferrack.thy Wed Jun 23 17:43:31 2021 +0000
+++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Jun 23 17:43:31 2021 +0000
@@ -751,17 +751,7 @@
by (induct t) (simp_all add: numadd_nz numneg_nz numsub_nz nummul_nz)
lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"
-proof (induct t rule: maxcoeff.induct)
- case (2 n c t)
- then have cnz: "c \<noteq> 0" and mx: "max \<bar>c\<bar> (maxcoeff t) = 0"
- by simp_all
- have "max \<bar>c\<bar> (maxcoeff t) \<ge> \<bar>c\<bar>"
- by simp
- with cnz have "max \<bar>c\<bar> (maxcoeff t) > 0"
- by arith
- with 2 show ?case
- by simp
-qed auto
+ by (induction t rule: maxcoeff.induct) auto
lemma numgcd_nz:
assumes nz: "nozerocoeff t"
--- a/src/HOL/HOLCF/Universal.thy Wed Jun 23 17:43:31 2021 +0000
+++ b/src/HOL/HOLCF/Universal.thy Wed Jun 23 17:43:31 2021 +0000
@@ -41,7 +41,7 @@
by (rule order_trans [OF le_prod_encode_1 le_prod_encode_2])
lemma nat_less_power2: "n < 2^n"
-by (induct n) simp_all
+ by (fact less_exp)
lemma node_gt2: "\<lbrakk>finite S; b \<in> S\<rbrakk> \<Longrightarrow> b < node i a S"
unfolding node_def less_Suc_eq_le set_encode_def
--- a/src/HOL/Homology/Simplices.thy Wed Jun 23 17:43:31 2021 +0000
+++ b/src/HOL/Homology/Simplices.thy Wed Jun 23 17:43:31 2021 +0000
@@ -3241,9 +3241,12 @@
apply (subst pr_def)
apply (simp add: chain_boundary_sum chain_boundary_cmul)
apply (subst chain_boundary_def)
+ apply simp
apply (simp add: frag_cmul_sum sum.cartesian_product eq sum.union_disjoint disjoint_iff_not_equal
- sum.atLeast_Suc_atMost_Suc_shift del: sum.cl_ivl_Suc flip: comm_monoid_add_class.sum.Sigma)
- apply (simp add: comm_monoid_add_class.sum.Sigma eq2 [of _ "\<lambda>i. {_ i.._ i}"])
+ sum.atLeast_Suc_atMost_Suc_shift del: sum.cl_ivl_Suc min.absorb2 min.absorb4
+ flip: comm_monoid_add_class.sum.Sigma)
+ apply (simp add: sum.Sigma eq2 [of _ "\<lambda>i. {_ i.._ i}"]
+ del: min.absorb2 min.absorb4)
apply (simp add: sum.union_disjoint disjoint_iff_not_equal * [OF 1 2])
done
next
--- a/src/HOL/Import/HOL_Light_Maps.thy Wed Jun 23 17:43:31 2021 +0000
+++ b/src/HOL/Import/HOL_Light_Maps.thy Wed Jun 23 17:43:31 2021 +0000
@@ -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: max.absorb_iff2 fun_eq_iff)
+ by (simp add: 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.absorb_iff1 fun_eq_iff)
+ by (simp add: fun_eq_iff)
definition even
where
--- a/src/HOL/Lattices.thy Wed Jun 23 17:43:31 2021 +0000
+++ b/src/HOL/Lattices.thy Wed Jun 23 17:43:31 2021 +0000
@@ -123,6 +123,12 @@
lemma absorb2: "b \<^bold>\<le> a \<Longrightarrow> a \<^bold>* b = b"
by (rule antisym) (auto simp: refl)
+lemma absorb3: "a \<^bold>< b \<Longrightarrow> a \<^bold>* b = a"
+ by (rule absorb1) (rule strict_implies_order)
+
+lemma absorb4: "b \<^bold>< a \<Longrightarrow> a \<^bold>* b = b"
+ by (rule absorb2) (rule strict_implies_order)
+
lemma absorb_iff1: "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>* b = a"
using order_iff by auto
@@ -650,7 +656,7 @@
then show ?thesis by simp
qed
-lemma compl_less_compl_iff: "- x < - y \<longleftrightarrow> y < x" (* TODO: declare [simp] ? *)
+lemma compl_less_compl_iff [simp]: "- x < - y \<longleftrightarrow> y < x"
by (auto simp add: less_le)
lemma compl_less_swap1:
@@ -671,16 +677,16 @@
qed
lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top"
- by (simp add: inf_sup_aci sup_compl_top)
+ by (simp add: ac_simps sup_compl_top)
lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"
- by (simp add: inf_sup_aci sup_compl_top)
+ by (simp add: ac_simps sup_compl_top)
lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"
- by (simp add: inf_sup_aci inf_compl_bot)
+ by (simp add: ac_simps inf_compl_bot)
lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
- by (simp add: inf_sup_aci inf_compl_bot)
+ by (simp add: ac_simps inf_compl_bot)
declare inf_compl_bot [simp]
and sup_compl_top [simp]
@@ -743,6 +749,11 @@
+ max: semilattice_order max greater_eq greater
by standard (auto simp add: min_def max_def)
+declare min.absorb1 [simp] min.absorb2 [simp]
+ min.absorb3 [simp] min.absorb4 [simp]
+ max.absorb1 [simp] max.absorb2 [simp]
+ max.absorb3 [simp] max.absorb4 [simp]
+
lemma min_le_iff_disj: "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
unfolding min_def using linear by (auto intro: order_trans)
@@ -783,11 +794,11 @@
lemma split_min_lin [no_atp]:
\<open>P (min a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P a) \<and> (b < a \<longrightarrow> P b)\<close>
- by (cases a b rule: linorder_cases) (auto simp add: min.absorb1 min.absorb2)
+ by (cases a b rule: linorder_cases) auto
lemma split_max_lin [no_atp]:
\<open>P (max a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P b) \<and> (b < a \<longrightarrow> P a)\<close>
- by (cases a b rule: linorder_cases) (auto simp add: max.absorb1 max.absorb2)
+ by (cases a b rule: linorder_cases) auto
lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder"
by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
--- a/src/HOL/Library/Bit_Operations.thy Wed Jun 23 17:43:31 2021 +0000
+++ b/src/HOL/Library/Bit_Operations.thy Wed Jun 23 17:43:31 2021 +0000
@@ -533,7 +533,10 @@
proof (cases \<open>k \<ge> 0\<close>)
case True
moreover from power_gt_expt [of 2 \<open>nat k\<close>]
- have \<open>k < 2 ^ nat k\<close> by simp
+ have \<open>nat k < 2 ^ nat k\<close>
+ by simp
+ then have \<open>int (nat k) < int (2 ^ nat k)\<close>
+ by (simp only: of_nat_less_iff)
ultimately have *: \<open>k div 2 ^ nat k = 0\<close>
by simp
show thesis
@@ -546,8 +549,10 @@
next
case False
moreover from power_gt_expt [of 2 \<open>nat (- k)\<close>]
- have \<open>- k \<le> 2 ^ nat (- k)\<close>
+ have \<open>nat (- k) < 2 ^ nat (- k)\<close>
by simp
+ then have \<open>int (nat (- k)) < int (2 ^ nat (- k))\<close>
+ by (simp only: of_nat_less_iff)
ultimately have \<open>- k div - (2 ^ nat (- k)) = - 1\<close>
by (subst div_pos_neg_trivial) simp_all
then have *: \<open>k div 2 ^ nat (- k) = - 1\<close>
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Wed Jun 23 17:43:31 2021 +0000
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Wed Jun 23 17:43:31 2021 +0000
@@ -1305,11 +1305,24 @@
using assms(1) continuous_at_enn2ereal isCont_tendsto_compose x by fastforce
qed
-lemma tendsto_ennreal_iff[simp]:
- "\<forall>\<^sub>F x in F. 0 \<le> f x \<Longrightarrow> 0 \<le> x \<Longrightarrow> ((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
- by (auto dest: tendsto_ennrealD)
- (auto simp: ennreal_def
- intro!: continuous_on_tendsto_compose[OF continuous_on_e2ennreal[of UNIV]] tendsto_max)
+lemma tendsto_ennreal_iff [simp]:
+ \<open>((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ if \<open>\<forall>\<^sub>F x in F. 0 \<le> f x\<close> \<open>0 \<le> x\<close>
+proof
+ assume \<open>?P\<close>
+ then show \<open>?Q\<close>
+ using that by (rule tendsto_ennrealD)
+next
+ assume \<open>?Q\<close>
+ have \<open>continuous_on UNIV ereal\<close>
+ using continuous_on_ereal [of _ id] by simp
+ then have \<open>continuous_on UNIV (e2ennreal \<circ> ereal)\<close>
+ by (rule continuous_on_compose) (simp_all add: continuous_on_e2ennreal)
+ then have \<open>((\<lambda>x. (e2ennreal \<circ> ereal) (f x)) \<longlongrightarrow> (e2ennreal \<circ> ereal) x) F\<close>
+ using \<open>?Q\<close> by (rule continuous_on_tendsto_compose) simp_all
+ then show \<open>?P\<close>
+ by (simp flip: e2ennreal_ereal)
+qed
lemma tendsto_enn2ereal_iff[simp]: "((\<lambda>i. enn2ereal (f i)) \<longlongrightarrow> enn2ereal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
using continuous_on_enn2ereal[THEN continuous_on_tendsto_compose, of f x F]
--- a/src/HOL/Power.thy Wed Jun 23 17:43:31 2021 +0000
+++ b/src/HOL/Power.thy Wed Jun 23 17:43:31 2021 +0000
@@ -908,7 +908,7 @@
lemma power_gt_expt: "n > Suc 0 \<Longrightarrow> n^k > k"
by (induction k) (auto simp: less_trans_Suc n_less_m_mult_n)
-lemma less_exp:
+lemma less_exp [simp]:
\<open>n < 2 ^ n\<close>
by (simp add: power_gt_expt)