# HG changeset patch
# User nipkow
# Date 752349737 -3600
# Node ID 61b65ffb418637dabeb26829dbe90973531b3d36
# Parent  201061643c4b0f44a45038554e86b1b211604fb1
added append "@"
Proved @ associativ

diff -r 201061643c4b -r 61b65ffb4186 List.ML
--- a/List.ML	Mon Oct 25 14:36:27 1993 +0100
+++ b/List.ML	Wed Nov 03 19:02:17 1993 +0100
@@ -310,6 +310,20 @@
 by (rtac list_rec_Cons 1);
 val list_case_Cons = result();
 
+(** @ - append **)
+
+goalw List.thy [append_def] "[]@xs = xs";
+by (rtac list_rec_Nil 1);
+val append_Nil = result();
+
+goalw List.thy [append_def] "Cons(x,xs)@ys = Cons(x,xs@ys)";
+by (rtac list_rec_Cons 1);
+val append_Cons = result();
+
+goal List.thy "(xs@ys)@zs = xs@(ys@zs)";
+by(res_inst_tac [("l","xs")] list_induct 1);
+by(REPEAT(asm_simp_tac (list_ss addsimps [append_Nil,append_Cons]) 1));
+val append_assoc = result();
 
 (** The functional "map" **)
 
diff -r 201061643c4b -r 61b65ffb4186 List.thy
--- a/List.thy	Mon Oct 25 14:36:27 1993 +0100
+++ b/List.thy	Wed Nov 03 19:02:17 1993 +0100
@@ -39,6 +39,7 @@
   tl            :: "'a list => 'a list"
   list_all      :: "('a => bool) => ('a list => bool)"
   map           :: "('a=>'b) => ('a list => 'b list)"
+  "@"		:: "['a list, 'a list] => 'a list"		(infixr 65)
   list_case     :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"
 
   (* List Enumeration *)
@@ -98,7 +99,7 @@
   tl_def        "tl(xs)              == list_rec(xs, @xs.True, %x xs r.xs)"
   list_all_def  "list_all(P, xs)     == list_rec(xs, True, %x l r. P(x) & r)"
   map_def       "map(f, xs)          == list_rec(xs, Nil, %x l r. Cons(f(x), r))"
+  append_def	"xs@ys               == list_rec(xs, ys, %x l r. Cons(x,r))"
   list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"
 
 end
-