8 |
8 |
9 theory Denotation imports Natural begin |
9 theory Denotation imports Natural begin |
10 |
10 |
11 types com_den = "(state\<times>state)set" |
11 types com_den = "(state\<times>state)set" |
12 |
12 |
13 constdefs |
13 definition |
14 Gamma :: "[bexp,com_den] => (com_den => com_den)" |
14 Gamma :: "[bexp,com_den] => (com_den => com_den)" where |
15 "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union> |
15 "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union> |
16 {(s,t). s=t \<and> \<not>b s})" |
16 {(s,t). s=t \<and> \<not>b s})" |
17 |
17 |
18 consts |
18 primrec C :: "com => com_den" |
19 C :: "com => com_den" |
19 where |
20 |
|
21 primrec |
|
22 C_skip: "C \<SKIP> = Id" |
20 C_skip: "C \<SKIP> = Id" |
23 C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}" |
21 | C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}" |
24 C_comp: "C (c0;c1) = C(c1) O C(c0)" |
22 | C_comp: "C (c0;c1) = C(c1) O C(c0)" |
25 C_if: "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union> |
23 | C_if: "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union> |
26 {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}" |
24 {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}" |
27 C_while: "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))" |
25 | C_while: "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))" |
28 |
26 |
29 |
27 |
30 (**** mono (Gamma(b,c)) ****) |
28 (**** mono (Gamma(b,c)) ****) |
31 |
29 |
32 lemma Gamma_mono: "mono (Gamma b c)" |
30 lemma Gamma_mono: "mono (Gamma b c)" |