src/HOL/IMP/Hoare.thy
author nipkow
Thu Mar 11 19:05:46 2010 +0100 (2010-03-11)
changeset 35735 f139a9bb6501
parent 27362 a6dc1769fdda
child 35754 8e7dba5f00f5
permissions -rw-r--r--
converted proofs to Isar
     1 (*  Title:      HOL/IMP/Hoare.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995 TUM
     5 *)
     6 
     7 header "Inductive Definition of Hoare Logic"
     8 
     9 theory Hoare imports Denotation begin
    10 
    11 types assn = "state => bool"
    12 
    13 definition
    14   hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
    15   "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
    16 
    17 inductive
    18   hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    19 where
    20   skip: "|- {P}\<SKIP>{P}"
    21 | ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
    22 | semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    23 | If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    24       |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
    25 | While: "|- {%s. P s & b s} c {P} ==>
    26          |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
    27 | conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    28           |- {P'}c{Q'}"
    29 
    30 definition
    31   wp :: "com => assn => assn" where
    32   "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
    33 
    34 (*
    35 Soundness (and part of) relative completeness of Hoare rules
    36 wrt denotational semantics
    37 *)
    38 
    39 lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
    40 by (blast intro: conseq)
    41 
    42 lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
    43 by (blast intro: conseq)
    44 
    45 lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    46 proof(induct rule: hoare.induct)
    47   case (While P b c)
    48   { fix s t
    49     let ?G = "Gamma b (C c)"
    50     assume "(s,t) \<in> lfp ?G"
    51     hence "P s \<longrightarrow> P t \<and> \<not> b t"
    52     proof(rule lfp_induct2)
    53       show "mono ?G" by(rule Gamma_mono)
    54     next
    55       fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
    56       thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
    57         by(auto simp: hoare_valid_def Gamma_def)
    58     qed
    59   }
    60   thus ?case by(simp add:hoare_valid_def)
    61 qed (auto simp: hoare_valid_def)
    62 
    63 
    64 lemma wp_SKIP: "wp \<SKIP> Q = Q"
    65 by (simp add: wp_def)
    66 
    67 lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
    68 by (simp add: wp_def)
    69 
    70 lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
    71 by (rule ext) (auto simp: wp_def)
    72 
    73 lemma wp_If:
    74  "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
    75 by (rule ext) (auto simp: wp_def)
    76 
    77 lemma wp_While_If:
    78  "wp (\<WHILE> b \<DO> c) Q s =
    79   wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
    80 by(simp only: wp_def C_While_If)
    81 
    82 (*Not suitable for rewriting: LOOPS!*)
    83 lemma wp_While_if:
    84   "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
    85 by(simp add:wp_While_If wp_If wp_SKIP)
    86 
    87 lemma wp_While_True: "b s ==>
    88   wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
    89 by(simp add: wp_While_if)
    90 
    91 lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
    92 by(simp add: wp_While_if)
    93 
    94 lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
    95 
    96 lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
    97    (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
    98 apply (simp (no_asm))
    99 apply (rule iffI)
   100  apply (rule weak_coinduct)
   101   apply (erule CollectI)
   102  apply safe
   103   apply simp
   104  apply simp
   105 apply (simp add: wp_def Gamma_def)
   106 apply (intro strip)
   107 apply (rule mp)
   108  prefer 2 apply (assumption)
   109 apply (erule lfp_induct2)
   110 apply (fast intro!: monoI)
   111 apply (subst gfp_unfold)
   112  apply (fast intro!: monoI)
   113 apply fast
   114 done
   115 
   116 declare C_while [simp del]
   117 
   118 lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
   119 
   120 lemma wp_is_pre: "|- {wp c Q} c {Q}"
   121 proof(induct c arbitrary: Q)
   122   case SKIP show ?case by auto
   123 next
   124   case Assign show ?case by auto
   125 next
   126   case Semi thus ?case by auto
   127 next
   128   case (Cond b c1 c2)
   129   let ?If = "IF b THEN c1 ELSE c2"
   130   show ?case
   131   proof(rule If)
   132     show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
   133     proof(rule strengthen_pre[OF _ Cond(1)])
   134       show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
   135     qed
   136     show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
   137     proof(rule strengthen_pre[OF _ Cond(2)])
   138       show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
   139     qed
   140   qed
   141 next
   142   case (While b c)
   143   let ?w = "WHILE b DO c"
   144   have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}"
   145   proof(rule hoare.While)
   146     show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
   147     proof(rule strengthen_pre[OF _ While(1)])
   148       show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
   149     qed
   150   qed
   151   thus ?case
   152   proof(rule weaken_post)
   153     show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
   154   qed
   155 qed
   156 
   157 lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
   158 proof(rule conseq)
   159   show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
   160     by (auto simp: hoare_valid_def wp_def)
   161   show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
   162   show "\<forall>s. Q s \<longrightarrow> Q s" by auto
   163 qed
   164 
   165 end