src/HOL/List.ML
changeset 4089 96fba19bcbe2
parent 4069 d6d06a03a2e9
child 4132 daff3c9987cc
     1.1 --- a/src/HOL/List.ML	Mon Nov 03 12:12:10 1997 +0100
     1.2 +++ b/src/HOL/List.ML	Mon Nov 03 12:13:18 1997 +0100
     1.3 @@ -40,8 +40,8 @@
     1.4  
     1.5  goal thy "lists (A Int B) = lists A Int lists B";
     1.6  br (mono_Int RS equalityI) 1;
     1.7 -by (simp_tac (!simpset addsimps [mono_def, lists_mono]) 1);
     1.8 -by (blast_tac (!claset addSIs [lists_IntI]) 1);
     1.9 +by (simp_tac (simpset() addsimps [mono_def, lists_mono]) 1);
    1.10 +by (blast_tac (claset() addSIs [lists_IntI]) 1);
    1.11  qed "lists_Int_eq";
    1.12  Addsimps [lists_Int_eq];
    1.13  
    1.14 @@ -155,11 +155,11 @@
    1.15   by(rtac allI 1);
    1.16   by(exhaust_tac "ys" 1);
    1.17    by(Asm_simp_tac 1);
    1.18 - by(fast_tac (!claset addIs [less_add_Suc2] addss !simpset
    1.19 + by(fast_tac (claset() addIs [less_add_Suc2] addss simpset()
    1.20                        addEs [less_not_refl2 RSN (2,rev_notE)]) 1);
    1.21  by(rtac allI 1);
    1.22  by(exhaust_tac "ys" 1);
    1.23 - by(fast_tac (!claset addIs [less_add_Suc2] addss !simpset
    1.24 + by(fast_tac (claset() addIs [less_add_Suc2] addss simpset()
    1.25                        addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
    1.26  by(Asm_simp_tac 1);
    1.27  qed_spec_mp "append_eq_append_conv";
    1.28 @@ -194,17 +194,17 @@
    1.29  qed "hd_append";
    1.30  
    1.31  goal thy "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs";
    1.32 -by (asm_simp_tac (!simpset addsimps [hd_append]
    1.33 +by (asm_simp_tac (simpset() addsimps [hd_append]
    1.34                             addsplits [split_list_case]) 1);
    1.35  qed "hd_append2";
    1.36  Addsimps [hd_append2];
    1.37  
    1.38  goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
    1.39 -by (simp_tac (!simpset addsplits [split_list_case]) 1);
    1.40 +by (simp_tac (simpset() addsplits [split_list_case]) 1);
    1.41  qed "tl_append";
    1.42  
    1.43  goal thy "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
    1.44 -by (asm_simp_tac (!simpset addsimps [tl_append]
    1.45 +by (asm_simp_tac (simpset() addsimps [tl_append]
    1.46                             addsplits [split_list_case]) 1);
    1.47  qed "tl_append2";
    1.48  Addsimps [tl_append2];
    1.49 @@ -301,13 +301,13 @@
    1.50  
    1.51  goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
    1.52  by (induct_tac "xs" 1);
    1.53 -by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
    1.54 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.55  qed "mem_append";
    1.56  Addsimps[mem_append];
    1.57  
    1.58  goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
    1.59  by (induct_tac "xs" 1);
    1.60 -by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
    1.61 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.62  qed "mem_filter";
    1.63  Addsimps[mem_filter];
    1.64  
    1.65 @@ -323,7 +323,7 @@
    1.66  
    1.67  goal thy "(x mem xs) = (x: set xs)";
    1.68  by (induct_tac "xs" 1);
    1.69 -by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
    1.70 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.71  by (Blast_tac 1);
    1.72  qed "set_mem_eq";
    1.73  
    1.74 @@ -369,7 +369,7 @@
    1.75  
    1.76  goal thy "list_all P xs = (!x. x mem xs --> P(x))";
    1.77  by (induct_tac "xs" 1);
    1.78 -by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
    1.79 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.80  by (Blast_tac 1);
    1.81  qed "list_all_mem_conv";
    1.82  
    1.83 @@ -380,13 +380,13 @@
    1.84  
    1.85  goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
    1.86  by (induct_tac "xs" 1);
    1.87 - by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
    1.88 + by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.89  qed "filter_append";
    1.90  Addsimps [filter_append];
    1.91  
    1.92  goal thy "size (filter P xs) <= size xs";
    1.93  by (induct_tac "xs" 1);
    1.94 - by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
    1.95 + by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    1.96  qed "filter_size";
    1.97  
    1.98  
    1.99 @@ -481,7 +481,7 @@
   1.100  (* case 0 *)
   1.101  by (Asm_full_simp_tac 1);
   1.102  (* case Suc x *)
   1.103 -by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   1.104 +by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.105  qed_spec_mp "nth_mem";
   1.106  Addsimps [nth_mem];
   1.107  
   1.108 @@ -489,35 +489,35 @@
   1.109  
   1.110  goal thy "last(xs@[x]) = x";
   1.111  by(induct_tac "xs" 1);
   1.112 -by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   1.113 +by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   1.114  qed "last_snoc";
   1.115  Addsimps [last_snoc];
   1.116  
   1.117  goal thy "butlast(xs@[x]) = xs";
   1.118  by(induct_tac "xs" 1);
   1.119 -by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   1.120 +by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   1.121  qed "butlast_snoc";
   1.122  Addsimps [butlast_snoc];
   1.123  
   1.124  goal thy
   1.125    "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
   1.126  by(induct_tac "xs" 1);
   1.127 -by(ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
   1.128 +by(ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   1.129  qed_spec_mp "butlast_append";
   1.130  
   1.131  goal thy "x:set(butlast xs) --> x:set xs";
   1.132  by(induct_tac "xs" 1);
   1.133 -by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   1.134 +by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   1.135  qed_spec_mp "in_set_butlastD";
   1.136  
   1.137  goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
   1.138 -by(asm_simp_tac (!simpset addsimps [butlast_append]
   1.139 +by(asm_simp_tac (simpset() addsimps [butlast_append]
   1.140                            addsplits [expand_if]) 1);
   1.141 -by(blast_tac (!claset addDs [in_set_butlastD]) 1);
   1.142 +by(blast_tac (claset() addDs [in_set_butlastD]) 1);
   1.143  qed "in_set_butlast_appendI1";
   1.144  
   1.145  goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
   1.146 -by(asm_simp_tac (!simpset addsimps [butlast_append]
   1.147 +by(asm_simp_tac (simpset() addsimps [butlast_append]
   1.148                            addsplits [expand_if]) 1);
   1.149  by(Clarify_tac 1);
   1.150  by(Full_simp_tac 1);
   1.151 @@ -670,14 +670,14 @@
   1.152  goal thy "takeWhile P xs @ dropWhile P xs = xs";
   1.153  by (induct_tac "xs" 1);
   1.154   by (Simp_tac 1);
   1.155 -by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   1.156 +by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.157  qed "takeWhile_dropWhile_id";
   1.158  Addsimps [takeWhile_dropWhile_id];
   1.159  
   1.160  goal thy  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
   1.161  by (induct_tac "xs" 1);
   1.162   by (Simp_tac 1);
   1.163 -by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   1.164 +by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.165  by (Blast_tac 1);
   1.166  bind_thm("takeWhile_append1", conjI RS (result() RS mp));
   1.167  Addsimps [takeWhile_append1];
   1.168 @@ -686,7 +686,7 @@
   1.169    "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
   1.170  by (induct_tac "xs" 1);
   1.171   by (Simp_tac 1);
   1.172 -by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   1.173 +by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.174  bind_thm("takeWhile_append2", ballI RS (result() RS mp));
   1.175  Addsimps [takeWhile_append2];
   1.176  
   1.177 @@ -694,7 +694,7 @@
   1.178    "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
   1.179  by (induct_tac "xs" 1);
   1.180   by (Simp_tac 1);
   1.181 -by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   1.182 +by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.183  by (Blast_tac 1);
   1.184  bind_thm("dropWhile_append1", conjI RS (result() RS mp));
   1.185  Addsimps [dropWhile_append1];
   1.186 @@ -703,14 +703,14 @@
   1.187    "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
   1.188  by (induct_tac "xs" 1);
   1.189   by (Simp_tac 1);
   1.190 -by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   1.191 +by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.192  bind_thm("dropWhile_append2", ballI RS (result() RS mp));
   1.193  Addsimps [dropWhile_append2];
   1.194  
   1.195  goal thy "x:set(takeWhile P xs) --> x:set xs & P x";
   1.196  by (induct_tac "xs" 1);
   1.197   by (Simp_tac 1);
   1.198 -by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   1.199 +by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   1.200  qed_spec_mp"set_take_whileD";
   1.201  
   1.202  (** replicate **)
   1.203 @@ -722,6 +722,6 @@
   1.204  val lemma = result();
   1.205  
   1.206  goal thy "!!n. n ~= 0 ==> set(replicate n x) = {x}";
   1.207 -by(fast_tac (!claset addSDs [not0_implies_Suc] addSIs [lemma]) 1);
   1.208 +by(fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
   1.209  qed "set_replicate";
   1.210  Addsimps [set_replicate];