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