author paulson Mon Apr 09 15:20:11 2018 +0100 (16 months ago) changeset 67969 83c8cafdebe8 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 file | annotate | diff | revisions src/HOL/Factorial.thy file | annotate | diff | revisions src/HOL/Fields.thy file | annotate | diff | revisions src/HOL/Groups_Big.thy file | annotate | diff | revisions src/HOL/Int.thy file | annotate | diff | revisions src/HOL/Lattices_Big.thy file | annotate | diff | revisions
```     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.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:
```