(* 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" \<leftharpoondown> (type) "state => bool"
(type) "vassn" \<leftharpoondown> (type) "val => assn"
(type) "triple" \<leftharpoondown> (type) "assn \<times> stmt \<times> assn"
(type) "etriple" \<leftharpoondown> (type) "assn \<times> expr \<times> vassn"
subsection "Hoare Logic Rules"
inductive
hoare :: "[triple set, triple set] => bool" ("_ |\/ _" [61, 61] 60)
and ehoare :: "[triple set, etriple] => bool" ("_ |\\<^sub>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"
("_ \\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60)
where
"A \ {P}c{Q} \ A |\ {(P,c,Q)}"
| "A \\<^sub>e {P}e{Q} \ A |\\<^sub>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 \\<^sub>e {P} e {Q};
\<forall>v. A \<turnstile> {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
A \<turnstile> {P} If(e) c1 Else c2 {R}"
| Loop: "A \ {\s. P s \ s \ Null} c {P} ==>
A \<turnstile> {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
| LAcc: "A \\<^sub>e {\s. P (s) s} LAcc x {P}"
| LAss: "A \\<^sub>e {P} e {\v s. Q (lupd(x\v) s)} ==>
A \<turnstile> {P} x:==e {Q}"
| FAcc: "A \\<^sub>e {P} e {\v s. \a. v=Addr a --> Q (get_field s a f) s} ==>
A \<turnstile>\<^sub>e {P} e..f {Q}"
| FAss: "[| A \\<^sub>e {P} e1 {\v s. \a. v=Addr a --> Q a s};
\<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
A \<turnstile> {P} e1..f:==e2 {R}"
| NewC: "A \\<^sub>e {\s. \a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
new C {P}"
| Cast: "A \\<^sub>e {P} e {\v s. (case v of Null => True
| Addr a => obj_class s a \<preceq>C C) --> Q v s} ==>
A \<turnstile>\<^sub>e {P} Cast C e {Q}"
| Call: "[| A \\<^sub>e {P} e1 {Q}; \a. A \\<^sub>e {Q a} e2 {R a};
\<forall>a p ls. A \<turnstile> {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and>
s' = lupd(This\a)(lupd(Par\p)(del_locs s))}
Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==>
A \<turnstile>\<^sub>e {P} {C}e1..m(e2) {S}"
| Meth: "\D. A \ {\s'. \s a. s = Addr a \ D = obj_class s a \ D \C C \
P s \<and> s' = init_locs D m s}
Impl (D,m) {Q} ==>
A \<turnstile> {P} Meth (C,m) {Q}"
\<comment> \<open>\<open>\<Union>Z\<close> instead of \<open>\<forall>Z\<close> in the conclusion and\\
Z restricted to type state due to limitations of the inductive package\<close>
| Impl: "\Z::state. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
\<comment> \<open>structural rules\<close>
| Asm: " a \ A ==> A |\ {a}"
| ConjI: " \c \ C. A |\ {c} ==> A |\ C"
| ConjE: "[|A |\ C; c \ C |] ==> A |\ {c}"
\<comment> \<open>Z restricted to type state due to limitations of the inductive package\<close>
| Conseq:"[| \Z::state. A \ {P' Z} c {Q' Z};
\<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
A \<turnstile> {P} c {Q }"
\<comment> \<open>Z restricted to type state due to limitations of the inductive package\<close>
| eConseq:"[| \Z::state. A \\<^sub>e {P' Z} e {Q' Z};
\<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
A \<turnstile>\<^sub>e {P} e {Q }"
subsection "Fully polymorphic variants, required for Example only"
axiomatization where
Conseq:"[| \Z. A \ {P' Z} c {Q' Z};
\<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
A \<turnstile> {P} c {Q }"
axiomatization where
eConseq:"[| \Z. A \\<^sub>e {P' Z} e {Q' Z};
\<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
A \<turnstile>\<^sub>e {P} e {Q }"
axiomatization where
Impl: "\Z. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
A |\<turnstile> (\<lambda>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 \\<^sub>e {P'} e {Q}; \s. P s \ P' s\ \ A \\<^sub>e {P} e {Q}"
apply (rule hoare_ehoare.eConseq)
apply (rule allI, assumption)
apply fast
done
lemma eConseq2: "\A \\<^sub>e {P} e {Q'}; \v t. Q' v t \ Q v t\ \ A \\<^sub>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' \\<^sub>e {P} e {Q} \ (\A. A' \ A \ A \\<^sub>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' \\<^sub>e {P} e {Q}; A' \ A\ \ A \\<^sub>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) |\
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms;
Cm \<in> Ms\<rbrakk> \<Longrightarrow>
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] for Cm
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
