# HG changeset patch
# User paulson
# Date 835107630 -7200
# Node ID debfc40b7756fdbf28476c6ca4eed0289f6692e4
# Parent  9083542fd8614426abe0fd9d32795edf5f34601e
Addition of setOfList

diff -r 9083542fd861 -r debfc40b7756 src/HOL/List.ML
--- a/src/HOL/List.ML	Tue Jun 18 16:18:44 1996 +0200
+++ b/src/HOL/List.ML	Tue Jun 18 16:20:30 1996 +0200
@@ -80,6 +80,21 @@
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_filter";
 
+(** setOfList **)
+
+goal thy "setOfList (xs@ys) = (setOfList xs Un setOfList ys)";
+by (list.induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+by (Fast_tac 1);
+qed "setOfList_append";
+
+goal thy "(x mem xs) = (x: setOfList xs)";
+by (list.induct_tac "xs" 1);
+by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (Fast_tac 1);
+qed "setOfList_mem_eq";
+
+
 (** list_all **)
 
 goal List.thy "(Alls x:xs.True) = True";
diff -r 9083542fd861 -r debfc40b7756 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jun 18 16:18:44 1996 +0200
+++ b/src/HOL/List.thy	Tue Jun 18 16:20:30 1996 +0200
@@ -5,6 +5,8 @@
 
 Definition of type 'a list as a datatype. This allows primrec to work.
 
+TODO: delete list_all from this theory and from ex/Sorting, etc.
+      use setOfList instead
 *)
 
 List = Arith +
@@ -20,6 +22,7 @@
   foldl     :: [['b,'a] => 'b, 'b, 'a list] => 'b
   hd        :: 'a list => 'a
   length    :: 'a list => nat
+  setOfList :: ('a list => 'a set)
   list_all  :: ('a => bool) => ('a list => bool)
   map       :: ('a=>'b) => ('a list => 'b list)
   mem       :: ['a, 'a list] => bool                    (infixl 55)
@@ -56,6 +59,9 @@
 primrec "op mem" list
   mem_Nil  "x mem [] = False"
   mem_Cons "x mem (y#ys) = (if y=x then True else x mem ys)"
+primrec setOfList list
+  setOfList_Nil  "setOfList [] = {}"
+  setOfList_Cons "setOfList (x#xs) = insert x (setOfList xs)"
 primrec list_all list
   list_all_Nil  "list_all P [] = True"
   list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"