src/HOL/IMP/Hoare.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45212 e87feee00a4c
child 47818 151d137f1095
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (* Author: Tobias Nipkow *)
     2 
     3 header "Hoare Logic"
     4 
     5 theory Hoare imports Big_Step begin
     6 
     7 subsection "Hoare Logic for Partial Correctness"
     8 
     9 type_synonym assn = "state \<Rightarrow> bool"
    10 
    11 abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
    12   ("_[_'/_]" [1000,0,0] 999)
    13 where "s[a/x] == s(x := aval a s)"
    14 
    15 inductive
    16   hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)
    17 where
    18 Skip: "\<turnstile> {P} SKIP {P}"  |
    19 
    20 Assign:  "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}"  |
    21 
    22 Semi: "\<lbrakk> \<turnstile> {P} c\<^isub>1 {Q};  \<turnstile> {Q} c\<^isub>2 {R} \<rbrakk>
    23        \<Longrightarrow> \<turnstile> {P} c\<^isub>1;c\<^isub>2 {R}"  |
    24 
    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>
    26      \<Longrightarrow> \<turnstile> {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}"  |
    27 
    28 While: "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
    29         \<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}"  |
    30 
    31 conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
    32         \<Longrightarrow> \<turnstile> {P'} c {Q'}"
    33 
    34 lemmas [simp] = hoare.Skip hoare.Assign hoare.Semi If
    35 
    36 lemmas [intro!] = hoare.Skip hoare.Assign hoare.Semi hoare.If
    37 
    38 lemma strengthen_pre:
    39   "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
    40 by (blast intro: conseq)
    41 
    42 lemma weaken_post:
    43   "\<lbrakk> \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile> {P} c {Q'}"
    44 by (blast intro: conseq)
    45 
    46 text{* The assignment and While rule are awkward to use in actual proofs
    47 because their pre and postcondition are of a very special form and the actual
    48 goal would have to match this form exactly. Therefore we derive two variants
    49 with arbitrary pre and postconditions. *}
    50 
    51 lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}"
    52 by (simp add: strengthen_pre[OF _ Assign])
    53 
    54 lemma While':
    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"
    56 shows "\<turnstile> {P} WHILE b DO c {Q}"
    57 by(rule weaken_post[OF While[OF assms(1)] assms(2)])
    58 
    59 end