# HG changeset patch
# User haftmann
# Date 1470848240 -7200
# Node ID 5cdcd51a4dadf1c21abfece124bf07cf84efcaf6
# Parent  92e0378036662d62903227293063e23d6e2e0f87
lists form a monoid

diff -r 92e037803666 -r 5cdcd51a4dad src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 10 18:57:20 2016 +0200
+++ b/src/HOL/List.thy	Wed Aug 10 18:57:20 2016 +0200
@@ -928,11 +928,20 @@
 
 subsubsection \<open>\<open>@\<close> -- append\<close>
 
+global_interpretation append: monoid append Nil
+proof
+  fix xs ys zs :: "'a list"
+  show "(xs @ ys) @ zs = xs @ (ys @ zs)"
+    by (induct xs) simp_all
+  show "xs @ [] = xs"
+    by (induct xs) simp_all
+qed simp
+
 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
-by (induct xs) auto
-
-lemma append_Nil2 [simp]: "xs @ [] = xs"
-by (induct xs) auto
+  by (fact append.assoc)
+
+lemma append_Nil2: "xs @ [] = xs"
+  by (fact append.right_neutral)
 
 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
 by (induct xs) auto
@@ -978,8 +987,8 @@
 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
 using append_same_eq [of "[]"] by auto
 
-lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
-by (induct xs) auto
+lemma hd_Cons_tl: "xs \<noteq> [] ==> hd xs # tl xs = xs"
+  by (fact list.collapse)
 
 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
 by (induct xs) auto