# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1523283611 -3600
# Node ID 83c8cafdebe875ce2c8e46093c28c0b631ca16ef
# Parent  5a4280946a256bf30da3d37804e6411846033f01
Syntax for the special cases Min(A`I) and Max (A`I)

diff -r 5a4280946a25 -r 83c8cafdebe8 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Apr 09 15:20:11 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 5a4280946a25 -r 83c8cafdebe8 src/HOL/Factorial.thy
--- a/src/HOL/Factorial.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Factorial.thy	Mon Apr 09 15:20:11 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 5a4280946a25 -r 83c8cafdebe8 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Fields.thy	Mon Apr 09 15:20:11 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 5a4280946a25 -r 83c8cafdebe8 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Groups_Big.thy	Mon Apr 09 15:20:11 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 5a4280946a25 -r 83c8cafdebe8 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Int.thy	Mon Apr 09 15:20:11 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 5a4280946a25 -r 83c8cafdebe8 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Lattices_Big.thy	Mon Apr 09 15:20:11 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: