src/HOL/IMP/VC.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45840 dadd139192d1
child 47818 151d137f1095
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     1
header "Verification Conditions"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     3
theory VC imports Hoare begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     4
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     5
subsection "VCG via Weakest Preconditions"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     7
text{* Annotated commands: commands where loops are annotated with
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     8
invariants. *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     9
45840
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    10
datatype acom =
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    11
  ASKIP |
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    12
  Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    13
  Asemi   acom acom      ("_;/ _"  [60, 61] 60) |
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    14
  Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    15
  Awhile assn bexp acom  ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    16
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    17
text{* Weakest precondition from annotated commands: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    18
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
45840
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    20
"pre ASKIP Q = Q" |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    21
"pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
"pre (Asemi c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    23
"pre (Aif b c\<^isub>1 c\<^isub>2) Q =
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    24
  (\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    25
       (\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" |
45745
3a8bc5623410 invariant holds before loop
nipkow
parents: 45212
diff changeset
    26
"pre (Awhile I b c) Q = I"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    27
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    28
text{* Verification condition: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    30
fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
45840
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    31
"vc ASKIP Q = (\<lambda>s. True)" |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
"vc (Aassign x a) Q = (\<lambda>s. True)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    33
"vc (Asemi c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 (pre c\<^isub>2 Q) s \<and> vc c\<^isub>2 Q s)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    34
"vc (Aif b c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 Q s \<and> vc c\<^isub>2 Q s)" |
45745
3a8bc5623410 invariant holds before loop
nipkow
parents: 45212
diff changeset
    35
"vc (Awhile I b c) Q =
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
  (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    37
       (I s \<and> bval b s \<longrightarrow> pre c I s) \<and>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    38
       vc c I s)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    39
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
text{* Strip annotations: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    41
45840
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    42
fun strip :: "acom \<Rightarrow> com" where
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    43
"strip ASKIP = SKIP" |
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    44
"strip (Aassign x a) = (x::=a)" |
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    45
"strip (Asemi c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1; strip c\<^isub>2)" |
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    46
"strip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" |
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    47
"strip (Awhile I b c) = (WHILE b DO strip c)"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    48
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    49
subsection "Soundness"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    50
45840
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    51
lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} strip c {Q}"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
    52
proof(induction c arbitrary: Q)
45745
3a8bc5623410 invariant holds before loop
nipkow
parents: 45212
diff changeset
    53
  case (Awhile I b c)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    54
  show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    55
  proof(simp, rule While')
45745
3a8bc5623410 invariant holds before loop
nipkow
parents: 45212
diff changeset
    56
    from `\<forall>s. vc (Awhile I b c) Q s`
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    57
    have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    58
         pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all
45840
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    59
    have "\<turnstile> {pre c I} strip c {I}" by(rule Awhile.IH[OF vc])
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    60
    with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip c {I}"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    61
      by(rule strengthen_pre)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    62
    show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    63
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    64
qed (auto intro: hoare.conseq)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    65
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    66
corollary vc_sound':
45840
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    67
  "(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} strip c {Q}"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    68
by (metis strengthen_pre vc_sound)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    69
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    70
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    71
subsection "Completeness"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    72
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    73
lemma pre_mono:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    74
  "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
    75
proof (induction c arbitrary: P P' s)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    76
  case Asemi thus ?case by simp metis
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    77
qed simp_all
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    78
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    79
lemma vc_mono:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    80
  "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
    81
proof(induction c arbitrary: P P')
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    82
  case Asemi thus ?case by simp (metis pre_mono)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    83
qed simp_all
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    84
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    85
lemma vc_complete:
45840
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    86
 "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. strip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    87
  (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
    88
proof (induction rule: hoare.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    89
  case Skip
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    90
  show ?case (is "\<exists>ac. ?C ac")
45840
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
    91
  proof show "?C ASKIP" by simp qed
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    92
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    93
  case (Assign P a x)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    94
  show ?case (is "\<exists>ac. ?C ac")
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    95
  proof show "?C(Aassign x a)" by simp qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    96
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    97
  case (Semi P c1 Q c2 R)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
    98
  from Semi.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
    99
  from Semi.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   100
  show ?case (is "\<exists>ac. ?C ac")
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   101
  proof
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   102
    show "?C(Asemi ac1 ac2)"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 43158
diff changeset
   103
      using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   104
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   105
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   106
  case (If P b c1 Q c2)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   107
  from If.IH obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   108
    by blast
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   109
  from If.IH obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   110
    by blast
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   111
  show ?case (is "\<exists>ac. ?C ac")
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   112
  proof
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   113
    show "?C(Aif b ac1 ac2)" using ih1 ih2 by simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   114
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   115
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   116
  case (While P b c)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   117
  from While.IH obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   118
  show ?case (is "\<exists>ac. ?C ac")
45745
3a8bc5623410 invariant holds before loop
nipkow
parents: 45212
diff changeset
   119
  proof show "?C(Awhile P b ac)" using ih by simp qed
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   120
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   121
  case conseq thus ?case by(fast elim!: pre_mono vc_mono)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   122
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   123
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   124
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   125
subsection "An Optimization"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   126
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   127
fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
45840
dadd139192d1 added concrete syntax
nipkow
parents: 45745
diff changeset
   128
"vcpre ASKIP Q = (\<lambda>s. True, Q)" |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   129
"vcpre (Aassign x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[a/x]))" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   130
"vcpre (Asemi c\<^isub>1 c\<^isub>2) Q =
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   131
  (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   132
       (vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 wp\<^isub>2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   133
   in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, wp\<^isub>1))" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   134
"vcpre (Aif b c\<^isub>1 c\<^isub>2) Q =
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   135
  (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   136
       (vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 Q
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   137
   in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, \<lambda>s. (bval b s \<longrightarrow> wp\<^isub>1 s) \<and> (\<not>bval b s \<longrightarrow> wp\<^isub>2 s)))" |
45745
3a8bc5623410 invariant holds before loop
nipkow
parents: 45212
diff changeset
   138
"vcpre (Awhile I b c) Q =
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   139
  (let (vcc,wpc) = vcpre c I
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   140
   in (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   141
           (I s \<and> bval b s \<longrightarrow> wpc s) \<and> vcc s, I))"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   142
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   143
lemma vcpre_vc_pre: "vcpre c Q = (vc c Q, pre c Q)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   144
by (induct c arbitrary: Q) (simp_all add: Let_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   145
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   146
end