src/HOL/IMP/Hoare.thy
author nipkow
Fri Aug 28 18:52:41 2009 +0200 (2009-08-28)
changeset 32436 10cd49e0c067
parent 27362 a6dc1769fdda
child 35735 f139a9bb6501
permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
     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 hoare_conseq1: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
    40 apply (erule hoare.conseq)
    41 apply  assumption
    42 apply fast
    43 done
    44 
    45 lemma hoare_conseq2: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
    46 apply (rule hoare.conseq)
    47 prefer 2 apply    (assumption)
    48 apply fast
    49 apply fast
    50 done
    51 
    52 lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    53 apply (unfold hoare_valid_def)
    54 apply (induct set: hoare)
    55      apply (simp_all (no_asm_simp))
    56   apply fast
    57  apply fast
    58 apply (rule allI, rule allI, rule impI)
    59 apply (erule lfp_induct2)
    60  apply (rule Gamma_mono)
    61 apply (unfold Gamma_def)
    62 apply fast
    63 done
    64 
    65 lemma wp_SKIP: "wp \<SKIP> Q = Q"
    66 apply (unfold wp_def)
    67 apply (simp (no_asm))
    68 done
    69 
    70 lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
    71 apply (unfold wp_def)
    72 apply (simp (no_asm))
    73 done
    74 
    75 lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
    76 apply (unfold wp_def)
    77 apply (simp (no_asm))
    78 apply (rule ext)
    79 apply fast
    80 done
    81 
    82 lemma wp_If:
    83  "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
    84 apply (unfold wp_def)
    85 apply (simp (no_asm))
    86 apply (rule ext)
    87 apply fast
    88 done
    89 
    90 lemma wp_While_True:
    91   "b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
    92 apply (unfold wp_def)
    93 apply (subst C_While_If)
    94 apply (simp (no_asm_simp))
    95 done
    96 
    97 lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
    98 apply (unfold wp_def)
    99 apply (subst C_While_If)
   100 apply (simp (no_asm_simp))
   101 done
   102 
   103 lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
   104 
   105 (*Not suitable for rewriting: LOOPS!*)
   106 lemma wp_While_if:
   107   "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
   108   by simp
   109 
   110 lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
   111    (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
   112 apply (simp (no_asm))
   113 apply (rule iffI)
   114  apply (rule weak_coinduct)
   115   apply (erule CollectI)
   116  apply safe
   117   apply simp
   118  apply simp
   119 apply (simp add: wp_def Gamma_def)
   120 apply (intro strip)
   121 apply (rule mp)
   122  prefer 2 apply (assumption)
   123 apply (erule lfp_induct2)
   124 apply (fast intro!: monoI)
   125 apply (subst gfp_unfold)
   126  apply (fast intro!: monoI)
   127 apply fast
   128 done
   129 
   130 declare C_while [simp del]
   131 
   132 lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
   133 
   134 lemma wp_is_pre: "|- {wp c Q} c {Q}"
   135 apply (induct c arbitrary: Q)
   136     apply (simp_all (no_asm))
   137     apply fast+
   138  apply (blast intro: hoare_conseq1)
   139 apply (rule hoare_conseq2)
   140  apply (rule hoare.While)
   141  apply (rule hoare_conseq1)
   142   prefer 2 apply fast
   143   apply safe
   144  apply simp
   145 apply simp
   146 done
   147 
   148 lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}"
   149 apply (rule hoare_conseq1 [OF _ wp_is_pre])
   150 apply (unfold hoare_valid_def wp_def)
   151 apply fast
   152 done
   153 
   154 end