349 apply (simp) |
349 apply (simp) |
350 apply (simp add: memb_cons_iff memb_def) |
350 apply (simp add: memb_cons_iff memb_def) |
351 apply auto |
351 apply auto |
352 apply (drule_tac x="e" in spec) |
352 apply (drule_tac x="e" in spec) |
353 apply blast |
353 apply blast |
354 apply (simp add: memb_cons_iff) |
354 apply (case_tac b) |
355 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
355 apply simp_all |
356 length_Suc_conv memb_absorb nil_not_cons(2)) |
|
357 apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))") |
356 apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))") |
358 apply (simp only:) |
357 apply (simp only:) |
359 apply (rule_tac f="f a1" in arg_cong) |
358 apply (rule_tac f="f a1" in arg_cong) |
360 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
359 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
361 apply simp |
360 apply simp |
362 apply (simp add: memb_delete_raw) |
361 apply (simp add: memb_delete_raw) |
363 apply (auto simp add: memb_cons_iff)[1] |
362 apply (auto simp add: memb_cons_iff)[1] |
364 apply (erule memb_commute_ffold_raw) |
363 apply (erule memb_commute_ffold_raw) |
365 apply (drule_tac x="a1" in spec) |
364 apply (drule_tac x="a1" in spec) |
366 apply (simp add: memb_cons_iff) |
365 apply (simp add: memb_cons_iff) |
367 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
366 apply (simp add: memb_cons_iff) |
368 length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2)) |
367 apply (case_tac b) |
|
368 apply simp_all |
369 done |
369 done |
370 |
370 |
371 lemma [quot_respect]: |
371 lemma [quot_respect]: |
372 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
372 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
373 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
373 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |