# HG changeset patch
# User paulson
# Date 1523290870 -3600
# Node ID e9f66b35d63603ccfb6947bd95d8143c1a31546e
# Parent  a5ad4c015d1c74b446e94819d4276d693036fe61# Parent  8c012a49293a4c47c2568ffdb19a1246b5c7c085
merged

diff -r a5ad4c015d1c -r e9f66b35d636 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Apr 09 16:20:23 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Apr 09 17:21:10 2018 +0100
@@ -297,7 +297,7 @@
 lemma norm_le_l1_cart: "norm x <= sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
   by (simp add: norm_vec_def L2_set_le_sum)
 
-lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"
+lemma scalar_mult_eq_scaleR [simp]: "c *s x = c *\<^sub>R x"
   unfolding scaleR_vec_def vector_scalar_mult_def by simp
 
 lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
diff -r a5ad4c015d1c -r e9f66b35d636 src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Mon Apr 09 16:20:23 2018 +0200
+++ b/src/HOL/Analysis/Determinants.thy	Mon Apr 09 17:21:10 2018 +0100
@@ -197,7 +197,7 @@
   by (simp add: det_diagonal mat_def)
 
 lemma det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
-  by (simp add: det_def prod_zero)
+  by (simp add: det_def prod_zero power_0_left)
 
 lemma det_permute_rows:
   fixes A :: "'a::comm_ring_1^'n^'n"
@@ -815,20 +815,16 @@
       apply (simp only: ab_left_minus add.assoc[symmetric])
       apply simp
       done
-    from c ci
     have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
-      unfolding sum.remove[OF fU iU] sum_cmul
-      apply -
       apply (rule vector_mul_lcancel_imp[OF ci])
-      apply (auto simp add: field_simps)
-      unfolding *
-      apply rule
+      using c ci  unfolding sum.remove[OF fU iU] sum_cmul
+      apply (auto simp add: field_simps *)
       done
     have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
       unfolding thr0
       apply (rule span_sum)
       apply simp
-      apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
+      apply (rule span_mul [where 'a="real^'n"])
       apply (rule span_superset)
       apply auto
       done
@@ -869,7 +865,7 @@
   have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A"
     apply (rule det_row_span)
     apply (rule span_sum)
-    apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
+    apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])
     apply (rule span_superset)
     apply auto
     done
diff -r a5ad4c015d1c -r e9f66b35d636 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Apr 09 16:20:23 2018 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Apr 09 17:21:10 2018 +0100
@@ -1289,7 +1289,8 @@
       have "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i::'M \<in> Basis. prj1 (vf X - uf X))"
         by (rule prod_constant [symmetric])
       also have "\<dots> = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)"
-        using prj1_idem [OF \<open>X \<in> \<D>\<close>] by (auto simp: algebra_simps intro: prod.cong)
+        apply (rule prod.cong [OF refl])
+        by (simp add: \<open>X \<in> \<D>\<close> inner_diff_left prj1_idem)
       finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)" .
       have "uf X \<in> cbox (uf X) (vf X)" "vf X \<in> cbox (uf X) (vf X)"
         using uvz [OF \<open>X \<in> \<D>\<close>] by (force simp: mem_box)+
diff -r a5ad4c015d1c -r e9f66b35d636 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Apr 09 16:20:23 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Apr 09 17:21:10 2018 +0100
@@ -660,12 +660,18 @@
 lemma integrable_cmul: "f integrable_on S \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on S"
   unfolding integrable_on_def by(auto intro: has_integral_cmul)
 
-lemma integrable_on_cmult_iff:
+lemma integrable_on_scaleR_iff [simp]:
+  fixes c :: real
+  assumes "c \<noteq> 0"
+  shows "(\<lambda>x. c *\<^sub>R f x) integrable_on S \<longleftrightarrow> f integrable_on S"
+  using integrable_cmul[of "\<lambda>x. c *\<^sub>R f x" S "1 / c"] integrable_cmul[of f S c] \<open>c \<noteq> 0\<close>
+  by auto
+
+lemma integrable_on_cmult_iff [simp]:
   fixes c :: real
   assumes "c \<noteq> 0"
   shows "(\<lambda>x. c * f x) integrable_on S \<longleftrightarrow> f integrable_on S"
-  using integrable_cmul[of "\<lambda>x. c * f x" S "1 / c"] integrable_cmul[of f S c] \<open>c \<noteq> 0\<close>
-  by auto
+  using integrable_on_scaleR_iff [of c f] assms by simp
 
 lemma integrable_on_cmult_left:
   assumes "f integrable_on S"
@@ -676,6 +682,9 @@
 lemma integrable_neg: "f integrable_on S \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on S"
   unfolding integrable_on_def by(auto intro: has_integral_neg)
 
+lemma integrable_neg_iff: "(\<lambda>x. -f(x)) integrable_on S \<longleftrightarrow> f integrable_on S"
+  using integrable_neg by fastforce
+
 lemma integrable_diff:
   "f integrable_on S \<Longrightarrow> g integrable_on S \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on S"
   unfolding integrable_on_def by(auto intro: has_integral_diff)
@@ -2295,20 +2304,20 @@
   using assms negligible_subset by force
 
 lemma negligible_Un:
-  assumes "negligible s"
-    and "negligible t"
-  shows "negligible (s \<union> t)"
-  unfolding negligible_def
-proof (safe, goal_cases)
-  case (1 a b)
-  note assms[unfolded negligible_def,rule_format,of a b]
-  then show ?case
-    apply (subst has_integral_spike_eq[OF assms(2)])
-    defer
-    apply assumption
-    unfolding indicator_def
-    apply auto
-    done
+  assumes "negligible S" and T: "negligible T"
+  shows "negligible (S \<union> T)"
+proof -
+  have "(indicat_real (S \<union> T) has_integral 0) (cbox a b)"
+    if S0: "(indicat_real S has_integral 0) (cbox a b)" 
+      and  "(indicat_real T has_integral 0) (cbox a b)" for a b
+  proof (subst has_integral_spike_eq[OF T])
+    show "indicat_real S x = indicat_real (S \<union> T) x" if "x \<in> cbox a b - T" for x
+      by (metis Diff_iff Un_iff indicator_def that)
+    show "(indicat_real S has_integral 0) (cbox a b)"
+      by (simp add: S0)
+  qed
+  with assms show ?thesis
+    unfolding negligible_def by blast
 qed
 
 lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
@@ -3430,7 +3439,7 @@
       by (simp add: inner_simps field_simps)
     ultimately show ?thesis using False
       by (simp add: image_affinity_cbox content_cbox'
-        prod.distrib[symmetric] prod_constant[symmetric] inner_diff_left)
+        prod.distrib[symmetric] prod_constant[symmetric] inner_diff_left del: prod_constant)
   qed
 qed
 
@@ -5235,19 +5244,21 @@
 
 lemma has_integral_Un:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes f: "(f has_integral i) s" "(f has_integral j) t"
-    and neg: "negligible (s \<inter> t)"
-  shows "(f has_integral (i + j)) (s \<union> t)"
-proof -
-  note * = has_integral_restrict_UNIV[symmetric, of f]
-  show ?thesis
-    unfolding *
-    apply (rule has_integral_spike[OF assms(3)])
-    defer
-    apply (rule has_integral_add[OF f[unfolded *]])
-    apply auto
-    done
-qed
+  assumes f: "(f has_integral i) S" "(f has_integral j) T"
+    and neg: "negligible (S \<inter> T)"
+  shows "(f has_integral (i + j)) (S \<union> T)"
+  unfolding has_integral_restrict_UNIV[symmetric, of f]
+proof (rule has_integral_spike[OF neg])
+  let ?f = "\<lambda>x. (if x \<in> S then f x else 0) + (if x \<in> T then f x else 0)"
+  show "(?f has_integral i + j) UNIV"
+    by (simp add: f has_integral_add)
+qed auto
+
+lemma integral_Un [simp]:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
+  assumes "f integrable_on S" "f integrable_on T" "negligible (S \<inter> T)"
+  shows "integral (S \<union> T) f = integral S f + integral T f"
+  using has_integral_Un by (simp add: has_integral_Un assms integrable_integral integral_unique)
 
 lemma integrable_Un:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"
diff -r a5ad4c015d1c -r e9f66b35d636 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Apr 09 16:20:23 2018 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Apr 09 17:21:10 2018 +0100
@@ -3434,10 +3434,12 @@
   then show ?thesis by simp
 next
   case (Suc m)
-  have th0: "a^n = prod (\<lambda>k. a) {0..m}" "(a oo c) ^ n = prod (\<lambda>k. a oo c) {0..m}"
+  have "(\<Prod>n = 0..m. a) oo c = (\<Prod>n = 0..m. a oo c)"
+    using c0 fps_compose_prod_distrib by blast
+  moreover have th0: "a^n = prod (\<lambda>k. a) {0..m}" "(a oo c) ^ n = prod (\<lambda>k. a oo c) {0..m}"
     by (simp_all add: prod_constant Suc)
-  then show ?thesis
-    by (simp add: fps_compose_prod_distrib[OF c0])
+  ultimately show ?thesis
+    by presburger
 qed
 
 lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
diff -r a5ad4c015d1c -r e9f66b35d636 src/HOL/Factorial.thy
--- a/src/HOL/Factorial.thy	Mon Apr 09 16:20:23 2018 +0200
+++ b/src/HOL/Factorial.thy	Mon Apr 09 17:21:10 2018 +0100
@@ -290,17 +290,13 @@
     using prod_constant [where A="{0.. h}" and y="- 1 :: 'a"]
     by auto
   with Suc show ?thesis
-    using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"]
-    by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff)
+    using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"] 
+    by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff simp del: prod_constant)
 qed
 
 lemma pochhammer_minus':
   "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
-  apply (simp only: pochhammer_minus [where b = b])
-  apply (simp only: mult.assoc [symmetric])
-  apply (simp only: power_add [symmetric])
-  apply simp
-  done
+  by (simp add: pochhammer_minus)
 
 lemma pochhammer_same: "pochhammer (- of_nat n) n =
     ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * fact n"
diff -r a5ad4c015d1c -r e9f66b35d636 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Mon Apr 09 16:20:23 2018 +0200
+++ b/src/HOL/Fields.thy	Mon Apr 09 17:21:10 2018 +0100
@@ -46,6 +46,14 @@
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 
+context linordered_nonzero_semiring
+begin
+lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
+  by (auto simp: max_def)
+
+lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
+  by (auto simp: min_def)
+end
 
 text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
 
diff -r a5ad4c015d1c -r e9f66b35d636 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Apr 09 16:20:23 2018 +0200
+++ b/src/HOL/Groups_Big.thy	Mon Apr 09 17:21:10 2018 +0100
@@ -1335,7 +1335,7 @@
   for f :: "'a \<Rightarrow> nat"
   using prod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
 
-lemma prod_constant: "(\<Prod>x\<in> A. y) = y ^ card A"
+lemma prod_constant [simp]: "(\<Prod>x\<in> A. y) = y ^ card A"
   for y :: "'a::comm_monoid_mult"
   by (induct A rule: infinite_finite_induct) simp_all
 
diff -r a5ad4c015d1c -r e9f66b35d636 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Apr 09 16:20:23 2018 +0200
+++ b/src/HOL/Int.thy	Mon Apr 09 17:21:10 2018 +0100
@@ -111,7 +111,6 @@
 
 end
 
-
 subsection \<open>Ordering properties of arithmetic operations\<close>
 
 instance int :: ordered_cancel_ab_semigroup_add
@@ -423,6 +422,12 @@
 lemma of_int_power_less_of_int_cancel_iff[simp]: "of_int x < (of_int b) ^ w\<longleftrightarrow> x < b ^ w"
   by (metis (mono_tags) of_int_less_iff of_int_power)
 
+lemma of_int_max: "of_int (max x y) = max (of_int x) (of_int y)"
+  by (auto simp: max_def)
+
+lemma of_int_min: "of_int (min x y) = min (of_int x) (of_int y)"
+  by (auto simp: min_def)
+
 end
 
 text \<open>Comparisons involving @{term of_int}.\<close>
diff -r a5ad4c015d1c -r e9f66b35d636 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Mon Apr 09 16:20:23 2018 +0200
+++ b/src/HOL/Lattices_Big.thy	Mon Apr 09 17:21:10 2018 +0100
@@ -462,8 +462,47 @@
 defines
   Min = Min.F and Max = Max.F ..
 
+abbreviation MINIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+  where "MINIMUM A f \<equiv> Min(f ` A)"
+abbreviation MAXIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+  where "MAXIMUM A f \<equiv> Max(f ` A)"
+
 end
 
+
+syntax (ASCII)
+  "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
+  "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _:_./ _)" [0, 0, 10] 10)
+  "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MAX _./ _)" [0, 10] 10)
+  "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _:_./ _)" [0, 0, 10] 10)
+
+syntax (output)
+  "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
+  "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _:_./ _)" [0, 0, 10] 10)
+  "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MAX _./ _)" [0, 10] 10)
+  "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _:_./ _)" [0, 0, 10] 10)
+
+syntax
+  "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
+  "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _\<in>_./ _)" [0, 0, 10] 10)
+  "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MAX _./ _)" [0, 10] 10)
+  "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _\<in>_./ _)" [0, 0, 10] 10)
+
+translations
+  "MIN x y. B"   \<rightleftharpoons> "MIN x. MIN y. B"
+  "MIN x. B"     \<rightleftharpoons> "CONST MINIMUM CONST UNIV (\<lambda>x. B)"
+  "MIN x. B"     \<rightleftharpoons> "MIN x \<in> CONST UNIV. B"
+  "MIN x\<in>A. B"   \<rightleftharpoons> "CONST MINIMUM A (\<lambda>x. B)"
+  "MAX x y. B"   \<rightleftharpoons> "MAX x. MAX y. B"
+  "MAX x. B"     \<rightleftharpoons> "CONST MAXIMUM CONST UNIV (\<lambda>x. B)"
+  "MAX x. B"     \<rightleftharpoons> "MAX x \<in> CONST UNIV. B"
+  "MAX x\<in>A. B"   \<rightleftharpoons> "CONST MAXIMUM A (\<lambda>x. B)"
+
+print_translation \<open>
+  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
+    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+
 text \<open>An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin}\<close>
 
 lemma Inf_fin_Min: