--- a/src/HOL/ex/NatSum.thy Mon Aug 01 19:20:46 2005 +0200
+++ b/src/HOL/ex/NatSum.thy Mon Aug 01 19:20:47 2005 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/ex/NatSum.ML
+(* Title: HOL/ex/NatSum.thy
ID: $Id$
Author: Tobias Nipkow
*)
@@ -10,9 +10,6 @@
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/}.
*}
@@ -28,7 +25,7 @@
*}
lemma sum_of_odds: "(\<Sum>i=0..<n. Suc (i + i)) = n * n"
- by (induct n, auto)
+ by (induct n) auto
text {*
@@ -37,7 +34,7 @@
lemma sum_of_odd_squares:
"3 * (\<Sum>i=0..<n. Suc(2*i) * Suc(2*i)) = n * (4 * n * n - 1)"
- by (induct n, auto)
+ by (induct n) auto
text {*
@@ -47,7 +44,7 @@
lemma sum_of_odd_cubes:
"(\<Sum>i=0..<n. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
n * n * (2 * n * n - 1)"
- by (induct n, auto)
+ by (induct n) auto
text {*
\medskip The sum of the first @{text n} positive integers equals
@@ -55,15 +52,15 @@
lemma sum_of_naturals:
"2 * (\<Sum>i=0..n. i) = n * Suc n"
- by (induct n, auto)
+ by (induct n) auto
lemma sum_of_squares:
"6 * (\<Sum>i=0..n. i * i) = n * Suc n * Suc (2 * n)"
- by (induct n, auto)
+ by (induct n) auto
lemma sum_of_cubes:
"4 * (\<Sum>i=0..n. i * i * i) = n * n * Suc n * Suc n"
- by (induct n, auto)
+ by (induct n) auto
text {*
@@ -87,13 +84,13 @@
"30 * int (\<Sum>i=0..<m. i * i * i * i) =
int m * (int m - 1) * (int(2 * m) - 1) *
(int(3 * m * m) - int(3 * m) - 1)"
- by (induct m, simp_all add: int_mult)
+ by (induct m) (simp_all add: int_mult)
lemma of_nat_sum_of_fourth_powers:
"30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
(of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
- by (induct m, simp_all)
+ by (induct m) simp_all
text {*
@@ -102,15 +99,12 @@
*}
lemma sum_of_2_powers: "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
- apply (induct n)
- apply (auto split: nat_diff_split)
- done
+ by (induct n) (auto split: nat_diff_split)
lemma sum_of_3_powers: "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
- by (induct n, auto)
+ by (induct n) auto
lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
- by (induct n, auto)
-
+ by (induct n) auto
end
--- a/src/Pure/ML-Systems/mosml.ML Mon Aug 01 19:20:46 2005 +0200
+++ b/src/Pure/ML-Systems/mosml.ML Mon Aug 01 19:20:47 2005 +0200
@@ -57,7 +57,7 @@
structure Process = Process
structure FileSys = FileSys
end;
-
+
(*limit the printing depth*)
fun print_depth n =
(Meta.printDepth := n div 2;
@@ -114,13 +114,13 @@
-(** interrupts **) (*Note: may get into race conditions*)
+(** interrupts **) (*Note: may get into race conditions*)
(* FIXME proper implementation available? *)
exception Interrupt;
-fun ignore_interrupt f x = f x;
+fun ignore_interrupt f x = f x;
fun raise_interrupt f x = f x;
@@ -135,8 +135,7 @@
fun execute command =
let
val tmp_name = FileSys.tmpName ();
- val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn
-tmp_name);
+ val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
val result = TextIO.inputAll is;
in
TextIO.closeIn is;
--- a/src/Pure/ML-Systems/polyml-time-limit.ML Mon Aug 01 19:20:46 2005 +0200
+++ b/src/Pure/ML-Systems/polyml-time-limit.ML Mon Aug 01 19:20:47 2005 +0200
@@ -6,29 +6,32 @@
Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
*)
-structure TimeLimit : sig
- exception TimeOut
- val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
-end = struct
-
- exception TimeOut
+structure TimeLimit:
+sig
+ exception TimeOut
+ val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
+end =
+struct
+ exception TimeOut
- fun timeLimit t f x =
- let
- datatype ('a, 'b) union =
- INL of 'a | INR of 'b
- val result = Process.channel ()
- fun workerThread () =
- Process.send (result, SOME (INL (f x) handle exn => INR exn))
- val interrupt = Process.console workerThread
- val old_handle = Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE
- (fn _ => ((Process.send (result, NONE)) before (interrupt ()))))
- in
- Posix.Process.alarm t;
- case Process.receive result of
- SOME (INL fx) => (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); fx)
- | SOME (INR exn) => (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); raise exn)
- | NONE => (Signal.signal (Posix.Signal.alrm, old_handle); raise TimeOut)
- end
+ fun timeLimit t f x =
+ let
+ datatype ('a, 'b) union = INL of 'a | INR of 'b
+ val result = Process.channel ()
+ fun workerThread () =
+ Process.send (result, SOME (INL (f x) handle exn => INR exn))
+ val interrupt = Process.console workerThread
+ val old_handle = Signal.signal (Posix.Signal.alrm,
+ Signal.SIG_HANDLE (fn _ => (Process.send (result, NONE)) before (interrupt ())))
+ in
+ Posix.Process.alarm t;
+ case Process.receive result of
+ SOME (INL fx) =>
+ (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); fx)
+ | SOME (INR exn) =>
+ (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle);
+ raise exn)
+ | NONE => (Signal.signal (Posix.Signal.alrm, old_handle); raise TimeOut)
+ end
end;