Added a verified verification-condition generator.

--- a/src/HOL/IMP/Hoare.ML	Sat Jan 20 02:00:11 1996 +0100
+++ b/src/HOL/IMP/Hoare.ML	Tue Jan 23 10:59:35 1996 +0100
@@ -3,55 +3,28 @@
     Author: 	Tobias Nipkow
     Copyright   1995 TUM
 
-Derivation of Hoare rules
+Soundness of Hoare rules wrt denotational semantics
 *)
 
 open Hoare;
 
-Unify.trace_bound := 30;
-Unify.search_bound := 30;
-
-goalw Hoare.thy [spec_def]
-  "!!P.[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] \
-\  ==> {{P'}}c{{Q'}}";
-by(fast_tac HOL_cs 1);
-bind_thm("hoare_conseq", impI RSN (3,allI RSN (3,impI RS allI RS result())));
-
-goalw Hoare.thy (spec_def::C_simps)  "{{P}} skip {{P}}";
-by(fast_tac comp_cs 1);
-qed"hoare_skip";
-
-goalw Hoare.thy (spec_def::C_simps)
-  "!!P. [| !s. P s --> Q(s[A a s/x]) |] ==> {{P}} x := a {{Q}}";
-by(Asm_full_simp_tac 1);
-qed"hoare_assign";
-
-goalw Hoare.thy (spec_def::C_simps)
-  "!!P. [| {{P}} c {{Q}}; {{Q}} d {{R}} |] ==> {{P}} c;d {{R}}";
-by(fast_tac comp_cs 1);
-qed"hoare_seq";
-
-goalw Hoare.thy (spec_def::C_simps)
-  "!!P. [| {{%s. P s & B b s}} c {{Q}}; {{%s. P s & ~B b s}} d {{Q}} |] ==> \
-\  {{P}} ifc b then c else d {{Q}}";
-by(Simp_tac 1);
-by(fast_tac comp_cs 1);
-qed"hoare_if";
-
-goalw Hoare.thy (spec_def::C_simps)
-  "!!P. [| {{%s. P s & B b s}} c {{P}} |] ==> \
-\  {{P}} while b do c {{%s. P s & ~B b s}}";
+goalw Hoare.thy [spec_def] "!P c Q. ({{P}}c{{Q}}) --> spec P c Q";
+br hoare.mutual_induct 1;
+    by(ALLGOALS Asm_simp_tac);
+  by(fast_tac rel_cs 1);
+ by(fast_tac HOL_cs 1);
 br allI 1;
 br allI 1;
 br impI 1;
 be induct2 1;
-br Gamma_mono 1;
+ br Gamma_mono 1;
 by (rewrite_goals_tac [Gamma_def]);  
 by(eres_inst_tac [("x","a")] allE 1);
 by (safe_tac comp_cs);
-by(ALLGOALS Asm_full_simp_tac);
-qed"hoare_while";
+  by(ALLGOALS Asm_full_simp_tac);
+qed "hoare_sound";
 
+(*
 fun while_tac inv ss i =
   EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i,
         asm_full_simp_tac ss (i+1)];
@@ -75,3 +48,4 @@
 by(while_tac "%s.s z = i + s u & s y = j" ss 3);
 by(hoare_tac ss);
 result();
+*)

--- a/src/HOL/IMP/Hoare.thy	Sat Jan 20 02:00:11 1996 +0100
+++ b/src/HOL/IMP/Hoare.thy	Tue Jan 23 10:59:35 1996 +0100
@@ -3,47 +3,32 @@
     Author: 	Tobias Nipkow
     Copyright   1995 TUM
 
-Semantic embedding of Hoare logic
+Inductive definition of Hoare logic
 *)
 
 Hoare = Denotation +
+
+types assn = state => bool
+
 consts
+  hoare :: "(assn * com * assn) set"
   spec :: [state=>bool,com,state=>bool] => bool
-(* syntax "@spec" :: [bool,com,bool] => bool *)
-          ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
 defs
   spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
-end
-(* Pretty-printing of assertions.
-   Not very helpful as long as programs are not pretty-printed.
-ML
 
-local open Syntax
-
-fun is_loc a = let val ch = hd(explode a)
-               in ord "A" <= ord ch andalso ord ch <= ord "Z" end;
-
-fun tr(s$t,i) = tr(s,i)$tr(t,i)
-  | tr(Abs(x,T,u),i) = Abs(x,T,tr(u,i+1))
-  | tr(t as Free(a,T),i) = if is_loc a then Bound(i) $ free(a) else t
-  | tr(t,_) = t;
+syntax "@hoare" :: [bool,com,bool] => bool ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
+translations "{{P}}c{{Q}}" == "(P,c,Q) : hoare"
 
-fun cond_tr(p) = Abs("",dummyT,tr(p,0))
-
-fun spec_tr[p,c,q] = const"spec" $ cond_tr p $ c $ cond_tr q;
-
-fun tr'(t as (Bound j $ (u as Free(a,_))),i) = if i=j then u else t
-  | tr'(s$t,i) = tr'(s,i)$tr'(t,i)
-  | tr'(Abs(x,T,u),i) = Abs(x,T,tr'(u,i+1))
-  | tr'(t,_) = t;
-
-fun spec_tr'[Abs(_,_,p),c,Abs(_,_,q)] =
-  const"@spec" $ tr'(p,0) $ c $ tr'(q,0);
-
-in
-
-val parse_translation = [("@spec", spec_tr)];
-val print_translation = [("spec", spec_tr')];
+inductive "hoare"
+intrs
+  hoare_skip "{{P}}skip{{P}}"
+  hoare_ass  "{{%s.P(s[A a s/x])}} x:=a {{P}}"
+  hoare_semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
+  hoare_if   "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
+              {{P}} ifc b then c else d {{Q}}"
+  hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==>
+	       {{P}} while b do c {{%s. P s & ~B b s}}"
+  hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
+		{{P'}}c{{Q'}}"
 
 end
-*)

--- a/src/HOL/IMP/README.html	Sat Jan 20 02:00:11 1996 +0100
+++ b/src/HOL/IMP/README.html	Tue Jan 23 10:59:35 1996 +0100
@@ -1,20 +1,21 @@
 <HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
 
-<H2>IMP --- A <KBD>while</KBD>-Language and its 3 Semantics</H2>
+<H2>IMP --- A <KBD>while</KBD>-language and its 3 Semantics</H2>
 
 The formalization of the denotational, operational and axiomatic semantics of
 a simple while-language, including
 <UL>
 <LI> an equivalence proof between denotational and operational semantics and
-<LI> the derivation of the Hoare rules from the denotational semantics.
+<LI> a soundness proof of the Hoare rules w.r.t. the denotational semantics.
 </UL>
 The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
 <P>
 <KBD>
-@book{Winskel,author={Glynn Winskel},
-title={The Formal Semantics of Programming Languages},
-publisher={MIT Press},year=1993}
+@book{Winskel, author = {Glynn Winskel},
+title = {The Formal Semantics of Programming Languages},
+publisher = {MIT Press}, year = 1993}
 </KBD>
 <P>
-Here is the documentation.
+In addition, a verification-condition-generator is proved sound and complete
+w.r.t. the Hoare rules.
 </BODY></HTML>

--- a/src/HOL/IMP/ROOT.ML	Sat Jan 20 02:00:11 1996 +0100
+++ b/src/HOL/IMP/ROOT.ML	Tue Jan 23 10:59:35 1996 +0100
@@ -10,4 +10,4 @@
 proof_timing := true;
 time_use_thy "Properties";
 time_use_thy "Equiv";
-time_use_thy "Hoare";
+time_use_thy "VC";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/VC.ML	Tue Jan 23 10:59:35 1996 +0100
@@ -0,0 +1,79 @@
+(*  Title: 	HOL/IMP/VC.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1996 TUM
+
+Soundness and completeness of vc
+*)
+
+open VC;
+
+val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[fast_tac HOL_cs 1]);
+
+goal VC.thy "!Q. (!s. vc c Q s) --> ({{wp c Q}} (astrip c) {{Q}})";
+by(acom.induct_tac "c" 1);
+    by(ALLGOALS Simp_tac);
+    by(fast_tac (HOL_cs addIs hoare.intrs) 1);
+   by(fast_tac (HOL_cs addIs hoare.intrs) 1);
+  by(fast_tac (HOL_cs addIs hoare.intrs) 1);
+ (* if *)
+ br allI 1;
+ br impI 1;
+ brs hoare.intrs 1;
+  brs hoare.intrs 1;
+    by(fast_tac HOL_cs 2);
+   by(fast_tac HOL_cs 1);
+  by(fast_tac HOL_cs 1);
+ brs hoare.intrs 1;
+   by(fast_tac HOL_cs 2);
+  by(fast_tac HOL_cs 1);
+ by(fast_tac HOL_cs 1);
+(* while *)
+by(safe_tac HOL_cs);
+brs hoare.intrs 1;
+  br lemma 1;
+ brs hoare.intrs 1;
+ brs hoare.intrs 1;
+   by(fast_tac HOL_cs 2);
+  by(ALLGOALS(fast_tac HOL_cs));
+qed "vc_sound";
+
+goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)";
+by(acom.induct_tac "c" 1);
+    by(ALLGOALS Asm_simp_tac);
+by(EVERY1[rtac allI, rtac allI, rtac impI]);
+by(EVERY1[etac allE, etac allE, etac mp]);
+by(EVERY1[etac allE, etac allE, etac mp, atac]);
+bind_thm("wp_mono", result() RS spec RS spec RS mp RS spec RS mp);
+
+goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
+by(acom.induct_tac "c" 1);
+    by(ALLGOALS Asm_simp_tac);
+by(safe_tac HOL_cs);
+by(EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
+by(fast_tac (HOL_cs addEs [wp_mono]) 1);
+bind_thm("vc_mono", result() RS spec RS spec RS mp RS spec RS mp);
+
+goal VC.thy
+  "!P c Q. ({{P}}c{{Q}}) --> \
+\          (? ac. astrip ac = c & (!s. P s --> wp ac Q s) & (!s. vc ac Q s))";
+br hoare.mutual_induct 1;
+     by(res_inst_tac [("x","Askip")] exI 1);
+     by(Simp_tac 1);
+    by(res_inst_tac [("x","Aass x a")] exI 1);
+    by(Simp_tac 1);
+   by(SELECT_GOAL(safe_tac HOL_cs)1);
+   by(res_inst_tac [("x","Asemi ac aca")] exI 1);
+   by(Asm_simp_tac 1);
+   by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
+  by(SELECT_GOAL(safe_tac HOL_cs)1);
+  by(res_inst_tac [("x","Aif b ac aca")] exI 1);
+  by(Asm_simp_tac 1);
+ by(SELECT_GOAL(safe_tac HOL_cs)1);
+ by(res_inst_tac [("x","Awhile b P ac")] exI 1);
+ by(Asm_simp_tac 1);
+by(SELECT_GOAL(safe_tac HOL_cs)1);
+by(res_inst_tac [("x","ac")] exI 1);
+by(Asm_simp_tac 1);
+by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
+qed "vc_complete";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/VC.thy	Tue Jan 23 10:59:35 1996 +0100
@@ -0,0 +1,45 @@
+(*  Title: 	HOL/IMP/VC.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1996 TUM
+
+acom: annotated commands
+vc:   verification-conditions
+wp:   weakest (liberal) precondition
+*)
+
+VC  =  Hoare +
+
+datatype  acom = Askip
+               | Aass   loc aexp
+               | Asemi  acom acom
+               | Aif    bexp acom acom
+               | Awhile bexp assn acom
+
+consts
+  vc,wp :: acom => assn => assn
+  astrip :: acom => com
+
+primrec wp acom
+  wp_Askip  "wp Askip Q = Q"
+  wp_Aass   "wp (Aass x a) Q = (%s.Q(s[A a s/x]))"
+  wp_Asemi  "wp (Asemi c d) Q = wp c (wp d Q)"
+  wp_Aif    "wp (Aif b c d) Q = (%s. (B b s-->wp c Q s)&(~B b s-->wp d Q s))" 
+  wp_Awhile "wp (Awhile b I c) Q = I"
+
+primrec vc acom
+  vc_Askip  "vc Askip Q = (%s.True)"
+  vc_Aass   "vc (Aass x a) Q = (%s.True)"
+  vc_Asemi  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
+  vc_Aif    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
+  vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~B b s --> Q s) &
+                              (I s & B b s --> wp c I s) & vc c I s)"
+
+primrec astrip acom
+  astrip_Askip  "astrip Askip = skip"
+  astrip_Aass   "astrip (Aass x a) = (x:=a)"
+  astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
+  astrip_Aif    "astrip (Aif b c d) = ifC b (astrip c) (astrip d)"
+  astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)"
+  
+end