12 {(s,t). s=t \<and> \<not>bval b s})" |
12 {(s,t). s=t \<and> \<not>bval b s})" |
13 |
13 |
14 fun C :: "com \<Rightarrow> com_den" where |
14 fun C :: "com \<Rightarrow> com_den" where |
15 "C SKIP = Id" | |
15 "C SKIP = Id" | |
16 "C (x ::= a) = {(s,t). t = s(x := aval a s)}" | |
16 "C (x ::= a) = {(s,t). t = s(x := aval a s)}" | |
17 "C (c0;c1) = C(c0) O C(c1)" | |
17 "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> |
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 lemma Gamma_mono: "mono (Gamma b c)" |
23 lemma Gamma_mono: "mono (Gamma b c)" |
24 by (unfold Gamma_def mono_def) fast |
24 by (unfold Gamma_def mono_def) fast |
25 |
25 |
26 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)" |
27 apply simp |
27 apply simp |
28 apply (subst lfp_unfold [OF Gamma_mono]) --{*lhs only*} |
28 apply (subst lfp_unfold [OF Gamma_mono]) --{*lhs only*} |
29 apply (simp add: Gamma_def) |
29 apply (simp add: Gamma_def) |
30 done |
30 done |
31 |
31 |