src/HOL/IMP/Hoare.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 23746 a455e69c31cc
child 27362 a6dc1769fdda
permissions -rw-r--r--
avoid rebinding of existing facts;
     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 constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
    14           "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
    15 
    16 inductive
    17   hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    18 where
    19   skip: "|- {P}\<SKIP>{P}"
    20 | ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
    21 | semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    22 | If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    23       |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
    24 | While: "|- {%s. P s & b s} c {P} ==>
    25          |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
    26 | conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    27           |- {P'}c{Q'}"
    28 
    29 constdefs wp :: "com => assn => assn"
    30           "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
    31 
    32 (*
    33 Soundness (and part of) relative completeness of Hoare rules
    34 wrt denotational semantics
    35 *)
    36 
    37 lemma hoare_conseq1: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
    38 apply (erule hoare.conseq)
    39 apply  assumption
    40 apply fast
    41 done
    42 
    43 lemma hoare_conseq2: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
    44 apply (rule hoare.conseq)
    45 prefer 2 apply    (assumption)
    46 apply fast
    47 apply fast
    48 done
    49 
    50 lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    51 apply (unfold hoare_valid_def)
    52 apply (induct set: hoare)
    53      apply (simp_all (no_asm_simp))
    54   apply fast
    55  apply fast
    56 apply (rule allI, rule allI, rule impI)
    57 apply (erule lfp_induct2)
    58  apply (rule Gamma_mono)
    59 apply (unfold Gamma_def)
    60 apply fast
    61 done
    62 
    63 lemma wp_SKIP: "wp \<SKIP> Q = Q"
    64 apply (unfold wp_def)
    65 apply (simp (no_asm))
    66 done
    67 
    68 lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
    69 apply (unfold wp_def)
    70 apply (simp (no_asm))
    71 done
    72 
    73 lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
    74 apply (unfold wp_def)
    75 apply (simp (no_asm))
    76 apply (rule ext)
    77 apply fast
    78 done
    79 
    80 lemma wp_If:
    81  "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
    82 apply (unfold wp_def)
    83 apply (simp (no_asm))
    84 apply (rule ext)
    85 apply fast
    86 done
    87 
    88 lemma wp_While_True:
    89   "b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
    90 apply (unfold wp_def)
    91 apply (subst C_While_If)
    92 apply (simp (no_asm_simp))
    93 done
    94 
    95 lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
    96 apply (unfold wp_def)
    97 apply (subst C_While_If)
    98 apply (simp (no_asm_simp))
    99 done
   100 
   101 lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
   102 
   103 (*Not suitable for rewriting: LOOPS!*)
   104 lemma wp_While_if:
   105   "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
   106   by simp
   107 
   108 lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
   109    (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
   110 apply (simp (no_asm))
   111 apply (rule iffI)
   112  apply (rule weak_coinduct)
   113   apply (erule CollectI)
   114  apply safe
   115   apply simp
   116  apply simp
   117 apply (simp add: wp_def Gamma_def)
   118 apply (intro strip)
   119 apply (rule mp)
   120  prefer 2 apply (assumption)
   121 apply (erule lfp_induct2)
   122 apply (fast intro!: monoI)
   123 apply (subst gfp_unfold)
   124  apply (fast intro!: monoI)
   125 apply fast
   126 done
   127 
   128 declare C_while [simp del]
   129 
   130 lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
   131 
   132 lemma wp_is_pre: "|- {wp c Q} c {Q}"
   133 apply (induct c arbitrary: Q)
   134     apply (simp_all (no_asm))
   135     apply fast+
   136  apply (blast intro: hoare_conseq1)
   137 apply (rule hoare_conseq2)
   138  apply (rule hoare.While)
   139  apply (rule hoare_conseq1)
   140   prefer 2 apply fast
   141   apply safe
   142  apply simp
   143 apply simp
   144 done
   145 
   146 lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}"
   147 apply (rule hoare_conseq1 [OF _ wp_is_pre])
   148 apply (unfold hoare_valid_def wp_def)
   149 apply fast
   150 done
   151 
   152 end