--- a/src/HOL/Finite.ML Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/Finite.ML Mon Oct 15 20:42:06 2001 +0200
@@ -716,14 +716,14 @@
Addsimps [setsum_empty];
Goalw [setsum_def]
- "!!f::'a=>'b::plus_ac0. [| finite F; a ~: F |] ==> \
-\ setsum f (insert a F) = f(a) + setsum f F";
+ "!!f. [| finite F; a ~: F |] ==> \
+\ setsum f (insert a F) = f a + setsum f F";
by (asm_simp_tac (simpset() addsimps [export fold_insert,
thm "plus_ac0_left_commute"]) 1);
qed "setsum_insert";
Addsimps [setsum_insert];
-Goal "setsum (%i. 0) A = (0::'a::plus_ac0)";
+Goal "setsum (%i. 0) A = 0";
by (case_tac "finite A" 1);
by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
by (etac finite_induct 1);
@@ -751,7 +751,7 @@
qed "card_eq_setsum";
(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
-Goal "!!g::'a=>'b::plus_ac0. [| finite A; finite B |] \
+Goal "!!g. [| finite A; finite B |] \
\ ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B";
by (etac finite_induct 1);
by (Simp_tac 1);
@@ -760,7 +760,7 @@
qed "setsum_Un_Int";
Goal "[| finite A; finite B; A Int B = {} |] \
-\ ==> setsum g (A Un B) = (setsum g A + setsum g B::'a::plus_ac0)";
+\ ==> setsum g (A Un B) = setsum g A + setsum g B";
by (stac (setsum_Un_Int RS sym) 1);
by Auto_tac;
qed "setsum_Un_disjoint";
@@ -779,7 +779,7 @@
by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1);
qed_spec_mp "setsum_UN_disjoint";
-Goal "setsum (%x. f x + g x) A = (setsum f A + setsum g A::'a::plus_ac0)";
+Goal "setsum (%x. f x + g x) A = (setsum f A + setsum g A)";
by (case_tac "finite A" 1);
by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2);
by (etac finite_induct 1);
@@ -808,7 +808,7 @@
val prems = Goal
"[| A = B; !!x. x:B ==> f x = g x|] \
-\ ==> setsum f A = (setsum g B::'a::plus_ac0)";
+\ ==> setsum f A = setsum g B";
by (case_tac "finite B" 1);
by (asm_simp_tac (simpset() addsimps [setsum_def]@prems) 2);
by (simp_tac (simpset() addsimps prems) 1);
--- a/src/HOL/Finite.thy Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/Finite.thy Mon Oct 15 20:42:06 2001 +0200
@@ -36,7 +36,7 @@
InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR"
constdefs
- card :: 'a set => nat
+ card :: 'a set => nat
"card A == THE n. (A,n) : cardR"
(*
@@ -55,12 +55,20 @@
==> (insert x A, f x y) : foldSet f e"
constdefs
- fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
+ fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
"fold f e A == THE x. (A,x) : foldSet f e"
- setsum :: "('a => 'b) => 'a set => ('b::{plus, zero})"
+ setsum :: "('a => 'b) => 'a set => 'b::plus_ac0"
"setsum f A == if finite A then fold (op+ o f) 0 A else 0"
+syntax
+ "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_:_. _" [0, 51, 10] 10)
+syntax (symbols)
+ "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_\\<in>_. _" [0, 51, 10] 10)
+translations
+ "\\<Sum>i:A. b" == "setsum (%i. b) A" (* Beware of argument permutation! *)
+
+
locale LC =
fixes
f :: ['b,'a] => 'a
--- a/src/HOL/NumberTheory/Fib.thy Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/NumberTheory/Fib.thy Mon Oct 15 20:42:06 2001 +0200
@@ -118,7 +118,7 @@
done
lemma fib_mult_eq_setsum:
- "fib (Suc n) * fib n = setsum (\<lambda>k. fib k * fib k) (atMost n)"
+ "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
apply (induct n rule: fib.induct)
apply (auto simp add: atMost_Suc fib.Suc_Suc)
apply (simp add: add_mult_distrib add_mult_distrib2)
--- a/src/HOL/UNITY/Comp/Alloc.ML Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.ML Mon Oct 15 20:42:06 2001 +0200
@@ -524,10 +524,8 @@
(*safety (1), step 3*)
Goal
- "System : Always {s. setsum (%i. (tokens o sub i o allocGiv) s) \
-\ (lessThan Nclients) \
-\ <= NbT + setsum (%i. (tokens o sub i o allocRel) s) \
-\ (lessThan Nclients)}";
+ "System : Always {s. (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocGiv) s) \
+\ <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel) s)}";
by (simp_tac (simpset() addsimps [o_apply]) 1);
by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1);
by (auto_tac (claset(),
--- a/src/HOL/UNITY/Comp/Alloc.thy Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Oct 15 20:42:06 2001 +0200
@@ -52,8 +52,8 @@
(*spec (1)*)
system_safety :: 'a systemState program set
"system_safety ==
- Always {s. setsum(%i.(tokens o giv o sub i o client)s) (lessThan Nclients)
- <= NbT + setsum(%i.(tokens o rel o sub i o client)s) (lessThan Nclients)}"
+ Always {s. (\\<Sum>i: lessThan Nclients. (tokens o giv o sub i o client)s)
+ <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
(*spec (2)*)
system_progress :: 'a systemState program set
@@ -111,8 +111,8 @@
"alloc_safety ==
(INT i : lessThan Nclients. Increasing (sub i o allocRel))
guarantees
- Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients)
- <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
+ Always {s. (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocGiv)s)
+ <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
(*spec (8)*)
alloc_progress :: 'a allocState_d program set
--- a/src/HOL/UNITY/Comp/AllocBase.ML Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.ML Mon Oct 15 20:42:06 2001 +0200
@@ -48,14 +48,14 @@
Addcongs [setsum_cong];
-Goal "setsum (%i. {#if i<k then f i else g i#}) (A Int lessThan k) = \
-\ setsum (%i. {#f i#}) (A Int lessThan k)";
+Goal "(\\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) = \
+\ (\\<Sum>i: A Int lessThan k. {#f i#})";
by (rtac setsum_cong 1);
by Auto_tac;
qed "bag_of_sublist_lemma";
Goal "bag_of (sublist l A) = \
-\ setsum (%i. {# l!i #}) (A Int lessThan (length l))";
+\ (\\<Sum>i: A Int lessThan (length l). {# l!i #})";
by (rev_induct_tac "l" 1);
by (Simp_tac 1);
by (asm_simp_tac
@@ -81,7 +81,7 @@
Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \
\ ==> bag_of (sublist l (UNION I A)) = \
-\ setsum (%i. bag_of (sublist l (A i))) I";
+\ (\\<Sum>i:I. bag_of (sublist l (A i)))";
by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
addsimps [bag_of_sublist]) 1);
by (stac setsum_UN_disjoint 1);
--- a/src/HOL/UNITY/Comp/AllocImpl.ML Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.ML Mon Oct 15 20:42:06 2001 +0200
@@ -44,9 +44,8 @@
Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
\ ==> M Join G : Always \
-\ {s. setsum (%i. bag_of (sublist (merge.Out s) \
-\ {k. k < length (iOut s) & iOut s ! k = i})) \
-\ (lessThan Nclients) = \
+\ {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (merge.Out s) \
+\ {k. k < length (iOut s) & iOut s ! k = i})) = \
\ (bag_of o merge.Out) s}";
by (rtac ([[Merge_Always_Out_eq_iOut, Merge_Bounded] MRS Always_Int_I,
UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
@@ -65,8 +64,7 @@
Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
\ guarantees \
\ (bag_of o merge.Out) Fols \
-\ (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
-\ (lessThan Nclients))";
+\ (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o merge.In) s)";
by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
by Auto_tac;
by (rtac Follows_setsum 1);
@@ -103,9 +101,8 @@
Goal "[| G : preserves distr.Out; \
\ D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
\ ==> D Join G : Always \
-\ {s. setsum (%i. bag_of (sublist (distr.In s) \
-\ {k. k < length (iIn s) & iIn s ! k = i})) \
-\ (lessThan Nclients) = \
+\ {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (distr.In s) \
+\ {k. k < length (iIn s) & iIn s ! k = i})) = \
\ bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}";
by (etac ([asm_rl, UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
by Auto_tac;
@@ -133,7 +130,7 @@
\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
\ guarantees \
\ (INT i : lessThan Nclients. \
-\ (%s. setsum (%i. (bag_of o sub i o distr.Out) s) (lessThan Nclients)) \
+\ (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o distr.Out) s) \
\ Fols \
\ (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
by (rtac guaranteesI 1);
@@ -152,8 +149,8 @@
Close_locale "Distrib";
-Goal "!!f::nat=>nat. (INT i:(lessThan n). {s. f i <= g i s}) \
-\ <= {s. setsum f (lessThan n) <= setsum (%i. g i s) (lessThan n)}";
+Goal "!!f::nat=>nat. (INT i: lessThan n. {s. f i <= g i s}) \
+\ <= {s. (\\<Sum>i: lessThan n. f i) <= (\\<Sum>i: lessThan n. g i s)}";
by (induct_tac "n" 1);
by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
qed "alloc_refinement_lemma";
@@ -177,8 +174,8 @@
\ Int \
\ (INT hf. (INT i : lessThan Nclients. \
\ {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) \
-\ LeadsTo {s. setsum (%i. tokens (hf i)) (lessThan Nclients) <= \
-\ setsum (%i. (tokens o sub i o allocRel)s) (lessThan Nclients) })";
+\ LeadsTo {s. (\\<Sum>i: lessThan Nclients. tokens (hf i)) <= \
+\ (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)})";
by (auto_tac (claset(), simpset() addsimps [ball_conj_distrib]));
by (rename_tac "F hf" 1);
by (rtac ([Finite_stable_completion, alloc_refinement_lemma]
--- a/src/HOL/UNITY/Follows.ML Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/UNITY/Follows.ML Mon Oct 15 20:42:06 2001 +0200
@@ -233,7 +233,7 @@
Goal "!!f ::['c,'b] => ('a::order) multiset. \
\ [| ALL i: I. F : f' i Fols f i; finite I |] \
-\ ==> F : (%s. setsum (%i. f' i s) I) Fols (%s. setsum (%i. f i s) I)";
+\ ==> F : (%s. \\<Sum>i:I. f' i s) Fols (%s. \\<Sum>i:I. f i s)";
by (etac rev_mp 1);
by (etac finite_induct 1);
by (asm_simp_tac (simpset() addsimps [Follows_union]) 2);
--- a/src/HOL/ex/NatSum.thy Mon Oct 15 20:41:14 2001 +0200
+++ b/src/HOL/ex/NatSum.thy Mon Oct 15 20:42:06 2001 +0200
@@ -1,21 +1,22 @@
(* Title: HOL/ex/NatSum.ML
ID: $Id$
Author: Tobias Nipkow
- Copyright 1994 TU Muenchen
-
-Summing natural numbers, squares, cubes, etc.
-
-Originally demonstrated permutative rewriting, but add_ac is no longer
-needed thanks to new simprocs.
-
-Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
-http://www.research.att.com/~njas/sequences/
*)
header {* Summing natural numbers *}
theory NatSum = Main:
+text {*
+ Summing natural numbers, squares, cubes, etc.
+
+ Originally demonstrated permutative rewriting, but @{thm [source]
+ add_ac} is no longer needed thanks to new simprocs.
+
+ Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
+ \url{http://www.research.att.com/~njas/sequences/}.
+*}
+
declare lessThan_Suc [simp] atMost_Suc [simp]
declare add_mult_distrib [simp] add_mult_distrib2 [simp]
declare diff_mult_distrib [simp] diff_mult_distrib2 [simp]
@@ -25,7 +26,7 @@
squared.
*}
-lemma sum_of_odds: "setsum (\<lambda>i. Suc (i + i)) (lessThan n) = n * n"
+lemma sum_of_odds: "(\<Sum>i \<in> {..n(}. Suc (i + i)) = n * n"
apply (induct n)
apply auto
done
@@ -36,11 +37,10 @@
*}
lemma sum_of_odd_squares:
- "3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
- n * (4 * n * n - Numeral1)"
+ "3 * (\<Sum>i \<in> {..n(}. Suc (i + i) * Suc (i + i)) =
+ n * (4 * n * n - 1)"
apply (induct n)
- txt {* This removes the @{term "-Numeral1"} from the inductive step *}
- apply (case_tac [2] n)
+ apply (case_tac [2] n) -- {* eliminates the subtraction *}
apply auto
done
@@ -50,11 +50,10 @@
*}
lemma sum_of_odd_cubes:
- "setsum (\<lambda>i. Suc (i + i) * Suc (i + i) * Suc (i + i)) (lessThan n) =
- n * n * (2 * n * n - Numeral1)"
- apply (induct "n")
- txt {* This removes the @{term "-Numeral1"} from the inductive step *}
- apply (case_tac [2] "n")
+ "(\<Sum>i \<in> {..n(}. Suc (i + i) * Suc (i + i) * Suc (i + i)) =
+ n * n * (2 * n * n - 1)"
+ apply (induct n)
+ apply (case_tac [2] n) -- {* eliminates the subtraction *}
apply auto
done
@@ -63,19 +62,19 @@
@{text "n (n + 1) / 2"}.*}
lemma sum_of_naturals:
- "2 * setsum id (atMost n) = n * Suc n"
+ "2 * (\<Sum>i \<in> {..n}. i) = n * Suc n"
apply (induct n)
apply auto
done
lemma sum_of_squares:
- "6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (2 * n)"
+ "6 * (\<Sum>i \<in> {..n}. i * i) = n * Suc n * Suc (2 * n)"
apply (induct n)
apply auto
done
lemma sum_of_cubes:
- "4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
+ "4 * (\<Sum>i \<in> {..n}. i * i * i) = n * n * Suc n * Suc n"
apply (induct n)
apply auto
done
@@ -86,12 +85,11 @@
*}
lemma sum_of_fourth_powers:
- "30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
- n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - Numeral1)"
+ "30 * (\<Sum>i \<in> {..n}. i * i * i * i) =
+ n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
apply (induct n)
apply auto
- txt {* Eliminates the subtraction *}
- apply (case_tac n)
+ apply (case_tac n) -- {* eliminates the subtraction *}
apply simp_all
done
@@ -107,28 +105,30 @@
zdiff_zmult_distrib2 [simp]
lemma int_sum_of_fourth_powers:
- "30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
- int m * (int m - Numeral1) * (int (2 * m) - Numeral1) *
- (int (3 * m * m) - int (3 * m) - Numeral1)"
+ "30 * int (\<Sum>i \<in> {..m(}. i * i * i * i) =
+ int m * (int m - 1) * (int (2 * m) - 1) *
+ (int (3 * m * m) - int (3 * m) - 1)"
apply (induct m)
apply simp_all
done
text {*
- \medskip Sums of geometric series: 2, 3 and the general case *}
+ \medskip Sums of geometric series: @{term 2}, @{term 3} and the
+ general case.
+*}
-lemma sum_of_2_powers: "setsum (\<lambda>i. 2^i) (lessThan n) = 2^n - (1::nat)"
+lemma sum_of_2_powers: "(\<Sum>i \<in> {..n(}. 2^i) = 2^n - (1::nat)"
apply (induct n)
- apply (auto split: nat_diff_split)
+ apply (auto split: nat_diff_split)
done
-lemma sum_of_3_powers: "2 * setsum (\<lambda>i. 3^i) (lessThan n) = 3^n - (1::nat)"
+lemma sum_of_3_powers: "2 * (\<Sum>i \<in> {..n(}. 3^i) = 3^n - (1::nat)"
apply (induct n)
apply auto
done
-lemma sum_of_powers: "0 < k ==> (k - 1) * setsum (\<lambda>i. k^i) (lessThan n) = k^n - (1::nat)"
+lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i \<in> {..n(}. k^i) = k^n - (1::nat)"
apply (induct n)
apply auto
done