equal
deleted
inserted
replaced
873 apply (induct_tac "A" rule: list_induct) |
873 apply (induct_tac "A" rule: list_induct) |
874 apply (simp_all add: r_neutr r_neutl, clarify) |
874 apply (simp_all add: r_neutr r_neutl, clarify) |
875 apply (erule all_dupE) |
875 apply (erule all_dupE) |
876 apply (rule trans) |
876 apply (rule trans) |
877 prefer 2 apply assumption |
877 prefer 2 apply assumption |
878 apply (simp add: assoc [THEN spec, THEN spec, THEN spec, THEN sym]) |
878 apply (simp (no_asm_use) add: assoc [THEN spec, THEN spec, THEN spec, THEN sym]) |
|
879 apply simp |
879 done |
880 done |
880 |
881 |
881 lemma foldl_append_sym: |
882 lemma foldl_append_sym: |
882 "[| !a. f a e = a; !a. f e a = a; |
883 "[| !a. f a e = a; !a. f e a = a; |
883 !a b c. f a (f b c) = f(f a b) c |] |
884 !a b c. f a (f b c) = f(f a b) c |] |