author nipkow Tue, 08 Jun 1999 12:53:20 +0200 changeset 6802 655a16e16c01 parent 6801 9e0037839d63 child 6803 8273e5a17a43
 src/HOL/Hoare/Examples.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Hoare/Examples.ML	Tue Jun 08 10:59:02 1999 +0200
+++ b/src/HOL/Hoare/Examples.ML	Tue Jun 08 12:53:20 1999 +0200
@@ -6,7 +6,7 @@

(*** ARITHMETIC ***)

-(*** multiplication by successive addition ***)
+(** multiplication by successive addition **)

Goal "|- VARS m s. \
\  {m=0 & s=0} \
@@ -17,7 +17,7 @@
by (hoare_tac (Asm_full_simp_tac) 1);

-(*** Euclid's algorithm for GCD ***)
+(** Euclid's algorithm for GCD **)

Goal "|- VARS a b. \
\ {0<A & 0<B & a=A & b=B} \
@@ -36,7 +36,7 @@
by (asm_simp_tac (simpset() addsimps [gcd_diff_r,less_imp_le]) 1);
qed "Euclid_GCD";

-(*** Power by iterated squaring and multiplication ***)
+(** Power by iterated squaring and multiplication **)

Goal "|- VARS a b c. \
\ {a=A & b=B} \
@@ -56,6 +56,8 @@
by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);
qed "power_by_mult";

+(** Factorial **)
+
Goal "|- VARS a b. \
\ {a=A} \
\ b := 1; \
@@ -71,6 +73,34 @@
qed"factorial";

+(** Square root **)
+
+(* the easy way: *
+
+Goal "|- VARS x r. \
+\ {u = 1 & w = 1 & r = 0} \
+\ WHILE (r+1)*(r+1) <= x \
+\ INV {r*r <= x} \
+\ DO r := r+1 OD \
+\ {r*r <= x & x < (r+1)*(r+1)}";
+by (hoare_tac Asm_full_simp_tac 1);
+by(arith_tac 1);
+qed "sqrt";
+
+(* without multiplication *)
+
+Goal "|- VARS x u w r. \
+\ {u = 1 & w = 1 & r = 0} \
+\ WHILE w <= x \
+\ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x} \
+\ DO r := r+1; w := w+u+2; u := u+2 OD \
+\ {r*r <= x & x < (r+1)*(r+1)}";
+by (hoare_tac Asm_full_simp_tac 1);
+by(arith_tac 1);
+by(arith_tac 1);
+qed "sqrt_without_multiplication";
+
+
(*** LISTS ***)

Goal "|- VARS y x. \```