src/HOL/IMP/Hoare_Sound_Complete.thy
author huffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165 d26a45f3c835
parent 43158 686fa0a0696e
child 45015 fdac1e9880eb
permissions -rw-r--r--
remove lemma stupid_ext
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
definition
kleing@43158
     8
hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
kleing@43158
     9
"\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t  \<longrightarrow>  P s \<longrightarrow>  Q t)"
kleing@43158
    10
kleing@43158
    11
lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
kleing@43158
    12
proof(induct rule: hoare.induct)
kleing@43158
    13
  case (While P b c)
kleing@43158
    14
  { fix s t
kleing@43158
    15
    have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s \<longrightarrow> P t \<and> \<not> bval b t"
kleing@43158
    16
    proof(induct "WHILE b DO c" s t rule: big_step_induct)
kleing@43158
    17
      case WhileFalse thus ?case by blast
kleing@43158
    18
    next
kleing@43158
    19
      case WhileTrue thus ?case
kleing@43158
    20
        using While(2) unfolding hoare_valid_def by blast
kleing@43158
    21
    qed
kleing@43158
    22
  }
kleing@43158
    23
  thus ?case unfolding hoare_valid_def by blast
kleing@43158
    24
qed (auto simp: hoare_valid_def)
kleing@43158
    25
kleing@43158
    26
kleing@43158
    27
subsection "Weakest Precondition"
kleing@43158
    28
kleing@43158
    29
definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
kleing@43158
    30
"wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t  \<longrightarrow>  Q t)"
kleing@43158
    31
kleing@43158
    32
lemma wp_SKIP[simp]: "wp SKIP Q = Q"
kleing@43158
    33
by (rule ext) (auto simp: wp_def)
kleing@43158
    34
kleing@43158
    35
lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
kleing@43158
    36
by (rule ext) (auto simp: wp_def)
kleing@43158
    37
kleing@43158
    38
lemma wp_Semi[simp]: "wp (c\<^isub>1;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"
kleing@43158
    39
by (rule ext) (auto simp: wp_def)
kleing@43158
    40
kleing@43158
    41
lemma wp_If[simp]:
kleing@43158
    42
 "wp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q =
kleing@43158
    43
 (\<lambda>s. (bval b s \<longrightarrow> wp c\<^isub>1 Q s) \<and>  (\<not> bval b s \<longrightarrow> wp c\<^isub>2 Q s))"
kleing@43158
    44
by (rule ext) (auto simp: wp_def)
kleing@43158
    45
kleing@43158
    46
lemma wp_While_If:
kleing@43158
    47
 "wp (WHILE b DO c) Q s =
kleing@43158
    48
  wp (IF b THEN c;WHILE b DO c ELSE SKIP) Q s"
kleing@43158
    49
unfolding wp_def by (metis unfold_while)
kleing@43158
    50
kleing@43158
    51
lemma wp_While_True[simp]: "bval b s \<Longrightarrow>
kleing@43158
    52
  wp (WHILE b DO c) Q s = wp (c; WHILE b DO c) Q s"
kleing@43158
    53
by(simp add: wp_While_If)
kleing@43158
    54
kleing@43158
    55
lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"
kleing@43158
    56
by(simp add: wp_While_If)
kleing@43158
    57
kleing@43158
    58
kleing@43158
    59
subsection "Completeness"
kleing@43158
    60
kleing@43158
    61
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
kleing@43158
    62
proof(induct c arbitrary: Q)
kleing@43158
    63
  case Semi thus ?case by(auto intro: Semi)
kleing@43158
    64
next
kleing@43158
    65
  case (If b c1 c2)
kleing@43158
    66
  let ?If = "IF b THEN c1 ELSE c2"
kleing@43158
    67
  show ?case
kleing@43158
    68
  proof(rule hoare.If)
kleing@43158
    69
    show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> bval b s} c1 {Q}"
kleing@43158
    70
    proof(rule strengthen_pre[OF _ If(1)])
kleing@43158
    71
      show "\<forall>s. wp ?If Q s \<and> bval b s \<longrightarrow> wp c1 Q s" by auto
kleing@43158
    72
    qed
kleing@43158
    73
    show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> \<not> bval b s} c2 {Q}"
kleing@43158
    74
    proof(rule strengthen_pre[OF _ If(2)])
kleing@43158
    75
      show "\<forall>s. wp ?If Q s \<and> \<not> bval b s \<longrightarrow> wp c2 Q s" by auto
kleing@43158
    76
    qed
kleing@43158
    77
  qed
kleing@43158
    78
next
kleing@43158
    79
  case (While b c)
kleing@43158
    80
  let ?w = "WHILE b DO c"
kleing@43158
    81
  have "\<turnstile> {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> bval b s}"
kleing@43158
    82
  proof(rule hoare.While)
kleing@43158
    83
    show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}"
kleing@43158
    84
    proof(rule strengthen_pre[OF _ While(1)])
kleing@43158
    85
      show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto
kleing@43158
    86
    qed
kleing@43158
    87
  qed
kleing@43158
    88
  thus ?case
kleing@43158
    89
  proof(rule weaken_post)
kleing@43158
    90
    show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto
kleing@43158
    91
  qed
kleing@43158
    92
qed auto
kleing@43158
    93
kleing@43158
    94
lemma hoare_relative_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}"
kleing@43158
    95
proof(rule strengthen_pre)
kleing@43158
    96
  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
kleing@43158
    97
    by (auto simp: hoare_valid_def wp_def)
kleing@43158
    98
  show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
kleing@43158
    99
qed
kleing@43158
   100
kleing@43158
   101
end