1 (* Title: HOL/IMP/Denotation.thy |
1 (* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *) |
2 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
3 *) |
|
4 |
2 |
5 header "Denotational Semantics of Commands" |
3 header "Denotational Semantics of Commands" |
6 |
4 |
7 theory Denotation imports Natural begin |
5 theory Denotation imports Big_Step begin |
8 |
6 |
9 type_synonym com_den = "(state \<times> state) set" |
7 type_synonym com_den = "(state \<times> state) set" |
10 |
8 |
11 definition |
9 definition |
12 Gamma :: "[bexp,com_den] => (com_den => com_den)" where |
10 Gamma :: "bexp \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where |
13 "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> b s} \<union> |
11 "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> bval b s} \<union> |
14 {(s,t). s=t \<and> \<not>b s})" |
12 {(s,t). s=t \<and> \<not>bval b s})" |
15 |
13 |
16 primrec C :: "com => com_den" |
14 fun C :: "com \<Rightarrow> com_den" where |
17 where |
15 "C SKIP = Id" | |
18 C_skip: "C \<SKIP> = Id" |
16 "C (x ::= a) = {(s,t). t = s(x := aval a s)}" | |
19 | C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}" |
17 "C (c0;c1) = C(c0) O C(c1)" | |
20 | C_comp: "C (c0;c1) = C(c0) O C(c1)" |
18 "C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union> |
21 | C_if: "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union> |
19 {(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" | |
22 {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}" |
20 "C(WHILE b DO c) = lfp (Gamma b (C c))" |
23 | C_while: "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))" |
|
24 |
21 |
25 |
22 |
26 (**** mono (Gamma(b,c)) ****) |
23 (**** mono (Gamma(b,c)) ****) |
27 |
24 |
28 lemma Gamma_mono: "mono (Gamma b c)" |
25 lemma Gamma_mono: "mono (Gamma b c)" |
29 by (unfold Gamma_def mono_def) fast |
26 by (unfold Gamma_def mono_def) fast |
30 |
27 |
31 lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)" |
28 lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)" |
32 apply simp |
29 apply simp |
33 apply (subst lfp_unfold [OF Gamma_mono]) --{*lhs only*} |
30 apply (subst lfp_unfold [OF Gamma_mono]) --{*lhs only*} |
34 apply (simp add: Gamma_def) |
31 apply (simp add: Gamma_def) |
35 done |
32 done |
36 |
33 |
37 (* Operational Semantics implies Denotational Semantics *) |
34 (* Operational Semantics implies Denotational Semantics *) |
38 |
35 |
39 lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)" |
36 lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)" |
40 (* start with rule induction *) |
37 (* start with rule induction *) |
41 apply (induct set: evalc) |
38 apply (induct rule: big_step_induct) |
42 apply auto |
39 apply auto |
43 (* while *) |
40 (* while *) |
44 apply (unfold Gamma_def) |
41 apply (unfold Gamma_def) |
45 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def]) |
42 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def]) |
46 apply fast |
43 apply fast |
48 apply auto |
45 apply auto |
49 done |
46 done |
50 |
47 |
51 (* Denotational Semantics implies Operational Semantics *) |
48 (* Denotational Semantics implies Operational Semantics *) |
52 |
49 |
53 lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" |
50 lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t" |
54 apply (induct c arbitrary: s t) |
51 apply (induct c arbitrary: s t) |
55 apply auto |
52 apply auto |
56 apply blast |
53 apply blast |
57 |
|
58 (* while *) |
54 (* while *) |
59 apply (erule lfp_induct2 [OF _ Gamma_mono]) |
55 apply (erule lfp_induct2 [OF _ Gamma_mono]) |
60 apply (unfold Gamma_def) |
56 apply (unfold Gamma_def) |
61 apply auto |
57 apply auto |
62 done |
58 done |
63 |
59 |
64 |
60 |
65 (**** Proof of Equivalence ****) |
61 (**** Proof of Equivalence ****) |
66 |
62 |
67 lemma denotational_is_natural: "(s,t) \<in> C(c) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)" |
63 lemma denotational_is_natural: "(s,t) \<in> C(c) = ((c,s) \<Rightarrow> t)" |
68 by (fast elim: com2 dest: com1) |
64 by (fast elim: com2 dest: com1) |
69 |
65 |
70 end |
66 end |