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