src/HOL/IMP/VC.thy
author kleing
Sun Dec 09 15:26:13 2001 +0100 (2001-12-09)
changeset 12434 ff2efde4574d
parent 12431 07ec657249e5
child 13596 ee5f79b210c1
permissions -rw-r--r--
tuned
     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 = Hoare:
    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: "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
    73 apply (induct_tac "c")
    74     apply (simp_all (no_asm))
    75     apply fast
    76    apply fast
    77   apply fast
    78  (* if *)
    79  apply (tactic "Deepen_tac 4 1")
    80 (* while *)
    81 apply (intro allI impI) 
    82 apply (rule conseq)
    83   apply (rule l)
    84  apply (rule While)
    85  defer
    86  apply fast
    87 apply (rule_tac P="awp acom fun2" in conseq)
    88   apply fast
    89  apply fast
    90 apply fast
    91 done
    92 
    93 lemma awp_mono [rule_format (no_asm)]: 
    94   "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
    95 apply (induct_tac "c")
    96     apply (simp_all (no_asm_simp))
    97 apply (rule allI, rule allI, rule impI)
    98 apply (erule allE, erule allE, erule mp)
    99 apply (erule allE, erule allE, erule mp, assumption)
   100 done
   101 
   102 
   103 lemma vc_mono [rule_format (no_asm)]: 
   104   "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
   105 apply (induct_tac "c")
   106     apply (simp_all (no_asm_simp))
   107 apply safe
   108 apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp) 
   109 prefer 2 apply assumption
   110 apply (fast elim: awp_mono)
   111 done
   112 
   113 lemma vc_complete: "|- {P}c{Q} ==>  
   114    (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))"
   115 apply (erule hoare.induct)
   116      apply (rule_tac x = "Askip" in exI)
   117      apply (simp (no_asm))
   118     apply (rule_tac x = "Aass x a" in exI)
   119     apply (simp (no_asm))
   120    apply clarify
   121    apply (rule_tac x = "Asemi ac aca" in exI)
   122    apply (simp (no_asm_simp))
   123    apply (fast elim!: awp_mono vc_mono)
   124   apply clarify
   125   apply (rule_tac x = "Aif b ac aca" in exI)
   126   apply (simp (no_asm_simp))
   127  apply clarify
   128  apply (rule_tac x = "Awhile b P ac" in exI)
   129  apply (simp (no_asm_simp))
   130 apply safe
   131 apply (rule_tac x = "ac" in exI)
   132 apply (simp (no_asm_simp))
   133 apply (fast elim!: awp_mono vc_mono)
   134 done
   135 
   136 lemma vcawp_vc_awp: "!Q. vcawp c Q = (vc c Q, awp c Q)"
   137 apply (induct_tac "c")
   138 apply (simp_all (no_asm_simp) add: Let_def)
   139 done
   140 
   141 end