# HG changeset patch
# User haftmann
# Date 1624470211 0
# Node ID 7181130f58724d6a57cc4df92ed9b51f6506b680
# Parent  465846b611d571d9cdb7811316fe3b5da643f0d4
more default simp rules

diff -r 465846b611d5 -r 7181130f5872 NEWS
--- 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 ***
 
diff -r 465846b611d5 -r 7181130f5872 src/HOL/Analysis/Bochner_Integration.thy
--- 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)"
diff -r 465846b611d5 -r 7181130f5872 src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
--- 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" .
diff -r 465846b611d5 -r 7181130f5872 src/HOL/Decision_Procs/Ferrack.thy
--- 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"
diff -r 465846b611d5 -r 7181130f5872 src/HOL/HOLCF/Universal.thy
--- 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
diff -r 465846b611d5 -r 7181130f5872 src/HOL/Homology/Simplices.thy
--- 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
diff -r 465846b611d5 -r 7181130f5872 src/HOL/Import/HOL_Light_Maps.thy
--- 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
diff -r 465846b611d5 -r 7181130f5872 src/HOL/Lattices.thy
--- 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)
diff -r 465846b611d5 -r 7181130f5872 src/HOL/Library/Bit_Operations.thy
--- 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>
diff -r 465846b611d5 -r 7181130f5872 src/HOL/Library/Extended_Nonnegative_Real.thy
--- 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]
diff -r 465846b611d5 -r 7181130f5872 src/HOL/Power.thy
--- 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)