dropped global Nil/Append interpretation
authorhaftmann
Tue Feb 03 16:39:52 2009 +0100 (2009-02-03)
changeset 2978202e76245e5af
parent 29711 64d41ad4ffc2
child 29783 dce05b909056
dropped global Nil/Append interpretation
src/HOL/List.thy
src/HOL/MetisExamples/BT.thy
     1.1 --- a/src/HOL/List.thy	Mon Feb 02 13:56:24 2009 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Feb 03 16:39:52 2009 +0100
     1.3 @@ -547,11 +547,6 @@
     1.4  lemma append_Nil2 [simp]: "xs @ [] = xs"
     1.5  by (induct xs) auto
     1.6  
     1.7 -interpretation semigroup_append!: semigroup_add "op @"
     1.8 -  proof qed simp
     1.9 -interpretation monoid_append!: monoid_add "[]" "op @"
    1.10 -  proof qed simp+
    1.11 -
    1.12  lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
    1.13  by (induct xs) auto
    1.14  
    1.15 @@ -2082,12 +2077,18 @@
    1.16  
    1.17  text{* @{const foldl} and @{text concat} *}
    1.18  
    1.19 -lemma concat_conv_foldl: "concat xss = foldl op@ [] xss"
    1.20 -by (induct xss) (simp_all add:monoid_append.foldl_absorb0)
    1.21 -
    1.22  lemma foldl_conv_concat:
    1.23 -  "foldl (op @) xs xxs = xs @ (concat xxs)"
    1.24 -by(simp add:concat_conv_foldl monoid_append.foldl_absorb0)
    1.25 +  "foldl (op @) xs xss = xs @ concat xss"
    1.26 +proof (induct xss arbitrary: xs)
    1.27 +  case Nil show ?case by simp
    1.28 +next
    1.29 +  interpret monoid_add "[]" "op @" proof qed simp_all
    1.30 +  case Cons then show ?case by (simp add: foldl_absorb0)
    1.31 +qed
    1.32 +
    1.33 +lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
    1.34 +  by (simp add: foldl_conv_concat)
    1.35 +
    1.36  
    1.37  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
    1.38  
     2.1 --- a/src/HOL/MetisExamples/BT.thy	Mon Feb 02 13:56:24 2009 +0100
     2.2 +++ b/src/HOL/MetisExamples/BT.thy	Tue Feb 03 16:39:52 2009 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/MetisTest/BT.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7  
     2.8  Testing the metis method
     2.9 @@ -181,7 +180,7 @@
    2.10  lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
    2.11    apply (induct t)
    2.12    apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv)
    2.13 -  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)
    2.14 +  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)
    2.15    done
    2.16  
    2.17  ML {*AtpWrapper.problem_name := "BT__inorder_reflect"*}