# HG changeset patch
# User oheimb
# Date 905354366 -7200
# Node ID e2459d18ff4735fac734e8f7dfb508f1e5a033e3
# Parent  e60b8698ab1568eeabf1a63b95a5316ba2df6307
changed constants mem and list_all to mere translations
added filter_is_subset

diff -r e60b8698ab15 -r e2459d18ff47 src/HOL/List.ML
--- a/src/HOL/List.ML	Wed Sep 09 17:14:19 1998 +0200
+++ b/src/HOL/List.ML	Wed Sep 09 17:19:26 1998 +0200
@@ -403,22 +403,6 @@
   impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
 
 
-(** mem **)
-
-section "mem";
-
-Goal "x mem (xs@ys) = (x mem xs | x mem ys)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "mem_append";
-Addsimps[mem_append];
-
-Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "mem_filter";
-Addsimps[mem_filter];
-
 (** set **)
 
 section "set";
@@ -434,11 +418,6 @@
 qed "set_append";
 Addsimps[set_append];
 
-Goal "(x mem xs) = (x: set xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "set_mem_eq";
-
 Goal "set l <= set (x#l)";
 by Auto_tac;
 qed "set_subset_Cons";
@@ -461,7 +440,7 @@
 qed "set_map";
 Addsimps [set_map];
 
-Goal "(x : set(filter P xs)) = (x : set xs & P x)";
+Goal "(x : set (filter P xs)) = (x : set xs & P x)";
 by (induct_tac "xs" 1);
 by Auto_tac;
 qed "in_set_filter";
@@ -494,22 +473,16 @@
 
 section "list_all";
 
-Goal "list_all (%x. True) xs = True";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "list_all_True";
-Addsimps [list_all_True];
-
-Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
+Goal "list_all P (xs@ys) = (list_all P xs & list_all P ys)";
 by (induct_tac "xs" 1);
 by Auto_tac;
 qed "list_all_append";
 Addsimps [list_all_append];
 
-Goal "list_all P xs = (!x. x mem xs --> P(x))";
+Goal "list_all P xs = (!x. x mem xs --> P x)";
 by (induct_tac "xs" 1);
 by Auto_tac;
-qed "list_all_mem_conv";
+qed "list_all_conv";
 
 
 (** filter **)
@@ -538,9 +511,13 @@
 by (induct_tac "xs" 1);
 by Auto_tac;
 qed "length_filter";
-
+Addsimps[length_filter];
 
-(** concat **)
+Goal "set (filter P xs) <= set xs";
+by Auto_tac;
+qed "filter_is_subset";
+Addsimps [filter_is_subset];
+
 
 section "concat";
 
diff -r e60b8698ab15 -r e2459d18ff47 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Sep 09 17:14:19 1998 +0200
+++ b/src/HOL/List.thy	Wed Sep 09 17:19:26 1998 +0200
@@ -17,9 +17,7 @@
   foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
   hd, last    :: 'a list => 'a
   set         :: '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)
   nth         :: ['a list, nat] => 'a			  (infixl "!" 100)
   list_update :: 'a list => nat => 'a => 'a list
   take, drop  :: [nat, 'a list] => 'a list
@@ -37,6 +35,9 @@
   lupdbinds  lupdbind
 
 syntax
+  mem         :: ['a, 'a list] => bool                    (infixl 55)
+  list_all    :: ('a => bool) => ('a list => bool)
+
   (* list Enumeration *)
   "@list"     :: args => 'a list                          ("[(_)]")
 
@@ -52,6 +53,9 @@
   upto        :: nat => nat => nat list                   ("(1[_../_])")
 
 translations
+  "x mem xs"      == "x:set xs"
+  "list_all P xs" == "Ball (set xs) P"
+  
   "[x, xs]"     == "x#[xs]"
   "[x]"         == "x#[]"
   "[x:xs . P]"  == "filter (%x. P) xs"
@@ -93,15 +97,9 @@
   "butlast [] = []"
   "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
 primrec
-  "x mem [] = False"
-  "x mem (y#ys) = (if y=x then True else x mem ys)"
-primrec
   "set [] = {}"
   "set (x#xs) = insert x (set xs)"
 primrec
-  list_all_Nil  "list_all P [] = True"
-  list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
-primrec
   "map f [] = []"
   "map f (x#xs) = f(x)#map f xs"
 primrec
@@ -151,7 +149,7 @@
   "remdups [] = []"
   "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
 primrec
-  replicate_0   "replicate 0 x       = []"
+  replicate_0   "replicate  0      x = []"
   replicate_Suc "replicate (Suc n) x = x # replicate n x"
 
 (** Lexcicographic orderings on lists **)