equal
deleted
inserted
replaced
10 "W b rc = (\<lambda>rw. {(s,t). if bval b s then (s,t) \<in> rc O rw else s=t})" |
10 "W b rc = (\<lambda>rw. {(s,t). if bval b s then (s,t) \<in> rc O rw else s=t})" |
11 |
11 |
12 fun D :: "com \<Rightarrow> com_den" where |
12 fun D :: "com \<Rightarrow> com_den" where |
13 "D SKIP = Id" | |
13 "D SKIP = Id" | |
14 "D (x ::= a) = {(s,t). t = s(x := aval a s)}" | |
14 "D (x ::= a) = {(s,t). t = s(x := aval a s)}" | |
15 "D (c0;;c1) = D(c0) O D(c1)" | |
15 "D (c1;;c2) = D(c1) O D(c2)" | |
16 "D (IF b THEN c1 ELSE c2) |
16 "D (IF b THEN c1 ELSE c2) |
17 = {(s,t). if bval b s then (s,t) \<in> D c1 else (s,t) \<in> D c2}" | |
17 = {(s,t). if bval b s then (s,t) \<in> D c1 else (s,t) \<in> D c2}" | |
18 "D (WHILE b DO c) = lfp (W b (D c))" |
18 "D (WHILE b DO c) = lfp (W b (D c))" |
19 |
19 |
20 lemma W_mono: "mono (W b r)" |
20 lemma W_mono: "mono (W b r)" |