equal
deleted
inserted
replaced
1 (* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *) |
1 (* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *) |
2 |
2 |
3 header "Denotational Semantics of Commands" |
3 header "Denotational Semantics of Commands" |
4 |
4 |
5 theory Denotation imports Big_Step begin |
5 theory Denotational 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 W :: "bexp \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where |
9 definition W :: "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})" |
10 "W b rc = (\<lambda>rw. {(s,t). if bval b s then (s,t) \<in> rc O rw else s=t})" |