Quelle  Hoare_Total.thy

(* Author: Tobias Nipkow *)

subsection "Hoare Logic for Total Correctness"

subsubsection "Separate Termination Relation"

theory Hoare_Total
imports Hoare_Examples
begin

text‹Note that this definition of total validity ‹⊨_t› only
  if execution is deterministic (which it is in our case).›

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

text‹Provability of Hoare triples in the proof system for total
  is written ‹⊨_t {P}c{Q}› and defined
 . The rules for ‹⊨_t› differ from those for
 ‹⊨› only in the one place where nontermination can arise: the
 term‹While›-rule.›

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₁} c₁ {P₂}; ⊨_t {P₂} c₂ {P₃} ] ==> ⊨_t {P₁} c₁;;c₂ {P₃}"  |

If: "[ ⊨_t {λs. P s ∧ bval b s} c₁ {Q}; ⊨_t {λs. P s ∧ ¬ bval b s} c₂ {Q} ]
  ==> ⊨_t {P} IF b THEN c₁ ELSE c₂ {Q}"  |

While:
  "(∧n::nat.
    ⊨_t {λs. P s ∧ bval b s ∧ T s n} c {λs. P s ∧ (∃n'<n. T s n')})
   ==> ⊨_t {λs. P s ∧ (∃n. T s n)} WHILE b DO c {λs. P s ∧ ¬bval b s}"  |

conseq: "[ ∀s. P' s ⟶ P s; ⊨_t {P}c{Q}; ∀s. Q s ⟶ Q' s ] ==>
           ⊨_t {P'}c{Q'}"

text‹The term‹While›-rule is like the one for partial correctness but it
  additionally that with every execution of the loop body some measure
  @{term[source]"T :: state ==> nat ==> bool"} decreases.
  following functional version is more intuitive:›

lemma While_fun:
  "[ ∧n::nat. ⊨_t {λs. P s ∧ bval b s ∧ n = f s} c {λs. P s ∧ f s < n}]
   ==> ⊨_t {P} WHILE b DO c {λs. P s ∧ ¬bval b s}"
  by (rule While [where T="λs n. n = f s", simplified])

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

lemma While_fun':
assumes "∧n::nat. ⊨_t {λs. P s ∧ bval b s ∧ n = f s} c {λs. P s ∧ f s < n}"
    and "∀s. P s ∧ ¬ bval b s ⟶ Q s"
shows "⊨_t {P} WHILE b DO c {Q}"
by(blast intro: assms(1) weaken_post[OF While_fun assms(2)])


text‹Our standard example:›

lemma "⊨_t {λs. s ''x'' = i} ''y'' ::= N 0;; wsum {λs. s ''y'' = sum i}"
apply(rule Seq)
 prefer 2
 apply(rule While_fun' [where P = "λs. (s ''y'' = sum i - sum(s ''x''))"
    and f = "λs. nat(s ''x'')"])
   apply(rule Seq)
   prefer 2
   apply(rule Assign)
  apply(rule Assign')
  apply simp
 apply(simp)
apply(rule Assign')
apply simp
done

text ‹Nested loops. This poses a problem for VCGs because the proof of the inner loop needs to
  to outer loops. This works here because the invariant is not written down statically but
  in the context of a proof that has already introduced/fixed outer ‹n›s that can be
  to.›

lemma
 "⊨_t {λ_. True}
  WHILE Less (N 0) (V ''x'')
  DO (''x'' ::= Plus (V ''x'') (N(-1));;
      ''y'' ::= V ''x'';;
      WHILE Less (N 0) (V ''y'') DO ''y'' ::= Plus (V ''y'') (N(-1)))
  {λ_. True}"
apply(rule While_fun'[where f = "λs. nat(s ''x'')"])
 prefer 2 apply simp
apply(rule_tac P₂ = "λs. nat(s ''x'') < n" in Seq)
 apply(rule_tac P₂ = "λs. nat(s ''x'') < n" in Seq)
  apply(rule Assign')
  apply simp
 apply(rule Assign')
 apply simp
(* note that the invariant refers to the outer \<open>n\<close>: *)
apply(rule While_fun'[where f = "λs. nat(s ''y'')"])
 prefer 2 apply simp
apply(rule Assign')
apply simp
done

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 b T c)
  have "[ P s; T s n ] ==> ∃t. (WHILE b DO c, s) ==> t ∧ P t ∧ ¬ bval b t" for s n
  proof(induction "n" arbitrary: s rule: less_induct)
    case (less n) thus ?case by (metis While.IH WhileFalse WhileTrue)
  qed
  thus ?case by auto
next
  case If thus ?case by auto blast
qed fastforce+


text‹
  completeness proof proceeds along the same lines as the one for partial
 . First we have to strengthen our notion of weakest precondition
  take termination into account:›

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₁;;c₂) Q = wp_t c₁ (wp_t c₂ Q)"
unfolding wpt_def
apply(rule ext)
apply auto
done

lemma [simp]:
 "wp_t (IF b THEN c₁ ELSE c₂) Q = (λs. wp_t (if bval b s then c₁ else c₂) Q s)"
apply(unfold wpt_def)
apply(rule ext)
apply auto
done


text‹Now we define the number of iterations term‹WHILE b DO c› needs to
  when started in state ‹s›. Because this is a truly partial
 , we define it as an (inductive) relation first:›

inductive Its :: "bexp ==> com ==> state ==> nat ==> bool" where
Its_0: "¬ bval b s ==> Its b c s 0" |
Its_Suc: "[ bval b s; (c,s) ==> s'; Its b c s' n ] ==> Its b c s (Suc n)"

text‹The relation is in fact a function:›

lemma Its_fun: "Its b c s n ==> Its b c s n' ==> n=n'"
proof(induction arbitrary: n' rule:Its.induct)
  case Its_0 thus ?case by(metis Its.cases)
next
  case Its_Suc thus ?case by(metis Its.cases big_step_determ)
qed

text‹For all terminating loops, const‹Its› yields a result:›

lemma WHILE_Its: "(WHILE b DO c,s) ==> t ==> ∃n. Its b c s n"
proof(induction "WHILE b DO c" s t rule: big_step_induct)
  case WhileFalse thus ?case by (metis Its_0)
next
  case WhileTrue thus ?case by (metis Its_Suc)
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"
  let ?T = "Its b c"
  have 1: "∀s. wp_t ?w Q s ⟶ wp_t ?w Q s ∧ (∃n. Its b c s n)"
    unfolding wpt_def by (metis WHILE_Its)
  let ?R = "λn s'. wp_t ?w Q s' ∧ (∃n'<n. ?T s' n')"
  have "∀s. wp_t ?w Q s ∧ bval b s ∧ ?T s n ⟶ wp_t c (?R n) s" for n
  proof -
    have "wp_t c (?R n) s" if "bval b s" and "?T s n" and "(?w, s) ==> t" and "Q t" for s t
    proof -
      from ‹bval b s› and ‹(?w, s) ==> t› obtain s' where
        "(c,s) ==> s'" "(?w,s') ==> t" by auto
      from ‹(?w, s') ==> t› obtain n' where "?T s' n'"
        by (blast dest: WHILE_Its)
      with ‹bval b s› and ‹(c, s) ==> s'› have "?T s (Suc n')" by (rule Its_Suc)
      with ‹?T s n› have "n = Suc n'" by (rule Its_fun)
      with ‹(c,s) ==> s'› and ‹(?w,s') ==> t› and ‹Q t› and ‹?T s' n'›
      show ?thesis by (auto simp: wpt_def)
    qed
    thus ?thesis
      unfolding wpt_def by auto
      (* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *) 
  qed
  note 2 = hoaret.While[OF strengthen_pre[OF this While.IH]]
  have "∀s. wp_t ?w Q s ∧ ¬ bval b s ⟶ Q s"
    by (auto simp add:wpt_def)
  with 1 2 show ?case by (rule conseq)
qed


text‹\noindent In the term‹While›-case, const‹Its› provides the obvious
  argument.

  actual completeness theorem follows directly, in the same manner
  for partial correctness:›

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