src/HOL/IMP/Hoare_Sound_Complete.thy
author nipkow
Wed, 18 Dec 2013 17:52:44 +0100
changeset 54809 319358e48bb1
parent 53015 a1119cf551e8
child 63538 d7b5e2a222c2
permissions -rw-r--r--
added lemma
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     3
theory Hoare_Sound_Complete 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 "Soundness"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     7
lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
     8
proof(induction rule: hoare.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     9
  case (While P b c)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    10
  { fix s t
52168
nipkow
parents: 52165
diff changeset
    11
    have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s  \<Longrightarrow>  P t \<and> \<not> bval b t"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    12
    proof(induction "WHILE b DO c" s t rule: big_step_induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    13
      case WhileFalse thus ?case by blast
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    14
    next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    15
      case WhileTrue thus ?case
52168
nipkow
parents: 52165
diff changeset
    16
        using While.IH unfolding hoare_valid_def by blast
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    17
    qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    18
  }
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
  thus ?case unfolding hoare_valid_def by blast
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    20
qed (auto simp: hoare_valid_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    21
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    23
subsection "Weakest Precondition"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    24
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    25
definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    26
"wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t  \<longrightarrow>  Q t)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    27
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    28
lemma wp_SKIP[simp]: "wp SKIP Q = Q"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
by (rule ext) (auto simp: wp_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    30
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    31
lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
by (rule ext) (auto simp: wp_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    33
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52373
diff changeset
    34
lemma wp_Seq[simp]: "wp (c\<^sub>1;;c\<^sub>2) Q = wp c\<^sub>1 (wp c\<^sub>2 Q)"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    35
by (rule ext) (auto simp: wp_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    37
lemma wp_If[simp]:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52373
diff changeset
    38
 "wp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q =
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52373
diff changeset
    39
 (\<lambda>s. if bval b s then wp c\<^sub>1 Q s else wp c\<^sub>2 Q s)"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
by (rule ext) (auto simp: wp_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    41
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    42
lemma wp_While_If:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    43
 "wp (WHILE b DO c) Q s =
52046
bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents: 47818
diff changeset
    44
  wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    45
unfolding wp_def by (metis unfold_while)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    46
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    47
lemma wp_While_True[simp]: "bval b s \<Longrightarrow>
52046
bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents: 47818
diff changeset
    48
  wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    49
by(simp add: wp_While_If)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    50
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    51
lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    52
by(simp add: wp_While_If)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    53
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    54
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    55
subsection "Completeness"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    56
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    57
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    58
proof(induction c arbitrary: Q)
52373
a231e6f89737 simplified proofs
nipkow
parents: 52316
diff changeset
    59
  case If thus ?case by(auto intro: conseq)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    60
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    61
  case (While b c)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    62
  let ?w = "WHILE b DO c"
52193
nipkow
parents: 52168
diff changeset
    63
  show "\<turnstile> {wp ?w Q} ?w {Q}"
nipkow
parents: 52168
diff changeset
    64
  proof(rule While')
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    65
    show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}"
52193
nipkow
parents: 52168
diff changeset
    66
    proof(rule strengthen_pre[OF _ While.IH])
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    67
      show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    68
    qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    69
    show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    70
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    71
qed auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    72
52291
b7c8675437ec corrected name
nipkow
parents: 52193
diff changeset
    73
lemma hoare_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    74
proof(rule strengthen_pre)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    75
  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    76
    by (auto simp: hoare_valid_def wp_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    77
  show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    78
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    79
54809
319358e48bb1 added lemma
nipkow
parents: 53015
diff changeset
    80
corollary hoare_sound_complete: "\<turnstile> {P}c{Q} \<longleftrightarrow> \<Turnstile> {P}c{Q}"
319358e48bb1 added lemma
nipkow
parents: 53015
diff changeset
    81
by (metis hoare_complete hoare_sound)
319358e48bb1 added lemma
nipkow
parents: 53015
diff changeset
    82
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    83
end