Theory Hoare_Total_EX

(* 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