src/HOL/IMP/Hoare.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45212 e87feee00a4c
child 47818 151d137f1095
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     3
header "Hoare Logic"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     4
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     5
theory Hoare imports Big_Step begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     7
subsection "Hoare Logic for Partial Correctness"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     8
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     9
type_synonym assn = "state \<Rightarrow> bool"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    10
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 43158
diff changeset
    11
abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    12
  ("_[_'/_]" [1000,0,0] 999)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    13
where "s[a/x] == s(x := aval a s)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    14
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    15
inductive
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    16
  hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    17
where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    18
Skip: "\<turnstile> {P} SKIP {P}"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    20
Assign:  "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    21
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
Semi: "\<lbrakk> \<turnstile> {P} c\<^isub>1 {Q};  \<turnstile> {Q} c\<^isub>2 {R} \<rbrakk>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    23
       \<Longrightarrow> \<turnstile> {P} c\<^isub>1;c\<^isub>2 {R}"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    24
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    25
If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q};  \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    26
     \<Longrightarrow> \<turnstile> {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    27
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    28
While: "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
        \<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    30
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    31
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
        \<Longrightarrow> \<turnstile> {P'} c {Q'}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    33
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    34
lemmas [simp] = hoare.Skip hoare.Assign hoare.Semi If
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    35
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
lemmas [intro!] = hoare.Skip hoare.Assign hoare.Semi hoare.If
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    37
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    38
lemma strengthen_pre:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    39
  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
by (blast intro: conseq)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    41
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    42
lemma weaken_post:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    43
  "\<lbrakk> \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile> {P} c {Q'}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    44
by (blast intro: conseq)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    45
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    46
text{* The assignment and While rule are awkward to use in actual proofs
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    47
because their pre and postcondition are of a very special form and the actual
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    48
goal would have to match this form exactly. Therefore we derive two variants
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    49
with arbitrary pre and postconditions. *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    50
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    51
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    52
by (simp add: strengthen_pre[OF _ Assign])
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    53
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    54
lemma While':
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    55
assumes "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    56
shows "\<turnstile> {P} WHILE b DO c {Q}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    57
by(rule weaken_post[OF While[OF assms(1)] assms(2)])
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    58
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    59
end