# HG changeset patch
# User wenzelm
# Date 953928956 -3600
# Node ID fc22f59f5ae7520dc62c460af27d78fc6ef3dd16
# Parent  794843a9d8b1df0f75c225198520beacddb39fe7
use abstract syntax;
'hoare' method;

diff -r 794843a9d8b1 -r fc22f59f5ae7 src/HOL/Hoare/Hoare.ML
--- a/src/HOL/Hoare/Hoare.ML	Fri Mar 24 21:09:34 2000 +0100
+++ b/src/HOL/Hoare/Hoare.ML	Fri Mar 24 21:15:56 2000 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Hoare/Hoare.ML
+(*  Title:      hoare_vcg.thy
     ID:         $Id$
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   1998 TUM
@@ -24,7 +24,7 @@
 Goalw [Valid_def]
  "[| p <= {s. (s:b --> s:w) & (s~:b --> s:w')}; \
 \    Valid w c1 q; Valid w' c2 q |] \
-\ ==> Valid p (IF b THEN c1 ELSE c2 FI) q";
+\ ==> Valid p (Cond b c1 c2) q";
 by (Asm_simp_tac 1);
 by (Blast_tac 1);
 qed "CondRule";
@@ -39,7 +39,7 @@
 
 Goalw [Valid_def]
  "[| p <= i; Valid (i Int b) c i;  i Int (-b) <= q |] \
-\ ==> Valid p (WHILE b INV {i} DO c OD) q";
+\ ==> Valid p (While b i c) q";
 by (Asm_simp_tac 1);
 by (Clarify_tac 1);
 by (dtac lemma 1);
@@ -133,7 +133,7 @@
 (** input does not suffer any unexpected transformation                     **)
 (*****************************************************************************)
 
-val Compl_Collect = prove_goal thy "-(Collect b) = {x. ~(b x)}"
+val Compl_Collect = prove_goal (the_context ()) "-(Collect b) = {x. ~(b x)}"
     (fn _ => [Fast_tac 1]);
 
 (**Simp_tacs**)
@@ -208,3 +208,13 @@
 fun hoare_tac tac i thm =
   let val Mlem = Mset(thm)
   in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end;
+
+
+(* proof method setup *)
+
+val hoare_method =
+  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac facts THEN' hoare_tac (K all_tac)));
+
+val hoare_setup =
+ [Method.add_methods
+  [("hoare", Method.no_args hoare_method, "verification condition generator for Hoare logic")]];