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