--- 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" **)
--- 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
-