src/HOL/IMP/VC.thy
author kleing
Sun Dec 09 14:35:36 2001 +0100 (2001-12-09)
changeset 12431 07ec657249e5
parent 9241 f961c1fdff50
child 12434 ff2efde4574d
permissions -rw-r--r--
converted to Isar
     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)]: "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
    94 apply (induct_tac "c")
    95     apply (simp_all (no_asm_simp))
    96 apply (rule allI, rule allI, rule impI)
    97 apply (erule allE, erule allE, erule mp)
    98 apply (erule allE, erule allE, erule mp, assumption)
    99 done
   100 
   101 
   102 lemma vc_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
   103 apply (induct_tac "c")
   104     apply (simp_all (no_asm_simp))
   105 apply safe
   106 apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp) 
   107 prefer 2 apply assumption
   108 apply (fast elim: awp_mono)
   109 done
   110 
   111 lemma vc_complete: "|- {P}c{Q} ==>  
   112    (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))"
   113 apply (erule hoare.induct)
   114      apply (rule_tac x = "Askip" in exI)
   115      apply (simp (no_asm))
   116     apply (rule_tac x = "Aass x a" in exI)
   117     apply (simp (no_asm))
   118    apply clarify
   119    apply (rule_tac x = "Asemi ac aca" in exI)
   120    apply (simp (no_asm_simp))
   121    apply (fast elim!: awp_mono vc_mono)
   122   apply clarify
   123   apply (rule_tac x = "Aif b ac aca" in exI)
   124   apply (simp (no_asm_simp))
   125  apply clarify
   126  apply (rule_tac x = "Awhile b P ac" in exI)
   127  apply (simp (no_asm_simp))
   128 apply safe
   129 apply (rule_tac x = "ac" in exI)
   130 apply (simp (no_asm_simp))
   131 apply (fast elim!: awp_mono vc_mono)
   132 done
   133 
   134 lemma vcawp_vc_awp: "!Q. vcawp c Q = (vc c Q, awp c Q)"
   135 apply (induct_tac "c")
   136 apply (simp_all (no_asm_simp) add: Let_def)
   137 done
   138 
   139 end