# Theory Hoare_Total

theory Hoare_Total
imports Hoare_Examples
(* Author: Tobias Nipkow *)

subsection "Hoare Logic for Total Correctness"

theory Hoare_Total
imports Hoare_Examples
begin

subsubsection "Hoare Logic for Total Correctness --- Separate Termination Relation"

text‹Note that this definition of total validity @{text"⊨⇩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 @{text"⊢⇩t {P}c{Q}"} and defined
inductively. The rules for @{text"⊢⇩t"} differ from those for
@{text"⊢"} 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⇩1} c⇩1 {P⇩2}; ⊢⇩t {P⇩2} c⇩2 {P⇩3} ⟧ ⟹ ⊢⇩t {P⇩1} c⇩1;;c⇩2 {P⇩3}"  |

If: "⟦ ⊢⇩t {λs. P s ∧ bval b s} c⇩1 {Q}; ⊢⇩t {λs. P s ∧ ¬ bval b s} c⇩2 {Q} ⟧
⟹ ⊢⇩t {P} IF b THEN c⇩1 ELSE c⇩2 {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‹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⇩1;;c⇩2) Q = wp⇩t c⇩1 (wp⇩t c⇩2 Q)"
unfolding wpt_def
apply(rule ext)
apply auto
done

lemma [simp]:
"wp⇩t (IF b THEN c⇩1 ELSE c⇩2) Q = (λs. wp⇩t (if bval b s then c⇩1 else c⇩2) 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 @{text 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"
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