equal
deleted
inserted
replaced
105 subsubsection "Annotated commands" |
105 subsubsection "Annotated commands" |
106 |
106 |
107 fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where |
107 fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where |
108 "map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" | |
108 "map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" | |
109 "map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" | |
109 "map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" | |
110 "map2_acom f (c1;c2) (c1';c2') = (map2_acom f c1 c1'; map2_acom f c2 c2')" | |
110 "map2_acom f (c1;;c2) (c1';;c2') = (map2_acom f c1 c1';; map2_acom f c2 c2')" | |
111 "map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) = |
111 "map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) = |
112 (IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" | |
112 (IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" | |
113 "map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) = |
113 "map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) = |
114 ({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})" |
114 ({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})" |
115 |
115 |