src/HOL/List.ML

--- a/src/HOL/List.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/List.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -38,8 +38,8 @@
 qed "expand_list_case";
 
 val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
-by(induct_tac "xs" 1);
-by(REPEAT(resolve_tac prems 1));
+by (induct_tac "xs" 1);
+by (REPEAT(resolve_tac prems 1));
 qed "list_cases";
 
 goal thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
@@ -73,7 +73,7 @@
 goal thy "([] = xs@ys) = (xs=[] & ys=[])";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "Nil_is_append_conv";
 AddIffs [Nil_is_append_conv];
 
@@ -84,19 +84,19 @@
 AddIffs [same_append_eq];
 
 goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
-by(induct_tac "xs" 1);
- br allI 1;
- by(induct_tac "ys" 1);
-  by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(induct_tac "ys" 1);
- by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+ by (rtac allI 1);
+ by (induct_tac "ys" 1);
+  by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (induct_tac "ys" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "append1_eq_conv";
 AddIffs [append1_eq_conv];
 
 goal thy "xs ~= [] --> hd xs # tl xs = xs";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "hd_Cons_tl";
 Addsimps [hd_Cons_tl];
 
@@ -106,15 +106,15 @@
 qed "hd_append";
 
 goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
-by(simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
+by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
 qed "tl_append";
 
 (** map **)
 
 goal thy
   "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
 
 goal thy "map (%x.x) = (%xs.xs)";
@@ -190,20 +190,20 @@
 qed "set_of_list_subset_Cons";
 
 goal thy "(set_of_list xs = {}) = (xs = [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "set_of_list_empty";
 Addsimps [set_of_list_empty];
 
 goal thy "set_of_list(rev xs) = set_of_list(xs)";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "set_of_list_rev";
 Addsimps [set_of_list_rev];
 
 goal thy "set_of_list(map f xs) = f``(set_of_list xs)";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "set_of_list_map";
 Addsimps [set_of_list_map];
 
@@ -232,14 +232,14 @@
 (** filter **)
 
 goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
-by(induct_tac "xs" 1);
- by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (induct_tac "xs" 1);
+ by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "filter_append";
 Addsimps [filter_append];
 
 goal thy "size (filter P xs) <= size xs";
-by(induct_tac "xs" 1);
- by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (induct_tac "xs" 1);
+ by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "filter_size";
 
 
@@ -277,14 +277,14 @@
 Addsimps [length_rev];
 
 goal thy "(length xs = 0) = (xs = [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "length_0_conv";
 AddIffs [length_0_conv];
 
 goal thy "(0 < length xs) = (xs ~= [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "length_greater_0_conv";
 AddIffs [length_greater_0_conv];
 
@@ -294,14 +294,14 @@
 goal thy
   "!xs. nth n (xs@ys) = \
 \          (if n < length xs then nth n xs else nth (n - length xs) ys)";
-by(nat_ind_tac "n" 1);
- by(Asm_simp_tac 1);
- br allI 1;
- by(exhaust_tac "xs" 1);
-  by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (Asm_simp_tac 1);
+ by (rtac allI 1);
+ by (exhaust_tac "xs" 1);
+  by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "nth_append";
 
 goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
@@ -365,118 +365,118 @@
 Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
 
 goal thy "!xs. length(take n xs) = min (length xs) n";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "length_take";
 Addsimps [length_take];
 
 goal thy "!xs. length(drop n xs) = (length xs - n)";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "length_drop";
 Addsimps [length_drop];
 
 goal thy "!xs. length xs <= n --> take n xs = xs";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "take_all";
 
 goal thy "!xs. length xs <= n --> drop n xs = []";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "drop_all";
 
 goal thy 
   "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "take_append";
 Addsimps [take_append];
 
 goal thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "drop_append";
 Addsimps [drop_append];
 
 goal thy "!xs n. take n (take m xs) = take (min n m) xs"; 
-by(nat_ind_tac "m" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "m" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "take_take";
 
 goal thy "!xs. drop n (drop m xs) = drop (n + m) xs"; 
-by(nat_ind_tac "m" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "m" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "drop_drop";
 
 goal thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
-by(nat_ind_tac "m" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "m" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "take_drop";
 
 goal thy "!xs. take n (map f xs) = map f (take n xs)"; 
-by(nat_ind_tac "n" 1);
-by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "take_map"; 
 
 goal thy "!xs. drop n (map f xs) = map f (drop n xs)"; 
-by(nat_ind_tac "n" 1);
-by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "drop_map";
 
 goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
-by(induct_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
-by(strip_tac 1);
-by(exhaust_tac "n" 1);
- by(Blast_tac 1);
-by(exhaust_tac "i" 1);
-by(ALLGOALS Asm_full_simp_tac);
+by (induct_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (strip_tac 1);
+by (exhaust_tac "n" 1);
+ by (Blast_tac 1);
+by (exhaust_tac "i" 1);
+by (ALLGOALS Asm_full_simp_tac);
 qed_spec_mp "nth_take";
 Addsimps [nth_take];
 
 goal thy  "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "nth_drop";
 Addsimps [nth_drop];
 
@@ -484,41 +484,41 @@
 
 goal thy
   "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Blast_tac 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (Blast_tac 1);
 bind_thm("takeWhile_append1", conjI RS (result() RS mp));
 Addsimps [takeWhile_append1];
 
 goal thy
   "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 bind_thm("takeWhile_append2", ballI RS (result() RS mp));
 Addsimps [takeWhile_append2];
 
 goal thy
   "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Blast_tac 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (Blast_tac 1);
 bind_thm("dropWhile_append1", conjI RS (result() RS mp));
 Addsimps [dropWhile_append1];
 
 goal thy
   "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 bind_thm("dropWhile_append2", ballI RS (result() RS mp));
 Addsimps [dropWhile_append2];
 
 goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 qed_spec_mp"set_of_list_take_whileD";