src/HOL/IMP/Hoare.thy
author nipkow
Thu Mar 11 19:05:46 2010 +0100 (2010-03-11)
changeset 35735 f139a9bb6501
parent 27362 a6dc1769fdda
child 35754 8e7dba5f00f5
permissions -rw-r--r--
converted proofs to Isar
clasohm@1476
     1
(*  Title:      HOL/IMP/Hoare.thy
nipkow@938
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Tobias Nipkow
nipkow@936
     4
    Copyright   1995 TUM
nipkow@936
     5
*)
nipkow@936
     6
kleing@12431
     7
header "Inductive Definition of Hoare Logic"
kleing@12431
     8
haftmann@16417
     9
theory Hoare imports Denotation begin
nipkow@1447
    10
kleing@12431
    11
types assn = "state => bool"
nipkow@1447
    12
wenzelm@27362
    13
definition
wenzelm@27362
    14
  hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
wenzelm@27362
    15
  "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
nipkow@939
    16
berghofe@23746
    17
inductive
berghofe@23746
    18
  hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
berghofe@23746
    19
where
kleing@12431
    20
  skip: "|- {P}\<SKIP>{P}"
berghofe@23746
    21
| ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
berghofe@23746
    22
| semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
berghofe@23746
    23
| If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
kleing@12431
    24
      |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
berghofe@23746
    25
| While: "|- {%s. P s & b s} c {P} ==>
kleing@12431
    26
         |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
berghofe@23746
    27
| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
nipkow@1486
    28
          |- {P'}c{Q'}"
nipkow@1481
    29
wenzelm@27362
    30
definition
wenzelm@27362
    31
  wp :: "com => assn => assn" where
wenzelm@27362
    32
  "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
nipkow@939
    33
wenzelm@18372
    34
(*
kleing@12431
    35
Soundness (and part of) relative completeness of Hoare rules
kleing@12431
    36
wrt denotational semantics
kleing@12431
    37
*)
kleing@12431
    38
nipkow@35735
    39
lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
nipkow@35735
    40
by (blast intro: conseq)
kleing@12431
    41
nipkow@35735
    42
lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
nipkow@35735
    43
by (blast intro: conseq)
kleing@12431
    44
kleing@12431
    45
lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
nipkow@35735
    46
proof(induct rule: hoare.induct)
nipkow@35735
    47
  case (While P b c)
nipkow@35735
    48
  { fix s t
nipkow@35735
    49
    let ?G = "Gamma b (C c)"
nipkow@35735
    50
    assume "(s,t) \<in> lfp ?G"
nipkow@35735
    51
    hence "P s \<longrightarrow> P t \<and> \<not> b t"
nipkow@35735
    52
    proof(rule lfp_induct2)
nipkow@35735
    53
      show "mono ?G" by(rule Gamma_mono)
nipkow@35735
    54
    next
nipkow@35735
    55
      fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
nipkow@35735
    56
      thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
nipkow@35735
    57
        by(auto simp: hoare_valid_def Gamma_def)
nipkow@35735
    58
    qed
nipkow@35735
    59
  }
nipkow@35735
    60
  thus ?case by(simp add:hoare_valid_def)
nipkow@35735
    61
qed (auto simp: hoare_valid_def)
nipkow@35735
    62
kleing@12431
    63
kleing@12431
    64
lemma wp_SKIP: "wp \<SKIP> Q = Q"
nipkow@35735
    65
by (simp add: wp_def)
kleing@12431
    66
kleing@12431
    67
lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
nipkow@35735
    68
by (simp add: wp_def)
kleing@12431
    69
kleing@12431
    70
lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
nipkow@35735
    71
by (rule ext) (auto simp: wp_def)
kleing@12431
    72
wenzelm@18372
    73
lemma wp_If:
kleing@12431
    74
 "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
nipkow@35735
    75
by (rule ext) (auto simp: wp_def)
kleing@12431
    76
nipkow@35735
    77
lemma wp_While_If:
nipkow@35735
    78
 "wp (\<WHILE> b \<DO> c) Q s =
nipkow@35735
    79
  wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
nipkow@35735
    80
by(simp only: wp_def C_While_If)
kleing@12431
    81
kleing@12431
    82
(*Not suitable for rewriting: LOOPS!*)
wenzelm@18372
    83
lemma wp_While_if:
kleing@12434
    84
  "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
nipkow@35735
    85
by(simp add:wp_While_If wp_If wp_SKIP)
nipkow@35735
    86
nipkow@35735
    87
lemma wp_While_True: "b s ==>
nipkow@35735
    88
  wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
nipkow@35735
    89
by(simp add: wp_While_if)
nipkow@35735
    90
nipkow@35735
    91
lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
nipkow@35735
    92
by(simp add: wp_While_if)
nipkow@35735
    93
nipkow@35735
    94
lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
kleing@12431
    95
wenzelm@18372
    96
lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
kleing@12431
    97
   (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
kleing@12431
    98
apply (simp (no_asm))
kleing@12431
    99
apply (rule iffI)
kleing@12431
   100
 apply (rule weak_coinduct)
kleing@12431
   101
  apply (erule CollectI)
kleing@12431
   102
 apply safe
kleing@12431
   103
  apply simp
kleing@12431
   104
 apply simp
kleing@12431
   105
apply (simp add: wp_def Gamma_def)
kleing@12431
   106
apply (intro strip)
kleing@12431
   107
apply (rule mp)
kleing@12431
   108
 prefer 2 apply (assumption)
kleing@12431
   109
apply (erule lfp_induct2)
kleing@12431
   110
apply (fast intro!: monoI)
kleing@12431
   111
apply (subst gfp_unfold)
kleing@12431
   112
 apply (fast intro!: monoI)
kleing@12431
   113
apply fast
kleing@12431
   114
done
kleing@12431
   115
kleing@12431
   116
declare C_while [simp del]
kleing@12431
   117
wenzelm@18372
   118
lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
kleing@12431
   119
wenzelm@18372
   120
lemma wp_is_pre: "|- {wp c Q} c {Q}"
nipkow@35735
   121
proof(induct c arbitrary: Q)
nipkow@35735
   122
  case SKIP show ?case by auto
nipkow@35735
   123
next
nipkow@35735
   124
  case Assign show ?case by auto
nipkow@35735
   125
next
nipkow@35735
   126
  case Semi thus ?case by auto
nipkow@35735
   127
next
nipkow@35735
   128
  case (Cond b c1 c2)
nipkow@35735
   129
  let ?If = "IF b THEN c1 ELSE c2"
nipkow@35735
   130
  show ?case
nipkow@35735
   131
  proof(rule If)
nipkow@35735
   132
    show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
nipkow@35735
   133
    proof(rule strengthen_pre[OF _ Cond(1)])
nipkow@35735
   134
      show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
nipkow@35735
   135
    qed
nipkow@35735
   136
    show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
nipkow@35735
   137
    proof(rule strengthen_pre[OF _ Cond(2)])
nipkow@35735
   138
      show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
nipkow@35735
   139
    qed
nipkow@35735
   140
  qed
nipkow@35735
   141
next
nipkow@35735
   142
  case (While b c)
nipkow@35735
   143
  let ?w = "WHILE b DO c"
nipkow@35735
   144
  have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}"
nipkow@35735
   145
  proof(rule hoare.While)
nipkow@35735
   146
    show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
nipkow@35735
   147
    proof(rule strengthen_pre[OF _ While(1)])
nipkow@35735
   148
      show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
nipkow@35735
   149
    qed
nipkow@35735
   150
  qed
nipkow@35735
   151
  thus ?case
nipkow@35735
   152
  proof(rule weaken_post)
nipkow@35735
   153
    show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
nipkow@35735
   154
  qed
nipkow@35735
   155
qed
kleing@12431
   156
nipkow@35735
   157
lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
nipkow@35735
   158
proof(rule conseq)
nipkow@35735
   159
  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
nipkow@35735
   160
    by (auto simp: hoare_valid_def wp_def)
nipkow@35735
   161
  show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
nipkow@35735
   162
  show "\<forall>s. Q s \<longrightarrow> Q s" by auto
nipkow@35735
   163
qed
kleing@12431
   164
nipkow@939
   165
end