equal
deleted
inserted
replaced
38 "Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')" |
38 "Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')" |
39 "Sem(IF b THEN c1 ELSE c2 FI) s s' = ((s : b --> Sem c1 s s') & |
39 "Sem(IF b THEN c1 ELSE c2 FI) s s' = ((s : b --> Sem c1 s s') & |
40 (s ~: b --> Sem c2 s s'))" |
40 (s ~: b --> Sem c2 s s'))" |
41 "Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')" |
41 "Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')" |
42 |
42 |
43 constdefs Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" |
43 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where |
44 "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q" |
44 "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q" |
45 |
45 |
46 |
46 |
47 |
47 |
48 (** parse translations **) |
48 (** parse translations **) |