author | wenzelm |
Thu, 22 Nov 2007 14:51:34 +0100 | |
changeset 25456 | 6f79698f294d |
parent 21404 | eb85850d3eb7 |
child 35762 | af3ff2ba4c54 |
permissions | -rw-r--r-- |
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 |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19749
diff
changeset
|
18 |
Gamma :: "[i,i,i] => i" ("\<Gamma>") where |
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 |