re-added mem and list_all

--- a/src/HOL/List.ML	Mon Sep 21 22:58:43 1998 +0200
+++ b/src/HOL/List.ML	Mon Sep 21 23:03:11 1998 +0200
@@ -469,21 +469,31 @@
 bind_thm("in_listsI",in_lists_conv_set RS iffD2);
 AddSIs [in_listsI];
 
+(** mem **)
+ 
+section "mem";
+
+Goal "(x mem xs) = (x: set xs)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "set_mem_eq";
+
+
 (** list_all **)
 
 section "list_all";
 
+Goal "list_all P xs = (!x:set xs. P x)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "list_all_conv";
+
 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)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "list_all_conv";
-
 
 (** filter **)
 
@@ -583,7 +593,7 @@
 qed_spec_mp "nth_map";
 Addsimps [nth_map];
 
-Goal "!n. n < length xs --> list_all P xs --> P(xs!n)";
+Goal "!n. n < length xs --> Ball (set xs) P --> P(xs!n)";
 by (induct_tac "xs" 1);
 (* case [] *)
 by (Simp_tac 1);
@@ -591,9 +601,9 @@
 by (rtac allI 1);
 by (induct_tac "n" 1);
 by Auto_tac;
-qed_spec_mp "list_all_nth";
+qed_spec_mp "list_ball_nth";
 
-Goal "!n. n < length xs --> xs!n mem xs";
+Goal "!n. n < length xs --> xs!n : set xs";
 by (induct_tac "xs" 1);
 (* case [] *)
 by (Simp_tac 1);
@@ -607,6 +617,7 @@
 qed_spec_mp "nth_mem";
 Addsimps [nth_mem];
 
+
 (** list update **)
 
 section "list update";

--- a/src/HOL/List.thy	Mon Sep 21 22:58:43 1998 +0200
+++ b/src/HOL/List.thy	Mon Sep 21 23:03:11 1998 +0200
@@ -17,7 +17,9 @@
   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
@@ -35,9 +37,6 @@
   lupdbinds  lupdbind
 
 syntax
-  mem         :: ['a, 'a list] => bool                    (infixl 55)
-  list_all    :: ('a => bool) => ('a list => bool)
-
   (* list Enumeration *)
   "@list"     :: args => 'a list                          ("[(_)]")
 
@@ -53,9 +52,6 @@
   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"
@@ -97,9 +93,15 @@
   "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

--- a/src/HOL/MiniML/Generalize.thy	Mon Sep 21 22:58:43 1998 +0200
+++ b/src/HOL/MiniML/Generalize.thy	Mon Sep 21 23:03:11 1998 +0200
@@ -26,7 +26,7 @@
   gen_ML_aux :: [nat list, typ] => type_scheme
 
 primrec
-  "gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
+  "gen_ML_aux A (TVar n) = (if (n: set A) then (FVar n) else (BVar n))"
   "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
 
 consts

--- a/src/HOL/MiniML/Type.ML	Mon Sep 21 22:58:43 1998 +0200
+++ b/src/HOL/MiniML/Type.ML	Mon Sep 21 23:03:11 1998 +0200
@@ -345,12 +345,12 @@
 
 Addsimps [free_tv_of_substitutions_extend_to_scheme_lists];
 
-Goal "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
+Goal "!!sch::type_scheme. (n : free_tv sch) = (n: set (free_tv_ML sch))";
 by (induct_tac "sch" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "free_tv_ML_scheme";
 
-Goal "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
+Goal "!!A::type_scheme list. (n : free_tv A) = (n: set (free_tv_ML A))";
 by (induct_tac "A" 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme]) 1);
@@ -405,7 +405,7 @@
 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
 qed "new_tv_subst";
 
-Goal "new_tv n x = list_all (new_tv n) x";
+Goal "new_tv n x = (!y:set x. new_tv n y)";
 by (induct_tac "x" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_tv_list";
@@ -488,8 +488,7 @@
 qed_spec_mp "new_tv_subst_scheme_list";
 Addsimps [new_tv_subst_scheme_list];
 
-Goal
-  "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
+Goal "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
 by (simp_tac (simpset() addsimps [new_tv_list]) 1);
 qed "new_tv_Suc_list";
 

--- a/src/HOL/W0/Type.ML	Mon Sep 21 22:58:43 1998 +0200
+++ b/src/HOL/W0/Type.ML	Mon Sep 21 23:03:11 1998 +0200
@@ -146,7 +146,7 @@
 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
 qed "new_tv_subst";
 
-Goal "new_tv n x = list_all (new_tv n) x";
+Goal "new_tv n x = (!y:set x. new_tv n y)";
 by (induct_tac "x" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_tv_list";
@@ -248,7 +248,7 @@
 Addsimps [new_tv_not_free_tv];
 
 Goal
-  "(t::typ) mem ts --> free_tv t <= free_tv ts";
+  "(t::typ): set ts --> free_tv t <= free_tv ts";
 by (induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);

--- a/src/HOL/ex/Recdefs.ML	Mon Sep 21 22:58:43 1998 +0200
+++ b/src/HOL/ex/Recdefs.ML	Mon Sep 21 23:03:11 1998 +0200
@@ -9,7 +9,7 @@
 
 Addsimps qsort.rules;
 
-Goal "(x mem qsort (ord,l)) = (x mem l)";
+Goal "(x: set (qsort (ord,l))) = (x: set l)";
 by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);