src/HOL/IMP/VC.thy
author nipkow
Mon Sep 30 15:44:21 2002 +0200 (2002-09-30)
changeset 13596 ee5f79b210c1
parent 12434 ff2efde4574d
child 16417 9bc16273c2d4
permissions -rw-r--r--
modified induct method
     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: assumes der: "|- {P}c{Q}"
   114   shows "(? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))"
   115   (is "? ac. ?Eq P c Q ac")
   116 using der
   117 proof induct
   118   case skip
   119   show ?case (is "? ac. ?C ac")
   120   proof show "?C Askip" by simp qed
   121 next
   122   case (ass P a x)
   123   show ?case (is "? ac. ?C ac")
   124   proof show "?C(Aass x a)" by simp qed
   125 next
   126   case (semi P Q R c1 c2)
   127   from semi.hyps obtain ac1 where ih1: "?Eq P c1 Q ac1" by fast
   128   from semi.hyps obtain ac2 where ih2: "?Eq Q c2 R ac2" by fast
   129   show ?case (is "? ac. ?C ac")
   130   proof
   131     show "?C(Asemi ac1 ac2)"
   132       using ih1 ih2 by simp (fast elim!: awp_mono vc_mono)
   133   qed
   134 next
   135   case (If P Q b c1 c2)
   136   from If.hyps obtain ac1 where ih1: "?Eq (%s. P s & b s) c1 Q ac1" by fast
   137   from If.hyps obtain ac2 where ih2: "?Eq (%s. P s & ~b s) c2 Q ac2" by fast
   138   show ?case (is "? ac. ?C ac")
   139   proof
   140     show "?C(Aif b ac1 ac2)"
   141       using ih1 ih2 by simp
   142   qed
   143 next
   144   case (While P b c)
   145   from While.hyps obtain ac where ih: "?Eq (%s. P s & b s) c P ac" by fast
   146   show ?case (is "? ac. ?C ac")
   147   proof show "?C(Awhile b P ac)" using ih by simp qed
   148 next
   149   case conseq thus ?case by(fast elim!: awp_mono vc_mono)
   150 qed
   151 
   152 lemma vcawp_vc_awp: "!Q. vcawp c Q = (vc c Q, awp c Q)"
   153 apply (induct_tac "c")
   154 apply (simp_all (no_asm_simp) add: Let_def)
   155 done
   156 
   157 end