Modified datatype com.
authornipkow
Wed Feb 07 12:22:32 1996 +0100 (1996-02-07)
changeset 148103f096efa26d
parent 1480 85ecd3439e01
child 1482 1a60df4fd63d
Modified datatype com.
Added (part of) relative completeness proof for Hoare logic.
src/HOL/IMP/Com.thy
src/HOL/IMP/Denotation.ML
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Properties.ML
src/HOL/IMP/VC.thy
     1.1 --- a/src/HOL/IMP/Com.thy	Tue Feb 06 12:44:31 1996 +0100
     1.2 +++ b/src/HOL/IMP/Com.thy	Wed Feb 07 12:22:32 1996 +0100
     1.3 @@ -71,11 +71,11 @@
     1.4  (** Commands **)
     1.5  
     1.6  datatype
     1.7 -  com = skip
     1.8 -      | ":="   loc aexp          (infixl  60)
     1.9 -      | semic  com com           ("_; _"  [60, 60] 10)
    1.10 -      | whileC bexp com          ("while _ do _"  60)
    1.11 -      | ifC    bexp com com      ("ifc _ then _ else _"  60)
    1.12 +  com = Skip
    1.13 +      | ":="  loc aexp         (infixl  60)
    1.14 +      | Semi  com com          ("_; _"  [60, 60] 10)
    1.15 +      | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
    1.16 +      | While bexp com         ("WHILE _ DO _"  60)
    1.17  
    1.18  (** Execution of commands **)
    1.19  consts  evalc    :: "(com*state*state)set"
    1.20 @@ -85,28 +85,28 @@
    1.21  translations
    1.22         "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
    1.23  
    1.24 -rules 
    1.25 -        assign_def      "s[m/x] == (%y. if y=x then m else s y)"
    1.26 +defs 
    1.27 +  assign_def   "s[m/x] == (%y. if y=x then m else s y)"
    1.28  
    1.29  inductive "evalc"
    1.30    intrs
    1.31 -    skip    "<skip,s> -c-> s"
    1.32 +    skip    "<Skip,s> -c-> s"
    1.33  
    1.34      assign  "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
    1.35  
    1.36      semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
    1.37              ==> <c0 ; c1, s> -c-> s1"
    1.38  
    1.39 -    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
    1.40 -            ==> <ifc b then c0 else c1, s> -c-> s1"
    1.41 +    IfTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
    1.42 +            ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
    1.43  
    1.44 -    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
    1.45 -             ==> <ifc b then c0 else c1, s> -c-> s1"
    1.46 +    IfFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
    1.47 +             ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
    1.48  
    1.49 -    whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s"
    1.50 +    WhileFalse "<b, s> -b-> False ==> <WHILE b DO c,s> -c-> s"
    1.51  
    1.52 -    whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; 
    1.53 -                  <while b do c, s2> -c-> s1 |] 
    1.54 -               ==> <while b do c, s> -c-> s1 "
    1.55 +    WhileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; 
    1.56 +                  <WHILE b DO c, s2> -c-> s1 |] 
    1.57 +               ==> <WHILE b DO c, s> -c-> s1"
    1.58   
    1.59  end
     2.1 --- a/src/HOL/IMP/Denotation.ML	Tue Feb 06 12:44:31 1996 +0100
     2.2 +++ b/src/HOL/IMP/Denotation.ML	Wed Feb 07 12:22:32 1996 +0100
     2.3 @@ -19,3 +19,10 @@
     2.4  qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
     2.5          "mono (Gamma b c)"
     2.6       (fn _ => [(best_tac comp_cs 1)]);
     2.7 +
     2.8 +goal Denotation.thy "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE Skip)";
     2.9 +by(Simp_tac 1);
    2.10 +by(EVERY1[stac (Gamma_mono RS lfp_Tarski),
    2.11 +          stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong), rtac refl]);
    2.12 +qed "C_While_If";
    2.13 +
     3.1 --- a/src/HOL/IMP/Denotation.thy	Tue Feb 06 12:44:31 1996 +0100
     3.2 +++ b/src/HOL/IMP/Denotation.thy	Wed Feb 07 12:22:32 1996 +0100
     3.3 @@ -35,12 +35,12 @@
     3.4                           {st. st : id & ~B b (fst st)})"
     3.5  
     3.6  primrec C com
     3.7 -  C_skip    "C(skip) = id"
     3.8 +  C_skip    "C(Skip) = id"
     3.9    C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
    3.10    C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    3.11 -  C_if      "C(ifc b then c0 else c1) =   
    3.12 +  C_if      "C(IF b THEN c0 ELSE c1) =   
    3.13                     {st. st:C(c0) & (B b (fst st))} Un 
    3.14                     {st. st:C(c1) & ~(B b (fst st))}"
    3.15 -  C_while   "C(while b do c) = lfp (Gamma b (C c))"
    3.16 +  C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
    3.17  
    3.18  end
     4.1 --- a/src/HOL/IMP/Hoare.ML	Tue Feb 06 12:44:31 1996 +0100
     4.2 +++ b/src/HOL/IMP/Hoare.ML	Wed Feb 07 12:22:32 1996 +0100
     4.3 @@ -3,12 +3,13 @@
     4.4      Author:     Tobias Nipkow
     4.5      Copyright   1995 TUM
     4.6  
     4.7 -Soundness of Hoare rules wrt denotational semantics
     4.8 +Soundness (and part of) relative completeness of Hoare rules
     4.9 +wrt denotational semantics
    4.10  *)
    4.11  
    4.12  open Hoare;
    4.13  
    4.14 -goalw Hoare.thy [spec_def] "!P c Q. ({{P}}c{{Q}}) --> spec P c Q";
    4.15 +goalw Hoare.thy [hoare_valid_def] "!P c Q. ({{P}}c{{Q}}) --> |= {{P}}c{{Q}}";
    4.16  by (rtac hoare.mutual_induct 1);
    4.17      by(ALLGOALS Asm_simp_tac);
    4.18    by(fast_tac rel_cs 1);
    4.19 @@ -24,28 +25,87 @@
    4.20    by(ALLGOALS Asm_full_simp_tac);
    4.21  qed "hoare_sound";
    4.22  
    4.23 -(*
    4.24 -fun while_tac inv ss i =
    4.25 -  EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i,
    4.26 -        asm_full_simp_tac ss (i+1)];
    4.27 +goalw Hoare.thy [swp_def] "swp Skip Q = Q";
    4.28 +by(Simp_tac 1);
    4.29 +br ext 1;
    4.30 +by(fast_tac HOL_cs 1);
    4.31 +qed "swp_Skip";
    4.32 +
    4.33 +goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[A a s/x]))";
    4.34 +by(Simp_tac 1);
    4.35 +br ext 1;
    4.36 +by(fast_tac HOL_cs 1);
    4.37 +qed "swp_Ass";
    4.38 +
    4.39 +goalw Hoare.thy [swp_def] "swp (c;d) Q = swp c (swp d Q)";
    4.40 +by(Simp_tac 1);
    4.41 +br ext 1;
    4.42 +by(fast_tac comp_cs 1);
    4.43 +qed "swp_Semi";
    4.44  
    4.45 -fun assign_tac ss = EVERY'[rtac hoare_assign, simp_tac ss,
    4.46 -                           TRY o (strip_tac THEN' atac)];
    4.47 +goalw Hoare.thy [swp_def]
    4.48 +  "swp (IF b THEN c ELSE d) Q = (%s. (B b s --> swp c Q s) & \
    4.49 +\                                    (~B b s --> swp d Q s))";
    4.50 +by(Simp_tac 1);
    4.51 +br ext 1;
    4.52 +by(fast_tac comp_cs 1);
    4.53 +qed "swp_If";
    4.54  
    4.55 -fun hoare_tac ss =
    4.56 -  REPEAT(STATE(fn th => FIRST'[rtac hoare_seq, assign_tac ss] (nprems_of th)));
    4.57 +goalw Hoare.thy [swp_def]
    4.58 +  "!!s. B b s ==> swp (WHILE b DO c) Q s = swp (c;WHILE b DO c) Q s";
    4.59 +by(stac C_While_If 1);
    4.60 +by(Asm_simp_tac 1);
    4.61 +qed "swp_While_True";
    4.62 +
    4.63 +goalw Hoare.thy [swp_def] "!!s. ~B b s ==> swp (WHILE b DO c) Q s = Q s";
    4.64 +by(stac C_While_If 1);
    4.65 +by(Asm_simp_tac 1);
    4.66 +by(fast_tac HOL_cs 1);
    4.67 +qed "swp_While_False";
    4.68 +
    4.69 +Addsimps [swp_Skip,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False];
    4.70 +
    4.71 +Delsimps [C_while];
    4.72  
    4.73 -(* example *)
    4.74 -val prems = goal Hoare.thy
    4.75 -  "[| u ~= y; u ~= z; y ~= z |] ==> \
    4.76 -\  {{%s.s(x)=i & s(y)=j}} \
    4.77 -\  z := X x; (u := N 0; \
    4.78 -\  while noti(ROp op = (X u) (X y)) \
    4.79 -\             do (u := Op1 Suc (X u); z := Op1 Suc (X z))) \
    4.80 -\  {{%s. s(z)=i+j}}";
    4.81 -val ss = !simpset addsimps (eq_sym_conv::assign_def::prems);
    4.82 -by(hoare_tac ss);
    4.83 -by(while_tac "%s.s z = i + s u & s y = j" ss 3);
    4.84 -by(hoare_tac ss);
    4.85 -result();
    4.86 -*)
    4.87 +goalw Hoare.thy [hoare_valid_def,swp_def]
    4.88 +  "!!c. |= {{P}}c{{Q}} ==> !s. P s --> swp c Q s";
    4.89 +by(fast_tac HOL_cs 1);
    4.90 +qed "swp_is_weakest";
    4.91 +
    4.92 +goal Hoare.thy "!Q. {{swp c Q}} c {{Q}}";
    4.93 +by(com.induct_tac "c" 1);
    4.94 +by(ALLGOALS Simp_tac);
    4.95 +    by(fast_tac (HOL_cs addIs [hoare.skip]) 1);
    4.96 +   by(fast_tac (HOL_cs addIs [hoare.ass]) 1);
    4.97 +  by(fast_tac (HOL_cs addIs [hoare.semi]) 1);
    4.98 + by(safe_tac (HOL_cs addSIs [hoare.If]));
    4.99 +  br hoare.conseq 1;
   4.100 +    by(fast_tac HOL_cs 2);
   4.101 +   by(fast_tac HOL_cs 2);
   4.102 +  by(fast_tac HOL_cs 1);
   4.103 + br hoare.conseq 1;
   4.104 +   by(fast_tac HOL_cs 2);
   4.105 +  by(fast_tac HOL_cs 2);
   4.106 + by(fast_tac HOL_cs 1);
   4.107 +br hoare.conseq 1;
   4.108 +  br hoare.While 2;
   4.109 +  be thin_rl 1;
   4.110 +  by(fast_tac HOL_cs 1);
   4.111 + br hoare.conseq 1;
   4.112 +   be thin_rl 3;
   4.113 +   br allI 3;
   4.114 +   br impI 3;
   4.115 +   ba 3;
   4.116 +  by(fast_tac HOL_cs 2);
   4.117 + by(safe_tac HOL_cs);
   4.118 + by(rotate_tac ~1 1);
   4.119 + by(Asm_full_simp_tac 1);
   4.120 +by(rotate_tac ~1 1);
   4.121 +by(Asm_full_simp_tac 1);
   4.122 +bind_thm("swp_is_pre", result() RS spec);
   4.123 +
   4.124 +goal Hoare.thy "!!c. |= {{P}}c{{Q}} ==> {{P}}c{{Q}}";
   4.125 +br (swp_is_pre RSN (2,hoare.conseq)) 1;
   4.126 + by(fast_tac HOL_cs 2);
   4.127 +be swp_is_weakest 1;
   4.128 +qed "hoare_relative_complete";
     5.1 --- a/src/HOL/IMP/Hoare.thy	Tue Feb 06 12:44:31 1996 +0100
     5.2 +++ b/src/HOL/IMP/Hoare.thy	Wed Feb 07 12:22:32 1996 +0100
     5.3 @@ -12,23 +12,26 @@
     5.4  
     5.5  consts
     5.6    hoare :: "(assn * com * assn) set"
     5.7 -  spec :: [state=>bool,com,state=>bool] => bool
     5.8 +  hoare_valid :: [assn,com,assn] => bool ("|= {{_}}_{{_}}")
     5.9  defs
    5.10 -  spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
    5.11 +  hoare_valid_def "|= {{P}}c{{Q}} == !s t. (s,t) : C(c) --> P s --> Q t"
    5.12  
    5.13  syntax "@hoare" :: [bool,com,bool] => bool ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
    5.14  translations "{{P}}c{{Q}}" == "(P,c,Q) : hoare"
    5.15  
    5.16  inductive "hoare"
    5.17  intrs
    5.18 -  hoare_skip "{{P}}skip{{P}}"
    5.19 -  hoare_ass  "{{%s.P(s[A a s/x])}} x:=a {{P}}"
    5.20 -  hoare_semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
    5.21 -  hoare_if   "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
    5.22 -              {{P}} ifc b then c else d {{Q}}"
    5.23 -  hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==>
    5.24 -               {{P}} while b do c {{%s. P s & ~B b s}}"
    5.25 -  hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
    5.26 -                {{P'}}c{{Q'}}"
    5.27 +  skip "{{P}}Skip{{P}}"
    5.28 +  ass  "{{%s.P(s[A a s/x])}} x:=a {{P}}"
    5.29 +  semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
    5.30 +  If "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
    5.31 +        {{P}} IF b THEN c ELSE d {{Q}}"
    5.32 +  While "[| {{%s. P s & B b s}} c {{P}} |] ==>
    5.33 +         {{P}} WHILE b DO c {{%s. P s & ~B b s}}"
    5.34 +  conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
    5.35 +          {{P'}}c{{Q'}}"
    5.36 +
    5.37 +consts swp :: com => assn => assn
    5.38 +defs swp_def "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
    5.39  
    5.40  end
     6.1 --- a/src/HOL/IMP/Properties.ML	Tue Feb 06 12:44:31 1996 +0100
     6.2 +++ b/src/HOL/IMP/Properties.ML	Wed Feb 07 12:22:32 1996 +0100
     6.3 @@ -21,8 +21,8 @@
     6.4  
     6.5  
     6.6  val evalc_elim_cases = map (evalc.mk_cases com.simps)
     6.7 -   ["<skip,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
     6.8 -    "<ifc b then c1 else c2, s> -c-> t", "<while b do c,s> -c-> t"];
     6.9 +   ["<Skip,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
    6.10 +    "<IF b THEN c1 ELSE c2, s> -c-> t", "<WHILE b DO c,s> -c-> t"];
    6.11  
    6.12  (* evaluation of com is deterministic *)
    6.13  goal Com.thy "!!c. <c,s> -c-> t ==> !u. <c,s> -c-> u --> u=t";
     7.1 --- a/src/HOL/IMP/VC.thy	Tue Feb 06 12:44:31 1996 +0100
     7.2 +++ b/src/HOL/IMP/VC.thy	Wed Feb 07 12:22:32 1996 +0100
     7.3 @@ -37,11 +37,11 @@
     7.4                                (I s & B b s --> wp c I s) & vc c I s)"
     7.5  
     7.6  primrec astrip acom
     7.7 -  astrip_Askip  "astrip Askip = skip"
     7.8 +  astrip_Askip  "astrip Askip = Skip"
     7.9    astrip_Aass   "astrip (Aass x a) = (x:=a)"
    7.10    astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
    7.11 -  astrip_Aif    "astrip (Aif b c d) = ifC b (astrip c) (astrip d)"
    7.12 -  astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)"
    7.13 +  astrip_Aif    "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
    7.14 +  astrip_Awhile "astrip (Awhile b I c) = (WHILE b DO astrip c)"
    7.15  
    7.16  (* simultaneous computation of vc and wp: *)
    7.17  primrec vcwp acom