equal
deleted
inserted
replaced
333 apply (rule_tac [!] impI) |
333 apply (rule_tac [!] impI) |
334 apply (rule_tac [!] conjI) |
334 apply (rule_tac [!] conjI) |
335 apply (rule_tac [!] impI) |
335 apply (rule_tac [!] impI) |
336 apply (simp add: in_set_code memb_cons_iff memb_def) |
336 apply (simp add: in_set_code memb_cons_iff memb_def) |
337 apply (metis) |
337 apply (metis) |
338 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
338 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
339 length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2)) |
|
340 defer |
|
341 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
|
342 length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2)) |
339 length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2)) |
343 apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))") |
340 apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))") |
344 apply (simp only:) |
341 apply (simp only:) |
345 apply (rule_tac f="f a1" in arg_cong) |
342 apply (rule_tac f="f a1" in arg_cong) |
346 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
343 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
348 apply (simp add: memb_delete_raw) |
345 apply (simp add: memb_delete_raw) |
349 apply (metis memb_cons_iff) |
346 apply (metis memb_cons_iff) |
350 apply (erule memb_commute_ffold_raw) |
347 apply (erule memb_commute_ffold_raw) |
351 apply (drule_tac x="a1" in spec) |
348 apply (drule_tac x="a1" in spec) |
352 apply (simp add: memb_cons_iff) |
349 apply (simp add: memb_cons_iff) |
|
350 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
|
351 length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2)) |
353 done |
352 done |
354 |
353 |
355 lemma [quot_respect]: |
354 lemma [quot_respect]: |
356 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
355 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
357 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
356 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |