# HG changeset patch
# User nipkow
# Date 823692152 -3600
# Node ID 03f096efa26d868de6680b5ba273b49e251b891f
# Parent  85ecd3439e019e3b268cc60494aeaa8229c19063
Modified datatype com.
Added (part of) relative completeness proof for Hoare logic.

diff -r 85ecd3439e01 -r 03f096efa26d src/HOL/IMP/Com.thy
--- a/src/HOL/IMP/Com.thy	Tue Feb 06 12:44:31 1996 +0100
+++ b/src/HOL/IMP/Com.thy	Wed Feb 07 12:22:32 1996 +0100
@@ -71,11 +71,11 @@
 (** Commands **)
 
 datatype
-  com = skip
-      | ":="   loc aexp          (infixl  60)
-      | semic  com com           ("_; _"  [60, 60] 10)
-      | whileC bexp com          ("while _ do _"  60)
-      | ifC    bexp com com      ("ifc _ then _ else _"  60)
+  com = Skip
+      | ":="  loc aexp         (infixl  60)
+      | Semi  com com          ("_; _"  [60, 60] 10)
+      | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
+      | While bexp com         ("WHILE _ DO _"  60)
 
 (** Execution of commands **)
 consts  evalc    :: "(com*state*state)set"
@@ -85,28 +85,28 @@
 translations
        "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
 
-rules 
-        assign_def      "s[m/x] == (%y. if y=x then m else s y)"
+defs 
+  assign_def   "s[m/x] == (%y. if y=x then m else s y)"
 
 inductive "evalc"
   intrs
-    skip    "<skip,s> -c-> s"
+    skip    "<Skip,s> -c-> s"
 
     assign  "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
 
     semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
             ==> <c0 ; c1, s> -c-> s1"
 
-    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
-            ==> <ifc b then c0 else c1, s> -c-> s1"
+    IfTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
+            ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
 
-    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
-             ==> <ifc b then c0 else c1, s> -c-> s1"
+    IfFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
+             ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
 
-    whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s"
+    WhileFalse "<b, s> -b-> False ==> <WHILE b DO c,s> -c-> s"
 
-    whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; 
-                  <while b do c, s2> -c-> s1 |] 
-               ==> <while b do c, s> -c-> s1 "
+    WhileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; 
+                  <WHILE b DO c, s2> -c-> s1 |] 
+               ==> <WHILE b DO c, s> -c-> s1"
  
 end
diff -r 85ecd3439e01 -r 03f096efa26d src/HOL/IMP/Denotation.ML
--- a/src/HOL/IMP/Denotation.ML	Tue Feb 06 12:44:31 1996 +0100
+++ b/src/HOL/IMP/Denotation.ML	Wed Feb 07 12:22:32 1996 +0100
@@ -19,3 +19,10 @@
 qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
         "mono (Gamma b c)"
      (fn _ => [(best_tac comp_cs 1)]);
+
+goal Denotation.thy "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE Skip)";
+by(Simp_tac 1);
+by(EVERY1[stac (Gamma_mono RS lfp_Tarski),
+          stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong), rtac refl]);
+qed "C_While_If";
+
diff -r 85ecd3439e01 -r 03f096efa26d src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Tue Feb 06 12:44:31 1996 +0100
+++ b/src/HOL/IMP/Denotation.thy	Wed Feb 07 12:22:32 1996 +0100
@@ -35,12 +35,12 @@
                          {st. st : id & ~B b (fst st)})"
 
 primrec C com
-  C_skip    "C(skip) = id"
+  C_skip    "C(Skip) = id"
   C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
   C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
-  C_if      "C(ifc b then c0 else c1) =   
+  C_if      "C(IF b THEN c0 ELSE c1) =   
                    {st. st:C(c0) & (B b (fst st))} Un 
                    {st. st:C(c1) & ~(B b (fst st))}"
-  C_while   "C(while b do c) = lfp (Gamma b (C c))"
+  C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
 
 end
diff -r 85ecd3439e01 -r 03f096efa26d src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Tue Feb 06 12:44:31 1996 +0100
+++ b/src/HOL/IMP/Hoare.ML	Wed Feb 07 12:22:32 1996 +0100
@@ -3,12 +3,13 @@
     Author:     Tobias Nipkow
     Copyright   1995 TUM
 
-Soundness of Hoare rules wrt denotational semantics
+Soundness (and part of) relative completeness of Hoare rules
+wrt denotational semantics
 *)
 
 open Hoare;
 
-goalw Hoare.thy [spec_def] "!P c Q. ({{P}}c{{Q}}) --> spec P c Q";
+goalw Hoare.thy [hoare_valid_def] "!P c Q. ({{P}}c{{Q}}) --> |= {{P}}c{{Q}}";
 by (rtac hoare.mutual_induct 1);
     by(ALLGOALS Asm_simp_tac);
   by(fast_tac rel_cs 1);
@@ -24,28 +25,87 @@
   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)];
+goalw Hoare.thy [swp_def] "swp Skip Q = Q";
+by(Simp_tac 1);
+br ext 1;
+by(fast_tac HOL_cs 1);
+qed "swp_Skip";
+
+goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[A a s/x]))";
+by(Simp_tac 1);
+br ext 1;
+by(fast_tac HOL_cs 1);
+qed "swp_Ass";
+
+goalw Hoare.thy [swp_def] "swp (c;d) Q = swp c (swp d Q)";
+by(Simp_tac 1);
+br ext 1;
+by(fast_tac comp_cs 1);
+qed "swp_Semi";
 
-fun assign_tac ss = EVERY'[rtac hoare_assign, simp_tac ss,
-                           TRY o (strip_tac THEN' atac)];
+goalw Hoare.thy [swp_def]
+  "swp (IF b THEN c ELSE d) Q = (%s. (B b s --> swp c Q s) & \
+\                                    (~B b s --> swp d Q s))";
+by(Simp_tac 1);
+br ext 1;
+by(fast_tac comp_cs 1);
+qed "swp_If";
 
-fun hoare_tac ss =
-  REPEAT(STATE(fn th => FIRST'[rtac hoare_seq, assign_tac ss] (nprems_of th)));
+goalw Hoare.thy [swp_def]
+  "!!s. B b s ==> swp (WHILE b DO c) Q s = swp (c;WHILE b DO c) Q s";
+by(stac C_While_If 1);
+by(Asm_simp_tac 1);
+qed "swp_While_True";
+
+goalw Hoare.thy [swp_def] "!!s. ~B b s ==> swp (WHILE b DO c) Q s = Q s";
+by(stac C_While_If 1);
+by(Asm_simp_tac 1);
+by(fast_tac HOL_cs 1);
+qed "swp_While_False";
+
+Addsimps [swp_Skip,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False];
+
+Delsimps [C_while];
 
-(* example *)
-val prems = goal Hoare.thy
-  "[| u ~= y; u ~= z; y ~= z |] ==> \
-\  {{%s.s(x)=i & s(y)=j}} \
-\  z := X x; (u := N 0; \
-\  while noti(ROp op = (X u) (X y)) \
-\             do (u := Op1 Suc (X u); z := Op1 Suc (X z))) \
-\  {{%s. s(z)=i+j}}";
-val ss = !simpset addsimps (eq_sym_conv::assign_def::prems);
-by(hoare_tac ss);
-by(while_tac "%s.s z = i + s u & s y = j" ss 3);
-by(hoare_tac ss);
-result();
-*)
+goalw Hoare.thy [hoare_valid_def,swp_def]
+  "!!c. |= {{P}}c{{Q}} ==> !s. P s --> swp c Q s";
+by(fast_tac HOL_cs 1);
+qed "swp_is_weakest";
+
+goal Hoare.thy "!Q. {{swp c Q}} c {{Q}}";
+by(com.induct_tac "c" 1);
+by(ALLGOALS Simp_tac);
+    by(fast_tac (HOL_cs addIs [hoare.skip]) 1);
+   by(fast_tac (HOL_cs addIs [hoare.ass]) 1);
+  by(fast_tac (HOL_cs addIs [hoare.semi]) 1);
+ by(safe_tac (HOL_cs addSIs [hoare.If]));
+  br hoare.conseq 1;
+    by(fast_tac HOL_cs 2);
+   by(fast_tac HOL_cs 2);
+  by(fast_tac HOL_cs 1);
+ br hoare.conseq 1;
+   by(fast_tac HOL_cs 2);
+  by(fast_tac HOL_cs 2);
+ by(fast_tac HOL_cs 1);
+br hoare.conseq 1;
+  br hoare.While 2;
+  be thin_rl 1;
+  by(fast_tac HOL_cs 1);
+ br hoare.conseq 1;
+   be thin_rl 3;
+   br allI 3;
+   br impI 3;
+   ba 3;
+  by(fast_tac HOL_cs 2);
+ by(safe_tac HOL_cs);
+ by(rotate_tac ~1 1);
+ by(Asm_full_simp_tac 1);
+by(rotate_tac ~1 1);
+by(Asm_full_simp_tac 1);
+bind_thm("swp_is_pre", result() RS spec);
+
+goal Hoare.thy "!!c. |= {{P}}c{{Q}} ==> {{P}}c{{Q}}";
+br (swp_is_pre RSN (2,hoare.conseq)) 1;
+ by(fast_tac HOL_cs 2);
+be swp_is_weakest 1;
+qed "hoare_relative_complete";
diff -r 85ecd3439e01 -r 03f096efa26d src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Tue Feb 06 12:44:31 1996 +0100
+++ b/src/HOL/IMP/Hoare.thy	Wed Feb 07 12:22:32 1996 +0100
@@ -12,23 +12,26 @@
 
 consts
   hoare :: "(assn * com * assn) set"
-  spec :: [state=>bool,com,state=>bool] => bool
+  hoare_valid :: [assn,com,assn] => bool ("|= {{_}}_{{_}}")
 defs
-  spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
+  hoare_valid_def "|= {{P}}c{{Q}} == !s t. (s,t) : C(c) --> P s --> Q t"
 
 syntax "@hoare" :: [bool,com,bool] => bool ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
 translations "{{P}}c{{Q}}" == "(P,c,Q) : hoare"
 
 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'}}"
+  skip "{{P}}Skip{{P}}"
+  ass  "{{%s.P(s[A a s/x])}} x:=a {{P}}"
+  semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
+  If "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
+        {{P}} IF b THEN c ELSE d {{Q}}"
+  While "[| {{%s. P s & B b s}} c {{P}} |] ==>
+         {{P}} WHILE b DO c {{%s. P s & ~B b s}}"
+  conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
+          {{P'}}c{{Q'}}"
+
+consts swp :: com => assn => assn
+defs swp_def "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
 
 end
diff -r 85ecd3439e01 -r 03f096efa26d src/HOL/IMP/Properties.ML
--- a/src/HOL/IMP/Properties.ML	Tue Feb 06 12:44:31 1996 +0100
+++ b/src/HOL/IMP/Properties.ML	Wed Feb 07 12:22:32 1996 +0100
@@ -21,8 +21,8 @@
 
 
 val evalc_elim_cases = map (evalc.mk_cases com.simps)
-   ["<skip,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
-    "<ifc b then c1 else c2, s> -c-> t", "<while b do c,s> -c-> t"];
+   ["<Skip,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
+    "<IF b THEN c1 ELSE c2, s> -c-> t", "<WHILE b DO c,s> -c-> t"];
 
 (* evaluation of com is deterministic *)
 goal Com.thy "!!c. <c,s> -c-> t ==> !u. <c,s> -c-> u --> u=t";
diff -r 85ecd3439e01 -r 03f096efa26d src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Tue Feb 06 12:44:31 1996 +0100
+++ b/src/HOL/IMP/VC.thy	Wed Feb 07 12:22:32 1996 +0100
@@ -37,11 +37,11 @@
                               (I s & B b s --> wp c I s) & vc c I s)"
 
 primrec astrip acom
-  astrip_Askip  "astrip Askip = skip"
+  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)"
+  astrip_Aif    "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
+  astrip_Awhile "astrip (Awhile b I c) = (WHILE b DO astrip c)"
 
 (* simultaneous computation of vc and wp: *)
 primrec vcwp acom