# HG changeset patch
# User nipkow
# Date 853492186 -3600
# Node ID 0231e4f467f26d8f842f700d0e40bdae90931cf9
# Parent  282e9a9eae9d8965a4686cd69c1f196e20767c82
Got rid of Alls in List.
Added Ball_insert and Ball_Un in equalities.ML.

diff -r 282e9a9eae9d -r 0231e4f467f2 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Jan 17 10:04:28 1997 +0100
+++ b/src/HOL/List.ML	Fri Jan 17 10:09:46 1997 +0100
@@ -17,6 +17,7 @@
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "not_Cons_self";
+Addsimps [not_Cons_self];
 
 goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)";
 by (list.induct_tac "xs" 1);
@@ -32,21 +33,25 @@
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "append_assoc";
+Addsimps [append_assoc];
 
 goal List.thy "xs @ [] = xs";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "append_Nil2";
+Addsimps [append_Nil2];
 
 goal List.thy "(xs@ys = []) = (xs=[] & ys=[])";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "append_is_Nil";
+Addsimps [append_is_Nil];
 
 goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "same_append_eq";
+Addsimps [same_append_eq];
 
 goal List.thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
 by (list.induct_tac "xs" 1);
@@ -57,14 +62,15 @@
 
 goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_Nil2,append_assoc])));
+by (ALLGOALS Asm_simp_tac);
 qed "rev_append";
+Addsimps[rev_append];
 
 goal List.thy "rev(rev l) = l";
 by (list.induct_tac "l" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [rev_append])));
+by (ALLGOALS Asm_simp_tac);
 qed "rev_rev_ident";
-
+Addsimps[rev_rev_ident];
 
 (** mem **)
 
@@ -72,11 +78,13 @@
 by (list.induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_append";
+Addsimps[mem_append];
 
 goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_filter";
+Addsimps[mem_filter];
 
 (** set_of_list **)
 
@@ -85,6 +93,7 @@
 by (ALLGOALS Asm_simp_tac);
 by (Fast_tac 1);
 qed "set_of_list_append";
+Addsimps[set_of_list_append];
 
 goal thy "(x mem xs) = (x: set_of_list xs)";
 by (list.induct_tac "xs" 1);
@@ -100,17 +109,19 @@
 
 (** list_all **)
 
-goal List.thy "(Alls x:xs.True) = True";
+goal List.thy "list_all (%x.True) xs = True";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "list_all_True";
+Addsimps [list_all_True];
 
 goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-qed "list_all_conj";
+qed "list_all_append";
+Addsimps [list_all_append];
 
-goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))";
+goal List.thy "list_all P xs = (!x. x mem xs --> P(x))";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 by (Fast_tac 1);
@@ -127,6 +138,11 @@
 by (Fast_tac 1);
 qed "expand_list_case";
 
+val prems = goal List.thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
+by(list.induct_tac "xs" 1);
+by(REPEAT(resolve_tac prems 1));
+qed "list_cases";
+
 goal List.thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
 by (list.induct_tac "xs" 1);
 by (Fast_tac 1);
@@ -138,8 +154,9 @@
 
 goal List.thy  "flat(xs@ys) = flat(xs)@flat(ys)";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_assoc])));
+by (ALLGOALS Asm_simp_tac);
 qed"flat_append";
+Addsimps [flat_append];
 
 (** length **)
 
@@ -238,32 +255,26 @@
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_ident";
+Addsimps[map_ident];
 
 goal List.thy "map f (xs@ys) = map f xs @ map f ys";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_append";
+Addsimps[map_append];
 
 goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_compose";
+Addsimps[map_compose];
 
 goal List.thy "rev(map f l) = map f (rev l)";
 by (list.induct_tac "l" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [map_append])));
+by (ALLGOALS Asm_simp_tac);
 qed "rev_map_distrib";
 
 goal List.thy "rev(flat ls) = flat (map rev (rev ls))";
 by (list.induct_tac "ls" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps 
-       [map_append, flat_append, rev_append, append_Nil2])));
+by (ALLGOALS Asm_simp_tac);
 qed "rev_flat";
-
-Addsimps
-  [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
-   mem_append, mem_filter,
-   rev_append, rev_rev_ident,
-   map_ident, map_append, map_compose,
-   flat_append, list_all_True, list_all_conj];
-
diff -r 282e9a9eae9d -r 0231e4f467f2 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jan 17 10:04:28 1997 +0100
+++ b/src/HOL/List.thy	Fri Jan 17 10:09:46 1997 +0100
@@ -3,10 +3,7 @@
     Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
 
-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 set_of_list instead
+The datatype of finite lists.
 *)
 
 List = Arith +
@@ -35,18 +32,15 @@
   (* list Enumeration *)
   "@list"     :: args => 'a list                          ("[(_)]")
 
-  (* Special syntax for list_all and filter *)
-  "@Alls"     :: [idt, 'a list, bool] => bool             ("(2Alls _:_./ _)" 10)
+  (* Special syntax for filter *)
   "@filter"   :: [idt, 'a list, bool] => 'a list          ("(1[_:_ ./ _])")
 
 translations
   "[x, xs]"     == "x#[xs]"
   "[x]"         == "x#[]"
   "[x:xs . P]"  == "filter (%x.P) xs"
-  "Alls x:xs.P" == "list_all (%x.P) xs"
 
 syntax (symbols)
-  "op #"      :: ['a, 'a list] => 'a list                 (infixr "\\<bullet>" 65)
   "@filter"   :: [idt, 'a list, bool] => 'a list          ("(1[_\\<in>_ ./ _])")
 
 
diff -r 282e9a9eae9d -r 0231e4f467f2 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Jan 17 10:04:28 1997 +0100
+++ b/src/HOL/equalities.ML	Fri Jan 17 10:09:46 1997 +0100
@@ -455,6 +455,18 @@
 by (Fast_tac 1);
 qed "Un_INT_distrib2";
 
+
+section"Bounded quantifiers";
+
+goal Set.thy "(!x:insert a A.P x) = (P a & (!x:A.P x))";
+by (Fast_tac 1);
+qed "Ball_insert";
+
+goal Set.thy "(!x:A Un B.P x) = ((!x:A.P x) & (!x:B.P x))";
+by (Fast_tac 1);
+qed "Ball_Un";
+
+
 section "-";
 
 goal Set.thy "A-A = {}";