--- a/src/HOL/GCD.thy Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/GCD.thy Mon Dec 28 19:23:15 2015 +0100
@@ -1489,14 +1489,14 @@
gcd_commute_int [of "n - 1" n] by auto
lemma setprod_coprime_nat [rule_format]:
- "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
+ "(ALL i: A. coprime (f i) (x::nat)) --> coprime (\<Prod>i\<in>A. f i) x"
apply (case_tac "finite A")
apply (induct set: finite)
apply (auto simp add: gcd_mult_cancel_nat)
done
lemma setprod_coprime_int [rule_format]:
- "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
+ "(ALL i: A. coprime (f i) (x::int)) --> coprime (\<Prod>i\<in>A. f i) x"
apply (case_tac "finite A")
apply (induct set: finite)
apply (auto simp add: gcd_mult_cancel_int)
--- a/src/HOL/Library/Indicator_Function.thy Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Mon Dec 28 19:23:15 2015 +0100
@@ -72,7 +72,7 @@
lemma setsum_indicator_eq_card:
assumes "finite A"
- shows "(SUM x : A. indicator B x) = card (A Int B)"
+ shows "(\<Sum>x \<in> A. indicator B x) = card (A Int B)"
using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
unfolding card_eq_setsum by simp
--- a/src/HOL/MacLaurin.thy Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/MacLaurin.thy Mon Dec 28 19:23:15 2015 +0100
@@ -223,7 +223,7 @@
have "(- 1) ^ n * diff n (- t) * (- h) ^ n / (fact n) = diff n (- t) * h ^ n / (fact n)"
by (auto simp add: power_mult_distrib[symmetric])
moreover
- have "(SUM m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / (fact m)) = (SUM m<n. diff m 0 * h ^ m / (fact m))"
+ have "(\<Sum>m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / (fact m)) = (\<Sum>m<n. diff m 0 * h ^ m / (fact m))"
by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
ultimately have " h < - t \<and>
- t < 0 \<and>
--- a/src/HOL/Metis_Examples/Big_O.thy Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Mon Dec 28 19:23:15 2015 +0100
@@ -493,7 +493,7 @@
lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 <= h x y \<Longrightarrow>
\<exists>c. \<forall>x. \<forall>y \<in> A x. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
- (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
+ (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
apply (auto simp add: bigo_def)
apply (rule_tac x = "\<bar>c\<bar>" in exI)
apply (subst abs_of_nonneg) back back
@@ -508,18 +508,18 @@
lemma bigo_setsum1: "\<forall>x y. 0 <= h x y \<Longrightarrow>
\<exists>c. \<forall>x y. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
- (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
+ (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
by (metis (no_types) bigo_setsum_main)
lemma bigo_setsum2: "\<forall>y. 0 <= h y \<Longrightarrow>
\<exists>c. \<forall>y. \<bar>f y\<bar> <= c * (h y) \<Longrightarrow>
- (\<lambda>x. SUM y : A x. f y) =o O(\<lambda>x. SUM y : A x. h y)"
+ (\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"
apply (rule bigo_setsum1)
by metis+
lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
- (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
- O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
+ (\<lambda>x. \<Sum>y \<in> A x. (l x y) * f(k x y)) =o
+ O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h(k x y)\<bar>)"
apply (rule bigo_setsum1)
apply (rule allI)+
apply (rule abs_ge_zero)
@@ -528,9 +528,9 @@
by (metis abs_ge_zero mult.left_commute mult_left_mono)
lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
- (\<lambda>x. SUM y : A x. l x y * f(k x y)) =o
- (\<lambda>x. SUM y : A x. l x y * g(k x y)) +o
- O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
+ (\<lambda>x. \<Sum>y \<in> A x. l x y * f(k x y)) =o
+ (\<lambda>x. \<Sum>y \<in> A x. l x y * g(k x y)) +o
+ O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h(k x y)\<bar>)"
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
apply (subst setsum_subtractf [symmetric])
@@ -540,10 +540,10 @@
lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
\<forall>x. 0 <= h x \<Longrightarrow>
- (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
- O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
-apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) =
- (\<lambda>x. SUM y : A x. \<bar>(l x y) * h(k x y)\<bar>)")
+ (\<lambda>x. \<Sum>y \<in> A x. (l x y) * f(k x y)) =o
+ O(\<lambda>x. \<Sum>y \<in> A x. (l x y) * h(k x y))"
+apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. (l x y) * h(k x y)) =
+ (\<lambda>x. \<Sum>y \<in> A x. \<bar>(l x y) * h(k x y)\<bar>)")
apply (erule ssubst)
apply (erule bigo_setsum3)
apply (rule ext)
@@ -553,9 +553,9 @@
lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
\<forall>x. 0 <= h x \<Longrightarrow>
- (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
- (\<lambda>x. SUM y : A x. (l x y) * g(k x y)) +o
- O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
+ (\<lambda>x. \<Sum>y \<in> A x. (l x y) * f(k x y)) =o
+ (\<lambda>x. \<Sum>y \<in> A x. (l x y) * g(k x y)) +o
+ O(\<lambda>x. \<Sum>y \<in> A x. (l x y) * h(k x y))"
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
apply (subst setsum_subtractf [symmetric])
--- a/src/HOL/Number_Theory/Cong.thy Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Mon Dec 28 19:23:15 2015 +0100
@@ -178,32 +178,32 @@
by (induct k) (auto simp add: cong_mult_int)
lemma cong_setsum_nat [rule_format]:
- "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
- [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
+ "(\<forall>x\<in>A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
+ [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
apply (cases "finite A")
apply (induct set: finite)
apply (auto intro: cong_add_nat)
done
lemma cong_setsum_int [rule_format]:
- "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
- [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
+ "(\<forall>x\<in>A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
+ [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
apply (cases "finite A")
apply (induct set: finite)
apply (auto intro: cong_add_int)
done
lemma cong_setprod_nat [rule_format]:
- "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
- [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
+ "(\<forall>x\<in>A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
+ [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
apply (cases "finite A")
apply (induct set: finite)
apply (auto intro: cong_mult_nat)
done
lemma cong_setprod_int [rule_format]:
- "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
- [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
+ "(\<forall>x\<in>A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
+ [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
apply (cases "finite A")
apply (induct set: finite)
apply (auto intro: cong_mult_int)
@@ -566,18 +566,18 @@
by (auto simp add: cong_altdef_int lcm_least_int) [1]
lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
- (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
- (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
- [x = y] (mod (PROD i:A. m i))"
+ (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
+ (\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
+ [x = y] (mod (\<Prod>i\<in>A. m i))"
apply (induct set: finite)
apply auto
apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat)
done
lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
- (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
- (ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
- [x = y] (mod (PROD i:A. m i))"
+ (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
+ (\<forall>i\<in>A. [(x::int) = y] (mod m i)) \<longrightarrow>
+ [x = y] (mod (\<Prod>i\<in>A. m i))"
apply (induct set: finite)
apply auto
apply (metis coprime_cong_mult_int gcd.commute setprod_coprime_int)
@@ -758,18 +758,18 @@
and m :: "'a \<Rightarrow> nat"
assumes fin: "finite A"
and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
- shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
+ shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))"
proof (rule finite_set_choice, rule fin, rule ballI)
fix i
assume "i : A"
- with cop have "coprime (PROD j : A - {i}. m j) (m i)"
+ with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
by (intro setprod_coprime_nat, auto)
- then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
+ then have "EX x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
by (elim cong_solve_coprime_nat)
- then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
+ then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
by auto
- moreover have "[(PROD j : A - {i}. m j) * x = 0]
- (mod (PROD j : A - {i}. m j))"
+ moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0]
+ (mod (\<Prod>j \<in> A - {i}. m j))"
by (subst mult.commute, rule cong_mult_self_nat)
ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
(mod setprod m (A - {i}))"
@@ -786,22 +786,22 @@
proof -
from chinese_remainder_aux_nat [OF fin cop] obtain b where
bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
- [b i = 0] (mod (PROD j : A - {i}. m j))"
+ [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
by blast
- let ?x = "SUM i:A. (u i) * (b i)"
+ let ?x = "\<Sum>i\<in>A. (u i) * (b i)"
show "?thesis"
proof (rule exI, clarify)
fix i
assume a: "i : A"
show "[?x = u i] (mod m i)"
proof -
- from fin a have "?x = (SUM j:{i}. u j * b j) +
- (SUM j:A-{i}. u j * b j)"
+ from fin a have "?x = (\<Sum>j \<in> {i}. u j * b j) +
+ (\<Sum>j \<in> A - {i}. u j * b j)"
by (subst setsum.union_disjoint [symmetric], auto intro: setsum.cong)
- then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
+ then have "[?x = u i * b i + (\<Sum>j \<in> A - {i}. u j * b j)] (mod m i)"
by auto
- also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
- u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
+ also have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) =
+ u i * 1 + (\<Sum>j \<in> A - {i}. u j * 0)] (mod m i)"
apply (rule cong_add_nat)
apply (rule cong_scalar2_nat)
using bprop a apply blast
@@ -822,9 +822,9 @@
qed
lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
- (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
- (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
- [x = y] (mod (PROD i:A. m i))"
+ (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
+ (\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
+ [x = y] (mod (\<Prod>i\<in>A. m i))"
apply (induct set: finite)
apply auto
apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat)
@@ -835,17 +835,17 @@
and m :: "'a \<Rightarrow> nat"
and u :: "'a \<Rightarrow> nat"
assumes fin: "finite A"
- and nz: "ALL i:A. m i \<noteq> 0"
- and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
- shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
+ and nz: "\<forall>i\<in>A. m i \<noteq> 0"
+ and cop: "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+ shows "EX! x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
proof -
from chinese_remainder_nat [OF fin cop]
obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
by blast
- let ?x = "y mod (PROD i:A. m i)"
- from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
+ let ?x = "y mod (\<Prod>i\<in>A. m i)"
+ from fin nz have prodnz: "(\<Prod>i\<in>A. m i) \<noteq> 0"
by auto
- then have less: "?x < (PROD i:A. m i)"
+ then have less: "?x < (\<Prod>i\<in>A. m i)"
by auto
have cong: "ALL i:A. [?x = u i] (mod m i)"
apply auto
@@ -859,11 +859,11 @@
apply (rule fin)
apply assumption
done
- have unique: "ALL z. z < (PROD i:A. m i) \<and>
+ have unique: "ALL z. z < (\<Prod>i\<in>A. m i) \<and>
(ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
proof (clarify)
fix z
- assume zless: "z < (PROD i:A. m i)"
+ assume zless: "z < (\<Prod>i\<in>A. m i)"
assume zcong: "(ALL i:A. [z = u i] (mod m i))"
have "ALL i:A. [?x = z] (mod m i)"
apply clarify
@@ -872,7 +872,7 @@
apply (rule cong_sym_nat)
using zcong apply auto
done
- with fin cop have "[?x = z] (mod (PROD i:A. m i))"
+ with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))"
apply (intro coprime_cong_prod_nat)
apply auto
done
--- a/src/HOL/Probability/Lebesgue_Measure.thy Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Mon Dec 28 19:23:15 2015 +0100
@@ -226,15 +226,15 @@
apply (subgoal_tac "delta i > 0")
apply arith
by (rule deltai_gt0)
- also have "... \<le> (SUM i : S. F(r i) - F(l i) + epsilon / 2^(i+2))"
+ also have "... \<le> (\<Sum>i \<in> S. F(r i) - F(l i) + epsilon / 2^(i+2))"
apply (rule setsum_mono)
apply simp
apply (rule order_trans)
apply (rule less_imp_le)
apply (rule deltai_prop)
by auto
- also have "... = (SUM i : S. F(r i) - F(l i)) +
- (epsilon / 4) * (SUM i : S. (1 / 2)^i)" (is "_ = ?t + _")
+ also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) +
+ (epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _")
by (subst setsum.distrib) (simp add: field_simps setsum_right_distrib)
also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)"
apply (rule add_left_mono)
--- a/src/HOL/Proofs/Extraction/Euclid.thy Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Euclid.thy Mon Dec 28 19:23:15 2015 +0100
@@ -123,7 +123,7 @@
qed
qed
-lemma dvd_prod [iff]: "n dvd (PROD m::nat:#mset (n # ns). m)"
+lemma dvd_prod [iff]: "n dvd (\<Prod>m::nat \<in># mset (n # ns). m)"
by (simp add: msetprod_Un msetprod_singleton)
definition all_prime :: "nat list \<Rightarrow> bool" where
@@ -140,13 +140,13 @@
lemma split_all_prime:
assumes "all_prime ms" and "all_prime ns"
- shows "\<exists>qs. all_prime qs \<and> (PROD m::nat:#mset qs. m) =
- (PROD m::nat:#mset ms. m) * (PROD m::nat:#mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
+ shows "\<exists>qs. all_prime qs \<and> (\<Prod>m::nat \<in># mset qs. m) =
+ (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
proof -
from assms have "all_prime (ms @ ns)"
by (simp add: all_prime_append)
- moreover from assms have "(PROD m::nat:#mset (ms @ ns). m) =
- (PROD m::nat:#mset ms. m) * (PROD m::nat:#mset ns. m)"
+ moreover from assms have "(\<Prod>m::nat \<in># mset (ms @ ns). m) =
+ (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)"
by (simp add: msetprod_Un)
ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
then show ?thesis ..
@@ -154,11 +154,11 @@
lemma all_prime_nempty_g_one:
assumes "all_prime ps" and "ps \<noteq> []"
- shows "Suc 0 < (PROD m::nat:#mset ps. m)"
+ shows "Suc 0 < (\<Prod>m::nat \<in># mset ps. m)"
using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
(simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
-lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = n)"
+lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = n)"
proof (induct n rule: nat_wf_ind)
case (1 n)
from `Suc 0 < n`
@@ -169,21 +169,21 @@
assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
and kn: "k < n" and nmk: "n = m * k" by iprover
- from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = m" by (rule 1)
- then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m::nat:#mset ps1. m) = m"
+ from mn and m have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = m" by (rule 1)
+ then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(\<Prod>m::nat \<in># mset ps1. m) = m"
by iprover
- from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = k" by (rule 1)
- then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m::nat:#mset ps2. m) = k"
+ from kn and k have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = k" by (rule 1)
+ then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(\<Prod>m::nat \<in># mset ps2. m) = k"
by iprover
from `all_prime ps1` `all_prime ps2`
- have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) =
- (PROD m::nat:#mset ps1. m) * (PROD m::nat:#mset ps2. m)"
+ have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) =
+ (\<Prod>m::nat \<in># mset ps1. m) * (\<Prod>m::nat \<in># mset ps2. m)"
by (rule split_all_prime)
with prod_ps1_m prod_ps2_k nmk show ?thesis by simp
next
assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps)
- moreover have "(PROD m::nat:#mset [n]. m) = n" by (simp add: msetprod_singleton)
- ultimately have "all_prime [n] \<and> (PROD m::nat:#mset [n]. m) = n" ..
+ moreover have "(\<Prod>m::nat \<in># mset [n]. m) = n" by (simp add: msetprod_singleton)
+ ultimately have "all_prime [n] \<and> (\<Prod>m::nat \<in># mset [n]. m) = n" ..
then show ?thesis ..
qed
qed
@@ -193,7 +193,7 @@
shows "\<exists>p. prime p \<and> p dvd n"
proof -
from N obtain ps where "all_prime ps"
- and prod_ps: "n = (PROD m::nat:#mset ps. m)" using factor_exists
+ and prod_ps: "n = (\<Prod>m::nat \<in># mset ps. m)" using factor_exists
by simp iprover
with N have "ps \<noteq> []"
by (auto simp add: all_prime_nempty_g_one msetprod_empty)
--- a/src/HOL/Taylor.thy Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Taylor.thy Mon Dec 28 19:23:15 2015 +0100
@@ -70,7 +70,7 @@
qed
ultimately obtain x where
"a - c < x & x < 0 &
- f (a - c + c) = (SUM m<n. diff m (0 + c) / (fact m) * (a - c) ^ m) +
+ f (a - c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (a - c) ^ m) +
diff n (x + c) / (fact n) * (a - c) ^ n"
by (rule Maclaurin_minus [THEN exE])
then have "a<x+c & x+c<c \<and> f a = (\<Sum>m<n. diff m c / (fact m) * (a - c) ^ m) +
--- a/src/HOL/UNITY/Comp/Alloc.thy Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Dec 28 19:23:15 2015 +0100
@@ -53,8 +53,8 @@
--{*spec (1)*}
system_safety :: "'a systemState program set"
where "system_safety =
- Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s)
- \<le> NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
+ Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o giv o sub i o client)s)
+ \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o rel o sub i o client)s)}"
definition
--{*spec (2)*}
@@ -120,8 +120,8 @@
where "alloc_safety =
(INT i : lessThan Nclients. Increasing (sub i o allocRel))
guarantees
- Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s)
- \<le> NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
+ Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv)s)
+ \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)}"
definition
--{*spec (8)*}
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy Mon Dec 28 19:23:15 2015 +0100
@@ -375,7 +375,7 @@
lemma alloc_refinement_lemma:
"!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
- \<subseteq> {s. (SUM x: lessThan n. f x) \<le> (SUM x: lessThan n. g x s)}"
+ \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<Sum>x \<in> lessThan n. g x s)}"
apply (induct_tac "n")
apply (auto simp add: lessThan_Suc)
done