Syntax for the special cases Min(A`I) and Max (A`I)
authorpaulson <lp15@cam.ac.uk>
Mon Apr 09 15:20:11 2018 +0100 (16 months ago)
changeset 6796983c8cafdebe8
parent 67967 5a4280946a25
child 67970 8c012a49293a
Syntax for the special cases Min(A`I) and Max (A`I)
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Factorial.thy
src/HOL/Fields.thy
src/HOL/Groups_Big.thy
src/HOL/Int.thy
src/HOL/Lattices_Big.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Apr 08 12:31:08 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Apr 09 15:20:11 2018 +0100
     1.3 @@ -297,7 +297,7 @@
     1.4  lemma norm_le_l1_cart: "norm x <= sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
     1.5    by (simp add: norm_vec_def L2_set_le_sum)
     1.6  
     1.7 -lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"
     1.8 +lemma scalar_mult_eq_scaleR [simp]: "c *s x = c *\<^sub>R x"
     1.9    unfolding scaleR_vec_def vector_scalar_mult_def by simp
    1.10  
    1.11  lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
     2.1 --- a/src/HOL/Factorial.thy	Sun Apr 08 12:31:08 2018 +0200
     2.2 +++ b/src/HOL/Factorial.thy	Mon Apr 09 15:20:11 2018 +0100
     2.3 @@ -290,17 +290,13 @@
     2.4      using prod_constant [where A="{0.. h}" and y="- 1 :: 'a"]
     2.5      by auto
     2.6    with Suc show ?thesis
     2.7 -    using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"]
     2.8 -    by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff)
     2.9 +    using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"] 
    2.10 +    by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff simp del: prod_constant)
    2.11  qed
    2.12  
    2.13  lemma pochhammer_minus':
    2.14    "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
    2.15 -  apply (simp only: pochhammer_minus [where b = b])
    2.16 -  apply (simp only: mult.assoc [symmetric])
    2.17 -  apply (simp only: power_add [symmetric])
    2.18 -  apply simp
    2.19 -  done
    2.20 +  by (simp add: pochhammer_minus)
    2.21  
    2.22  lemma pochhammer_same: "pochhammer (- of_nat n) n =
    2.23      ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * fact n"
     3.1 --- a/src/HOL/Fields.thy	Sun Apr 08 12:31:08 2018 +0200
     3.2 +++ b/src/HOL/Fields.thy	Mon Apr 09 15:20:11 2018 +0100
     3.3 @@ -46,6 +46,14 @@
     3.4  
     3.5  lemmas [arith_split] = nat_diff_split split_min split_max
     3.6  
     3.7 +context linordered_nonzero_semiring
     3.8 +begin
     3.9 +lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
    3.10 +  by (auto simp: max_def)
    3.11 +
    3.12 +lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
    3.13 +  by (auto simp: min_def)
    3.14 +end
    3.15  
    3.16  text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
    3.17  
     4.1 --- a/src/HOL/Groups_Big.thy	Sun Apr 08 12:31:08 2018 +0200
     4.2 +++ b/src/HOL/Groups_Big.thy	Mon Apr 09 15:20:11 2018 +0100
     4.3 @@ -1335,7 +1335,7 @@
     4.4    for f :: "'a \<Rightarrow> nat"
     4.5    using prod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
     4.6  
     4.7 -lemma prod_constant: "(\<Prod>x\<in> A. y) = y ^ card A"
     4.8 +lemma prod_constant [simp]: "(\<Prod>x\<in> A. y) = y ^ card A"
     4.9    for y :: "'a::comm_monoid_mult"
    4.10    by (induct A rule: infinite_finite_induct) simp_all
    4.11  
     5.1 --- a/src/HOL/Int.thy	Sun Apr 08 12:31:08 2018 +0200
     5.2 +++ b/src/HOL/Int.thy	Mon Apr 09 15:20:11 2018 +0100
     5.3 @@ -111,7 +111,6 @@
     5.4  
     5.5  end
     5.6  
     5.7 -
     5.8  subsection \<open>Ordering properties of arithmetic operations\<close>
     5.9  
    5.10  instance int :: ordered_cancel_ab_semigroup_add
    5.11 @@ -423,6 +422,12 @@
    5.12  lemma of_int_power_less_of_int_cancel_iff[simp]: "of_int x < (of_int b) ^ w\<longleftrightarrow> x < b ^ w"
    5.13    by (metis (mono_tags) of_int_less_iff of_int_power)
    5.14  
    5.15 +lemma of_int_max: "of_int (max x y) = max (of_int x) (of_int y)"
    5.16 +  by (auto simp: max_def)
    5.17 +
    5.18 +lemma of_int_min: "of_int (min x y) = min (of_int x) (of_int y)"
    5.19 +  by (auto simp: min_def)
    5.20 +
    5.21  end
    5.22  
    5.23  text \<open>Comparisons involving @{term of_int}.\<close>
     6.1 --- a/src/HOL/Lattices_Big.thy	Sun Apr 08 12:31:08 2018 +0200
     6.2 +++ b/src/HOL/Lattices_Big.thy	Mon Apr 09 15:20:11 2018 +0100
     6.3 @@ -462,8 +462,47 @@
     6.4  defines
     6.5    Min = Min.F and Max = Max.F ..
     6.6  
     6.7 +abbreviation MINIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
     6.8 +  where "MINIMUM A f \<equiv> Min(f ` A)"
     6.9 +abbreviation MAXIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    6.10 +  where "MAXIMUM A f \<equiv> Max(f ` A)"
    6.11 +
    6.12  end
    6.13  
    6.14 +
    6.15 +syntax (ASCII)
    6.16 +  "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
    6.17 +  "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _:_./ _)" [0, 0, 10] 10)
    6.18 +  "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MAX _./ _)" [0, 10] 10)
    6.19 +  "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _:_./ _)" [0, 0, 10] 10)
    6.20 +
    6.21 +syntax (output)
    6.22 +  "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
    6.23 +  "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _:_./ _)" [0, 0, 10] 10)
    6.24 +  "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MAX _./ _)" [0, 10] 10)
    6.25 +  "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _:_./ _)" [0, 0, 10] 10)
    6.26 +
    6.27 +syntax
    6.28 +  "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
    6.29 +  "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _\<in>_./ _)" [0, 0, 10] 10)
    6.30 +  "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MAX _./ _)" [0, 10] 10)
    6.31 +  "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _\<in>_./ _)" [0, 0, 10] 10)
    6.32 +
    6.33 +translations
    6.34 +  "MIN x y. B"   \<rightleftharpoons> "MIN x. MIN y. B"
    6.35 +  "MIN x. B"     \<rightleftharpoons> "CONST MINIMUM CONST UNIV (\<lambda>x. B)"
    6.36 +  "MIN x. B"     \<rightleftharpoons> "MIN x \<in> CONST UNIV. B"
    6.37 +  "MIN x\<in>A. B"   \<rightleftharpoons> "CONST MINIMUM A (\<lambda>x. B)"
    6.38 +  "MAX x y. B"   \<rightleftharpoons> "MAX x. MAX y. B"
    6.39 +  "MAX x. B"     \<rightleftharpoons> "CONST MAXIMUM CONST UNIV (\<lambda>x. B)"
    6.40 +  "MAX x. B"     \<rightleftharpoons> "MAX x \<in> CONST UNIV. B"
    6.41 +  "MAX x\<in>A. B"   \<rightleftharpoons> "CONST MAXIMUM A (\<lambda>x. B)"
    6.42 +
    6.43 +print_translation \<open>
    6.44 +  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
    6.45 +    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
    6.46 +\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
    6.47 +
    6.48  text \<open>An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin}\<close>
    6.49  
    6.50  lemma Inf_fin_Min: