1478

1 
(* Title: ZF/IMP/Denotation.thy

482

2 
ID: $Id$

12610

3 
Author: Heiko Loetzbeyer and Robert Sandner, TU München


4 
*)

511

5 

12610

6 
header {* Denotational semantics of expressions and commands *}

482

7 

16417

8 
theory Denotation imports Com begin

12606

9 

12610

10 
subsection {* Definitions *}

482

11 


12 
consts

12606

13 
A :: "i => i => i"


14 
B :: "i => i => i"


15 
C :: "i => i"


16 

19747

17 
definition

12610

18 
Gamma :: "[i,i,i] => i" ("\<Gamma>")

19749

19 
"\<Gamma>(b,cden) ==

12610

20 
(\<lambda>phi. {io \<in> (phi O cden). B(b,fst(io))=1} \<union>


21 
{io \<in> id(loc>nat). B(b,fst(io))=0})"

482

22 

12606

23 
primrec

12610

24 
"A(N(n), sigma) = n"


25 
"A(X(x), sigma) = sigma`x"


26 
"A(Op1(f,a), sigma) = f`A(a,sigma)"


27 
"A(Op2(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"

482

28 

12606

29 
primrec

12610

30 
"B(true, sigma) = 1"


31 
"B(false, sigma) = 0"


32 
"B(ROp(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"


33 
"B(noti(b), sigma) = not(B(b,sigma))"


34 
"B(b0 andi b1, sigma) = B(b0,sigma) and B(b1,sigma)"


35 
"B(b0 ori b1, sigma) = B(b0,sigma) or B(b1,sigma)"

12606

36 

12610

37 
primrec


38 
"C(\<SKIP>) = id(loc>nat)"


39 
"C(x \<ASSN> a) =


40 
{io \<in> (loc>nat) \<times> (loc>nat). snd(io) = fst(io)(x := A(a,fst(io)))}"


41 
"C(c0\<SEQ> c1) = C(c1) O C(c0)"


42 
"C(\<IF> b \<THEN> c0 \<ELSE> c1) =


43 
{io \<in> C(c0). B(b,fst(io)) = 1} \<union> {io \<in> C(c1). B(b,fst(io)) = 0}"


44 
"C(\<WHILE> b \<DO> c) = lfp((loc>nat) \<times> (loc>nat), \<Gamma>(b,C(c)))"

12606

45 


46 

12610

47 
subsection {* Misc lemmas *}

12606

48 


49 
lemma A_type [TC]: "[a \<in> aexp; sigma \<in> loc>nat] ==> A(a,sigma) \<in> nat"

12610

50 
by (erule aexp.induct) simp_all

12606

51 


52 
lemma B_type [TC]: "[b \<in> bexp; sigma \<in> loc>nat] ==> B(b,sigma) \<in> bool"


53 
by (erule bexp.induct, simp_all)

511

54 

12610

55 
lemma C_subset: "c \<in> com ==> C(c) \<subseteq> (loc>nat) \<times> (loc>nat)"


56 
apply (erule com.induct)


57 
apply simp_all


58 
apply (blast dest: lfp_subset [THEN subsetD])+


59 
done

12606

60 


61 
lemma C_type_D [dest]:

12610

62 
"[ <x,y> \<in> C(c); c \<in> com ] ==> x \<in> loc>nat & y \<in> loc>nat"


63 
by (blast dest: C_subset [THEN subsetD])

482

64 

12606

65 
lemma C_type_fst [dest]: "[ x \<in> C(c); c \<in> com ] ==> fst(x) \<in> loc>nat"

12610

66 
by (auto dest!: C_subset [THEN subsetD])

482

67 

12610

68 
lemma Gamma_bnd_mono:


69 
"cden \<subseteq> (loc>nat) \<times> (loc>nat)


70 
==> bnd_mono ((loc>nat) \<times> (loc>nat), \<Gamma>(b,cden))"


71 
by (unfold bnd_mono_def Gamma_def) blast

482

72 


73 
end
