src/HOL/List.ML
changeset 4686 74a12e86b20b
parent 4681 a331c1f5a23e
child 4830 bd73675adbed
     1.1 --- a/src/HOL/List.ML	Fri Mar 06 18:25:28 1998 +0100
     1.2 +++ b/src/HOL/List.ML	Sat Mar 07 16:29:29 1998 +0100
     1.3 @@ -311,13 +311,13 @@
     1.4  
     1.5  goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
     1.6  by (induct_tac "xs" 1);
     1.7 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
     1.8 +by (ALLGOALS Asm_simp_tac);
     1.9  qed "mem_append";
    1.10  Addsimps[mem_append];
    1.11  
    1.12  goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
    1.13  by (induct_tac "xs" 1);
    1.14 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.15 +by (ALLGOALS Asm_simp_tac);
    1.16  qed "mem_filter";
    1.17  Addsimps[mem_filter];
    1.18  
    1.19 @@ -333,7 +333,7 @@
    1.20  
    1.21  goal thy "(x mem xs) = (x: set xs)";
    1.22  by (induct_tac "xs" 1);
    1.23 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.24 +by (ALLGOALS Asm_simp_tac);
    1.25  by (Blast_tac 1);
    1.26  qed "set_mem_eq";
    1.27  
    1.28 @@ -368,7 +368,7 @@
    1.29  
    1.30  goal thy "(x : set(filter P xs)) = (x : set xs & P x)";
    1.31  by (induct_tac "xs" 1);
    1.32 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.33 +by (ALLGOALS Asm_simp_tac);
    1.34  by(Blast_tac 1);
    1.35  qed "in_set_filter";
    1.36  Addsimps [in_set_filter];
    1.37 @@ -392,7 +392,7 @@
    1.38  
    1.39  goal thy "list_all P xs = (!x. x mem xs --> P(x))";
    1.40  by (induct_tac "xs" 1);
    1.41 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.42 +by (ALLGOALS Asm_simp_tac);
    1.43  by (Blast_tac 1);
    1.44  qed "list_all_mem_conv";
    1.45  
    1.46 @@ -403,7 +403,7 @@
    1.47  
    1.48  goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
    1.49  by (induct_tac "xs" 1);
    1.50 - by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.51 +by (ALLGOALS Asm_simp_tac);
    1.52  qed "filter_append";
    1.53  Addsimps [filter_append];
    1.54  
    1.55 @@ -421,7 +421,7 @@
    1.56  
    1.57  goal thy "length (filter P xs) <= length xs";
    1.58  by (induct_tac "xs" 1);
    1.59 - by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.60 +by (ALLGOALS Asm_simp_tac);
    1.61  qed "length_filter";
    1.62  
    1.63  
    1.64 @@ -512,7 +512,7 @@
    1.65  (* case 0 *)
    1.66  by (Asm_full_simp_tac 1);
    1.67  (* case Suc x *)
    1.68 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
    1.69 +by (Asm_full_simp_tac 1);
    1.70  qed_spec_mp "nth_mem";
    1.71  Addsimps [nth_mem];
    1.72  
    1.73 @@ -565,42 +565,40 @@
    1.74  
    1.75  goal thy "last(xs@[x]) = x";
    1.76  by (induct_tac "xs" 1);
    1.77 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.78 +by (ALLGOALS Asm_simp_tac);
    1.79  qed "last_snoc";
    1.80  Addsimps [last_snoc];
    1.81  
    1.82  goal thy "butlast(xs@[x]) = xs";
    1.83  by (induct_tac "xs" 1);
    1.84 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.85 +by (ALLGOALS Asm_simp_tac);
    1.86  qed "butlast_snoc";
    1.87  Addsimps [butlast_snoc];
    1.88  
    1.89  goal thy "length(butlast xs) = length xs - 1";
    1.90 -by(res_inst_tac [("xs","xs")] snoc_induct 1);
    1.91 -by(ALLGOALS Asm_simp_tac);
    1.92 +by (res_inst_tac [("xs","xs")] snoc_induct 1);
    1.93 +by (ALLGOALS Asm_simp_tac);
    1.94  qed "length_butlast";
    1.95  Addsimps [length_butlast];
    1.96  
    1.97  goal thy
    1.98    "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
    1.99  by (induct_tac "xs" 1);
   1.100 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   1.101 +by (ALLGOALS Asm_simp_tac);
   1.102  qed_spec_mp "butlast_append";
   1.103  
   1.104  goal thy "x:set(butlast xs) --> x:set xs";
   1.105  by (induct_tac "xs" 1);
   1.106 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   1.107 +by (ALLGOALS Asm_simp_tac);
   1.108  qed_spec_mp "in_set_butlastD";
   1.109  
   1.110  goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
   1.111 -by (asm_simp_tac (simpset() addsimps [butlast_append]
   1.112 -                          addsplits [expand_if]) 1);
   1.113 +by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
   1.114  by (blast_tac (claset() addDs [in_set_butlastD]) 1);
   1.115  qed "in_set_butlast_appendI1";
   1.116  
   1.117  goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
   1.118 -by (asm_simp_tac (simpset() addsimps [butlast_append]
   1.119 -                          addsplits [expand_if]) 1);
   1.120 +by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
   1.121  by (Clarify_tac 1);
   1.122  by (Full_simp_tac 1);
   1.123  qed "in_set_butlast_appendI2";
   1.124 @@ -751,15 +749,13 @@
   1.125  
   1.126  goal thy "takeWhile P xs @ dropWhile P xs = xs";
   1.127  by (induct_tac "xs" 1);
   1.128 - by (Simp_tac 1);
   1.129 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.130 +by (ALLGOALS Asm_full_simp_tac);
   1.131  qed "takeWhile_dropWhile_id";
   1.132  Addsimps [takeWhile_dropWhile_id];
   1.133  
   1.134  goal thy  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
   1.135  by (induct_tac "xs" 1);
   1.136 - by (Simp_tac 1);
   1.137 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.138 +by (ALLGOALS Asm_full_simp_tac);
   1.139  by (Blast_tac 1);
   1.140  bind_thm("takeWhile_append1", conjI RS (result() RS mp));
   1.141  Addsimps [takeWhile_append1];
   1.142 @@ -767,16 +763,14 @@
   1.143  goal thy
   1.144    "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
   1.145  by (induct_tac "xs" 1);
   1.146 - by (Simp_tac 1);
   1.147 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.148 +by (ALLGOALS Asm_full_simp_tac);
   1.149  bind_thm("takeWhile_append2", ballI RS (result() RS mp));
   1.150  Addsimps [takeWhile_append2];
   1.151  
   1.152  goal thy
   1.153    "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
   1.154  by (induct_tac "xs" 1);
   1.155 - by (Simp_tac 1);
   1.156 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.157 +by (ALLGOALS Asm_full_simp_tac);
   1.158  by (Blast_tac 1);
   1.159  bind_thm("dropWhile_append1", conjI RS (result() RS mp));
   1.160  Addsimps [dropWhile_append1];
   1.161 @@ -784,15 +778,13 @@
   1.162  goal thy
   1.163    "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
   1.164  by (induct_tac "xs" 1);
   1.165 - by (Simp_tac 1);
   1.166 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.167 +by (ALLGOALS Asm_full_simp_tac);
   1.168  bind_thm("dropWhile_append2", ballI RS (result() RS mp));
   1.169  Addsimps [dropWhile_append2];
   1.170  
   1.171  goal thy "x:set(takeWhile P xs) --> x:set xs & P x";
   1.172  by (induct_tac "xs" 1);
   1.173 - by (Simp_tac 1);
   1.174 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.175 +by (ALLGOALS Asm_full_simp_tac);
   1.176  qed_spec_mp"set_take_whileD";
   1.177  
   1.178  qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
   1.179 @@ -805,21 +797,18 @@
   1.180  goal thy "set(remdups xs) = set xs";
   1.181  by (induct_tac "xs" 1);
   1.182   by (Simp_tac 1);
   1.183 -by (asm_full_simp_tac (simpset() addsimps [insert_absorb]
   1.184 -                                 addsplits [expand_if]) 1);
   1.185 +by (asm_full_simp_tac (simpset() addsimps [insert_absorb]) 1);
   1.186  qed "set_remdups";
   1.187  Addsimps [set_remdups];
   1.188  
   1.189  goal thy "nodups(remdups xs)";
   1.190  by (induct_tac "xs" 1);
   1.191 - by (Simp_tac 1);
   1.192 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.193 +by (ALLGOALS Asm_full_simp_tac);
   1.194  qed "nodups_remdups";
   1.195  
   1.196  goal thy "nodups xs --> nodups (filter P xs)";
   1.197  by (induct_tac "xs" 1);
   1.198 - by (Simp_tac 1);
   1.199 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.200 +by (ALLGOALS Asm_full_simp_tac);
   1.201  qed_spec_mp "nodups_filter";
   1.202  
   1.203  (** replicate **)