Theory HoarePartialDef

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

(*  Title:      HoarePartialDef.thy
    Author:     Norbert Schirmer, TU Muenchen

Copyright (C) 2004-2008 Norbert Schirmer 
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

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: @{text "Γ,Θ⊨⇘/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)
    moreover
    from this t' have "t'=t"
      by auto
    ultimately 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)
    moreover
    from this t' have "t'=t"
      by auto
    ultimately show ?thesis
      by simp
  qed
qed


subsection {* The Hoare Rules: @{text "Γ,Θ⊢⇘/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⇩1 R,A; Γ,Θ⊢⇘/F⇙ R c⇩2 Q,A⟧
        ⟹
        Γ,Θ⊢⇘/F⇙ P (Seq c⇩1 c⇩2) Q,A"
  
| Cond: "⟦Γ,Θ⊢⇘/F⇙ (P ∩ b) c⇩1 Q,A; Γ,Θ⊢⇘/F⇙ (P ∩ - b) c⇩2 Q,A⟧
         ⟹ 
         Γ,Θ⊢⇘/F⇙ P (Cond b c⇩1 c⇩2) 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⇩1 Q,R; Γ,Θ⊢⇘/F⇙ R c⇩2 Q,A⟧ ⟹  Γ,Θ⊢⇘/F⇙ P Catch c⇩1 c⇩2 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 @{text "Θ"}, from completeness for an empty context.›  



text {* Does not work, because of rule ExFalso, the context @{text "Θ"} 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 Γ Θ init p
         result return )
  from CallRec.hyps
  have "∀p∈Procs. ∀Z. (strip Γ),Θ ∪
             (⋃⇘p∈Procs⇙
                 ⋃⇘Z⇙ {(Pre p Z, Call (Init p) p (Return p) (Result p),
                      Post p Z, Abr p Z)})⊢
            (Pre p Z) (the (Γ p)) (R p Z),(Abr' p Z)" by blast
  hence "∀p∈Procs. ∀Z. (strip Γ),Θ ∪
             (⋃⇘p∈Procs⇙
                 ⋃⇘Z⇙ {(Pre p Z, Call (Init p) p (Return p) (Result p),
                      Post p Z, Abr p Z)})⊢
            (Pre p Z) (the ((strip Γ) 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