# HG changeset patch
# User oheimb
# Date 962029131 -7200
# Node ID 9a64807da0235f1bf54d4688eddc85ace479bf58
# Parent  dde1affac73ea620823998bc4bff3ee341c56fdf
corrected specifications and simplified proofs

diff -r dde1affac73e -r 9a64807da023 src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Mon Jun 26 11:43:56 2000 +0200
+++ b/src/HOL/Hoare/Examples.ML	Mon Jun 26 16:18:51 2000 +0200
@@ -8,30 +8,31 @@
 
 (** multiplication by successive addition **)
 
-Goal "|- VARS m s. \
-\  {m=0 & s=0} \
+Goal "|- VARS m s a b. \
+\  {a=A & b=B} \
+\  m := 0; s := 0; \
 \  WHILE m~=a \
-\  INV {s=m*b} \  
+\  INV {s=m*b & a=A & b=B} \  
 \  DO s := s+b; m := m+1 OD \
-\  {s = a*b}";
+\  {s = A*B}"; 
 by (hoare_tac (Asm_full_simp_tac) 1);
 qed "multiply_by_add";
 
 (** Euclid's algorithm for GCD **)
 
 Goal "|- VARS a b. \
-\ {0<A & 0<B & a=A & b=B} \
+\ {0<A & 0<B} \
+\ a := A; b := B; \
 \ WHILE  a~=b  \
 \ INV {0<a & 0<b & gcd A B = gcd a b} \
 \ DO IF a<b THEN b := b-a ELSE a := a-b FI OD \
 \ {a = gcd A B}";
 by (hoare_tac (K all_tac) 1);
-
 (*Now prove the verification conditions*)
-by Auto_tac;
-by (etac gcd_nnn 4);
-by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3);
-by (force_tac (claset(),
+by   Auto_tac;
+by    (etac gcd_nnn 4);
+by   (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3);
+by  (force_tac (claset(),
                simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2);
 by (asm_simp_tac (simpset() addsimps [gcd_diff_r,less_imp_le]) 1);
 qed "Euclid_GCD";
@@ -51,7 +52,7 @@
 \ {c = A^B}";
 by (hoare_tac (Asm_full_simp_tac) 1);
 by (case_tac "b" 1);
-by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
+by  (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
 by (Asm_simp_tac 1);
 qed "power_by_mult";
 
@@ -67,36 +68,34 @@
 by (hoare_tac Asm_full_simp_tac 1);
 by (Clarify_tac 1);
 by (case_tac "a" 1);
-by (ALLGOALS
-    (asm_simp_tac
+by  (ALLGOALS (asm_simp_tac
      (simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
-qed"factorial";
+qed "factorial";
 
 (** Square root **)
 
 (* the easy way: *)
 
-Goal "|- VARS x r. \
-\ {u = 1 & w = 1 & r = 0} \
+Goal "|- VARS r x. \
+\ {True} \
+\ x := X; r := 0; \
 \ WHILE (r+1)*(r+1) <= x \
-\ INV {r*r <= x} \
+\ INV {r*r <= x & x=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);
+\ {r*r <= X & X < (r+1)*(r+1)}";
+by (hoare_tac (SELECT_GOAL Auto_tac) 1);
 qed "sqrt";
 
 (* without multiplication *)
 
-Goal "|- VARS x u w r. \
-\ {u = 1 & w = 1 & r = 0} \
+Goal "|- VARS u w r x. \
+\ {True} \
+\ x := X; u := 1; w := 1; r := 0; \
 \ WHILE w <= x \
-\ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x} \
+\ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=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);
+\ {r*r <= X & X < (r+1)*(r+1)}";
+by (hoare_tac (SELECT_GOAL Auto_tac) 1);
 qed "sqrt_without_multiplication";
 
 
@@ -110,9 +109,8 @@
 \ DO y := (hd x # y); x := tl x OD \
 \ {y=rev(X)}";
 by (hoare_tac Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-by Safe_tac;
-by (ALLGOALS(Asm_full_simp_tac ));
+by  (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
+by  Auto_tac;
 qed "imperative_reverse";
 
 Goal
@@ -126,9 +124,8 @@
 \ OD \
 \ {y = X@Y}";
 by (hoare_tac Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-by Safe_tac;
-by (ALLGOALS(Asm_full_simp_tac));
+by  (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
+by  Auto_tac;
 qed "imperative_append";
 
 
@@ -176,29 +173,12 @@
 \ {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}";
 (* expand and delete abbreviations first *)
 by (asm_simp_tac HOL_basic_ss 1);
-by (REPEAT(etac thin_rl 1));
+by (REPEAT (etac thin_rl 1));
 by (hoare_tac Asm_full_simp_tac 1);
-    by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-    by (Clarify_tac 1);
-    by (asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
+    by (SELECT_GOAL (auto_tac (claset(), simpset() addsimps [neq_Nil_conv])) 1);
    by (blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
-  by (rtac conjI 1);
-   by (Clarify_tac 1);
-   by (dtac (pred_less_imp_le RS le_imp_less_Suc) 1);
-   by (blast_tac (claset() addSEs [less_SucE]) 1);
-  by (rtac less_imp_diff_less 1);
-  by (Blast_tac 1);
- by (Clarify_tac 1);
- by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
- by (Clarify_tac 1);
- by (Simp_tac 1);
-by (Clarify_tac 1);
-by (Asm_simp_tac 1);
-by (rtac conjI 1);
- by (Clarify_tac 1);
- by (rtac order_antisym 1);
-  by (Asm_simp_tac 1);
- by (Asm_simp_tac 1);
-by (Clarify_tac 1);
-by (Asm_simp_tac 1);
+  by (blast_tac (claset() addSEs [less_SucE] addIs [less_imp_diff_less]
+                          addDs [pred_less_imp_le RS le_imp_less_Suc] ) 1);
+ by (SELECT_GOAL (auto_tac (claset(), simpset() addsimps [nth_list_update])) 1);
+by (SELECT_GOAL (auto_tac (claset() addIs [order_antisym], simpset())) 1);
 qed "Partition";