4 |
4 |
5 theory Denotation imports Big_Step begin |
5 theory Denotation imports Big_Step begin |
6 |
6 |
7 type_synonym com_den = "(state \<times> state) set" |
7 type_synonym com_den = "(state \<times> state) set" |
8 |
8 |
9 definition |
9 definition W :: "bexp \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where |
10 Gamma :: "bexp \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where |
10 "W b rc = (\<lambda>rw. {(s,t). if bval b s then (s,t) \<in> rc O rw else s=t})" |
11 "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> bval b s} \<union> |
|
12 {(s,t). s=t \<and> \<not>bval b s})" |
|
13 |
11 |
14 fun C :: "com \<Rightarrow> com_den" where |
12 fun C :: "com \<Rightarrow> com_den" where |
15 "C SKIP = Id" | |
13 "C SKIP = {(s,t). s=t}" | |
16 "C (x ::= a) = {(s,t). t = s(x := aval a s)}" | |
14 "C (x ::= a) = {(s,t). t = s(x := aval a s)}" | |
17 "C (c0;;c1) = C(c0) O C(c1)" | |
15 "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> |
16 "C (IF b THEN c1 ELSE c2) |
19 {(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" | |
17 = {(s,t). if bval b s then (s,t) \<in> C c1 else (s,t) \<in> C c2}" | |
20 "C(WHILE b DO c) = lfp (Gamma b (C c))" |
18 "C(WHILE b DO c) = lfp (W b (C c))" |
21 |
19 |
|
20 lemma W_mono: "mono (W b r)" |
|
21 by (unfold W_def mono_def) auto |
22 |
22 |
23 lemma Gamma_mono: "mono (Gamma b c)" |
23 lemma C_While_If: |
24 by (unfold Gamma_def mono_def) fast |
24 "C(WHILE b DO c) = C(IF b THEN c;;WHILE b DO c ELSE SKIP)" |
25 |
|
26 lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;;WHILE b DO c ELSE SKIP)" |
|
27 apply simp |
25 apply simp |
28 apply (subst lfp_unfold [OF Gamma_mono]) --{*lhs only*} |
26 apply (subst lfp_unfold [OF W_mono]) --{*lhs only*} |
29 apply (simp add: Gamma_def) |
27 apply (simp add: W_def) |
30 done |
28 done |
31 |
29 |
32 text{* Equivalence of denotational and big-step semantics: *} |
30 text{* Equivalence of denotational and big-step semantics: *} |
33 |
31 |
34 lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)" |
32 lemma C_if_big_step: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)" |
35 apply (induction rule: big_step_induct) |
33 proof (induction rule: big_step_induct) |
36 apply auto |
34 case WhileFalse |
37 (* while *) |
35 with C_While_If show ?case by auto |
38 apply (unfold Gamma_def) |
36 next |
39 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def]) |
37 case WhileTrue |
40 apply fast |
38 show ?case unfolding C_While_If using WhileTrue by auto |
41 apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def]) |
39 qed auto |
42 apply auto |
|
43 done |
|
44 |
40 |
45 lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t" |
41 abbreviation Big_step :: "com \<Rightarrow> com_den" where |
46 apply (induction c arbitrary: s t) |
42 "Big_step c \<equiv> {(s,t). (c,s) \<Rightarrow> t}" |
47 apply auto |
|
48 apply blast |
|
49 (* while *) |
|
50 apply (erule lfp_induct2 [OF _ Gamma_mono]) |
|
51 apply (unfold Gamma_def) |
|
52 apply auto |
|
53 done |
|
54 |
43 |
55 lemma denotational_is_big_step: "(s,t) \<in> C(c) = ((c,s) \<Rightarrow> t)" |
44 lemma Big_step_if_C: "(s,t) \<in> C(c) \<Longrightarrow> (s,t) : Big_step c" |
56 by (fast elim: com2 dest: com1) |
45 proof (induction c arbitrary: s t) |
|
46 case Seq thus ?case by fastforce |
|
47 next |
|
48 case (While b c) |
|
49 let ?B = "Big_step (WHILE b DO c)" |
|
50 have "W b (C c) ?B <= ?B" using While.IH by (auto simp: W_def) |
|
51 from lfp_lowerbound[where ?f = "W b (C c)", OF this] While.prems |
|
52 show ?case by auto |
|
53 qed (auto split: if_splits) |
|
54 |
|
55 theorem denotational_is_big_step: |
|
56 "(s,t) \<in> C(c) = ((c,s) \<Rightarrow> t)" |
|
57 by (metis C_if_big_step Big_step_if_C[simplified]) |
57 |
58 |
58 end |
59 end |