108 by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) |
108 by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) |
109 qed |
109 qed |
110 |
110 |
111 end |
111 end |
112 |
112 |
113 |
113 text_raw{*\snip{maptwoacomdef}{2}{2}{% *} |
114 fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where |
114 fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" |
115 "map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" | |
115 where |
116 "map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" | |
116 "map2_acom f (SKIP {a\<^isub>1}) (SKIP {a\<^isub>2}) = (SKIP {f a\<^isub>1 a\<^isub>2})" | |
117 "map2_acom f (C1;C2) (D1;D2) = (map2_acom f C1 D1; map2_acom f C2 D2)" | |
117 "map2_acom f (x ::= e {a\<^isub>1}) (x' ::= e' {a\<^isub>2}) = (x ::= e {f a\<^isub>1 a\<^isub>2})" | |
118 "map2_acom f (IF b THEN {p1} C1 ELSE {p2} C2 {a1}) (IF b' THEN {q1} D1 ELSE {q2} D2 {a2}) = |
118 "map2_acom f (C\<^isub>1;C\<^isub>2) (D\<^isub>1;D\<^isub>2) |
119 (IF b THEN {f p1 q1} map2_acom f C1 D1 ELSE {f p2 q2} map2_acom f C2 D2 {f a1 a2})" | |
119 = (map2_acom f C\<^isub>1 D\<^isub>1; map2_acom f C\<^isub>2 D\<^isub>2)" | |
120 "map2_acom f ({a1} WHILE b DO {p} C {a2}) ({a3} WHILE b' DO {p'} C' {a4}) = |
120 "map2_acom f (IF b THEN {p\<^isub>1} C\<^isub>1 ELSE {p\<^isub>2} C\<^isub>2 {a\<^isub>1}) |
121 ({f a1 a3} WHILE b DO {f p p'} map2_acom f C C' {f a2 a4})" |
121 (IF b' THEN {q\<^isub>1} D\<^isub>1 ELSE {q\<^isub>2} D\<^isub>2 {a\<^isub>2}) |
|
122 = (IF b THEN {f p\<^isub>1 q\<^isub>1} map2_acom f C\<^isub>1 D\<^isub>1 |
|
123 ELSE {f p\<^isub>2 q\<^isub>2} map2_acom f C\<^isub>2 D\<^isub>2 {f a\<^isub>1 a\<^isub>2})" | |
|
124 "map2_acom f ({a\<^isub>1} WHILE b DO {p} C {a\<^isub>2}) |
|
125 ({a\<^isub>3} WHILE b' DO {q} D {a\<^isub>4}) |
|
126 = ({f a\<^isub>1 a\<^isub>3} WHILE b DO {f p q} map2_acom f C D {f a\<^isub>2 a\<^isub>4})" |
|
127 text_raw{*}%endsnip*} |
122 |
128 |
123 lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow> |
129 lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow> |
124 annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))" |
130 annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))" |
125 by(induction f C1 C2 rule: map2_acom.induct)(simp_all add: size_annos_same2) |
131 by(induction f C1 C2 rule: map2_acom.induct)(simp_all add: size_annos_same2) |
126 |
132 |