Theory Hoare_Total

(* Author: Tobias Nipkow *)

subsection "Hoare Logic for Total Correctness"

subsubsection "Separate Termination Relation"

theory Hoare_Total
imports Hoare_Examples
begin

text‹Note that this definition of total validity ‹⊨⇩_t› only
works if execution is deterministic (which it is in our case).›

definition hoare_tvalid :: "assn ⇒ com ⇒ assn ⇒ bool"
  ("⊨⇩_t {(1_)}/ (_)/ {(1_)}" 50) where
"⊨⇩_t {P}c{Q}  ⟷  (∀s. P s ⟶ (∃t. (c,s) ⇒ t ∧ Q t))"

text‹Provability of Hoare triples in the proof system for total
correctness is written ‹⊢⇩_t {P}c{Q}› and defined
inductively. The rules for ‹⊢⇩_t› differ from those for
‹⊢› only in the one place where nontermination can arise: the
\<^term>‹While›-rule.›

inductive
  hoaret :: "assn ⇒ com ⇒ assn ⇒ bool" ("⊢⇩_t ({(1_)}/ (_)/ {(1_)})" 50)
where

Skip:  "⊢⇩_t {P} SKIP {P}"  |

Assign:  "⊢⇩_t {λs. P(s[a/x])} x::=a {P}"  |

Seq: "⟦ ⊢⇩_t {P⇩₁} c⇩₁ {P⇩₂}; ⊢⇩_t {P⇩₂} c⇩₂ {P⇩₃} ⟧ ⟹ ⊢⇩_t {P⇩₁} c⇩₁;;c⇩₂ {P⇩₃}"  |

If: "⟦ ⊢⇩_t {λs. P s ∧ bval b s} c⇩₁ {Q}; ⊢⇩_t {λs. P s ∧ ¬ bval b s} c⇩₂ {Q} ⟧
  ⟹ ⊢⇩_t {P} IF b THEN c⇩₁ ELSE c⇩₂ {Q}"  |

While:
  "(⋀n::nat.
    ⊢⇩_t {λs. P s ∧ bval b s ∧ T s n} c {λs. P s ∧ (∃n'<n. T s n')})
   ⟹ ⊢⇩_t {λs. P s ∧ (∃n. T s n)} WHILE b DO c {λs. P s ∧ ¬bval b s}"  |

conseq: "⟦ ∀s. P' s ⟶ P s; ⊢⇩_t {P}c{Q}; ∀s. Q s ⟶ Q' s  ⟧ ⟹
           ⊢⇩_t {P'}c{Q'}"

text‹The \<^term>‹While›-rule is like the one for partial correctness but it
requires additionally that with every execution of the loop body some measure
relation @{term[source]"T :: state ⇒ nat ⇒ bool"} decreases.
The following functional version is more intuitive:›

lemma While_fun:
  "⟦ ⋀n::nat. ⊢⇩_t {λs. P s ∧ bval b s ∧ n = f s} c {λs. P s ∧ f s < n}⟧
   ⟹ ⊢⇩_t {P} WHILE b DO c {λs. P s ∧ ¬bval b s}"
  by (rule While [where T="λs n. n = f s", simplified])

text‹Building in the consequence rule:›

lemma strengthen_pre:
  "⟦ ∀s. P' s ⟶ P s;  ⊢⇩_t {P} c {Q} ⟧ ⟹ ⊢⇩_t {P'} c {Q}"
by (metis conseq)

lemma weaken_post:
  "⟦ ⊢⇩_t {P} c {Q};  ∀s. Q s ⟶ Q' s ⟧ ⟹  ⊢⇩_t {P} c {Q'}"
by (metis conseq)

lemma Assign': "∀s. P s ⟶ Q(s[a/x]) ⟹ ⊢⇩_t {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])

lemma While_fun':
assumes "⋀n::nat. ⊢⇩_t {λs. P s ∧ bval b s ∧ n = f s} c {λs. P s ∧ f s < n}"
    and "∀s. P s ∧ ¬ bval b s ⟶ Q s"
shows "⊢⇩_t {P} WHILE b DO c {Q}"
by(blast intro: assms(1) weaken_post[OF While_fun assms(2)])


text‹Our standard example:›

lemma "⊢⇩_t {λs. s ''x'' = i} ''y'' ::= N 0;; wsum {λs. s ''y'' = sum i}"
apply(rule Seq)
 prefer 2
 apply(rule While_fun' [where P = "λs. (s ''y'' = sum i - sum(s ''x''))"
    and f = "λs. nat(s ''x'')"])
   apply(rule Seq)
   prefer 2
   apply(rule Assign)
  apply(rule Assign')
  apply simp
 apply(simp)
apply(rule Assign')
apply simp
done

text ‹Nested loops. This poses a problem for VCGs because the proof of the inner loop needs to
refer to outer loops. This works here because the invariant is not written down statically but
created in the context of a proof that has already introduced/fixed outer ‹n›s that can be
referred to.›

lemma
 "⊢⇩_t {λ_. True}
  WHILE Less (N 0) (V ''x'')
  DO (''x'' ::= Plus (V ''x'') (N(-1));;
      ''y'' ::= V ''x'';;
      WHILE Less (N 0) (V ''y'') DO ''y'' ::= Plus (V ''y'') (N(-1)))
  {λ_. True}"
apply(rule While_fun'[where f = "λs. nat(s ''x'')"])
 prefer 2 apply simp
apply(rule_tac P⇩₂ = "λs. nat(s ''x'') < n" in Seq)
 apply(rule_tac P⇩₂ = "λs. nat(s ''x'') < n" in Seq)
  apply(rule Assign')
  apply simp
 apply(rule Assign')
 apply simp
(* note that the invariant refers to the outer ‹n›: *)
apply(rule While_fun'[where f = "λs. nat(s ''y'')"])
 prefer 2 apply simp
apply(rule Assign')
apply simp
done

text‹The soundness theorem:›

theorem hoaret_sound: "⊢⇩_t {P}c{Q}  ⟹  ⊨⇩_t {P}c{Q}"
proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
  case (While P b T c)
  have "⟦ P s; T s n ⟧ ⟹ ∃t. (WHILE b DO c, s) ⇒ t ∧ P t ∧ ¬ bval b t" for s n
  proof(induction "n" arbitrary: s rule: less_induct)
    case (less n) thus ?case by (metis While.IH WhileFalse WhileTrue)
  qed
  thus ?case by auto
next
  case If thus ?case by auto blast
qed fastforce+


text‹
The completeness proof proceeds along the same lines as the one for partial
correctness. First we have to strengthen our notion of weakest precondition
to take termination into account:›

definition wpt :: "com ⇒ assn ⇒ assn" ("wp⇩_t") where
"wp⇩_t c Q  =  (λs. ∃t. (c,s) ⇒ t ∧ Q t)"

lemma [simp]: "wp⇩_t SKIP Q = Q"
by(auto intro!: ext simp: wpt_def)

lemma [simp]: "wp⇩_t (x ::= e) Q = (λs. Q(s(x := aval e s)))"
by(auto intro!: ext simp: wpt_def)

lemma [simp]: "wp⇩_t (c⇩₁;;c⇩₂) Q = wp⇩_t c⇩₁ (wp⇩_t c⇩₂ Q)"
unfolding wpt_def
apply(rule ext)
apply auto
done

lemma [simp]:
 "wp⇩_t (IF b THEN c⇩₁ ELSE c⇩₂) Q = (λs. wp⇩_t (if bval b s then c⇩₁ else c⇩₂) Q s)"
apply(unfold wpt_def)
apply(rule ext)
apply auto
done


text‹Now we define the number of iterations \<^term>‹WHILE b DO c› needs to
terminate when started in state ‹s›. Because this is a truly partial
function, we define it as an (inductive) relation first:›

inductive Its :: "bexp ⇒ com ⇒ state ⇒ nat ⇒ bool" where
Its_0: "¬ bval b s ⟹ Its b c s 0" |
Its_Suc: "⟦ bval b s;  (c,s) ⇒ s';  Its b c s' n ⟧ ⟹ Its b c s (Suc n)"

text‹The relation is in fact a function:›

lemma Its_fun: "Its b c s n ⟹ Its b c s n' ⟹ n=n'"
proof(induction arbitrary: n' rule:Its.induct)
  case Its_0 thus ?case by(metis Its.cases)
next
  case Its_Suc thus ?case by(metis Its.cases big_step_determ)
qed

text‹For all terminating loops, \<^const>‹Its› yields a result:›

lemma WHILE_Its: "(WHILE b DO c,s) ⇒ t ⟹ ∃n. Its b c s n"
proof(induction "WHILE b DO c" s t rule: big_step_induct)
  case WhileFalse thus ?case by (metis Its_0)
next
  case WhileTrue thus ?case by (metis Its_Suc)
qed

lemma wpt_is_pre: "⊢⇩_t {wp⇩_t c Q} c {Q}"
proof (induction c arbitrary: Q)
  case SKIP show ?case by (auto intro:hoaret.Skip)
next
  case Assign show ?case by (auto intro:hoaret.Assign)
next
  case Seq thus ?case by (auto intro:hoaret.Seq)
next
  case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
next
  case (While b c)
  let ?w = "WHILE b DO c"
  let ?T = "Its b c"
  have 1: "∀s. wp⇩_t ?w Q s ⟶ wp⇩_t ?w Q s ∧ (∃n. Its b c s n)"
    unfolding wpt_def by (metis WHILE_Its)
  let ?R = "λn s'. wp⇩_t ?w Q s' ∧ (∃n'<n. ?T s' n')"
  have "∀s. wp⇩_t ?w Q s ∧ bval b s ∧ ?T s n ⟶ wp⇩_t c (?R n) s" for n
  proof -
    have "wp⇩_t c (?R n) s" if "bval b s" and "?T s n" and "(?w, s) ⇒ t" and "Q t" for s t
    proof -
      from ‹bval b s› and ‹(?w, s) ⇒ t› obtain s' where
        "(c,s) ⇒ s'" "(?w,s') ⇒ t" by auto
      from ‹(?w, s') ⇒ t› obtain n' where "?T s' n'"
        by (blast dest: WHILE_Its)
      with ‹bval b s› and ‹(c, s) ⇒ s'› have "?T s (Suc n')" by (rule Its_Suc)
      with ‹?T s n› have "n = Suc n'" by (rule Its_fun)
      with ‹(c,s) ⇒ s'› and ‹(?w,s') ⇒ t› and ‹Q t› and ‹?T s' n'›
      show ?thesis by (auto simp: wpt_def)
    qed
    thus ?thesis
      unfolding wpt_def by auto
      (* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *) 
  qed
  note 2 = hoaret.While[OF strengthen_pre[OF this While.IH]]
  have "∀s. wp⇩_t ?w Q s ∧ ¬ bval b s ⟶ Q s"
    by (auto simp add:wpt_def)
  with 1 2 show ?case by (rule conseq)
qed


text‹\noindent In the \<^term>‹While›-case, \<^const>‹Its› provides the obvious
termination argument.

The actual completeness theorem follows directly, in the same manner
as for partial correctness:›

theorem hoaret_complete: "⊨⇩_t {P}c{Q} ⟹ ⊢⇩_t {P}c{Q}"
apply(rule strengthen_pre[OF _ wpt_is_pre])
apply(auto simp: hoare_tvalid_def wpt_def)
done

corollary hoaret_sound_complete: "⊢⇩_t {P}c{Q} ⟷ ⊨⇩_t {P}c{Q}"
by (metis hoaret_sound hoaret_complete)

end