181 fixes a b :: "'a list" |
181 fixes a b :: "'a list" |
182 assumes e: "a \<approx> b" |
182 assumes e: "a \<approx> b" |
183 shows "card1 a = card1 b" |
183 shows "card1 a = card1 b" |
184 using e by induct (simp_all add:memb_rsp) |
184 using e by induct (simp_all add:memb_rsp) |
185 |
185 |
186 lemma ho_card1_rsp: "op \<approx> ===> op = card1 card1" |
186 lemma ho_card1_rsp: "(op \<approx> ===> op =) card1 card1" |
187 by (simp add: card1_rsp) |
187 by (simp add: card1_rsp) |
188 |
188 |
189 lemma cons_rsp: |
189 lemma cons_rsp: |
190 fixes z |
190 fixes z |
191 assumes a: "xs \<approx> ys" |
191 assumes a: "xs \<approx> ys" |
192 shows "(z # xs) \<approx> (z # ys)" |
192 shows "(z # xs) \<approx> (z # ys)" |
193 using a by (rule list_eq.intros(5)) |
193 using a by (rule list_eq.intros(5)) |
194 |
194 |
195 lemma ho_cons_rsp: |
195 lemma ho_cons_rsp: |
196 "op = ===> op \<approx> ===> op \<approx> op # op #" |
196 "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
197 by (simp add: cons_rsp) |
197 by (simp add: cons_rsp) |
198 |
198 |
199 lemma append_rsp_fst: |
199 lemma append_rsp_fst: |
200 assumes a : "list_eq l1 l2" |
200 assumes a : "list_eq l1 l2" |
201 shows "(l1 @ s) \<approx> (l2 @ s)" |
201 shows "(l1 @ s) \<approx> (l2 @ s)" |
248 using b apply (assumption) |
248 using b apply (assumption) |
249 apply (rule append_sym_rsp) |
249 apply (rule append_sym_rsp) |
250 done |
250 done |
251 |
251 |
252 lemma ho_append_rsp: |
252 lemma ho_append_rsp: |
253 "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @" |
253 "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
254 by (simp add: append_rsp) |
254 by (simp add: append_rsp) |
255 |
255 |
256 lemma map_rsp: |
256 lemma map_rsp: |
257 assumes a: "a \<approx> b" |
257 assumes a: "a \<approx> b" |
258 shows "map f a \<approx> map f b" |
258 shows "map f a \<approx> map f b" |
260 apply (induct) |
260 apply (induct) |
261 apply(auto intro: list_eq.intros) |
261 apply(auto intro: list_eq.intros) |
262 done |
262 done |
263 |
263 |
264 lemma fun_rel_id: |
264 lemma fun_rel_id: |
265 "op = ===> op = \<equiv> op =" |
265 "(op = ===> op =) \<equiv> op =" |
266 apply (rule eq_reflection) |
266 apply (rule eq_reflection) |
267 apply (rule ext) |
267 apply (rule ext) |
268 apply (rule ext) |
268 apply (rule ext) |
269 apply (simp) |
269 apply (simp) |
270 apply (auto) |
270 apply (auto) |
271 apply (rule ext) |
271 apply (rule ext) |
272 apply (simp) |
272 apply (simp) |
273 done |
273 done |
274 |
274 |
275 lemma ho_map_rsp: |
275 lemma ho_map_rsp: |
276 "op = ===> op = ===> op \<approx> ===> op \<approx> map map" |
276 "((op = ===> op =) ===> op \<approx> ===> op \<approx>) map map" |
277 by (simp add: fun_rel_id map_rsp) |
277 by (simp add: fun_rel_id map_rsp) |
278 |
278 |
279 lemma map_append : |
279 lemma map_append : |
280 "(map f ((a::'a list) @ b)) \<approx> |
280 "(map f ((a::'a list) @ b)) \<approx> |
281 ((map f a) ::'a list) @ (map f b)" |
281 ((map f a) ::'a list) @ (map f b)" |