src/HOL/IMP/VC.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 26342 0f65fa163304
child 27362 a6dc1769fdda
permissions -rw-r--r--
avoid rebinding of existing facts;
     1 (*  Title:      HOL/IMP/VC.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996 TUM
     5 
     6 acom: annotated commands
     7 vc:   verification-conditions
     8 awp:   weakest (liberal) precondition
     9 *)
    10 
    11 header "Verification Conditions"
    12 
    13 theory VC imports Hoare begin
    14 
    15 datatype  acom = Askip
    16                | Aass   loc aexp
    17                | Asemi  acom acom
    18                | Aif    bexp acom acom
    19                | Awhile bexp assn acom
    20 
    21 consts
    22   vc :: "acom => assn => assn"
    23   awp :: "acom => assn => assn"
    24   vcawp :: "acom => assn => assn \<times> assn"
    25   astrip :: "acom => com"
    26 
    27 primrec
    28   "awp Askip Q = Q"
    29   "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
    30   "awp (Asemi c d) Q = awp c (awp d Q)"
    31   "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
    32   "awp (Awhile b I c) Q = I"
    33 
    34 primrec
    35   "vc Askip Q = (\<lambda>s. True)"
    36   "vc (Aass x a) Q = (\<lambda>s. True)"
    37   "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
    38   "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
    39   "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
    40                               (I s & b s --> awp c I s) & vc c I s)"
    41 
    42 primrec
    43   "astrip Askip = SKIP"
    44   "astrip (Aass x a) = (x:==a)"
    45   "astrip (Asemi c d) = (astrip c;astrip d)"
    46   "astrip (Aif b c d) = (\<IF> b \<THEN> astrip c \<ELSE> astrip d)"
    47   "astrip (Awhile b I c) = (\<WHILE> b \<DO> astrip c)"
    48 
    49 (* simultaneous computation of vc and awp: *)
    50 primrec
    51   "vcawp Askip Q = (\<lambda>s. True, Q)"
    52   "vcawp (Aass x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[x\<mapsto>a s]))"
    53   "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
    54                               (vcc,wpc) = vcawp c wpd
    55                           in (\<lambda>s. vcc s & vcd s, wpc))"
    56   "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
    57                               (vcc,wpc) = vcawp c Q
    58                           in (\<lambda>s. vcc s & vcd s,
    59                               \<lambda>s.(b s --> wpc s) & (~b s --> wpd s)))"
    60   "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
    61                              in (\<lambda>s. (I s & ~b s --> Q s) &
    62                                      (I s & b s --> wpc s) & vcc s, I))"
    63 
    64 (*
    65 Soundness and completeness of vc
    66 *)
    67 
    68 declare hoare.intros [intro]
    69 
    70 lemma l: "!s. P s --> P s" by fast
    71 
    72 lemma vc_sound: "(!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
    73 apply (induct c arbitrary: Q)
    74     apply (simp_all (no_asm))
    75     apply fast
    76    apply fast
    77   apply fast
    78  (* if *)
    79  apply atomize
    80  apply (tactic "deepen_tac @{claset} 4 1")
    81 (* while *)
    82 apply atomize
    83 apply (intro allI impI)
    84 apply (rule conseq)
    85   apply (rule l)
    86  apply (rule While)
    87  defer
    88  apply fast
    89 apply (rule_tac P="awp c fun2" in conseq)
    90   apply fast
    91  apply fast
    92 apply fast
    93 done
    94 
    95 lemma awp_mono [rule_format (no_asm)]:
    96   "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
    97 apply (induct c)
    98     apply (simp_all (no_asm_simp))
    99 apply (rule allI, rule allI, rule impI)
   100 apply (erule allE, erule allE, erule mp)
   101 apply (erule allE, erule allE, erule mp, assumption)
   102 done
   103 
   104 lemma vc_mono [rule_format (no_asm)]:
   105   "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
   106 apply (induct c)
   107     apply (simp_all (no_asm_simp))
   108 apply safe
   109 apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp)
   110 prefer 2 apply assumption
   111 apply (fast elim: awp_mono)
   112 done
   113 
   114 lemma vc_complete: assumes der: "|- {P}c{Q}"
   115   shows "(\<exists>ac. astrip ac = c & (\<forall>s. vc ac Q s) & (\<forall>s. P s --> awp ac Q s))"
   116   (is "? ac. ?Eq P c Q ac")
   117 using der
   118 proof induct
   119   case skip
   120   show ?case (is "? ac. ?C ac")
   121   proof show "?C Askip" by simp qed
   122 next
   123   case (ass P x a)
   124   show ?case (is "? ac. ?C ac")
   125   proof show "?C(Aass x a)" by simp qed
   126 next
   127   case (semi P c1 Q c2 R)
   128   from semi.hyps obtain ac1 where ih1: "?Eq P c1 Q ac1" by fast
   129   from semi.hyps obtain ac2 where ih2: "?Eq Q c2 R ac2" by fast
   130   show ?case (is "? ac. ?C ac")
   131   proof
   132     show "?C(Asemi ac1 ac2)"
   133       using ih1 ih2 by simp (fast elim!: awp_mono vc_mono)
   134   qed
   135 next
   136   case (If P b c1 Q c2)
   137   from If.hyps obtain ac1 where ih1: "?Eq (%s. P s & b s) c1 Q ac1" by fast
   138   from If.hyps obtain ac2 where ih2: "?Eq (%s. P s & ~b s) c2 Q ac2" by fast
   139   show ?case (is "? ac. ?C ac")
   140   proof
   141     show "?C(Aif b ac1 ac2)"
   142       using ih1 ih2 by simp
   143   qed
   144 next
   145   case (While P b c)
   146   from While.hyps obtain ac where ih: "?Eq (%s. P s & b s) c P ac" by fast
   147   show ?case (is "? ac. ?C ac")
   148   proof show "?C(Awhile b P ac)" using ih by simp qed
   149 next
   150   case conseq thus ?case by(fast elim!: awp_mono vc_mono)
   151 qed
   152 
   153 lemma vcawp_vc_awp: "vcawp c Q = (vc c Q, awp c Q)"
   154   by (induct c arbitrary: Q) (simp_all add: Let_def)
   155 
   156 end