# HG changeset patch
# User nipkow
# Date 858704539 -3600
# Node ID c4e16b36bc57286e2cfd1dae9c66c30a0a783c38
# Parent  174d03b1798f6988e8c3ae7a37fe8a736f5be01e
Added wp_while.

diff -r 174d03b1798f -r c4e16b36bc57 src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Tue Mar 18 17:03:55 1997 +0100
+++ b/src/HOL/IMP/Hoare.ML	Tue Mar 18 18:02:19 1997 +0100
@@ -23,53 +23,75 @@
 by (Fast_tac 1);
 qed "hoare_sound";
 
-goalw Hoare.thy [swp_def] "swp SKIP Q = Q";
+goalw Hoare.thy [wp_def] "wp SKIP Q = Q";
 by (Simp_tac 1);
-qed "swp_SKIP";
+qed "wp_SKIP";
 
-goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[a s/x]))";
+goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s.Q(s[a s/x]))";
 by (Simp_tac 1);
-qed "swp_Ass";
+qed "wp_Ass";
 
-goalw Hoare.thy [swp_def] "swp (c;d) Q = swp c (swp d Q)";
+goalw Hoare.thy [wp_def] "wp (c;d) Q = wp c (wp d Q)";
 by (Simp_tac 1);
 by (rtac ext 1);
 by (Fast_tac 1);
-qed "swp_Semi";
+qed "wp_Semi";
 
-goalw Hoare.thy [swp_def]
-  "swp (IF b THEN c ELSE d) Q = (%s. (b s --> swp c Q s) & \
-\                                    (~b s --> swp d Q s))";
+goalw Hoare.thy [wp_def]
+  "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) & \
+\                                    (~b s --> wp d Q s))";
 by (Simp_tac 1);
 by (rtac ext 1);
 by (Fast_tac 1);
-qed "swp_If";
+qed "wp_If";
 
-goalw Hoare.thy [swp_def]
-  "!!s. b s ==> swp (WHILE b DO c) Q s = swp (c;WHILE b DO c) Q s";
+goalw Hoare.thy [wp_def]
+  "!!s. b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";
 by (stac C_While_If 1);
 by (Asm_simp_tac 1);
-qed "swp_While_True";
+qed "wp_While_True";
 
-goalw Hoare.thy [swp_def] "!!s. ~b s ==> swp (WHILE b DO c) Q s = Q s";
+goalw Hoare.thy [wp_def] "!!s. ~b s ==> wp (WHILE b DO c) Q s = Q s";
 by (stac C_While_If 1);
 by (Asm_simp_tac 1);
-qed "swp_While_False";
+qed "wp_While_False";
 
-Addsimps [swp_SKIP,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False];
+Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
 
 (*Not suitable for rewriting: LOOPS!*)
-goal Hoare.thy "swp (WHILE b DO c) Q s = \
-\                 (if b s then swp (c;WHILE b DO c) Q s else Q s)";
+goal Hoare.thy "wp (WHILE b DO c) Q s = \
+\                 (if b s then wp (c;WHILE b DO c) Q s else Q s)";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-qed "swp_While_if";
+qed "wp_While_if";
 
+goal thy
+  "wp (WHILE b DO c) Q s = \
+\  (s : gfp(%S.{s.if b s then wp c (%s.s:S) s else Q s}))";
+by(simp_tac (!simpset setloop(split_tac[expand_if])) 1);
+br iffI 1;
+ br weak_coinduct 1;
+  by(Best_tac 1);
+ by(safe_tac (!claset));
+  by(rotate_tac ~1 1);
+  by(Asm_full_simp_tac 1);
+ by(rotate_tac ~1 1);
+ by(Asm_full_simp_tac 1);
+by(asm_full_simp_tac (!simpset addsimps [wp_def,Gamma_def]) 1);
+by(strip_tac 1);
+br mp 1;
+ ba 2;
+be induct2 1;
+by(fast_tac (!claset addSIs [monoI]) 1);
+by(stac gfp_Tarski 1);
+ by(fast_tac (!claset addSIs [monoI]) 1);
+by(Fast_tac 1);
+qed "wp_While";
 
 Delsimps [C_while];
 
 AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
 
-goal Hoare.thy "!Q. |- {swp c Q} c {Q}";
+goal Hoare.thy "!Q. |- {wp c Q} c {Q}";
 by (com.induct_tac "c" 1);
 by (ALLGOALS Simp_tac);
 by (REPEAT_FIRST Fast_tac);
@@ -90,11 +112,11 @@
  by (Asm_full_simp_tac 1);
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac 1);
-qed_spec_mp "swp_is_pre";
+qed_spec_mp "wp_is_pre";
 
 goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
-by (rtac (swp_is_pre RSN (2,hoare.conseq)) 1);
+by (rtac (wp_is_pre RSN (2,hoare.conseq)) 1);
  by (Fast_tac 2);
-by (rewrite_goals_tac [hoare_valid_def,swp_def]);
+by (rewrite_goals_tac [hoare_valid_def,wp_def]);
 by (Fast_tac 1);
 qed "hoare_relative_complete";
diff -r 174d03b1798f -r c4e16b36bc57 src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Tue Mar 18 17:03:55 1997 +0100
+++ b/src/HOL/IMP/Hoare.thy	Tue Mar 18 18:02:19 1997 +0100
@@ -6,7 +6,7 @@
 Inductive definition of Hoare logic
 *)
 
-Hoare = Denotation +
+Hoare = Denotation + Gfp +
 
 types assn = state => bool
 
@@ -29,7 +29,7 @@
   conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
           |- {P'}c{Q'}"
 
-constdefs swp :: com => assn => assn
-          "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
+constdefs wp :: com => assn => assn
+          "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
 
 end
diff -r 174d03b1798f -r c4e16b36bc57 src/HOL/IMP/VC.ML
--- a/src/HOL/IMP/VC.ML	Tue Mar 18 17:03:55 1997 +0100
+++ b/src/HOL/IMP/VC.ML	Tue Mar 18 18:02:19 1997 +0100
@@ -12,7 +12,7 @@
 
 val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[Fast_tac 1]);
 
-goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}";
+goal VC.thy "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}";
 by (acom.induct_tac "c" 1);
     by (ALLGOALS Simp_tac);
     by (Fast_tac 1);
@@ -29,25 +29,25 @@
    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)";
+goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp 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]);
-qed_spec_mp "wp_mono";
+qed_spec_mp "awp_mono";
 
 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);
+by (fast_tac (HOL_cs addEs [awp_mono]) 1);
 qed_spec_mp "vc_mono";
 
 goal VC.thy
   "!!P c Q. |- {P}c{Q} ==> \
-\          (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> wp ac Q s))";
+\          (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))";
 by (etac hoare.induct 1);
      by (res_inst_tac [("x","Askip")] exI 1);
      by (Simp_tac 1);
@@ -56,7 +56,7 @@
    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 (fast_tac (HOL_cs addSEs [awp_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);
@@ -66,10 +66,10 @@
 by (safe_tac HOL_cs);
 by (res_inst_tac [("x","ac")] exI 1);
 by (Asm_simp_tac 1);
-by (fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
+by (fast_tac (HOL_cs addSEs [awp_mono,vc_mono]) 1);
 qed "vc_complete";
 
-goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)";
+goal VC.thy "!Q. vcawp c Q = (vc c Q, awp c Q)";
 by (acom.induct_tac "c" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def])));
-qed "vcwp_vc_wp";
+qed "vcawp_vc_awp";
diff -r 174d03b1798f -r c4e16b36bc57 src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Tue Mar 18 17:03:55 1997 +0100
+++ b/src/HOL/IMP/VC.thy	Tue Mar 18 18:02:19 1997 +0100
@@ -5,7 +5,7 @@
 
 acom: annotated commands
 vc:   verification-conditions
-wp:   weakest (liberal) precondition
+awp:   weakest (liberal) precondition
 *)
 
 VC  =  Hoare +
@@ -17,24 +17,24 @@
                | Awhile bexp assn acom
 
 consts
-  vc,wp :: acom => assn => assn
-  vcwp :: "acom => assn => assn * assn"
+  vc,awp :: acom => assn => assn
+  vcawp :: "acom => assn => assn * assn"
   astrip :: acom => com
 
-primrec wp acom
-  "wp Askip Q = Q"
-  "wp (Aass x a) Q = (%s.Q(s[a s/x]))"
-  "wp (Asemi c d) Q = wp c (wp d Q)"
-  "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))" 
-  "wp (Awhile b I c) Q = I"
+primrec awp acom
+  "awp Askip Q = Q"
+  "awp (Aass x a) Q = (%s.Q(s[a s/x]))"
+  "awp (Asemi c d) Q = awp c (awp d Q)"
+  "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
+  "awp (Awhile b I c) Q = I"
 
 primrec vc acom
   "vc Askip Q = (%s.True)"
   "vc (Aass x a) Q = (%s.True)"
-  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
+  "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
   "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
   "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
-                              (I s & b s --> wp c I s) & vc c I s)"
+                              (I s & b s --> awp c I s) & vc c I s)"
 
 primrec astrip acom
   "astrip Askip = SKIP"
@@ -43,19 +43,19 @@
   "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
   "astrip (Awhile b I c) = (WHILE b DO astrip c)"
 
-(* simultaneous computation of vc and wp: *)
-primrec vcwp acom
-  "vcwp Askip Q = (%s.True, Q)"
-  "vcwp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
-  "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q;
-                            (vcc,wpc) = vcwp c wpd
-                         in (%s. vcc s & vcd s, wpc))"
-  "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q;
-                            (vcc,wpc) = vcwp c Q
-                         in (%s. vcc s & vcd s,
-                             %s.(b s-->wpc s) & (~b s-->wpd s)))"
-  "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I
-                            in (%s. (I s & ~b s --> Q s) &
-                                    (I s & b s --> wpc s) & vcc s, I))"
+(* simultaneous computation of vc and awp: *)
+primrec vcawp acom
+  "vcawp Askip Q = (%s.True, Q)"
+  "vcawp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
+  "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
+                              (vcc,wpc) = vcawp c wpd
+                          in (%s. vcc s & vcd s, wpc))"
+  "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
+                              (vcc,wpc) = vcawp c Q
+                          in (%s. vcc s & vcd s,
+                              %s.(b s --> wpc s) & (~b s --> wpd s)))"
+  "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
+                             in (%s. (I s & ~b s --> Q s) &
+                                     (I s & b s --> wpc s) & vcc s, I))"
 
 end