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