# Theory Hoare_Total_EX

theory Hoare_Total_EX
imports Hoare
```(* Author: Tobias Nipkow *)

theory Hoare_Total_EX
imports Hoare
begin

subsubsection "Hoare Logic for Total Correctness --- ‹nat›-Indexed Invariant"

text{* This is the standard set of rules that you find in many publications.
The While-rule is different from the one in Concrete Semantics in that the
invariant is indexed by natural numbers and goes down by 1 with
every iteration. The completeness proof is easier but the rule is harder
to apply in program proofs. *}

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))"

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 {P (Suc n)} c {P n};
∀n s. P (Suc n) s ⟶ bval b s;  ∀s. P 0 s ⟶ ¬ bval b s ⟧
⟹ ⊢⇩t {λs. ∃n. P n s} WHILE b DO c {P 0}"  |

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

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])

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 c b)
{
fix n s
have "⟦ P n s ⟧ ⟹ ∃t. (WHILE b DO c, s) ⇒ t ∧ P 0 t"
proof(induction "n" arbitrary: s)
case 0 thus ?case using While.hyps(3) WhileFalse by blast
next
case (Suc n)
thus ?case by (meson While.IH While.hyps(2) WhileTrue)
qed
}
thus ?case by auto
next
case If thus ?case by auto blast
qed fastforce+

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{* Function @{text wpw} computes the weakest precondition of a While-loop
that is unfolded a fixed number of times. *}

fun wpw :: "bexp ⇒ com ⇒ nat ⇒ assn ⇒ assn" where
"wpw b c 0 Q s = (¬ bval b s ∧ Q s)" |
"wpw b c (Suc n) Q s = (bval b s ∧ (∃s'. (c,s) ⇒ s' ∧  wpw b c n Q s'))"

lemma WHILE_Its: "(WHILE b DO c,s) ⇒ t ⟹ Q t ⟹ ∃n. wpw b c n Q s"
proof(induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case using wpw.simps(1) by blast
next
case WhileTrue thus ?case using wpw.simps(2) by blast
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"
have c1: "∀s. wp⇩t ?w Q s ⟶ (∃n. wpw b c n Q s)"
unfolding wpt_def by (metis WHILE_Its)
have c3: "∀s. wpw b c 0 Q s ⟶ Q s" by simp
have w2: "∀n s. wpw b c (Suc n) Q s ⟶ bval b s" by simp
have w3: "∀s. wpw b c 0 Q s ⟶ ¬ bval b s" by simp
{ fix n
have 1: "∀s. wpw b c (Suc n) Q s ⟶ (∃t. (c, s) ⇒ t ∧ wpw b c n Q t)"
by simp
note strengthen_pre[OF 1 While.IH[of "wpw b c n Q", unfolded wpt_def]]
}
from conseq[OF c1 hoaret.While[OF this w2 w3] c3]
show ?case .
qed

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
```