18 "C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union> |
18 "C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union> |
19 {(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" | |
19 {(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" | |
20 "C(WHILE b DO c) = lfp (Gamma b (C c))" |
20 "C(WHILE b DO c) = lfp (Gamma b (C c))" |
21 |
21 |
22 |
22 |
23 (**** mono (Gamma(b,c)) ****) |
|
24 |
|
25 lemma Gamma_mono: "mono (Gamma b c)" |
23 lemma Gamma_mono: "mono (Gamma b c)" |
26 by (unfold Gamma_def mono_def) fast |
24 by (unfold Gamma_def mono_def) fast |
27 |
25 |
28 lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)" |
26 lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)" |
29 apply simp |
27 apply simp |
30 apply (subst lfp_unfold [OF Gamma_mono]) --{*lhs only*} |
28 apply (subst lfp_unfold [OF Gamma_mono]) --{*lhs only*} |
31 apply (simp add: Gamma_def) |
29 apply (simp add: Gamma_def) |
32 done |
30 done |
33 |
31 |
34 (* Operational Semantics implies Denotational Semantics *) |
32 text{* Equivalence of denotational and big-step semantics: *} |
35 |
33 |
36 lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)" |
34 lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)" |
37 (* start with rule induction *) |
|
38 apply (induct rule: big_step_induct) |
35 apply (induct rule: big_step_induct) |
39 apply auto |
36 apply auto |
40 (* while *) |
37 (* while *) |
41 apply (unfold Gamma_def) |
38 apply (unfold Gamma_def) |
42 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def]) |
39 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def]) |
43 apply fast |
40 apply fast |
44 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def]) |
41 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def]) |
45 apply auto |
42 apply auto |
46 done |
43 done |
47 |
|
48 (* Denotational Semantics implies Operational Semantics *) |
|
49 |
44 |
50 lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t" |
45 lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t" |
51 apply (induct c arbitrary: s t) |
46 apply (induct c arbitrary: s t) |
52 apply auto |
47 apply auto |
53 apply blast |
48 apply blast |
55 apply (erule lfp_induct2 [OF _ Gamma_mono]) |
50 apply (erule lfp_induct2 [OF _ Gamma_mono]) |
56 apply (unfold Gamma_def) |
51 apply (unfold Gamma_def) |
57 apply auto |
52 apply auto |
58 done |
53 done |
59 |
54 |
60 |
55 lemma denotational_is_big_step: "(s,t) \<in> C(c) = ((c,s) \<Rightarrow> t)" |
61 (**** Proof of Equivalence ****) |
|
62 |
|
63 lemma denotational_is_natural: "(s,t) \<in> C(c) = ((c,s) \<Rightarrow> t)" |
|
64 by (fast elim: com2 dest: com1) |
56 by (fast elim: com2 dest: com1) |
65 |
57 |
66 end |
58 end |