Theory HoareTotal

(*  Title:       Inductive definition of Hoare logic for total correctness
    Author:      Tobias Nipkow, 2001/2006
    Maintainer:  Tobias Nipkow
*)

theory HoareTotal imports Hoare Termi begin

subsection‹Hoare logic for total correctness›

text‹
Now that we have termination, we can define
total validity, ‹⊨⇩t›, as partial validity and guaranteed termination:›

definition
 hoare_tvalid :: "assn ⇒ com ⇒ assn ⇒ bool" (‹⊨⇩t {(1_)}/ (_)/ {(1_)}› 50) where
  "⊨⇩t {P}c{Q} ⟷ ⊨ {P}c{Q} ∧ (∀s. P s ⟶ c↓s)"

text‹Proveability of Hoare triples in the proof system for total
correctness is written ‹⊢⇩t {P}c{Q}› and defined
inductively. The rules for ‹⊢⇩t› differ from those for
‹⊢› only in the one place where nontermination can arise: the
@{term While}-rule.›

inductive
  thoare :: "assn ⇒ com ⇒ assn ⇒ bool" (‹⊢⇩t ({(1_)}/ (_)/ {(1_)})› 50)
where
  Do:  "⊢⇩t {λs. (∀t ∈ f s. P t) ∧ f s ≠ {}} Do f {P}"
| Semi: "⟦ ⊢⇩t {P}c{Q}; ⊢⇩t {Q}d{R} ⟧ ⟹ ⊢⇩t {P} c;d {R}"
| If: "⟦ ⊢⇩t {λs. P s ∧ b s}c{Q}; ⊢⇩t {λs. P s ∧ ~b s}d{Q}  ⟧ ⟹
      ⊢⇩t {P} IF b THEN c ELSE d {Q}"
| While:
  "⟦wf r;  ∀s'. ⊢⇩t {λs. P s ∧ b s ∧ s' = s} c {λs. P s ∧ (s,s') ∈ r}⟧
   ⟹ ⊢⇩t {P} WHILE b DO c {λs. P s ∧ ¬b s}"
| Conseq: "⟦ ∀s. P' s ⟶ P s; ⊢⇩t {P}c{Q}; ∀s. Q s ⟶ Q' s  ⟧ ⟹
           ⊢⇩t {P'}c{Q'}"

| Local: "(!!s. P s ⟹ P' s (f s)) ⟹ ∀p. ⊢⇩t {P' p} c {Q o (g p)} ⟹
        ⊢⇩t {P} LOCAL f;c;g {Q}"

text‹\noindent The@{term While}- rule is like the one for partial
correctness but it requires additionally that with every execution of
the loop body a wellfounded relation (@{prop"wf r"}) on the state
space decreases.

The soundness theorem›

(* Tried to use this lemma to simplify the soundness proof.
   But "⊢⇩t {P}c{Q} ⟹ (!s. P s ⟶ c↓s)" is not provable because too weak
lemma total_implies_partial: "⊢⇩t {P} c {Q} ⟹ ⊢ {P} c {Q}"
apply(erule thoare.induct)
      apply(rule hoare.intros)
        apply (clarify) apply assumption
      apply(rule hoare.intros)
      apply blast
     apply(blast intro:hoare.intros)
    apply(blast intro:hoare.intros)
   defer
   apply(blast intro:hoare.intros)
  apply(blast intro:hoare.intros)
apply(rule hoare.intros)
apply(rule hoare_relative_complete)
apply(unfold hoare_valid_def)
apply(clarify)
apply(erule allE, erule conjE)
apply(drule hoare_sound)
apply(unfold hoare_valid_def)
apply(blast)
done
*)

theorem "⊢⇩t {P}c{Q}  ⟹  ⊨⇩t {P}c{Q}"
apply(unfold hoare_tvalid_def hoare_valid_def)
apply(erule thoare.induct)
      apply blast
     apply blast
    apply clarsimp
   defer
   apply blast
 apply(rule conjI)
  apply clarify
  apply(erule allE)
  apply clarify
  apply(erule allE, erule allE, erule impE, erule asm_rl)
  apply simp
  apply(erule mp)
  apply(simp)
 apply blast
apply(rule conjI)
 apply(rule allI)
 apply(erule wf_induct)
 apply clarify
 apply(drule unfold_while[THEN iffD1])
 apply (simp split: if_split_asm)
 apply blast
apply(rule allI)
apply(erule wf_induct)
apply clarify
apply(case_tac "b x")
 apply (blast intro: termi.WhileTrue)
apply (erule termi.WhileFalse)
done
(*>*)

text‹\noindent In the @{term While}-case we perform a
local proof by wellfounded induction over the given relation @{term r}.

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. wp c Q s ∧ c↓s)"

lemmas wp_defs = wp_def wpt_def

lemma [simp]: "wp⇩t (Do f) Q = (λs. (∀t ∈ f s. Q t) ∧ f s ≠ {})"
by(simp add: wpt_def)

lemma [simp]: "wp⇩t (c⇩1;c⇩2) R = wp⇩t c⇩1 (wp⇩t c⇩2 R)"
apply(unfold wp_defs)
apply(rule ext)
apply blast
done

lemma [simp]:
 "wp⇩t (IF b THEN c⇩1 ELSE c⇩2) Q = (λs. wp⇩t (if b s then c⇩1 else c⇩2) Q s)"
apply(unfold wp_defs)
apply(rule ext)
apply auto
done

lemma [simp]: "wp⇩t (LOCAL f;c;g) Q = (λs. wp⇩t c (Q o (g s)) (f s))"
apply(unfold wp_defs)
apply(rule ext)
apply auto
done

lemma strengthen_pre: "⟦ ∀s. P' s ⟶ P s; ⊢⇩t {P}c{Q}  ⟧ ⟹ ⊢⇩t {P'}c{Q}"
by(erule thoare.Conseq, assumption, blast)

lemma weaken_post: "⟦ ⊢⇩t {P}c{Q}; ∀s. Q s ⟶ Q' s  ⟧ ⟹ ⊢⇩t {P}c{Q'}"
apply(rule thoare.Conseq)
apply(fast, assumption, assumption)
done

inductive_cases [elim!]: "WHILE b DO c ↓ s"

lemma wp_is_pre[rule_format]: "⊢⇩t {wp⇩t c Q} c {Q}"
apply (induct c arbitrary: Q)
     apply simp_all
     apply(blast intro:thoare.Do thoare.Conseq)
    apply(blast intro:thoare.Semi thoare.Conseq)
   apply(blast intro:thoare.If thoare.Conseq)
  defer
 apply(fastforce intro!: thoare.Local)
apply(rename_tac b c Q)
apply(rule weaken_post)
 apply(rule_tac b=b and c=c in thoare.While)
  apply(rule_tac b=b and c=c in wf_termi)
 defer
 apply (simp add:wp_defs unfold_while)
apply(rule allI)
apply(rule strengthen_pre)
 prefer 2
 apply fast
apply(clarsimp simp add: wp_defs)
apply(blast intro:exec.intros)
done

text‹\noindent The @{term While}-case is interesting because we now have to furnish a
suitable wellfounded relation. Of course the execution of the loop
body directly yields the required relation.
The actual completeness theorem follows directly, in the same manner
as for partial correctness.›

theorem "⊨⇩t {P}c{Q} ⟹ ⊢⇩t {P}c{Q}"
apply (rule strengthen_pre[OF _ wp_is_pre])
apply(unfold hoare_tvalid_def hoare_valid_def wp_defs)
apply blast
done

end