Theory Denotation
section ‹Denotational semantics of expressions and commands›
theory Denotation imports Com begin
subsection ‹Definitions›
consts
A :: "i ⇒ i ⇒ i"
B :: "i ⇒ i ⇒ i"
C :: "i ⇒ i"
definition
Gamma :: "[i,i,i] ⇒ i" (‹Γ›) where
"Γ(b,cden) ≡
(λphi. {io ∈ (phi O cden). B(b,fst(io))=1} ∪
{io ∈ id(loc->nat). B(b,fst(io))=0})"
primrec
"A(N(n), sigma) = n"
"A(X(x), sigma) = sigma`x"
"A(Op1(f,a), sigma) = f`A(a,sigma)"
"A(Op2(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
primrec
"B(true, sigma) = 1"
"B(false, sigma) = 0"
"B(ROp(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
"B(noti(b), sigma) = not(B(b,sigma))"
"B(b0 andi b1, sigma) = B(b0,sigma) and B(b1,sigma)"
"B(b0 ori b1, sigma) = B(b0,sigma) or B(b1,sigma)"
primrec
"C(\<SKIP>) = id(loc->nat)"
"C(x \<ASSN> a) =
{io ∈ (loc->nat) × (loc->nat). snd(io) = fst(io)(x := A(a,fst(io)))}"
"C(c0\<SEQ> c1) = C(c1) O C(c0)"
"C(\<IF> b \<THEN> c0 \<ELSE> c1) =
{io ∈ C(c0). B(b,fst(io)) = 1} ∪ {io ∈ C(c1). B(b,fst(io)) = 0}"
"C(\<WHILE> b \<DO> c) = lfp((loc->nat) × (loc->nat), Γ(b,C(c)))"
subsection ‹Misc lemmas›
lemma A_type [TC]: "⟦a ∈ aexp; sigma ∈ loc->nat⟧ ⟹ A(a,sigma) ∈ nat"
by (erule aexp.induct) simp_all
lemma B_type [TC]: "⟦b ∈ bexp; sigma ∈ loc->nat⟧ ⟹ B(b,sigma) ∈ bool"
by (erule bexp.induct, simp_all)
lemma C_subset: "c ∈ com ⟹ C(c) ⊆ (loc->nat) × (loc->nat)"
apply (erule com.induct)
apply simp_all
apply (blast dest: lfp_subset [THEN subsetD])+
done
lemma C_type_D [dest]:
"⟦⟨x,y⟩ ∈ C(c); c ∈ com⟧ ⟹ x ∈ loc->nat ∧ y ∈ loc->nat"
by (blast dest: C_subset [THEN subsetD])
lemma C_type_fst [dest]: "⟦x ∈ C(c); c ∈ com⟧ ⟹ fst(x) ∈ loc->nat"
by (auto dest!: C_subset [THEN subsetD])
lemma Gamma_bnd_mono:
"cden ⊆ (loc->nat) × (loc->nat)
⟹ bnd_mono ((loc->nat) × (loc->nat), Γ(b,cden))"
by (unfold bnd_mono_def Gamma_def) blast
end