--- a/src/HOL/List.thy Tue Feb 03 15:29:52 2009 +0100
+++ b/src/HOL/List.thy Tue Feb 03 16:52:01 2009 +0100
@@ -547,11 +547,6 @@
lemma append_Nil2 [simp]: "xs @ [] = xs"
by (induct xs) auto
-interpretation semigroup_append!: semigroup_add "op @"
- proof qed simp
-interpretation monoid_append!: monoid_add "[]" "op @"
- proof qed simp+
-
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
by (induct xs) auto
@@ -2082,12 +2077,18 @@
text{* @{const foldl} and @{text concat} *}
-lemma concat_conv_foldl: "concat xss = foldl op@ [] xss"
-by (induct xss) (simp_all add:monoid_append.foldl_absorb0)
-
lemma foldl_conv_concat:
- "foldl (op @) xs xxs = xs @ (concat xxs)"
-by(simp add:concat_conv_foldl monoid_append.foldl_absorb0)
+ "foldl (op @) xs xss = xs @ concat xss"
+proof (induct xss arbitrary: xs)
+ case Nil show ?case by simp
+next
+ interpret monoid_add "[]" "op @" proof qed simp_all
+ case Cons then show ?case by (simp add: foldl_absorb0)
+qed
+
+lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
+ by (simp add: foldl_conv_concat)
+
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
--- a/src/HOL/MetisExamples/BT.thy Tue Feb 03 15:29:52 2009 +0100
+++ b/src/HOL/MetisExamples/BT.thy Tue Feb 03 16:52:01 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MetisTest/BT.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Testing the metis method
@@ -181,7 +180,7 @@
lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
apply (induct t)
apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv)
- apply (metis Cons_eq_append_conv monoid_append.add_0_left postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident)
+ apply (metis append_Nil Cons_eq_append_conv postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident)
done
ML {*AtpWrapper.problem_name := "BT__inorder_reflect"*}