src/HOL/IMP/Hoare_Sound_Complete.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 54809 319358e48bb1
child 63538 d7b5e2a222c2
permissions -rw-r--r--
Lots of new material for multivariate analysis
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
kleing@43158
     3
theory Hoare_Sound_Complete imports Hoare begin
kleing@43158
     4
kleing@43158
     5
subsection "Soundness"
kleing@43158
     6
kleing@43158
     7
lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
nipkow@45015
     8
proof(induction rule: hoare.induct)
kleing@43158
     9
  case (While P b c)
kleing@43158
    10
  { fix s t
nipkow@52168
    11
    have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s  \<Longrightarrow>  P t \<and> \<not> bval b t"
nipkow@45015
    12
    proof(induction "WHILE b DO c" s t rule: big_step_induct)
kleing@43158
    13
      case WhileFalse thus ?case by blast
kleing@43158
    14
    next
kleing@43158
    15
      case WhileTrue thus ?case
nipkow@52168
    16
        using While.IH unfolding hoare_valid_def by blast
kleing@43158
    17
    qed
kleing@43158
    18
  }
kleing@43158
    19
  thus ?case unfolding hoare_valid_def by blast
kleing@43158
    20
qed (auto simp: hoare_valid_def)
kleing@43158
    21
kleing@43158
    22
kleing@43158
    23
subsection "Weakest Precondition"
kleing@43158
    24
kleing@43158
    25
definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
kleing@43158
    26
"wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t  \<longrightarrow>  Q t)"
kleing@43158
    27
kleing@43158
    28
lemma wp_SKIP[simp]: "wp SKIP Q = Q"
kleing@43158
    29
by (rule ext) (auto simp: wp_def)
kleing@43158
    30
kleing@43158
    31
lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
kleing@43158
    32
by (rule ext) (auto simp: wp_def)
kleing@43158
    33
wenzelm@53015
    34
lemma wp_Seq[simp]: "wp (c\<^sub>1;;c\<^sub>2) Q = wp c\<^sub>1 (wp c\<^sub>2 Q)"
kleing@43158
    35
by (rule ext) (auto simp: wp_def)
kleing@43158
    36
kleing@43158
    37
lemma wp_If[simp]:
wenzelm@53015
    38
 "wp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q =
wenzelm@53015
    39
 (\<lambda>s. if bval b s then wp c\<^sub>1 Q s else wp c\<^sub>2 Q s)"
kleing@43158
    40
by (rule ext) (auto simp: wp_def)
kleing@43158
    41
kleing@43158
    42
lemma wp_While_If:
kleing@43158
    43
 "wp (WHILE b DO c) Q s =
nipkow@52046
    44
  wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s"
kleing@43158
    45
unfolding wp_def by (metis unfold_while)
kleing@43158
    46
kleing@43158
    47
lemma wp_While_True[simp]: "bval b s \<Longrightarrow>
nipkow@52046
    48
  wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s"
kleing@43158
    49
by(simp add: wp_While_If)
kleing@43158
    50
kleing@43158
    51
lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"
kleing@43158
    52
by(simp add: wp_While_If)
kleing@43158
    53
kleing@43158
    54
kleing@43158
    55
subsection "Completeness"
kleing@43158
    56
kleing@43158
    57
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
nipkow@45015
    58
proof(induction c arbitrary: Q)
nipkow@52373
    59
  case If thus ?case by(auto intro: conseq)
kleing@43158
    60
next
kleing@43158
    61
  case (While b c)
kleing@43158
    62
  let ?w = "WHILE b DO c"
nipkow@52193
    63
  show "\<turnstile> {wp ?w Q} ?w {Q}"
nipkow@52193
    64
  proof(rule While')
kleing@43158
    65
    show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}"
nipkow@52193
    66
    proof(rule strengthen_pre[OF _ While.IH])
kleing@43158
    67
      show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto
kleing@43158
    68
    qed
kleing@43158
    69
    show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto
kleing@43158
    70
  qed
kleing@43158
    71
qed auto
kleing@43158
    72
nipkow@52291
    73
lemma hoare_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}"
kleing@43158
    74
proof(rule strengthen_pre)
kleing@43158
    75
  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
kleing@43158
    76
    by (auto simp: hoare_valid_def wp_def)
kleing@43158
    77
  show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
kleing@43158
    78
qed
kleing@43158
    79
nipkow@54809
    80
corollary hoare_sound_complete: "\<turnstile> {P}c{Q} \<longleftrightarrow> \<Turnstile> {P}c{Q}"
nipkow@54809
    81
by (metis hoare_complete hoare_sound)
nipkow@54809
    82
kleing@43158
    83
end