src/HOL/IMP/Hoare.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 20503 503ac4c5ef91
child 23746 a455e69c31cc
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
clasohm@1476
     1
(*  Title:      HOL/IMP/Hoare.thy
nipkow@938
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Tobias Nipkow
nipkow@936
     4
    Copyright   1995 TUM
nipkow@936
     5
*)
nipkow@936
     6
kleing@12431
     7
header "Inductive Definition of Hoare Logic"
kleing@12431
     8
haftmann@16417
     9
theory Hoare imports Denotation begin
nipkow@1447
    10
kleing@12431
    11
types assn = "state => bool"
nipkow@1447
    12
kleing@12431
    13
constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
nipkow@1696
    14
          "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
nipkow@939
    15
nipkow@1696
    16
consts hoare :: "(assn * com * assn) set"
wenzelm@12546
    17
syntax "_hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
nipkow@1486
    18
translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
nipkow@939
    19
paulson@1789
    20
inductive hoare
kleing@12431
    21
intros
kleing@12431
    22
  skip: "|- {P}\<SKIP>{P}"
kleing@12431
    23
  ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
kleing@12431
    24
  semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
kleing@12431
    25
  If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
kleing@12431
    26
      |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
kleing@12431
    27
  While: "|- {%s. P s & b s} c {P} ==>
kleing@12431
    28
         |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
kleing@12431
    29
  conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
nipkow@1486
    30
          |- {P'}c{Q'}"
nipkow@1481
    31
kleing@12431
    32
constdefs wp :: "com => assn => assn"
nipkow@2810
    33
          "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
nipkow@939
    34
wenzelm@18372
    35
(*
kleing@12431
    36
Soundness (and part of) relative completeness of Hoare rules
kleing@12431
    37
wrt denotational semantics
kleing@12431
    38
*)
kleing@12431
    39
kleing@12431
    40
lemma hoare_conseq1: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
kleing@12431
    41
apply (erule hoare.conseq)
kleing@12431
    42
apply  assumption
kleing@12431
    43
apply fast
kleing@12431
    44
done
kleing@12431
    45
kleing@12431
    46
lemma hoare_conseq2: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
kleing@12431
    47
apply (rule hoare.conseq)
kleing@12431
    48
prefer 2 apply    (assumption)
kleing@12431
    49
apply fast
kleing@12431
    50
apply fast
kleing@12431
    51
done
kleing@12431
    52
kleing@12431
    53
lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
kleing@12431
    54
apply (unfold hoare_valid_def)
wenzelm@18372
    55
apply (induct set: hoare)
kleing@12431
    56
     apply (simp_all (no_asm_simp))
kleing@12431
    57
  apply fast
kleing@12431
    58
 apply fast
kleing@12431
    59
apply (rule allI, rule allI, rule impI)
kleing@12431
    60
apply (erule lfp_induct2)
kleing@12431
    61
 apply (rule Gamma_mono)
kleing@12431
    62
apply (unfold Gamma_def)
kleing@12431
    63
apply fast
kleing@12431
    64
done
kleing@12431
    65
kleing@12431
    66
lemma wp_SKIP: "wp \<SKIP> Q = Q"
kleing@12431
    67
apply (unfold wp_def)
kleing@12431
    68
apply (simp (no_asm))
kleing@12431
    69
done
kleing@12431
    70
kleing@12431
    71
lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
kleing@12431
    72
apply (unfold wp_def)
kleing@12431
    73
apply (simp (no_asm))
kleing@12431
    74
done
kleing@12431
    75
kleing@12431
    76
lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
kleing@12431
    77
apply (unfold wp_def)
kleing@12431
    78
apply (simp (no_asm))
kleing@12431
    79
apply (rule ext)
kleing@12431
    80
apply fast
kleing@12431
    81
done
kleing@12431
    82
wenzelm@18372
    83
lemma wp_If:
kleing@12431
    84
 "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
kleing@12431
    85
apply (unfold wp_def)
kleing@12431
    86
apply (simp (no_asm))
kleing@12431
    87
apply (rule ext)
kleing@12431
    88
apply fast
kleing@12431
    89
done
kleing@12431
    90
wenzelm@18372
    91
lemma wp_While_True:
kleing@12431
    92
  "b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
kleing@12431
    93
apply (unfold wp_def)
kleing@12431
    94
apply (subst C_While_If)
kleing@12431
    95
apply (simp (no_asm_simp))
kleing@12431
    96
done
kleing@12431
    97
kleing@12431
    98
lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
kleing@12431
    99
apply (unfold wp_def)
kleing@12431
   100
apply (subst C_While_If)
kleing@12431
   101
apply (simp (no_asm_simp))
kleing@12431
   102
done
kleing@12431
   103
kleing@12434
   104
lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
kleing@12431
   105
kleing@12431
   106
(*Not suitable for rewriting: LOOPS!*)
wenzelm@18372
   107
lemma wp_While_if:
kleing@12434
   108
  "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
wenzelm@18372
   109
  by simp
kleing@12431
   110
wenzelm@18372
   111
lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
kleing@12431
   112
   (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
kleing@12431
   113
apply (simp (no_asm))
kleing@12431
   114
apply (rule iffI)
kleing@12431
   115
 apply (rule weak_coinduct)
kleing@12431
   116
  apply (erule CollectI)
kleing@12431
   117
 apply safe
kleing@12431
   118
  apply simp
kleing@12431
   119
 apply simp
kleing@12431
   120
apply (simp add: wp_def Gamma_def)
kleing@12431
   121
apply (intro strip)
kleing@12431
   122
apply (rule mp)
kleing@12431
   123
 prefer 2 apply (assumption)
kleing@12431
   124
apply (erule lfp_induct2)
kleing@12431
   125
apply (fast intro!: monoI)
kleing@12431
   126
apply (subst gfp_unfold)
kleing@12431
   127
 apply (fast intro!: monoI)
kleing@12431
   128
apply fast
kleing@12431
   129
done
kleing@12431
   130
kleing@12431
   131
declare C_while [simp del]
kleing@12431
   132
wenzelm@18372
   133
lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
kleing@12431
   134
wenzelm@18372
   135
lemma wp_is_pre: "|- {wp c Q} c {Q}"
wenzelm@20503
   136
apply (induct c arbitrary: Q)
kleing@12431
   137
    apply (simp_all (no_asm))
kleing@12431
   138
    apply fast+
kleing@12431
   139
 apply (blast intro: hoare_conseq1)
kleing@12431
   140
apply (rule hoare_conseq2)
kleing@12431
   141
 apply (rule hoare.While)
kleing@12431
   142
 apply (rule hoare_conseq1)
wenzelm@18372
   143
  prefer 2 apply fast
kleing@12431
   144
  apply safe
nipkow@13630
   145
 apply simp
nipkow@13630
   146
apply simp
kleing@12431
   147
done
kleing@12431
   148
kleing@12431
   149
lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}"
kleing@12431
   150
apply (rule hoare_conseq1 [OF _ wp_is_pre])
kleing@12431
   151
apply (unfold hoare_valid_def wp_def)
kleing@12431
   152
apply fast
kleing@12431
   153
done
kleing@12431
   154
nipkow@939
   155
end