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