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