more symbols;
authorwenzelm
Mon Dec 28 19:23:15 2015 +0100 (2015-12-28)
changeset 619541d43f86f48be
parent 61953 7247cb62406c
child 61955 e96292f32c3c
more symbols;
src/HOL/GCD.thy
src/HOL/Library/Indicator_Function.thy
src/HOL/MacLaurin.thy
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Proofs/Extraction/Euclid.thy
src/HOL/Taylor.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Comp/AllocImpl.thy
     1.1 --- a/src/HOL/GCD.thy	Mon Dec 28 18:03:26 2015 +0100
     1.2 +++ b/src/HOL/GCD.thy	Mon Dec 28 19:23:15 2015 +0100
     1.3 @@ -1489,14 +1489,14 @@
     1.4      gcd_commute_int [of "n - 1" n] by auto
     1.5  
     1.6  lemma setprod_coprime_nat [rule_format]:
     1.7 -    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
     1.8 +    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (\<Prod>i\<in>A. f i) x"
     1.9    apply (case_tac "finite A")
    1.10    apply (induct set: finite)
    1.11    apply (auto simp add: gcd_mult_cancel_nat)
    1.12  done
    1.13  
    1.14  lemma setprod_coprime_int [rule_format]:
    1.15 -    "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
    1.16 +    "(ALL i: A. coprime (f i) (x::int)) --> coprime (\<Prod>i\<in>A. f i) x"
    1.17    apply (case_tac "finite A")
    1.18    apply (induct set: finite)
    1.19    apply (auto simp add: gcd_mult_cancel_int)
     2.1 --- a/src/HOL/Library/Indicator_Function.thy	Mon Dec 28 18:03:26 2015 +0100
     2.2 +++ b/src/HOL/Library/Indicator_Function.thy	Mon Dec 28 19:23:15 2015 +0100
     2.3 @@ -72,7 +72,7 @@
     2.4  
     2.5  lemma setsum_indicator_eq_card:
     2.6    assumes "finite A"
     2.7 -  shows "(SUM x : A. indicator B x) = card (A Int B)"
     2.8 +  shows "(\<Sum>x \<in> A. indicator B x) = card (A Int B)"
     2.9    using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
    2.10    unfolding card_eq_setsum by simp
    2.11  
     3.1 --- a/src/HOL/MacLaurin.thy	Mon Dec 28 18:03:26 2015 +0100
     3.2 +++ b/src/HOL/MacLaurin.thy	Mon Dec 28 19:23:15 2015 +0100
     3.3 @@ -223,7 +223,7 @@
     3.4    have "(- 1) ^ n * diff n (- t) * (- h) ^ n / (fact n) = diff n (- t) * h ^ n / (fact n)"
     3.5      by (auto simp add: power_mult_distrib[symmetric])
     3.6    moreover
     3.7 -  have "(SUM m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / (fact m)) = (SUM m<n. diff m 0 * h ^ m / (fact m))"
     3.8 +  have "(\<Sum>m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / (fact m)) = (\<Sum>m<n. diff m 0 * h ^ m / (fact m))"
     3.9      by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
    3.10    ultimately have " h < - t \<and>
    3.11      - t < 0 \<and>
     4.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Mon Dec 28 18:03:26 2015 +0100
     4.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Mon Dec 28 19:23:15 2015 +0100
     4.3 @@ -493,7 +493,7 @@
     4.4  
     4.5  lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 <= h x y \<Longrightarrow>
     4.6      \<exists>c. \<forall>x. \<forall>y \<in> A x. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
     4.7 -      (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
     4.8 +      (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
     4.9  apply (auto simp add: bigo_def)
    4.10  apply (rule_tac x = "\<bar>c\<bar>" in exI)
    4.11  apply (subst abs_of_nonneg) back back
    4.12 @@ -508,18 +508,18 @@
    4.13  
    4.14  lemma bigo_setsum1: "\<forall>x y. 0 <= h x y \<Longrightarrow>
    4.15      \<exists>c. \<forall>x y. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
    4.16 -      (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
    4.17 +      (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
    4.18  by (metis (no_types) bigo_setsum_main)
    4.19  
    4.20  lemma bigo_setsum2: "\<forall>y. 0 <= h y \<Longrightarrow>
    4.21      \<exists>c. \<forall>y. \<bar>f y\<bar> <= c * (h y) \<Longrightarrow>
    4.22 -      (\<lambda>x. SUM y : A x. f y) =o O(\<lambda>x. SUM y : A x. h y)"
    4.23 +      (\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"
    4.24  apply (rule bigo_setsum1)
    4.25  by metis+
    4.26  
    4.27  lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
    4.28 -    (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
    4.29 -      O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
    4.30 +    (\<lambda>x. \<Sum>y \<in> A x. (l x y) * f(k x y)) =o
    4.31 +      O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h(k x y)\<bar>)"
    4.32  apply (rule bigo_setsum1)
    4.33   apply (rule allI)+
    4.34   apply (rule abs_ge_zero)
    4.35 @@ -528,9 +528,9 @@
    4.36  by (metis abs_ge_zero mult.left_commute mult_left_mono)
    4.37  
    4.38  lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
    4.39 -    (\<lambda>x. SUM y : A x. l x y * f(k x y)) =o
    4.40 -      (\<lambda>x. SUM y : A x. l x y * g(k x y)) +o
    4.41 -        O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
    4.42 +    (\<lambda>x. \<Sum>y \<in> A x. l x y * f(k x y)) =o
    4.43 +      (\<lambda>x. \<Sum>y \<in> A x. l x y * g(k x y)) +o
    4.44 +        O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h(k x y)\<bar>)"
    4.45  apply (rule set_minus_imp_plus)
    4.46  apply (subst fun_diff_def)
    4.47  apply (subst setsum_subtractf [symmetric])
    4.48 @@ -540,10 +540,10 @@
    4.49  
    4.50  lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
    4.51      \<forall>x. 0 <= h x \<Longrightarrow>
    4.52 -      (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
    4.53 -        O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
    4.54 -apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) =
    4.55 -      (\<lambda>x. SUM y : A x. \<bar>(l x y) * h(k x y)\<bar>)")
    4.56 +      (\<lambda>x. \<Sum>y \<in> A x. (l x y) * f(k x y)) =o
    4.57 +        O(\<lambda>x. \<Sum>y \<in> A x. (l x y) * h(k x y))"
    4.58 +apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. (l x y) * h(k x y)) =
    4.59 +      (\<lambda>x. \<Sum>y \<in> A x. \<bar>(l x y) * h(k x y)\<bar>)")
    4.60   apply (erule ssubst)
    4.61   apply (erule bigo_setsum3)
    4.62  apply (rule ext)
    4.63 @@ -553,9 +553,9 @@
    4.64  
    4.65  lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
    4.66      \<forall>x. 0 <= h x \<Longrightarrow>
    4.67 -      (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
    4.68 -        (\<lambda>x. SUM y : A x. (l x y) * g(k x y)) +o
    4.69 -          O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
    4.70 +      (\<lambda>x. \<Sum>y \<in> A x. (l x y) * f(k x y)) =o
    4.71 +        (\<lambda>x. \<Sum>y \<in> A x. (l x y) * g(k x y)) +o
    4.72 +          O(\<lambda>x. \<Sum>y \<in> A x. (l x y) * h(k x y))"
    4.73    apply (rule set_minus_imp_plus)
    4.74    apply (subst fun_diff_def)
    4.75    apply (subst setsum_subtractf [symmetric])
     5.1 --- a/src/HOL/Number_Theory/Cong.thy	Mon Dec 28 18:03:26 2015 +0100
     5.2 +++ b/src/HOL/Number_Theory/Cong.thy	Mon Dec 28 19:23:15 2015 +0100
     5.3 @@ -178,32 +178,32 @@
     5.4    by (induct k) (auto simp add: cong_mult_int)
     5.5  
     5.6  lemma cong_setsum_nat [rule_format]:
     5.7 -    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
     5.8 -      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
     5.9 +    "(\<forall>x\<in>A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
    5.10 +      [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
    5.11    apply (cases "finite A")
    5.12    apply (induct set: finite)
    5.13    apply (auto intro: cong_add_nat)
    5.14    done
    5.15  
    5.16  lemma cong_setsum_int [rule_format]:
    5.17 -    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
    5.18 -      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
    5.19 +    "(\<forall>x\<in>A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
    5.20 +      [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
    5.21    apply (cases "finite A")
    5.22    apply (induct set: finite)
    5.23    apply (auto intro: cong_add_int)
    5.24    done
    5.25  
    5.26  lemma cong_setprod_nat [rule_format]:
    5.27 -    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
    5.28 -      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
    5.29 +    "(\<forall>x\<in>A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
    5.30 +      [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
    5.31    apply (cases "finite A")
    5.32    apply (induct set: finite)
    5.33    apply (auto intro: cong_mult_nat)
    5.34    done
    5.35  
    5.36  lemma cong_setprod_int [rule_format]:
    5.37 -    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
    5.38 -      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
    5.39 +    "(\<forall>x\<in>A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
    5.40 +      [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
    5.41    apply (cases "finite A")
    5.42    apply (induct set: finite)
    5.43    apply (auto intro: cong_mult_int)
    5.44 @@ -566,18 +566,18 @@
    5.45    by (auto simp add: cong_altdef_int lcm_least_int) [1]
    5.46  
    5.47  lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
    5.48 -    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
    5.49 -    (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
    5.50 -      [x = y] (mod (PROD i:A. m i))"
    5.51 +    (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
    5.52 +    (\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
    5.53 +      [x = y] (mod (\<Prod>i\<in>A. m i))"
    5.54    apply (induct set: finite)
    5.55    apply auto
    5.56    apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat)
    5.57    done
    5.58  
    5.59  lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
    5.60 -    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
    5.61 -    (ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
    5.62 -      [x = y] (mod (PROD i:A. m i))"
    5.63 +    (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
    5.64 +    (\<forall>i\<in>A. [(x::int) = y] (mod m i)) \<longrightarrow>
    5.65 +      [x = y] (mod (\<Prod>i\<in>A. m i))"
    5.66    apply (induct set: finite)
    5.67    apply auto
    5.68    apply (metis coprime_cong_mult_int gcd.commute setprod_coprime_int)
    5.69 @@ -758,18 +758,18 @@
    5.70      and m :: "'a \<Rightarrow> nat"
    5.71    assumes fin: "finite A"
    5.72      and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
    5.73 -  shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
    5.74 +  shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))"
    5.75  proof (rule finite_set_choice, rule fin, rule ballI)
    5.76    fix i
    5.77    assume "i : A"
    5.78 -  with cop have "coprime (PROD j : A - {i}. m j) (m i)"
    5.79 +  with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
    5.80      by (intro setprod_coprime_nat, auto)
    5.81 -  then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
    5.82 +  then have "EX x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
    5.83      by (elim cong_solve_coprime_nat)
    5.84 -  then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
    5.85 +  then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
    5.86      by auto
    5.87 -  moreover have "[(PROD j : A - {i}. m j) * x = 0]
    5.88 -    (mod (PROD j : A - {i}. m j))"
    5.89 +  moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0]
    5.90 +    (mod (\<Prod>j \<in> A - {i}. m j))"
    5.91      by (subst mult.commute, rule cong_mult_self_nat)
    5.92    ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
    5.93        (mod setprod m (A - {i}))"
    5.94 @@ -786,22 +786,22 @@
    5.95  proof -
    5.96    from chinese_remainder_aux_nat [OF fin cop] obtain b where
    5.97      bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
    5.98 -      [b i = 0] (mod (PROD j : A - {i}. m j))"
    5.99 +      [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
   5.100      by blast
   5.101 -  let ?x = "SUM i:A. (u i) * (b i)"
   5.102 +  let ?x = "\<Sum>i\<in>A. (u i) * (b i)"
   5.103    show "?thesis"
   5.104    proof (rule exI, clarify)
   5.105      fix i
   5.106      assume a: "i : A"
   5.107      show "[?x = u i] (mod m i)"
   5.108      proof -
   5.109 -      from fin a have "?x = (SUM j:{i}. u j * b j) +
   5.110 -          (SUM j:A-{i}. u j * b j)"
   5.111 +      from fin a have "?x = (\<Sum>j \<in> {i}. u j * b j) +
   5.112 +          (\<Sum>j \<in> A - {i}. u j * b j)"
   5.113          by (subst setsum.union_disjoint [symmetric], auto intro: setsum.cong)
   5.114 -      then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
   5.115 +      then have "[?x = u i * b i + (\<Sum>j \<in> A - {i}. u j * b j)] (mod m i)"
   5.116          by auto
   5.117 -      also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
   5.118 -                  u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
   5.119 +      also have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) =
   5.120 +                  u i * 1 + (\<Sum>j \<in> A - {i}. u j * 0)] (mod m i)"
   5.121          apply (rule cong_add_nat)
   5.122          apply (rule cong_scalar2_nat)
   5.123          using bprop a apply blast
   5.124 @@ -822,9 +822,9 @@
   5.125  qed
   5.126  
   5.127  lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
   5.128 -    (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   5.129 -      (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
   5.130 -         [x = y] (mod (PROD i:A. m i))"
   5.131 +    (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   5.132 +      (\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
   5.133 +         [x = y] (mod (\<Prod>i\<in>A. m i))"
   5.134    apply (induct set: finite)
   5.135    apply auto
   5.136    apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat)
   5.137 @@ -835,17 +835,17 @@
   5.138      and m :: "'a \<Rightarrow> nat"
   5.139      and u :: "'a \<Rightarrow> nat"
   5.140    assumes fin: "finite A"
   5.141 -    and nz: "ALL i:A. m i \<noteq> 0"
   5.142 -    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   5.143 -  shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
   5.144 +    and nz: "\<forall>i\<in>A. m i \<noteq> 0"
   5.145 +    and cop: "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   5.146 +  shows "EX! x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
   5.147  proof -
   5.148    from chinese_remainder_nat [OF fin cop]
   5.149    obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
   5.150      by blast
   5.151 -  let ?x = "y mod (PROD i:A. m i)"
   5.152 -  from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
   5.153 +  let ?x = "y mod (\<Prod>i\<in>A. m i)"
   5.154 +  from fin nz have prodnz: "(\<Prod>i\<in>A. m i) \<noteq> 0"
   5.155      by auto
   5.156 -  then have less: "?x < (PROD i:A. m i)"
   5.157 +  then have less: "?x < (\<Prod>i\<in>A. m i)"
   5.158      by auto
   5.159    have cong: "ALL i:A. [?x = u i] (mod m i)"
   5.160      apply auto
   5.161 @@ -859,11 +859,11 @@
   5.162      apply (rule fin)
   5.163      apply assumption
   5.164      done
   5.165 -  have unique: "ALL z. z < (PROD i:A. m i) \<and>
   5.166 +  have unique: "ALL z. z < (\<Prod>i\<in>A. m i) \<and>
   5.167        (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
   5.168    proof (clarify)
   5.169      fix z
   5.170 -    assume zless: "z < (PROD i:A. m i)"
   5.171 +    assume zless: "z < (\<Prod>i\<in>A. m i)"
   5.172      assume zcong: "(ALL i:A. [z = u i] (mod m i))"
   5.173      have "ALL i:A. [?x = z] (mod m i)"
   5.174        apply clarify
   5.175 @@ -872,7 +872,7 @@
   5.176        apply (rule cong_sym_nat)
   5.177        using zcong apply auto
   5.178        done
   5.179 -    with fin cop have "[?x = z] (mod (PROD i:A. m i))"
   5.180 +    with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))"
   5.181        apply (intro coprime_cong_prod_nat)
   5.182        apply auto
   5.183        done
     6.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Dec 28 18:03:26 2015 +0100
     6.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Dec 28 19:23:15 2015 +0100
     6.3 @@ -226,15 +226,15 @@
     6.4        apply (subgoal_tac "delta i > 0")
     6.5        apply arith
     6.6        by (rule deltai_gt0)
     6.7 -    also have "... \<le> (SUM i : S. F(r i) - F(l i) + epsilon / 2^(i+2))"
     6.8 +    also have "... \<le> (\<Sum>i \<in> S. F(r i) - F(l i) + epsilon / 2^(i+2))"
     6.9        apply (rule setsum_mono)
    6.10        apply simp
    6.11        apply (rule order_trans)
    6.12        apply (rule less_imp_le)
    6.13        apply (rule deltai_prop)
    6.14        by auto
    6.15 -    also have "... = (SUM i : S. F(r i) - F(l i)) +
    6.16 -        (epsilon / 4) * (SUM i : S. (1 / 2)^i)" (is "_ = ?t + _")
    6.17 +    also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) +
    6.18 +        (epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _")
    6.19        by (subst setsum.distrib) (simp add: field_simps setsum_right_distrib)
    6.20      also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)"
    6.21        apply (rule add_left_mono)
     7.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy	Mon Dec 28 18:03:26 2015 +0100
     7.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy	Mon Dec 28 19:23:15 2015 +0100
     7.3 @@ -123,7 +123,7 @@
     7.4    qed
     7.5  qed
     7.6  
     7.7 -lemma dvd_prod [iff]: "n dvd (PROD m::nat:#mset (n # ns). m)"
     7.8 +lemma dvd_prod [iff]: "n dvd (\<Prod>m::nat \<in># mset (n # ns). m)"
     7.9    by (simp add: msetprod_Un msetprod_singleton)
    7.10  
    7.11  definition all_prime :: "nat list \<Rightarrow> bool" where
    7.12 @@ -140,13 +140,13 @@
    7.13  
    7.14  lemma split_all_prime:
    7.15    assumes "all_prime ms" and "all_prime ns"
    7.16 -  shows "\<exists>qs. all_prime qs \<and> (PROD m::nat:#mset qs. m) =
    7.17 -    (PROD m::nat:#mset ms. m) * (PROD m::nat:#mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
    7.18 +  shows "\<exists>qs. all_prime qs \<and> (\<Prod>m::nat \<in># mset qs. m) =
    7.19 +    (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
    7.20  proof -
    7.21    from assms have "all_prime (ms @ ns)"
    7.22      by (simp add: all_prime_append)
    7.23 -  moreover from assms have "(PROD m::nat:#mset (ms @ ns). m) =
    7.24 -    (PROD m::nat:#mset ms. m) * (PROD m::nat:#mset ns. m)"
    7.25 +  moreover from assms have "(\<Prod>m::nat \<in># mset (ms @ ns). m) =
    7.26 +    (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)"
    7.27      by (simp add: msetprod_Un)
    7.28    ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
    7.29    then show ?thesis ..
    7.30 @@ -154,11 +154,11 @@
    7.31  
    7.32  lemma all_prime_nempty_g_one:
    7.33    assumes "all_prime ps" and "ps \<noteq> []"
    7.34 -  shows "Suc 0 < (PROD m::nat:#mset ps. m)"
    7.35 +  shows "Suc 0 < (\<Prod>m::nat \<in># mset ps. m)"
    7.36    using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
    7.37      (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
    7.38  
    7.39 -lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = n)"
    7.40 +lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = n)"
    7.41  proof (induct n rule: nat_wf_ind)
    7.42    case (1 n)
    7.43    from `Suc 0 < n`
    7.44 @@ -169,21 +169,21 @@
    7.45      assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
    7.46      then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
    7.47        and kn: "k < n" and nmk: "n = m * k" by iprover
    7.48 -    from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = m" by (rule 1)
    7.49 -    then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m::nat:#mset ps1. m) = m"
    7.50 +    from mn and m have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = m" by (rule 1)
    7.51 +    then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(\<Prod>m::nat \<in># mset ps1. m) = m"
    7.52        by iprover
    7.53 -    from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = k" by (rule 1)
    7.54 -    then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m::nat:#mset ps2. m) = k"
    7.55 +    from kn and k have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = k" by (rule 1)
    7.56 +    then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(\<Prod>m::nat \<in># mset ps2. m) = k"
    7.57        by iprover
    7.58      from `all_prime ps1` `all_prime ps2`
    7.59 -    have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) =
    7.60 -      (PROD m::nat:#mset ps1. m) * (PROD m::nat:#mset ps2. m)"
    7.61 +    have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) =
    7.62 +      (\<Prod>m::nat \<in># mset ps1. m) * (\<Prod>m::nat \<in># mset ps2. m)"
    7.63        by (rule split_all_prime)
    7.64      with prod_ps1_m prod_ps2_k nmk show ?thesis by simp
    7.65    next
    7.66      assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps)
    7.67 -    moreover have "(PROD m::nat:#mset [n]. m) = n" by (simp add: msetprod_singleton)
    7.68 -    ultimately have "all_prime [n] \<and> (PROD m::nat:#mset [n]. m) = n" ..
    7.69 +    moreover have "(\<Prod>m::nat \<in># mset [n]. m) = n" by (simp add: msetprod_singleton)
    7.70 +    ultimately have "all_prime [n] \<and> (\<Prod>m::nat \<in># mset [n]. m) = n" ..
    7.71      then show ?thesis ..
    7.72    qed
    7.73  qed
    7.74 @@ -193,7 +193,7 @@
    7.75    shows "\<exists>p. prime p \<and> p dvd n"
    7.76  proof -
    7.77    from N obtain ps where "all_prime ps"
    7.78 -    and prod_ps: "n = (PROD m::nat:#mset ps. m)" using factor_exists
    7.79 +    and prod_ps: "n = (\<Prod>m::nat \<in># mset ps. m)" using factor_exists
    7.80      by simp iprover
    7.81    with N have "ps \<noteq> []"
    7.82      by (auto simp add: all_prime_nempty_g_one msetprod_empty)
     8.1 --- a/src/HOL/Taylor.thy	Mon Dec 28 18:03:26 2015 +0100
     8.2 +++ b/src/HOL/Taylor.thy	Mon Dec 28 19:23:15 2015 +0100
     8.3 @@ -70,7 +70,7 @@
     8.4    qed
     8.5    ultimately obtain x where 
     8.6           "a - c < x & x < 0 &
     8.7 -      f (a - c + c) = (SUM m<n. diff m (0 + c) / (fact m) * (a - c) ^ m) +
     8.8 +      f (a - c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (a - c) ^ m) +
     8.9          diff n (x + c) / (fact n) * (a - c) ^ n"
    8.10       by (rule Maclaurin_minus [THEN exE])
    8.11    then have "a<x+c & x+c<c \<and> f a = (\<Sum>m<n. diff m c / (fact m) * (a - c) ^ m) +
     9.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Mon Dec 28 18:03:26 2015 +0100
     9.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon Dec 28 19:23:15 2015 +0100
     9.3 @@ -53,8 +53,8 @@
     9.4    --{*spec (1)*}
     9.5    system_safety :: "'a systemState program set"
     9.6    where "system_safety =
     9.7 -     Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s)
     9.8 -     \<le> NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
     9.9 +     Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o giv o sub i o client)s)
    9.10 +     \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o rel o sub i o client)s)}"
    9.11  
    9.12  definition
    9.13    --{*spec (2)*}
    9.14 @@ -120,8 +120,8 @@
    9.15    where "alloc_safety =
    9.16           (INT i : lessThan Nclients. Increasing (sub i o allocRel))
    9.17           guarantees
    9.18 -         Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s)
    9.19 -         \<le> NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
    9.20 +         Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv)s)
    9.21 +         \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)}"
    9.22  
    9.23  definition
    9.24    --{*spec (8)*}
    10.1 --- a/src/HOL/UNITY/Comp/AllocImpl.thy	Mon Dec 28 18:03:26 2015 +0100
    10.2 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Mon Dec 28 19:23:15 2015 +0100
    10.3 @@ -375,7 +375,7 @@
    10.4  
    10.5  lemma alloc_refinement_lemma:
    10.6       "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
    10.7 -      \<subseteq> {s. (SUM x: lessThan n. f x) \<le> (SUM x: lessThan n. g x s)}"
    10.8 +      \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<Sum>x \<in> lessThan n. g x s)}"
    10.9  apply (induct_tac "n")
   10.10  apply (auto simp add: lessThan_Suc)
   10.11  done