src/HOL/IMP/Hoare_Total.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 55132 ee5a0ca00b6f
child 63538 d7b5e2a222c2
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Hoare_Total imports Hoare_Sound_Complete Hoare_Examples begin
     4 
     5 subsection "Hoare Logic for Total Correctness"
     6 
     7 text{* Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only
     8 works if execution is deterministic (which it is in our case). *}
     9 
    10 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
    11   ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
    12 "\<Turnstile>\<^sub>t {P}c{Q}  \<longleftrightarrow>  (\<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t))"
    13 
    14 text{* Provability of Hoare triples in the proof system for total
    15 correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined
    16 inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for
    17 @{text"\<turnstile>"} only in the one place where nontermination can arise: the
    18 @{term While}-rule. *}
    19 
    20 inductive
    21   hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
    22 where
    23 
    24 Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}"  |
    25 
    26 Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}"  |
    27 
    28 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}"  |
    29 
    30 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>
    31   \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"  |
    32 
    33 While:
    34   "(\<And>n::nat.
    35     \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'<n. T s n')})
    36    \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T s n)} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"  |
    37 
    38 conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
    39            \<turnstile>\<^sub>t {P'}c{Q'}"
    40 
    41 text{* The @{term While}-rule is like the one for partial correctness but it
    42 requires additionally that with every execution of the loop body some measure
    43 relation @{term[source]"T :: state \<Rightarrow> nat \<Rightarrow> bool"} decreases.
    44 The following functional version is more intuitive: *}
    45 
    46 lemma While_fun:
    47   "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>
    48    \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"
    49   by (rule While [where T="\<lambda>s n. n = f s", simplified])
    50 
    51 text{* Building in the consequence rule: *}
    52 
    53 lemma strengthen_pre:
    54   "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
    55 by (metis conseq)
    56 
    57 lemma weaken_post:
    58   "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
    59 by (metis conseq)
    60 
    61 lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
    62 by (simp add: strengthen_pre[OF _ Assign])
    63 
    64 lemma While_fun':
    65 assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}"
    66     and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
    67 shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}"
    68 by(blast intro: assms(1) weaken_post[OF While_fun assms(2)])
    69 
    70 
    71 text{* Our standard example: *}
    72 
    73 lemma "\<turnstile>\<^sub>t {\<lambda>s. s ''x'' = i} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum i}"
    74 apply(rule Seq)
    75  prefer 2
    76  apply(rule While_fun' [where P = "\<lambda>s. (s ''y'' = sum i - sum(s ''x''))"
    77     and f = "\<lambda>s. nat(s ''x'')"])
    78    apply(rule Seq)
    79    prefer 2
    80    apply(rule Assign)
    81   apply(rule Assign')
    82   apply simp
    83  apply(simp)
    84 apply(rule Assign')
    85 apply simp
    86 done
    87 
    88 
    89 text{* The soundness theorem: *}
    90 
    91 theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
    92 proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
    93   case (While P b T c)
    94   {
    95     fix s n
    96     have "\<lbrakk> P s; T s n \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t"
    97     proof(induction "n" arbitrary: s rule: less_induct)
    98       case (less n)
    99       thus ?case by (metis While.IH WhileFalse WhileTrue)
   100     qed
   101   }
   102   thus ?case by auto
   103 next
   104   case If thus ?case by auto blast
   105 qed fastforce+
   106 
   107 
   108 text{*
   109 The completeness proof proceeds along the same lines as the one for partial
   110 correctness. First we have to strengthen our notion of weakest precondition
   111 to take termination into account: *}
   112 
   113 definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where
   114 "wp\<^sub>t c Q  =  (\<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"
   115 
   116 lemma [simp]: "wp\<^sub>t SKIP Q = Q"
   117 by(auto intro!: ext simp: wpt_def)
   118 
   119 lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
   120 by(auto intro!: ext simp: wpt_def)
   121 
   122 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)"
   123 unfolding wpt_def
   124 apply(rule ext)
   125 apply auto
   126 done
   127 
   128 lemma [simp]:
   129  "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)"
   130 apply(unfold wpt_def)
   131 apply(rule ext)
   132 apply auto
   133 done
   134 
   135 
   136 text{* Now we define the number of iterations @{term "WHILE b DO c"} needs to
   137 terminate when started in state @{text s}. Because this is a truly partial
   138 function, we define it as an (inductive) relation first: *}
   139 
   140 inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where
   141 Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" |
   142 Its_Suc: "\<lbrakk> bval b s;  (c,s) \<Rightarrow> s';  Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)"
   143 
   144 text{* The relation is in fact a function: *}
   145 
   146 lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
   147 proof(induction arbitrary: n' rule:Its.induct)
   148   case Its_0 thus ?case by(metis Its.cases)
   149 next
   150   case Its_Suc thus ?case by(metis Its.cases big_step_determ)
   151 qed
   152 
   153 text{* For all terminating loops, @{const Its} yields a result: *}
   154 
   155 lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
   156 proof(induction "WHILE b DO c" s t rule: big_step_induct)
   157   case WhileFalse thus ?case by (metis Its_0)
   158 next
   159   case WhileTrue thus ?case by (metis Its_Suc)
   160 qed
   161 
   162 lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
   163 proof (induction c arbitrary: Q)
   164   case SKIP show ?case by (auto intro:hoaret.Skip)
   165 next
   166   case Assign show ?case by (auto intro:hoaret.Assign)
   167 next
   168   case Seq thus ?case by (auto intro:hoaret.Seq)
   169 next
   170   case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
   171 next
   172   case (While b c)
   173   let ?w = "WHILE b DO c"
   174   let ?T = "Its b c"
   175   have "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> wp\<^sub>t ?w Q s \<and> (\<exists>n. Its b c s n)"
   176     unfolding wpt_def by (metis WHILE_Its)
   177   moreover
   178   { fix n
   179     let ?R = "\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'<n. ?T s' n')"
   180     { fix s t assume "bval b s" and "?T s n" and "(?w, s) \<Rightarrow> t" and "Q t"
   181       from `bval b s` and `(?w, s) \<Rightarrow> t` obtain s' where
   182         "(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto
   183       from `(?w, s') \<Rightarrow> t` obtain n' where "?T s' n'"
   184         by (blast dest: WHILE_Its)
   185       with `bval b s` and `(c, s) \<Rightarrow> s'` have "?T s (Suc n')" by (rule Its_Suc)
   186       with `?T s n` have "n = Suc n'" by (rule Its_fun)
   187       with `(c,s) \<Rightarrow> s'` and `(?w,s') \<Rightarrow> t` and `Q t` and `?T s' n'`
   188       have "wp\<^sub>t c ?R s" by (auto simp: wpt_def)
   189     }
   190     hence "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow> wp\<^sub>t c ?R s"
   191       unfolding wpt_def by auto
   192       (* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *) 
   193     note strengthen_pre[OF this While.IH]
   194   } note hoaret.While[OF this]
   195   moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s"
   196     by (auto simp add:wpt_def)
   197   ultimately show ?case by (rule conseq)
   198 qed
   199 
   200 
   201 text{*\noindent In the @{term While}-case, @{const Its} provides the obvious
   202 termination argument.
   203 
   204 The actual completeness theorem follows directly, in the same manner
   205 as for partial correctness: *}
   206 
   207 theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
   208 apply(rule strengthen_pre[OF _ wpt_is_pre])
   209 apply(auto simp: hoare_tvalid_def wpt_def)
   210 done
   211 
   212 corollary hoaret_sound_complete: "\<turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> \<Turnstile>\<^sub>t {P}c{Q}"
   213 by (metis hoaret_sound hoaret_complete)
   214 
   215 end