(* 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
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}