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 {P1} c1 {P2}; ⊢t {P2} c2 {P3} ⟧ ⟹ ⊢t {P1} c1;;c2 {P3}"  |

If: "⟦ ⊢t {λs. P s ∧ bval b s} c1 {Q}; ⊢t {λs. P s ∧ ¬ bval b s} c2 {Q} ⟧
  ⟹ ⊢t {P} IF b THEN c1 ELSE c2 {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)
  have "P n s ⟹ ∃t. (WHILE b DO c, s) ⇒ t ∧ P 0 t" for n s
  proof(induction "n" arbitrary: s)
    case 0 thus ?case using While.hyps(3) WhileFalse by blast
  next
    case Suc
    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" ("wpt") where
"wpt c Q  =  (λs. ∃t. (c,s) ⇒ t ∧ Q t)"

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

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

lemma [simp]: "wpt (c1;;c2) Q = wpt c1 (wpt c2 Q)"
unfolding wpt_def
apply(rule ext)
apply auto
done

lemma [simp]:
 "wpt (IF b THEN c1 ELSE c2) Q = (λs. wpt (if bval b s then c1 else c2) 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 {wpt 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. wpt ?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
  have "⊢t {wpw b c (Suc n) Q} c {wpw b c n Q}" for n
  proof -
    have *: "∀s. wpw b c (Suc n) Q s ⟶ (∃t. (c, s) ⇒ t ∧ wpw b c n Q t)" by simp
    show ?thesis by(rule strengthen_pre[OF * While.IH[of "wpw b c n Q", unfolded wpt_def]])
  qed
  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