src/HOL/Hoare/Examples.thy

  DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD
  {a = gcd A B & 2*A*B = a*(x+y)}"
 apply vcg
   apply simp
  apply(simp add: distribs gcd_diff_r not_less_iff_le gcd_diff_l)
- apply arith
 apply(simp add: distribs gcd_nnn)
 done
 
 (** Power by iterated squaring and multiplication **)
 

  WHILE (r+1)*(r+1) <= x
  INV {r*r <= x & x=X}
  DO r := r+1 OD
  {r*r <= X & X < (r+1)*(r+1)}"
 apply vcg_simp
-apply auto
 done
 
 (* without multiplication *)
 
 lemma sqrt_without_multiplication: "VARS u w r x

  WHILE w <= 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)}"
 apply vcg_simp
-apply auto
 done
 
 
 (*** LISTS ***)
 

  {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
 (* expand and delete abbreviations first *)
 apply (simp);
 apply (erule thin_rl)+
 apply vcg_simp
-    apply (force simp: neq_Nil_conv)
-   apply (blast elim!: less_SucE intro: Suc_leI)
-  apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
- apply (force simp: nth_list_update)
-apply (auto intro: order_antisym)
+   apply (force simp: neq_Nil_conv)
+  apply (blast elim!: less_SucE intro: Suc_leI)
+ apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
+apply (force simp: nth_list_update)
 done
 
 end