# HG changeset patch
# User nipkow
# Date 792684728 -3600
# Node ID 2740293cc458700733362776938636b2a02208ee
# Parent  9b403e123c1b310022c40c9cbcb8d2464b93dda1
Added "flat"

diff -r 9b403e123c1b -r 2740293cc458 List.ML
--- a/List.ML	Wed Feb 08 14:06:37 1995 +0100
+++ b/List.ML	Mon Feb 13 15:12:08 1995 +0100
@@ -34,6 +34,7 @@
    mem_Nil, mem_Cons,
    append_Nil, append_Cons,
    map_Nil, map_Cons,
+   flat_Nil, flat_Cons,
    list_all_Nil, list_all_Cons,
    filter_Nil, filter_Cons];
 
@@ -109,6 +110,13 @@
 bind_thm("list_eq_cases",
   impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
 
+(** flat **)
+
+goal List.thy  "flat(xs@ys) = flat(xs)@flat(ys)";
+by (list.induct_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (list_ss addsimps [append_assoc])));
+qed"flat_append";
+
 (** nth **)
 
 val [nth_0,nth_Suc] = nat_recs nth_def; 
@@ -136,5 +144,5 @@
   [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
    mem_append, mem_filter,
    map_ident, map_append, map_compose,
-   list_all_True, list_all_conj, nth_0, nth_Suc];
+   flat_append, list_all_True, list_all_conj, nth_0, nth_Suc];
 
diff -r 9b403e123c1b -r 2740293cc458 List.thy
--- a/List.thy	Wed Feb 08 14:06:37 1995 +0100
+++ b/List.thy	Mon Feb 13 15:12:08 1995 +0100
@@ -23,6 +23,7 @@
   filter    :: "['a => bool, 'a list] => 'a list"
   foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
   length    :: "'a list => nat"
+  flat      :: "'a list list => 'a list"
   nth       :: "[nat, 'a list] => 'a"
 
 syntax
@@ -74,6 +75,9 @@
 primrec length list
   length_Nil  "length([]) = 0"
   length_Cons "length(x#xs) = Suc(length(xs))"
+primrec flat list
+  flat_Nil  "flat([]) = []"
+  flat_Cons "flat(x#xs) = x @ flat(xs)"
 defs
   nth_def "nth(n) == nat_rec(n, hd, %m r xs. r(tl(xs)))"
 end