# Theory AxSem

theory AxSem
imports State
```(*  Title:      HOL/NanoJava/AxSem.thy
Author:     David von Oheimb, Technische Universitaet Muenchen
*)

section "Axiomatic Semantics"

theory AxSem imports State begin

type_synonym assn = "state => bool"
type_synonym vassn = "val => assn"
type_synonym triple = "assn × stmt ×  assn"
type_synonym etriple = "assn × expr × vassn"
translations
(type) "assn" ↽ (type) "state => bool"
(type) "vassn" ↽ (type) "val => assn"
(type) "triple" ↽ (type) "assn × stmt × assn"
(type) "etriple" ↽ (type) "assn × expr × vassn"

subsection "Hoare Logic Rules"

inductive
hoare :: "[triple set, triple set] => bool"  ("_ |⊢/ _" [61, 61] 60)
and ehoare :: "[triple set, etriple] => bool"  ("_ |⊢⇩e/ _" [61, 61] 60)
and hoare1 :: "[triple set, assn,stmt,assn] => bool"
("_ ⊢/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60)
and ehoare1 :: "[triple set, assn,expr,vassn]=> bool"
("_ ⊢⇩e/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60)
where

"A  ⊢ {P}c{Q} ≡ A |⊢ {(P,c,Q)}"
| "A  ⊢⇩e {P}e{Q} ≡ A |⊢⇩e (P,e,Q)"

| 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↦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↦a)(lupd(Par↦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}"

― ‹‹⋃Z› instead of ‹∀Z› in the conclusion and\\
Z restricted to type state due to limitations of the inductive package›
| Impl: "∀Z::state. A∪ (⋃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"

axiomatization where
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 }"

axiomatization where
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 }"

axiomatization where
Impl: "∀Z. A∪ (⋃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 ⊢ {P'} c {Q}; ∀s. P s ⟶ P' s⟧ ⟹ A ⊢ {P} c {Q}"
apply (rule hoare_ehoare.Conseq)
apply  (rule allI, assumption)
apply fast
done

lemma Conseq2: "⟦A ⊢ {P} c {Q'}; ∀t. Q' t ⟶ Q t⟧ ⟹ A ⊢ {P} c {Q}"
apply (rule hoare_ehoare.Conseq)
apply  (rule allI, assumption)
apply fast
done

lemma eConseq1: "⟦A ⊢⇩e {P'} e {Q}; ∀s. P s ⟶ P' s⟧ ⟹ A ⊢⇩e {P} e {Q}"
apply (rule hoare_ehoare.eConseq)
apply  (rule allI, assumption)
apply fast
done

lemma eConseq2: "⟦A ⊢⇩e {P} e {Q'}; ∀v t. Q' v t ⟶ Q v t⟧ ⟹ A ⊢⇩e {P} e {Q}"
apply (rule hoare_ehoare.eConseq)
apply  (rule allI, assumption)
apply fast
done

lemma Weaken: "⟦A |⊢ C'; C ⊆ C'⟧ ⟹ A |⊢ C"
apply (rule hoare_ehoare.ConjI)
apply clarify
apply (drule hoare_ehoare.ConjE)
apply  fast
apply assumption
done

lemma Thin_lemma:
"(A' |⊢  C         ⟶ (∀A. A' ⊆ A ⟶ A |⊢  C       )) ∧
(A'  ⊢⇩e {P} e {Q} ⟶ (∀A. A' ⊆ A ⟶ A  ⊢⇩e {P} e {Q}))"
apply (rule hoare_ehoare.induct)
apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac @{context} 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 @{context} 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 @{context} 1 1", assumption+)
apply (rule hoare_ehoare.eConseq)
apply  (rule, drule spec, erule conjE, tactic "smp_tac @{context} 1 1", assumption+)
done

lemma cThin: "⟦A' |⊢ C; A' ⊆ A⟧ ⟹ A |⊢ C"
by (erule (1) conjunct1 [OF Thin_lemma, rule_format])

lemma eThin: "⟦A' ⊢⇩e {P} e {Q}; A' ⊆ A⟧ ⟹ A ⊢⇩e {P} e {Q}"
by (erule (1) conjunct2 [OF Thin_lemma, rule_format])

lemma Union: "A |⊢ (⋃Z. C Z) = (∀Z. A |⊢ C Z)"
by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)

lemma Impl1':
"⟦∀Z::state. A∪ (⋃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}"
apply (drule AxSem.Impl)
apply (erule Weaken)
apply (auto del: image_eqI intro: rev_image_eqI)
done

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

end
```