Theory HoareTotalDef

(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer
*)

section ‹Hoare Logic for Total Correctness›

theory HoareTotalDef imports HoarePartialDef Termination begin

subsection ‹Validity of Hoare Tuples: ‹Γ⊨⇩t⇘/F⇙ P c Q,A››

definition
  validt :: "[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com,'s assn,'s assn] ⇒ bool"
                (‹_⊨⇩t⇘'/_⇙/ _ _ _,_›  [61,60,1000, 20, 1000,1000] 60)
where
 "Γ⊨⇩t⇘/F⇙ P c Q,A ≡ Γ⊨⇘/F⇙ P c Q,A ∧ (∀s ∈ Normal ` P. Γ⊢c↓s)"

definition
  cvalidt::
  "[('s,'p,'f) body,('s,'p) quadruple set,'f set,
    's assn,('s,'p,'f) com,'s assn,'s assn] ⇒ bool"
                (‹_,_⊨⇩t⇘'/_⇙/ _ _ _,_›  [61,60, 60,1000, 20, 1000,1000] 60)
where
 "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A ≡ (∀(P,p,Q,A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A) ⟶ Γ ⊨⇩t⇘/F⇙ P c Q,A"



notation (ASCII)
  validt  (‹_|=t'/_/ _ _ _,_›  [61,60,1000, 20, 1000,1000] 60) and
  cvalidt  (‹_,_|=t'/_ / _ _ _,_›  [61,60,60,1000, 20, 1000,1000] 60)

subsection ‹Properties of Validity›

lemma validtI:
 "⟦⋀s t. ⟦Γ⊢⟨c,Normal s⟩ ⇒ t;s ∈ P;t ∉ Fault ` F⟧ ⟹ t ∈ Normal ` Q ∪ Abrupt ` A;
   ⋀s. s ∈ P ⟹ Γ⊢ c↓(Normal s) ⟧
  ⟹ Γ⊨⇩t⇘/F⇙ P c Q,A"
  by (auto simp add: validt_def valid_def)

lemma cvalidtI:
 "⟦⋀s t. ⟦∀(P,p,Q,A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A;Γ⊢⟨c,Normal s⟩ ⇒ t;s ∈ P;
          t ∉ Fault ` F⟧
          ⟹ t ∈ Normal ` Q ∪ Abrupt ` A;
   ⋀s. ⟦∀(P,p,Q,A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A; s∈P⟧ ⟹  Γ⊢c↓(Normal s)⟧
  ⟹ Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
  by (auto simp add: cvalidt_def validt_def valid_def)

lemma cvalidt_postD:
 "⟦Γ,Θ⊨⇩t⇘/F⇙ P c Q,A; ∀(P,p,Q,A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A;Γ⊢⟨c,Normal s ⟩ ⇒ t;
   s ∈ P;t ∉ Fault ` F⟧
  ⟹ t ∈ Normal ` Q ∪ Abrupt ` A"
  by (simp add: cvalidt_def validt_def valid_def)

lemma cvalidt_termD:
 "⟦Γ,Θ⊨⇩t⇘/F⇙ P c Q,A; ∀(P,p,Q,A)∈Θ. Γ⊨⇩t⇘/F⇙ P (Call p) Q,A;s ∈ P⟧
  ⟹ Γ⊢c↓(Normal s)"
  by (simp add: cvalidt_def validt_def valid_def)


lemma validt_augment_Faults:
  assumes valid:"Γ⊨⇩t⇘/F⇙ P c Q,A"
  assumes F': "F ⊆ F'"
  shows "Γ⊨⇩t⇘/F'⇙ P c Q,A"
  using valid F'
  by (auto intro: valid_augment_Faults simp add: validt_def)

subsection ‹The Hoare Rules: ‹Γ,Θ⊢⇩t⇘/F⇙ P c Q,A››

inductive "hoaret"::"[('s,'p,'f) body,('s,'p) quadruple set,'f set,
                        's assn,('s,'p,'f) com,'s assn,'s assn]
                       => bool"
    (‹(3_,_/⊢⇩t⇘'/_⇙ (_/ (_)/ _,_))› [61,60,60,1000,20,1000,1000]60)
   for Γ::"('s,'p,'f) body"
where
  Skip: "Γ,Θ⊢⇩t⇘/F⇙ Q Skip Q,A"

| Basic: "Γ,Θ⊢⇩t⇘/F⇙ {s. f s ∈ Q} (Basic f) Q,A"

| Spec: "Γ,Θ⊢⇩t⇘/F⇙ {s. (∀t. (s,t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s,t) ∈ r)} (Spec r) Q,A"

| Seq: "⟦Γ,Θ⊢⇩t⇘/F⇙ P c⇩1 R,A; Γ,Θ⊢⇩t⇘/F⇙ R c⇩2 Q,A⟧
        ⟹
        Γ,Θ⊢⇩t⇘/F⇙ P Seq c⇩1 c⇩2 Q,A"

| Cond: "⟦Γ,Θ⊢⇩t⇘/F⇙ (P ∩ b) c⇩1 Q,A; Γ,Θ⊢⇩t⇘/F⇙ (P ∩ - b) c⇩2 Q,A⟧
         ⟹
         Γ,Θ⊢⇩t⇘/F⇙ P (Cond b c⇩1 c⇩2) Q,A"

| While: "⟦wf r; ∀σ. Γ,Θ⊢⇩t⇘/F⇙ ({σ} ∩ P ∩ b) c ({t. (t,σ)∈r} ∩ P),A⟧
          ⟹
          Γ,Θ⊢⇩t⇘/F⇙ P (While b c) (P ∩ - b),A"

| Guard: "Γ,Θ⊢⇩t⇘/F⇙ (g ∩ P) c Q,A
          ⟹
          Γ,Θ⊢⇩t⇘/F⇙ (g ∩ P) Guard f g c Q,A"

| Guarantee: "⟦f ∈ F; Γ,Θ⊢⇩t⇘/F⇙ (g ∩ P) c Q,A⟧
              ⟹
              Γ,Θ⊢⇩t⇘/F⇙ P (Guard f g c) Q,A"

| CallRec:
  "⟦(P,p,Q,A) ∈ Specs;
    wf r;
    Specs_wf = (λp σ. (λ(P,q,Q,A). (P ∩ {s. ((s,q),(σ,p)) ∈ r},q,Q,A)) ` Specs);
    ∀(P,p,Q,A)∈ Specs.
      p ∈ dom Γ ∧ (∀σ. Γ,Θ ∪ Specs_wf p σ⊢⇩t⇘/F⇙ ({σ} ∩ P) (the (Γ p)) Q,A)
    ⟧
    ⟹
    Γ,Θ⊢⇩t⇘/F⇙ P (Call p) Q,A"


| DynCom:  "∀s ∈ P. Γ,Θ⊢⇩t⇘/F⇙ P (c s) Q,A
            ⟹
            Γ,Θ⊢⇩t⇘/F⇙ P (DynCom c) Q,A"


| Throw: "Γ,Θ⊢⇩t⇘/F⇙ A Throw Q,A"

| Catch: "⟦Γ,Θ⊢⇩t⇘/F⇙ P c⇩1 Q,R; Γ,Θ⊢⇩t⇘/F⇙ R c⇩2 Q,A⟧ ⟹  Γ,Θ⊢⇩t⇘/F⇙ P Catch c⇩1 c⇩2 Q,A"

| Conseq: "∀s ∈ P. ∃P' Q' A'. Γ,Θ⊢⇩t⇘/F⇙ P' c Q',A' ∧ s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A
           ⟹ Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"


| Asm: "(P,p,Q,A) ∈ Θ
        ⟹
        Γ,Θ⊢⇩t⇘/F⇙ P (Call p) Q,A"

| ExFalso: "⟦Γ,Θ⊨⇩t⇘/F⇙ P c Q,A; ¬ Γ⊨⇩t⇘/F⇙ P c Q,A⟧ ⟹ Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
  ― ‹This is a hack rule that enables us to derive completeness for
        an arbitrary context ‹Θ›, from completeness for an empty context.›


text ‹Does not work, because of rule ExFalso, the context ‹Θ› is to blame.
 A weaker version with empty context can be derived from soundness
 later on.›
lemma hoaret_to_hoarep:
  assumes hoaret: "Γ,Θ⊢⇩t⇘/F⇙ P p Q,A"
  shows "Γ,Θ⊢⇘/F⇙ P p Q,A"
using hoaret
proof (induct)
  case Skip thus ?case by (rule hoarep.intros)
next
  case Basic thus ?case by (rule hoarep.intros)
next
  case Seq thus ?case by - (rule hoarep.intros)
next
  case Cond thus ?case by - (rule hoarep.intros)
next
  case (While r Θ F P b c A)
  hence "∀σ. Γ,Θ⊢⇘/F⇙ ({σ} ∩ P ∩ b) c ({t. (t, σ) ∈ r} ∩ P),A"
    by iprover
  hence "Γ,Θ⊢⇘/F⇙ (P ∩ b) c P,A"
    by (rule HoarePartialDef.conseq) blast
  then show "Γ,Θ⊢⇘/F⇙ P While b c (P ∩ - b),A"
    by (rule hoarep.While)
next
  case Guard thus ?case by - (rule hoarep.intros)
(*next
  case (CallRec A F P Procs Q Z Θ  p r)
  hence hyp: "∀p∈Procs. ∀τ Z.
           Γ,Θ ∪ (⋃q∈Procs. ⋃Z. {(P q Z ∩ {s. ((s, q), τ, p) ∈ r},
                      Call q, Q q Z,A q Z)})⊢⇘/F⇙
              ({τ} ∩ P p Z) (the (Γ p)) (Q p Z),(A p Z)"
    by blast
  have "∀p∈Procs. ∀Z.
           Γ,Θ ∪ (⋃q∈Procs. ⋃Z. {(P q Z,
                      Call q, Q q Z,A q Z)})⊢⇘/F⇙
              (P p Z) (the (Γ p)) (Q p Z),(A p Z)"
  proof (intro ballI allI)
    fix p Z
    assume "p ∈ Procs"
    with hyp
    have hyp': "⋀ τ.
           Γ,Θ ∪ (⋃q∈Procs. ⋃Z. {(P q Z ∩ {s. ((s, q), τ, p) ∈ r},
                      Call q, Q q Z, A q Z)})⊢⇘/F⇙
              ({τ} ∩ P p Z) (the (Γ p)) (Q p Z),(A p Z)"
      by blast
    have "∀τ.
           Γ,Θ ∪ (⋃q∈Procs. ⋃Z. {(P q Z,
                      Call q, Q q Z,A q Z)})⊢⇘/F⇙
              ({τ} ∩ P p Z) (the (Γ p)) (Q p Z),(A p Z)"
      (is "∀τ. Γ,?Θ'⊢⇘/F⇙ ({τ} ∩ P p Z) (the (Γ p)) (Q p Z),(A p Z)")
    proof (rule allI, rule WeakenContext [OF hyp'],clarify)
      fix τ P' c Q' A'
      assume "(P', c, Q', A') ∈ Θ ∪
         (⋃q∈Procs.
             ⋃Z. {(P q Z ∩ {s. ((s, q), τ, p) ∈ r},
                  Call q, Q q Z,
                  A q Z)})" (is "(P', c, Q', A') ∈ Θ ∪ ?Spec")
      then show "Γ,?Θ'⊢⇘/F⇙ P' c Q',A'"
      proof (cases rule: UnE [consumes 1])
        assume "(P',c,Q',A') ∈ Θ"
        then show ?thesis
          by (blast intro: HoarePartialDef.Asm)
      next
        assume "(P',c,Q',A') ∈ ?Spec"
        then show ?thesis
        proof (clarify)
          fix q Z
          assume q: "q ∈ Procs"
          show "Γ,?Θ'⊢⇘/F⇙ (P q Z ∩ {s. ((s, q), τ, p) ∈ r})
                         Call  q
                        (Q q Z),(A q Z)"
          proof -
            from q
            have "Γ,?Θ'⊢⇘/F⇙ (P q Z) Call q (Q q Z),(A q Z)"
              by - (rule HoarePartialDef.Asm,blast)
            thus ?thesis
              by (rule HoarePartialDef.conseqPre) blast
          qed
        qed
      qed
    qed
    then show "Γ,Θ ∪ (⋃q∈Procs. ⋃Z. {(P q Z, Call q, Q q Z,A q Z)})
                ⊢⇘/F⇙ (P p Z) (the (Γ p)) (Q p Z),(A p Z)"
      by (rule HoarePartialDef.conseq) blast
  qed
  thus ?case
    by - (rule hoarep.CallRec)*)
next
  case DynCom thus ?case by (blast intro: hoarep.DynCom)
next
  case Throw thus ?case by - (rule hoarep.Throw)
next
  case Catch thus ?case by - (rule hoarep.Catch)
next
  case Conseq thus ?case by - (rule hoarep.Conseq,blast)
next
  case Asm thus ?case by (rule HoarePartialDef.Asm)
next
  case (ExFalso Θ F P c Q A)
  assume "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A"
  hence "Γ,Θ⊨⇘/F⇙ P c Q,A"
    oops


lemma hoaret_augment_context:
  assumes deriv: "Γ,Θ⊢⇩t⇘/F⇙ P p Q,A"
  shows "⋀Θ'. Θ ⊆ Θ' ⟹ Γ,Θ'⊢⇩t⇘/F⇙ P p Q,A"
using deriv
proof (induct)
  case (CallRec P p Q A Specs r Specs_wf Θ F Θ')
  have aug: "Θ ⊆ Θ'" by fact
  then
  have h: "⋀τ p. Θ ∪ Specs_wf p τ
       ⊆ Θ' ∪ Specs_wf p τ"
    by blast
  have "∀(P,p,Q,A)∈Specs. p ∈ dom Γ ∧
     (∀τ. Γ,Θ ∪ Specs_wf p τ⊢⇩t⇘/F⇙ ({τ} ∩ P) (the (Γ p)) Q,A ∧
           (∀x. Θ ∪ Specs_wf p τ
                 ⊆ x ⟶
                 Γ,x⊢⇩t⇘/F⇙ ({τ} ∩ P) (the (Γ p)) Q,A))" by fact
  hence "∀(P,p,Q,A)∈Specs. p ∈ dom Γ ∧
         (∀τ. Γ,Θ'∪ Specs_wf p τ ⊢⇩t⇘/F⇙ ({τ} ∩ P) (the (Γ p)) Q,A)"
    apply (clarify)
    apply (rename_tac P p Q A)
    apply (drule (1) bspec)
    apply (clarsimp)
    apply (erule_tac x=τ in allE)
    apply clarify
    apply (erule_tac x="Θ' ∪ Specs_wf p τ" in allE)
    apply (insert aug)
    apply auto
    done
  with CallRec show ?case by - (rule hoaret.CallRec)
next
  case DynCom thus ?case by (blast intro: hoaret.DynCom)
next
  case (Conseq P Θ F c Q A Θ')
  from Conseq
  have "∀s ∈ P. (∃P' Q' A'. (Γ,Θ' ⊢⇩t⇘/F⇙ P' c Q',A') ∧ s ∈ P'∧ Q' ⊆ Q ∧ A' ⊆ A)"
    by blast
  with Conseq show ?case by - (rule hoaret.Conseq)
next
  case (ExFalso Θ F P  c Q A Θ')
  have "Γ,Θ⊨⇩t⇘/F⇙ P c Q,A" "¬ Γ⊨⇩t⇘/F⇙ P c Q,A" "Θ ⊆ Θ'"  by fact+
  then show ?case
    by (fastforce intro: hoaret.ExFalso simp add: cvalidt_def)
qed (blast intro: hoaret.intros)+

subsection ‹Some Derived Rules›


lemma  Conseq': "∀s. s ∈ P ⟶
            (∃P' Q' A'.
              (∀ Z. Γ,Θ⊢⇩t⇘/F⇙ (P' Z) c (Q' Z),(A' Z)) ∧
                    (∃Z. s ∈ P' Z ∧ (Q' Z ⊆ Q) ∧ (A' Z ⊆ A)))
           ⟹
           Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
apply (rule Conseq)
apply (rule ballI)
apply (erule_tac x=s in allE)
apply (clarify)
apply (rule_tac x="P' Z" in exI)
apply (rule_tac x="Q' Z" in exI)
apply (rule_tac x="A' Z" in exI)
apply blast
done

lemma conseq:"⟦∀Z. Γ,Θ ⊢⇩t⇘/F⇙ (P' Z) c (Q' Z),(A' Z);
              ∀s. s ∈ P ⟶ (∃ Z. s∈P' Z ∧ (Q' Z ⊆ Q)∧ (A' Z ⊆ A))⟧
              ⟹
              Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
  by (rule Conseq) blast

theorem conseqPrePost:
  "Γ,Θ⊢⇩t⇘/F⇙ P' c Q',A' ⟹ P ⊆ P' ⟹  Q' ⊆ Q ⟹ A' ⊆ A ⟹  Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
  by (rule conseq [where ?P'="λZ. P'" and ?Q'="λZ. Q'"]) auto

lemma conseqPre: "Γ,Θ⊢⇩t⇘/F⇙ P' c Q,A ⟹ P ⊆ P' ⟹ Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
by (rule conseq) auto

lemma conseqPost: "Γ,Θ⊢⇩t⇘/F⇙ P c Q',A'⟹ Q' ⊆ Q ⟹ A' ⊆ A ⟹   Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
  by (rule conseq) auto


lemma Spec_wf_conv:
  "(λ(P, q, Q, A). (P ∩ {s. ((s, q), τ, p) ∈ r}, q, Q, A)) `
                (⋃p∈Procs. ⋃Z. {(P p Z, p, Q p Z, A p Z)}) =
        (⋃q∈Procs. ⋃Z. {(P q Z ∩ {s. ((s, q), τ, p) ∈ r}, q, Q q Z, A q Z)})"
  by (auto intro!: image_eqI)

lemma CallRec':
  "⟦p∈Procs; Procs ⊆ dom Γ;
    wf r;
   ∀p∈Procs. ∀τ Z.
   Γ,Θ∪(⋃q∈Procs. ⋃Z.
    {((P q Z) ∩ {s. ((s,q),(τ,p)) ∈ r},q,Q q Z,(A q Z))})
     ⊢⇩t⇘/F⇙ ({τ} ∩ (P p Z)) (the (Γ p)) (Q p Z),(A p Z)⟧
   ⟹
   Γ,Θ⊢⇩t⇘/F⇙ (P p Z) (Call p) (Q p Z),(A p Z)"
apply (rule CallRec [where Specs="⋃p∈Procs. ⋃Z. {((P p Z),p,Q p Z,A p Z)}" and
         r=r])
apply    blast
apply   assumption
apply  (rule refl)
apply (clarsimp)
apply (rename_tac p')
apply (rule conjI)
apply  blast
apply (intro allI)
apply (rename_tac Z τ)
apply (drule_tac x=p' in bspec, assumption)
apply (erule_tac x=τ in allE)
apply (erule_tac x=Z in allE)
apply (fastforce simp add: Spec_wf_conv)
done

end