# HG changeset patch
# User paulson
# Date 840537418 -7200
# Node ID 1957ae3f930191ede34faecbfd6a64c78583941f
# Parent  1150f128c7fecb13bc42299af3faa50425c662d5
Addition of function set_of_list

diff -r 1150f128c7fe -r 1957ae3f9301 src/ZF/List.ML
--- a/src/ZF/List.ML	Tue Aug 20 12:32:16 1996 +0200
+++ b/src/ZF/List.ML	Tue Aug 20 12:36:58 1996 +0200
@@ -213,6 +213,25 @@
 qed "flat_type";
 
 
+(** set_of_list **)
+
+val [set_of_list_Nil,set_of_list_Cons] = list_recs set_of_list_def;
+
+goalw List.thy [set_of_list_def] 
+    "!!l. l: list(A) ==> set_of_list(l) : Pow(A)";
+be list_rec_type 1;
+by (ALLGOALS (fast_tac ZF_cs));
+qed "set_of_list_type";
+
+goal List.thy
+    "!!l. xs: list(A) ==> \
+\         set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)";
+by (etac list.induct 1);
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [set_of_list_Nil,set_of_list_Cons,
+					    app_Nil,app_Cons,Un_cons])));
+qed "set_of_list_append";
+
+
 (** list_add **)
 
 val [list_add_Nil,list_add_Cons] = list_recs list_add_def;
diff -r 1150f128c7fe -r 1957ae3f9301 src/ZF/List.thy
--- a/src/ZF/List.thy	Tue Aug 20 12:32:16 1996 +0200
+++ b/src/ZF/List.thy	Tue Aug 20 12:36:58 1996 +0200
@@ -49,6 +49,8 @@
   length :: i=>i
   "length(l)   == list_rec(l,  0,  %x xs r. succ(r))"
 
+  set_of_list :: i=>i
+  "set_of_list(l)   == list_rec(l,  0,  %x xs r. cons(x,r))"
 
 consts  (*Cannot use constdefs because @ is not an identifier*)
   "@"        :: [i,i]=>i                        (infixr 60)