src/HOL/IMP/Hoare_Op.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 35754 8e7dba5f00f5
child 41589 bbd861837ebc
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
nipkow@35749
     1
(*  Title:      HOL/IMP/Hoare_Op.thy
nipkow@35749
     2
    ID:         $Id$
nipkow@35749
     3
    Author:     Tobias Nipkow
nipkow@35749
     4
*)
nipkow@35749
     5
nipkow@35754
     6
header "Soundness and Completeness wrt Operational Semantics"
nipkow@35749
     7
nipkow@35754
     8
theory Hoare_Op imports Hoare begin
nipkow@35749
     9
nipkow@35749
    10
definition
nipkow@35749
    11
  hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
nipkow@35749
    12
  "|= {P}c{Q} = (!s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> P s --> Q t)"
nipkow@35749
    13
nipkow@35749
    14
lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
nipkow@35749
    15
proof(induct rule: hoare.induct)
nipkow@35749
    16
  case (While P b c)
nipkow@35749
    17
  { fix s t
nipkow@35749
    18
    assume "\<langle>WHILE b DO c,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@35749
    19
    hence "P s \<longrightarrow> P t \<and> \<not> b t"
nipkow@35749
    20
    proof(induct "WHILE b DO c" s t)
nipkow@35749
    21
      case WhileFalse thus ?case by blast
nipkow@35749
    22
    next
nipkow@35749
    23
      case WhileTrue thus ?case
nipkow@35749
    24
        using While(2) unfolding hoare_valid_def by blast
nipkow@35749
    25
    qed
nipkow@35749
    26
nipkow@35749
    27
  }
nipkow@35749
    28
  thus ?case unfolding hoare_valid_def by blast
nipkow@35749
    29
qed (auto simp: hoare_valid_def)
nipkow@35749
    30
nipkow@35749
    31
definition
nipkow@35749
    32
  wp :: "com => assn => assn" where
nipkow@35749
    33
  "wp c Q = (%s. !t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> Q t)"
nipkow@35749
    34
nipkow@35749
    35
lemma wp_SKIP: "wp \<SKIP> Q = Q"
nipkow@35749
    36
by (simp add: wp_def)
nipkow@35749
    37
nipkow@35749
    38
lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
nipkow@35749
    39
by (simp add: wp_def)
nipkow@35749
    40
nipkow@35749
    41
lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
nipkow@35749
    42
by (rule ext) (auto simp: wp_def)
nipkow@35749
    43
nipkow@35749
    44
lemma wp_If:
nipkow@35749
    45
 "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
nipkow@35749
    46
by (rule ext) (auto simp: wp_def)
nipkow@35749
    47
nipkow@35749
    48
lemma wp_While_If:
nipkow@35749
    49
 "wp (\<WHILE> b \<DO> c) Q s =
nipkow@35749
    50
  wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
nipkow@35749
    51
unfolding wp_def by (metis equivD1 equivD2 unfold_while)
nipkow@35749
    52
nipkow@35749
    53
lemma wp_While_True: "b s ==>
nipkow@35749
    54
  wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
nipkow@35749
    55
by(simp add: wp_While_If wp_If wp_SKIP)
nipkow@35749
    56
nipkow@35749
    57
lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
nipkow@35749
    58
by(simp add: wp_While_If wp_If wp_SKIP)
nipkow@35749
    59
nipkow@35749
    60
lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
nipkow@35749
    61
nipkow@35749
    62
lemma wp_is_pre: "|- {wp c Q} c {Q}"
nipkow@35749
    63
proof(induct c arbitrary: Q)
nipkow@35749
    64
  case SKIP show ?case by auto
nipkow@35749
    65
next
nipkow@35749
    66
  case Assign show ?case by auto
nipkow@35749
    67
next
nipkow@35749
    68
  case Semi thus ?case by(auto intro: semi)
nipkow@35749
    69
next
nipkow@35749
    70
  case (Cond b c1 c2)
nipkow@35749
    71
  let ?If = "IF b THEN c1 ELSE c2"
nipkow@35749
    72
  show ?case
nipkow@35749
    73
  proof(rule If)
nipkow@35749
    74
    show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
nipkow@35749
    75
    proof(rule strengthen_pre[OF _ Cond(1)])
nipkow@35749
    76
      show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
nipkow@35749
    77
    qed
nipkow@35749
    78
    show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
nipkow@35749
    79
    proof(rule strengthen_pre[OF _ Cond(2)])
nipkow@35749
    80
      show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
nipkow@35749
    81
    qed
nipkow@35749
    82
  qed
nipkow@35749
    83
next
nipkow@35749
    84
  case (While b c)
nipkow@35749
    85
  let ?w = "WHILE b DO c"
nipkow@35749
    86
  have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}"
nipkow@35749
    87
  proof(rule hoare.While)
nipkow@35749
    88
    show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
nipkow@35749
    89
    proof(rule strengthen_pre[OF _ While(1)])
nipkow@35749
    90
      show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
nipkow@35749
    91
    qed
nipkow@35749
    92
  qed
nipkow@35749
    93
  thus ?case
nipkow@35749
    94
  proof(rule weaken_post)
nipkow@35749
    95
    show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
nipkow@35749
    96
  qed
nipkow@35749
    97
qed
nipkow@35749
    98
nipkow@35749
    99
lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
nipkow@35749
   100
proof(rule strengthen_pre)
nipkow@35749
   101
  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
nipkow@35749
   102
    by (auto simp: hoare_valid_def wp_def)
nipkow@35749
   103
  show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
nipkow@35749
   104
qed
nipkow@35749
   105
nipkow@35749
   106
end