src/HOL/IMP/Hoare_Total_EX.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 63070 952714a20087
child 63538 d7b5e2a222c2
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Hoare_Total_EX imports Hoare_Sound_Complete Hoare_Examples begin
     4 
     5 subsection "Hoare Logic for Total Correctness"
     6 
     7 text{* This is the standard set of rules that you find in many publications.
     8 The While-rule is different from the one in Concrete Semantics in that the
     9 invariant is indexed by natural numbers and goes down by 1 with
    10 every iteration. The completeness proof is easier but the rule is harder
    11 to apply in program proofs. *}
    12 
    13 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
    14   ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
    15 "\<Turnstile>\<^sub>t {P}c{Q}  \<longleftrightarrow>  (\<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t))"
    16 
    17 inductive
    18   hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
    19 where
    20 
    21 Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}"  |
    22 
    23 Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}"  |
    24 
    25 Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \<turnstile>\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}"  |
    26 
    27 If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
    28   \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"  |
    29 
    30 While:
    31   "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {P (Suc n)} c {P n};
    32      \<forall>n s. P (Suc n) s \<longrightarrow> bval b s;  \<forall>s. P 0 s \<longrightarrow> \<not> bval b s \<rbrakk>
    33    \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. \<exists>n. P n s} WHILE b DO c {P 0}"  |
    34 
    35 conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
    36            \<turnstile>\<^sub>t {P'}c{Q'}"
    37 
    38 text{* Building in the consequence rule: *}
    39 
    40 lemma strengthen_pre:
    41   "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
    42 by (metis conseq)
    43 
    44 lemma weaken_post:
    45   "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
    46 by (metis conseq)
    47 
    48 lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
    49 by (simp add: strengthen_pre[OF _ Assign])
    50 
    51 text{* The soundness theorem: *}
    52 
    53 theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
    54 proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
    55   case (While P c b)
    56   {
    57     fix n s
    58     have "\<lbrakk> P n s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P 0 t"
    59     proof(induction "n" arbitrary: s)
    60       case 0 thus ?case using While.hyps(3) WhileFalse by blast
    61     next
    62       case (Suc n)
    63       thus ?case by (meson While.IH While.hyps(2) WhileTrue)
    64     qed
    65   }
    66   thus ?case by auto
    67 next
    68   case If thus ?case by auto blast
    69 qed fastforce+
    70 
    71 
    72 definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where
    73 "wp\<^sub>t c Q  =  (\<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"
    74 
    75 lemma [simp]: "wp\<^sub>t SKIP Q = Q"
    76 by(auto intro!: ext simp: wpt_def)
    77 
    78 lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
    79 by(auto intro!: ext simp: wpt_def)
    80 
    81 lemma [simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)"
    82 unfolding wpt_def
    83 apply(rule ext)
    84 apply auto
    85 done
    86 
    87 lemma [simp]:
    88  "wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q s)"
    89 apply(unfold wpt_def)
    90 apply(rule ext)
    91 apply auto
    92 done
    93 
    94 
    95 text{* Function @{text wpw} computes the weakest precondition of a While-loop
    96 that is unfolded a fixed number of times. *}
    97 
    98 fun wpw :: "bexp \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> assn \<Rightarrow> assn" where
    99 "wpw b c 0 Q s = (\<not> bval b s \<and> Q s)" |
   100 "wpw b c (Suc n) Q s = (bval b s \<and> (\<exists>s'. (c,s) \<Rightarrow> s' \<and>  wpw b c n Q s'))"
   101 
   102 lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> Q t \<Longrightarrow> \<exists>n. wpw b c n Q s"
   103 proof(induction "WHILE b DO c" s t rule: big_step_induct)
   104   case WhileFalse thus ?case using wpw.simps(1) by blast 
   105 next
   106   case WhileTrue thus ?case using wpw.simps(2) by blast
   107 qed
   108 
   109 lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
   110 proof (induction c arbitrary: Q)
   111   case SKIP show ?case by (auto intro:hoaret.Skip)
   112 next
   113   case Assign show ?case by (auto intro:hoaret.Assign)
   114 next
   115   case Seq thus ?case by (auto intro:hoaret.Seq)
   116 next
   117   case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
   118 next
   119   case (While b c)
   120   let ?w = "WHILE b DO c"
   121   have c1: "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> (\<exists>n. wpw b c n Q s)"
   122     unfolding wpt_def by (metis WHILE_Its)
   123   have c3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> Q s" by simp
   124   have w2: "\<forall>n s. wpw b c (Suc n) Q s \<longrightarrow> bval b s" by simp
   125   have w3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> \<not> bval b s" by simp
   126   { fix n
   127     have 1: "\<forall>s. wpw b c (Suc n) Q s \<longrightarrow> (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c n Q t)"
   128       by simp
   129     note strengthen_pre[OF 1 While.IH[of "wpw b c n Q", unfolded wpt_def]]
   130   }
   131   from conseq[OF c1 hoaret.While[OF this w2 w3] c3]
   132   show ?case .
   133 qed
   134 
   135 theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
   136 apply(rule strengthen_pre[OF _ wpt_is_pre])
   137 apply(auto simp: hoare_tvalid_def wpt_def)
   138 done
   139 
   140 corollary hoaret_sound_complete: "\<turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> \<Turnstile>\<^sub>t {P}c{Q}"
   141 by (metis hoaret_sound hoaret_complete)
   142 
   143 end