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

Copyright (C) 2006-2008 Norbert Schirmer
*)

section ‹Hoare Logic for Partial Correctness›
theory HoarePartialDef imports Semantic begin

type_synonym ('s,'p) quadruple = "('s assn × 'p × 's assn × 's assn)"

subsection ‹Validity of Hoare Tuples: ‹Γ,Θ⊨_F P c Q,A››

definition
  valid :: "[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com,'s assn,'s assn] => bool"
                (‹_⊨_{/_}/ _ _ _,_›  [61,60,1000, 20, 1000,1000] 60)
where
 "Γ⊨_F P c Q,A ≡ ∀s t. Γ⊨⟨c,s⟩ → t ⟶ s ∈ Normal ` P ⟶ t ∉ Fault ` F
                      ⟶ t ∈ Normal ` Q ∪ Abrupt ` A"

definition
  cvalid::
  "[('s,'p,'f) body,('s,'p) quadruple set,'f set,
      's assn,('s,'p,'f) com,'s assn,'s assn] =>bool"
                (‹_,_⊨_{/_}/ _ _ _,_›  [61,60,60,1000, 20, 1000,1000] 60)
where
 "Γ,Θ⊨_F P c Q,A ≡ (∀(P,p,Q,A)∈Θ. Γ⊨_F P (Call p) Q,A) ⟶ Γ ⊨_F P c Q,A"


definition
  nvalid :: "[('s,'p,'f) body,nat,'f set,
                's assn,('s,'p,'f) com,'s assn,'s assn] => bool"
                (‹_⊨_:_{/_}/ _ _ _,_›  [61,60,60,1000, 20, 1000,1000] 60)
where
 "Γ⊨n:_F P c Q,A ≡ ∀s t. Γ⊨⟨c,s ⟩ =n→ t ⟶ s ∈ Normal ` P ⟶ t ∉ Fault ` F
                        ⟶ t ∈ Normal ` Q ∪ Abrupt ` A"


definition
  cnvalid::
  "[('s,'p,'f) body,('s,'p) quadruple set,nat,'f set,
     's assn,('s,'p,'f) com,'s assn,'s assn] → bool"
                (‹_,_⊨_:_{/_}/ _ _ _,_›  [61,60,60,60,1000, 20, 1000,1000] 60)
where
 "Γ,Θ⊨n:_F P c Q,A ≡ (∀(P,p,Q,A)∈Θ. Γ⊨n:_F P (Call p) Q,A) ⟶ Γ ⊨n:_F P c Q,A"


notation (ASCII)
  valid  (‹_|='/_/ _ _ _,_›  [61,60,1000, 20, 1000,1000] 60) and
  cvalid  (‹_,_|='/_/ _ _ _,_›  [61,60,60,1000, 20, 1000,1000] 60) and
  nvalid  (‹_|=_:'/_/ _ _ _,_›  [61,60,60,1000, 20, 1000,1000] 60) and
  cnvalid  (‹_,_|=_:'/_/ _ _ _,_›  [61,60,60,60,1000, 20, 1000,1000] 60)


subsection ‹Properties of Validity›

lemma valid_iff_nvalid: "Γ⊨_F P c Q,A = (∀n. Γ⊨n:_F P c Q,A)"
  apply (simp only: valid_def nvalid_def exec_iff_execn )
  apply (blast dest: exec_final_notin_to_execn)
  done

lemma cnvalid_to_cvalid: "(∀n. Γ,Θ⊨n:_F P c Q,A) ==> Γ,Θ⊨_F P c Q,A"
  apply (unfold cvalid_def cnvalid_def valid_iff_nvalid [THEN eq_reflection])
  apply fast
  done

lemma nvalidI:
 "[∧s t. [Γ⊨⟨c,Normal s ⟩ =n→ t;s ∈ P; t∉ Fault ` F] ==> t ∈ Normal ` Q ∪ Abrupt ` A]
  ==> Γ⊨n:_F P c Q,A"
  by (auto simp add: nvalid_def)

lemma validI:
 "[∧s t. [Γ⊨⟨c,Normal s ⟩ → t;s ∈ P; t∉Fault ` F] ==> t ∈ Normal ` Q ∪ Abrupt ` A]
  ==> Γ⊨_F P c Q,A"
  by (auto simp add: valid_def)

lemma cvalidI:
 "[∧s t. [∀(P,p,Q,A)∈Θ. Γ⊨_F P (Call p) Q,A;Γ⊨⟨c,Normal s⟩ → t;s ∈ P;t∉Fault ` F]
          ==> t ∈ Normal ` Q ∪ Abrupt ` A]
  ==> Γ,Θ⊨_F P c Q,A"
  by (auto simp add: cvalid_def valid_def)

lemma cvalidD:
 "[Γ,Θ⊨_F P c Q,A;∀(P,p,Q,A)∈Θ. Γ⊨_F P (Call p) Q,A;Γ⊨⟨c,Normal s⟩ → t;s ∈ P;t∉Fault ` F]
  ==> t ∈ Normal ` Q ∪ Abrupt ` A"
  by (auto simp add: cvalid_def valid_def)

lemma cnvalidI:
 "[∧s t. [∀(P,p,Q,A)∈Θ. Γ⊨n:_F P (Call p) Q,A;
   Γ⊨⟨c,Normal s ⟩ =n→ t;s ∈ P;t∉Fault ` F]
          ==> t ∈ Normal ` Q ∪ Abrupt ` A]
  ==> Γ,Θ⊨n:_F P c Q,A"
  by (auto simp add: cnvalid_def nvalid_def)


lemma cnvalidD:
 "[Γ,Θ⊨n:_F P c Q,A;∀(P,p,Q,A)∈Θ. Γ⊨n:_F P (Call p) Q,A;
   Γ⊨⟨c,Normal s ⟩ =n→ t;s ∈ P;
   t∉Fault ` F]
  ==> t ∈ Normal ` Q ∪ Abrupt ` A"
  by (auto simp add: cnvalid_def nvalid_def)

lemma nvalid_augment_Faults:
  assumes validn:"Γ⊨n:_F P c Q,A"
  assumes F': "F ⊆ F'"
  shows "Γ⊨n:_F' P c Q,A"
proof (rule nvalidI)
  fix s t
  assume exec: "Γ⊨⟨c,Normal s ⟩ =n→ t"
  assume P: "s ∈ P"
  assume F: "t ∉ Fault ` F'"
  with F' have "t ∉ Fault ` F"
    by blast
  with exec P validn
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
    by (auto simp add: nvalid_def)
qed

lemma valid_augment_Faults:
  assumes validn:"Γ⊨_F P c Q,A"
  assumes F': "F ⊆ F'"
  shows "Γ⊨_F' P c Q,A"
proof (rule validI)
  fix s t
  assume exec: "Γ⊨⟨c,Normal s ⟩ → t"
  assume P: "s ∈ P"
  assume F: "t ∉ Fault ` F'"
  with F' have "t ∉ Fault ` F"
    by blast
  with exec P validn
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
    by (auto simp add: valid_def)
qed

lemma nvalid_to_nvalid_strip:
  assumes validn:"Γ⊨n:_F P c Q,A"
  assumes F': "F' ⊆ -F"
  shows "strip F' Γ⊨n:_F P c Q,A"
proof (rule nvalidI)
  fix s t
  assume exec_strip: "strip F' Γ⊨⟨c,Normal s ⟩ =n→ t"
  assume P: "s ∈ P"
  assume F: "t ∉ Fault ` F"
  from exec_strip obtain t' where
    exec: "Γ⊨⟨c,Normal s ⟩ =n→ t'" and
    t': "t' ∈ Fault ` (-F') ⟶ t'=t" "¬ isFault t' ⟶ t'=t"
    by (blast dest: execn_strip_to_execn)
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases "t' ∈ Fault ` F")
    case True
    with t' F F' have False
      by blast
    thus ?thesis ..
  next
    case False
    with exec P validn
    have *: "t' ∈ Normal ` Q ∪ Abrupt ` A"
      by (auto simp add: nvalid_def)
    with t' have "t'=t"
      by auto
    with * show ?thesis
      by simp
  qed
qed


lemma valid_to_valid_strip:
  assumes valid:"Γ⊨_F P c Q,A"
  assumes F': "F' ⊆ -F"
  shows "strip F' Γ⊨_F P c Q,A"
proof (rule validI)
  fix s t
  assume exec_strip: "strip F' Γ⊨⟨c,Normal s ⟩ → t"
  assume P: "s ∈ P"
  assume F: "t ∉ Fault ` F"
  from exec_strip obtain t' where
    exec: "Γ⊨⟨c,Normal s ⟩ → t'" and
    t': "t' ∈ Fault ` (-F') ⟶ t'=t" "¬ isFault t' ⟶ t'=t"
    by (blast dest: exec_strip_to_exec)
  show "t ∈ Normal ` Q ∪ Abrupt ` A"
  proof (cases "t' ∈ Fault ` F")
    case True
    with t' F F' have False
      by blast
    thus ?thesis ..
  next
    case False
    with exec P valid
    have *: "t' ∈ Normal ` Q ∪ Abrupt ` A"
      by (auto simp add: valid_def)
    with t' have "t'=t"
      by auto
    with * show ?thesis
      by simp
  qed
qed


subsection ‹The Hoare Rules: ‹Γ,Θ⊨_F P c Q,A››

lemma mono_WeakenContext: "A ⊆ B ==>
        (λ(P, c, Q, A'). (Γ, Θ, F, P, c, Q, A') ∈ A) x ⟶
        (λ(P, c, Q, A'). (Γ, Θ, F, P, c, Q, A') ∈ B) x"
apply blast
done


inductive "hoarep"::"[('s,'p,'f) body,('s,'p) quadruple set,'f set,
    's assn,('s,'p,'f) com, 's assn,'s assn] => bool"
    (‹(3_,_/⊨_{/_} (_/ (_)/ _,/_))› [60,60,60,1000,20,1000,1000]60)
  for Γ::"('s,'p,'f) body"
where
  Skip: "Γ,Θ⊨_F Q Skip Q,A"

| Basic: "Γ,Θ⊨_F {s. f s ∈ Q} (Basic f) Q,A"

| Spec: "Γ,Θ⊨_F {s. (∀t. (s,t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s,t) ∈ r)} (Spec r) Q,A"

| Seq: "[Γ,Θ⊨_F P c₁ R,A; Γ,Θ⊨_F R c₂ Q,A]
        ==>
        Γ,Θ⊨_F P (Seq c₁ c₂) Q,A"

| Cond: "[Γ,Θ⊨_F (P ∩ b) c₁ Q,A; Γ,Θ⊨_F (P ∩ - b) c₂ Q,A]
         ==>
         Γ,Θ⊨_F P (Cond b c₁ c₂) Q,A"

| While: "Γ,Θ⊨_F (P ∩ b) c P,A
          ==>
          Γ,Θ⊨_F P (While b c) (P ∩ - b),A"

| Guard: "Γ,Θ⊨_F (g ∩ P) c Q,A
          ==>
          Γ,Θ⊨_F (g ∩ P) (Guard f g c) Q,A"

| Guarantee: "[f ∈ F; Γ,Θ⊨_F (g ∩ P) c Q,A]
              ==>
              Γ,Θ⊨_F P (Guard f g c) Q,A"

| CallRec:
  "[(P,p,Q,A) ∈ Specs;
    ∀(P,p,Q,A) ∈ Specs. p ∈ dom Γ ∧ Γ,Θ∪Specs⊨_F P (the (Γ p)) Q,A ]
  ==> Γ,Θ⊨_F P (Call p) Q,A"

| DynCom:
      "∀s ∈ P. Γ,Θ⊨_F P (c s) Q,A
      ==>
      Γ,Θ⊨_F P (DynCom c) Q,A"

| Throw: "Γ,Θ⊨_F A Throw Q,A"

| Catch: "[Γ,Θ⊨_F P c₁ Q,R; Γ,Θ⊨_F R c₂ Q,A] ==> Γ,Θ⊨_F P Catch c₁ c₂ Q,A"

| Conseq: "∀s ∈ P. ∃P' Q' A'. Γ,Θ⊨_F P' c Q',A' ∧ s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A
           ==> Γ,Θ⊨_F P c Q,A"


| Asm: "[(P,p,Q,A) ∈ Θ]
         ==>
         Γ,Θ⊨_F P (Call p) Q,A"


| ExFalso: "[∀n. Γ,Θ⊨n:_F P c Q,A; ¬ Γ⊨_F P c Q,A] ==> Γ,Θ⊨_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
 and completeness later on.›
lemma hoare_strip_Γ:
  assumes deriv: "Γ,Θ⊨_F P p Q,A"
  shows "strip (-F) Γ,Θ⊨_F P p Q,A"
using deriv
proof induct
  case Skip thus ?case by (iprover intro: hoarep.Skip)
next
  case Basic thus ?case by (iprover intro: hoarep.Basic)
next
  case Spec thus ?case by (iprover intro: hoarep.Spec)
next
  case Seq thus ?case by (iprover intro: hoarep.Seq)
next
  case Cond thus ?case by (iprover intro: hoarep.Cond)
next
  case While thus ?case by (iprover intro: hoarep.While)
next
  case Guard thus ?case by (iprover intro: hoarep.Guard)
(*next
  case CallSpec thus ?case by (iprover intro: hoarep.CallSpec)
next
  case (CallRec A Abr Abr' Init P Post Pre Procs Q R Result Return Z \<Gamma> \<Theta> init p
         result return )
  from CallRec.hyps
  have "\<forall>p\<in>Procs. \<forall>Z. (strip \<Gamma>),\<Theta> \<union>
             (\<Union>\<^bsub>p\<in>Procs\<^esub>
                 \<Union>\<^bsub>Z\<^esub> {(Pre p Z, Call (Init p) p (Return p) (Result p),
                      Post p Z, Abr p Z)})\<turnstile>
            (Pre p Z) (the (\<Gamma> p)) (R p Z),(Abr' p Z)" by blast
  hence "\<forall>p\<in>Procs. \<forall>Z. (strip \<Gamma>),\<Theta> \<union>
             (\<Union>\<^bsub>p\<in>Procs\<^esub>
                 \<Union>\<^bsub>Z\<^esub> {(Pre p Z, Call (Init p) p (Return p) (Result p),
                      Post p Z, Abr p Z)})\<turnstile>
            (Pre p Z) (the ((strip \<Gamma>) p)) (R p Z),(Abr' p Z)"
    by (auto intro: hoarep.StripI)
  then show ?case
    apply -
    apply (rule hoarep.CallRec)
    apply (assumption | simp only:dom_strip)+
    done*)
next
  case DynCom
  thus ?case
    by - (rule hoarep.DynCom,best  elim!: ballE exE)
next
  case Throw thus ?case by (iprover intro: hoarep.Throw)
next
  case Catch thus ?case by (iprover intro: hoarep.Catch)
(*next
  case CONSEQ thus ?case apply (auto intro: hoarep.CONSEQ)*)
next
  case Asm thus ?case by (iprover intro: hoarep.Asm)
next
  case ExFalso
  thus ?case
    oops

lemma hoare_augment_context:
  assumes deriv: "Γ,Θ⊨_F P p Q,A"
  shows "∧Θ'. Θ ⊆ Θ' ==> Γ,Θ'⊨_F P p Q,A"
using deriv
proof (induct)
  case CallRec
  case (CallRec P p Q A Specs Θ F Θ')
  from CallRec.prems
  have "Θ∪Specs
       ⊆ Θ'∪Specs"
    by blast
  with CallRec.hyps (2)
  have "∀(P,p,Q,A)∈Specs. p ∈ dom Γ ∧ Γ,Θ'∪Specs ⊨_F P (the (Γ p)) Q,A"
    by fastforce

  with CallRec show ?case by - (rule hoarep.CallRec)
next
  case DynCom thus ?case by (blast intro: hoarep.DynCom)
next
  case (Conseq P Θ F c Q A Θ')
  from Conseq
  have "∀s ∈ P.
         (∃P' Q' A'. Γ,Θ' ⊨_F P' c Q',A' ∧ s ∈ P' ∧ Q' ⊆ Q ∧ A' ⊆ A)"
    by blast
  with Conseq show ?case by - (rule hoarep.Conseq)
next
  case (ExFalso Θ F P c Q A Θ')
  have valid_ctxt: "∀n. Γ,Θ⊨n:_F P c Q,A" "Θ ⊆ Θ'" by fact+
  hence "∀n. Γ,Θ'⊨n:_F P c Q,A"
    by (simp add: cnvalid_def) blast
  moreover have invalid: "¬ Γ⊨_F P c Q,A"  by fact
  ultimately show ?case
    by (rule hoarep.ExFalso)
qed (blast intro: hoarep.intros)+


subsection ‹Some Derived Rules›

lemma  Conseq': "∀s. s ∈ P ⟶
            (∃P' Q' A'.
              (∀ Z. Γ,Θ⊨_F (P' Z) c (Q' Z),(A' Z)) ∧
                    (∃Z. s ∈ P' Z ∧ (Q' Z ⊆ Q) ∧ (A' Z ⊆ A)))
           ==>
           Γ,Θ⊨_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. Γ,Θ ⊨_F (P' Z) c (Q' Z),(A' Z);
              ∀s. s ∈ P ⟶ (∃ Z. s∈P' Z ∧ (Q' Z ⊆ Q) ∧ (A' Z ⊆ A))]
              ==>
              Γ,Θ⊨_F P c Q,A"
  by (rule Conseq) blast

theorem conseqPrePost [trans]:
  "Γ,Θ⊨_F P' c Q',A' ==> P ⊆ P' ==> Q' ⊆ Q ==> A' ⊆ A ==> Γ,Θ⊨_F P c Q,A"
  by (rule conseq [where ?P'="λZ. P'" and ?Q'="λZ. Q'"]) auto

lemma conseqPre [trans]: "Γ,Θ⊨_F P' c Q,A ==> P ⊆ P' ==> Γ,Θ⊨_F P c Q,A"
by (rule conseq) auto

lemma conseqPost [trans]: "Γ,Θ⊨_F P c Q',A' ==> Q' ⊆ Q ==> A' ⊆ A
 ==> Γ,Θ⊨_F P c Q,A"
  by (rule conseq) auto


lemma CallRec':
  "[p∈Procs; Procs ⊆ dom Γ;
   ∀p∈Procs.
    ∀Z. Γ,Θ ∪ (∪p∈Procs. ∪Z. {((P p Z),p,Q p Z,A p Z)})
        ⊨_F (P p Z) (the (Γ p)) (Q p Z),(A p Z)]
   ==>
   Γ,Θ⊨_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)}"])
apply  blast
apply blast
done

end