(* Title: ZF/IMP/Denotation.thy Author: Heiko Loetzbeyer and Robert Sandner, TU München \<open>Denotational semantics of expressions and commands\<close> theory Denotation imports Com begin \<open>Definitions\<close> consts "i \ i \ i" "i \ i \ i" "i \ i" definition "[i,i,i] \ i" (\\\) where "\(b,cden) \ \<lambda>phi. {io \<in> (phi O cden). B(b,fst(io))=1} \<union> \<in> 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`" primrec "B(true, sigma) = 1" "B(false, sigma) = 0" "B(ROp(f,a0,a1), sigma) = f`" "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(\) = id(loc->nat)" "C(x \ a) = \<in> (loc->nat) \<times> (loc->nat). snd(io) = fst(io)(x := A(a,fst(io)))}" "C(c0\ c1) = C(c1) O C(c0)" "C(\ b \ c0 \ c1) = \<in> C(c0). B(b,fst(io)) = 1} \<union> {io \<in> C(c1). B(b,fst(io)) = 0}" "C(\ b \ c) = lfp((loc->nat) \ (loc->nat), \(b,C(c)))" \<open>Misc lemmas\<close> lemma A_type [TC]: "\a \ aexp; sigma \ loc->nat\ \ A(a,sigma) \ nat" by (erule aexp.induct) simp_alllemma 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_allapply (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) \<Longrightarrow> bnd_mono ((loc->nat) \<times> (loc->nat), \<Gamma>(b,cden))" by (unfold bnd_mono_def Gamma_def) blastend quality 100%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
