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