src/HOL/IMP/HoareT.thy
 changeset 43158 686fa0a0696e child 44177 b4b5cbca2519
equal inserted replaced
43157:b505be6f029a 43158:686fa0a0696e

     1 header{* Hoare Logic for Total Correctness *}

     2

     3 theory HoareT imports Hoare_Sound_Complete Util 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{* Proveability 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 fastsimp

    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(induct "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 fastsimp+

    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(induct 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(induct "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 (induct 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