# Theory AxSem

Up to index of Isabelle/HOL/NanoJava

theory AxSem
imports State
begin

    (*  Title:      HOL/NanoJava/AxSem.thy
        ID:         $Id: AxSem.thy,v 1.14 2005/06/17 14:13:09 haftmann Exp $
        Author:     David von Oheimb
        Copyright   2001 Technische Universitaet Muenchen
    *)

    header "Axiomatic Semantics"

    theory AxSem imports State begin

    types assn   = "state => bool"
         vassn   = "val => assn"
          triple = "assn × stmt ×  assn"
         etriple = "assn × expr × vassn"
    translations
      "assn"   \<leftharpoondown> (type)"state => bool"
     "vassn"   \<leftharpoondown> (type)"val => assn"
      "triple" \<leftharpoondown> (type)"assn × stmt ×  assn"
     "etriple" \<leftharpoondown> (type)"assn × expr × vassn"

    consts   hoare   :: "(triple set ×  triple set) set"
    consts  ehoare   :: "(triple set × etriple    ) set"
    syntax (xsymbols)
     "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ |\<turnstile>/ _" [61,61]    60)
     "@hoare1" :: "[triple set,  assn,stmt,assn] => bool"
                                       ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
    "@ehoare"  :: "[triple set,  etriple       ] => bool" ("_ |\<turnstile>e/ _"[61,61]60)
    "@ehoare1" :: "[triple set,  assn,expr,vassn]=> bool"
                                      ("_ \<turnstile>e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
    syntax
     "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ ||-/ _" [61,61] 60)
     "@hoare1" :: "[triple set,  assn,stmt,assn] => bool"
                                      ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
    "@ehoare"  :: "[triple set,  etriple       ] => bool" ("_ ||-e/ _"[61,61] 60)
    "@ehoare1" :: "[triple set,  assn,expr,vassn]=> bool"
                                     ("_ |-e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)

    translations "A |\<turnstile> C"        \<rightleftharpoons> "(A,C) ∈ hoare"
                 "A  \<turnstile> {P}c{Q}"  \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
                 "A |\<turnstile>e t"       \<rightleftharpoons> "(A,t) ∈ ehoare"
                 "A |\<turnstile>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) ∈ ehoare" (* shouldn't be necessary *)
                 "A  \<turnstile>e {P}e{Q}" \<rightleftharpoons> "A |\<turnstile>e (P,e,Q)"

    subsection "Hoare Logic Rules"

    inductive hoare ehoare
    intros

      Skip:  "A |- {P} Skip {P}"

      Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"

      Cond: "[| A |-e {P} e {Q};
                ∀v. A |- {Q v} (if v ≠ Null then c1 else c2) {R} |] ==>
                A |- {P} If(e) c1 Else c2 {R}"

      Loop: "A |- {λs. P s ∧ s<x> ≠ Null} c {P} ==>
             A |- {P} While(x) c {λs. P s ∧ s<x> = Null}"

      LAcc: "A |-e {λs. P (s<x>) s} LAcc x {P}"

      LAss: "A |-e {P} e {λv s.  Q (lupd(x\<mapsto>v) s)} ==>
             A |-  {P} x:==e {Q}"

      FAcc: "A |-e {P} e {λv s. ∀a. v=Addr a --> Q (get_field s a f) s} ==>
             A |-e {P} e..f {Q}"

      FAss: "[| A |-e {P} e1 {λv s. ∀a. v=Addr a --> Q a s};
            ∀a. A |-e {Q a} e2 {λv s. R (upd_obj a f v s)} |] ==>
                A |-  {P} e1..f:==e2 {R}"

      NewC: "A |-e {λs. ∀a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
                    new C {P}"

      Cast: "A |-e {P} e {λv s. (case v of Null => True
                                     | Addr a => obj_class s a <=C C) --> Q v s} ==>
             A |-e {P} Cast C e {Q}"

      Call: "[| A |-e {P} e1 {Q}; ∀a. A |-e {Q a} e2 {R a};
        ∀a p ls. A |- {λs'. ∃s. R a p s ∧ ls = s ∧
                        s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s))}
                      Meth (C,m) {λs. S (s<Res>) (set_locs ls s)} |] ==>
                 A |-e {P} {C}e1..m(e2) {S}"

      Meth: "∀D. A |- {λs'. ∃s a. s<This> = Addr a ∧ D = obj_class s a ∧ D <=C C ∧
                            P s ∧ s' = init_locs D m s}
                      Impl (D,m) {Q} ==>
                 A |- {P} Meth (C,m) {Q}"

      --{* @{text "\<Union>Z"} instead of @{text "∀Z"} in the conclusion and\\
           Z restricted to type state due to limitations of the inductive package *}
      Impl: "∀Z::state. A∪ (\<Union>Z. (λCm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||-
                                (λCm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
                          A ||- (λCm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"

    --{* structural rules *}

      Asm:  "   a ∈ A ==> A ||- {a}"

      ConjI: " ∀c ∈ C. A ||- {c} ==> A ||- C"

      ConjE: "[|A ||- C; c ∈ C |] ==> A ||- {c}"

      --{* Z restricted to type state due to limitations of the inductive package *}
      Conseq:"[| ∀Z::state. A |- {P' Z} c {Q' Z};
                 ∀s t. (∀Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
                A |- {P} c {Q }"

      --{* Z restricted to type state due to limitations of the inductive package *}
     eConseq:"[| ∀Z::state. A |-e {P' Z} e {Q' Z};
                 ∀s v t. (∀Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
                A |-e {P} e {Q }"

    subsection "Fully polymorphic variants, required for Example only"

    axioms

      Conseq:"[| ∀Z. A |- {P' Z} c {Q' Z};
                 ∀s t. (∀Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
                     A |- {P} c {Q }"

     eConseq:"[| ∀Z. A |-e {P' Z} e {Q' Z};
                 ∀s v t. (∀Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
                     A |-e {P} e {Q }"

     Impl: "∀Z. A∪ (\<Union>Z. (λCm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||-
                              (λCm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
                        A ||- (λCm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"

    subsection "Derived Rules"

    lemma Conseq1: "[|A \<turnstile> {P'} c {Q}; ∀s. P s --> P' s|] ==> A \<turnstile> {P} c {Q}"
    apply (rule hoare_ehoare.Conseq)
    apply  (rule allI, assumption)
    apply fast
    done

    lemma Conseq2: "[|A \<turnstile> {P} c {Q'}; ∀t. Q' t --> Q t|] ==> A \<turnstile> {P} c {Q}"
    apply (rule hoare_ehoare.Conseq)
    apply  (rule allI, assumption)
    apply fast
    done

    lemma eConseq1: "[|A \<turnstile>e {P'} e {Q}; ∀s. P s --> P' s|] ==> A \<turnstile>e {P} e {Q}"
    apply (rule hoare_ehoare.eConseq)
    apply  (rule allI, assumption)
    apply fast
    done

    lemma eConseq2: "[|A \<turnstile>e {P} e {Q'}; ∀v t. Q' v t --> Q v t|] ==> A \<turnstile>e {P} e {Q}"
    apply (rule hoare_ehoare.eConseq)
    apply  (rule allI, assumption)
    apply fast
    done

    lemma Weaken: "[|A |\<turnstile> C'; C ⊆ C'|] ==> A |\<turnstile> C"
    apply (rule hoare_ehoare.ConjI)
    apply clarify
    apply (drule hoare_ehoare.ConjE)
    apply  fast
    apply assumption
    done

    lemma Thin_lemma:
      "(A' |\<turnstile>  C         --> (∀A. A' ⊆ A --> A |\<turnstile>  C       )) ∧
       (A'  \<turnstile>e {P} e {Q} --> (∀A. A' ⊆ A --> A  \<turnstile>e {P} e {Q}))"
    apply (rule hoare_ehoare.induct)
    apply (tactic "ALLGOALS(EVERY'[Clarify_tac, REPEAT o smp_tac 1])")
    apply (blast intro: hoare_ehoare.Skip)
    apply (blast intro: hoare_ehoare.Comp)
    apply (blast intro: hoare_ehoare.Cond)
    apply (blast intro: hoare_ehoare.Loop)
    apply (blast intro: hoare_ehoare.LAcc)
    apply (blast intro: hoare_ehoare.LAss)
    apply (blast intro: hoare_ehoare.FAcc)
    apply (blast intro: hoare_ehoare.FAss)
    apply (blast intro: hoare_ehoare.NewC)
    apply (blast intro: hoare_ehoare.Cast)
    apply (erule hoare_ehoare.Call)
    apply   (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption)
    apply  blast
    apply (blast intro!: hoare_ehoare.Meth)
    apply (blast intro!: hoare_ehoare.Impl)
    apply (blast intro!: hoare_ehoare.Asm)
    apply (blast intro: hoare_ehoare.ConjI)
    apply (blast intro: hoare_ehoare.ConjE)
    apply (rule hoare_ehoare.Conseq)
    apply  (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+)
    apply (rule hoare_ehoare.eConseq)
    apply  (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+)
    done

    lemma cThin: "[|A' |\<turnstile> C; A' ⊆ A|] ==> A |\<turnstile> C"
    by (erule (1) conjunct1 [OF Thin_lemma, rule_format])

    lemma eThin: "[|A' \<turnstile>e {P} e {Q}; A' ⊆ A|] ==> A \<turnstile>e {P} e {Q}"
    by (erule (1) conjunct2 [OF Thin_lemma, rule_format])

    lemma Union: "A |\<turnstile> (\<Union>Z. C Z) = (∀Z. A |\<turnstile> C Z)"
    by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)

    lemma Impl1':
       "[|∀Z::state. A∪ (\<Union>Z. (λCm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile>
                     (λCm. (P Z Cm, body Cm, Q Z Cm))`Ms;
        Cm ∈ Ms|] ==>
                    A   \<turnstile>  {P Z Cm} Impl Cm {Q Z Cm}"
    apply (drule AxSem.Impl)
    apply (erule Weaken)
    apply (auto del: image_eqI intro: rev_image_eqI)
    done

    lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified, standard]

    end

### Hoare Logic Rules

### Fully polymorphic variants, required for Example only

### Derived Rules

lemma Conseq1:

      [| A |- {P'} c {Q}; ∀s. P s --> P' s |] ==> A |- {P} c {Q}

lemma Conseq2:

      [| A |- {P} c {Q'}; ∀t. Q' t --> Q t |] ==> A |- {P} c {Q}

lemma eConseq1:

      [| A |-e {P'} e {Q}; ∀s. P s --> P' s |] ==> A |-e {P} e {Q}

lemma eConseq2:

      [| A |-e {P} e {Q'}; ∀v t. Q' v t --> Q v t |] ==> A |-e {P} e {Q}

lemma Weaken:

      [| A ||- C'; C ⊆ C' |] ==> A ||- C

lemma Thin_lemma:

      (A' ||- C --> (∀A≥A'. A ||- C)) ∧
      (A' |-e {P} e {Q} --> (∀A≥A'. A |-e {P} e {Q}))

lemma cThin:

      [| A' ||- C; A' ⊆ A |] ==> A ||- C

lemma eThin:

      [| A' |-e {P} e {Q}; A' ⊆ A |] ==> A |-e {P} e {Q}

lemma Union:

      A ||- (UN Z. C Z) = (∀Z. A ||- C Z)

lemma Impl1':

      [| ∀Z. A ∪ (UN Z. (%Cm. (P Z Cm, Impl Cm, Q Z Cm)) ` Ms) ||-
            (%Cm. (P Z Cm, body Cm, Q Z Cm)) ` Ms;
         Cm ∈ Ms |]
      ==> A |- {P Z Cm} Impl Cm {Q Z Cm}

lemmas Impl1:

      ∀Z. A ∪ (UN Z. {(P Z Cm, Impl Cm, Q Z Cm)}) |- {P Z Cm} body Cm {Q Z Cm}
      ==> A |- {P Z Cm} Impl Cm {Q Z Cm}

lemmas Impl1:

      ∀Z. A ∪ (UN Z. {(P Z Cm, Impl Cm, Q Z Cm)}) |- {P Z Cm} body Cm {Q Z Cm}
      ==> A |- {P Z Cm} Impl Cm {Q Z Cm}