src/HOL/List.ML
changeset 4423 a129b817b58a
parent 4132 daff3c9987cc
child 4502 337c073de95e
     1.1 --- a/src/HOL/List.ML	Tue Dec 16 15:17:26 1997 +0100
     1.2 +++ b/src/HOL/List.ML	Tue Dec 16 17:58:03 1997 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4  qed_spec_mp "lists_IntI";
     1.5  
     1.6  goal thy "lists (A Int B) = lists A Int lists B";
     1.7 -br (mono_Int RS equalityI) 1;
     1.8 +by (rtac (mono_Int RS equalityI) 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 @@ -85,8 +85,8 @@
    1.13  Addsimps [length_rev];
    1.14  
    1.15  goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = pred(length xs)";
    1.16 -by(exhaust_tac "xs" 1);
    1.17 -by(ALLGOALS Asm_full_simp_tac);
    1.18 +by (exhaust_tac "xs" 1);
    1.19 +by (ALLGOALS Asm_full_simp_tac);
    1.20  qed "length_tl";
    1.21  Addsimps [length_tl];
    1.22  
    1.23 @@ -151,17 +151,17 @@
    1.24  
    1.25  goal thy "!ys. length xs = length ys | length us = length vs \
    1.26  \              --> (xs@us = ys@vs) = (xs=ys & us=vs)";
    1.27 -by(induct_tac "xs" 1);
    1.28 - by(rtac allI 1);
    1.29 - by(exhaust_tac "ys" 1);
    1.30 -  by(Asm_simp_tac 1);
    1.31 - by(fast_tac (claset() addIs [less_add_Suc2] addss simpset()
    1.32 +by (induct_tac "xs" 1);
    1.33 + by (rtac allI 1);
    1.34 + by (exhaust_tac "ys" 1);
    1.35 +  by (Asm_simp_tac 1);
    1.36 + by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()
    1.37                        addEs [less_not_refl2 RSN (2,rev_notE)]) 1);
    1.38 -by(rtac allI 1);
    1.39 -by(exhaust_tac "ys" 1);
    1.40 - by(fast_tac (claset() addIs [less_add_Suc2] addss simpset()
    1.41 +by (rtac allI 1);
    1.42 +by (exhaust_tac "ys" 1);
    1.43 + by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()
    1.44                        addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
    1.45 -by(Asm_simp_tac 1);
    1.46 +by (Asm_simp_tac 1);
    1.47  qed_spec_mp "append_eq_append_conv";
    1.48  Addsimps [append_eq_append_conv];
    1.49  
    1.50 @@ -246,22 +246,22 @@
    1.51  (* a congruence rule for map: *)
    1.52  goal thy
    1.53   "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
    1.54 -by(rtac impI 1);
    1.55 -by(hyp_subst_tac 1);
    1.56 -by(induct_tac "ys" 1);
    1.57 -by(ALLGOALS Asm_simp_tac);
    1.58 +by (rtac impI 1);
    1.59 +by (hyp_subst_tac 1);
    1.60 +by (induct_tac "ys" 1);
    1.61 +by (ALLGOALS Asm_simp_tac);
    1.62  val lemma = result();
    1.63  bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
    1.64  
    1.65  goal List.thy "(map f xs = []) = (xs = [])";
    1.66 -by(induct_tac "xs" 1);
    1.67 -by(ALLGOALS Asm_simp_tac);
    1.68 +by (induct_tac "xs" 1);
    1.69 +by (ALLGOALS Asm_simp_tac);
    1.70  qed "map_is_Nil_conv";
    1.71  AddIffs [map_is_Nil_conv];
    1.72  
    1.73  goal List.thy "([] = map f xs) = (xs = [])";
    1.74 -by(induct_tac "xs" 1);
    1.75 -by(ALLGOALS Asm_simp_tac);
    1.76 +by (induct_tac "xs" 1);
    1.77 +by (ALLGOALS Asm_simp_tac);
    1.78  qed "Nil_is_map_conv";
    1.79  AddIffs [Nil_is_map_conv];
    1.80  
    1.81 @@ -283,14 +283,14 @@
    1.82  Addsimps[rev_rev_ident];
    1.83  
    1.84  goal thy "(rev xs = []) = (xs = [])";
    1.85 -by(induct_tac "xs" 1);
    1.86 -by(ALLGOALS Asm_simp_tac);
    1.87 +by (induct_tac "xs" 1);
    1.88 +by (ALLGOALS Asm_simp_tac);
    1.89  qed "rev_is_Nil_conv";
    1.90  AddIffs [rev_is_Nil_conv];
    1.91  
    1.92  goal thy "([] = rev xs) = (xs = [])";
    1.93 -by(induct_tac "xs" 1);
    1.94 -by(ALLGOALS Asm_simp_tac);
    1.95 +by (induct_tac "xs" 1);
    1.96 +by (ALLGOALS Asm_simp_tac);
    1.97  qed "Nil_is_rev_conv";
    1.98  AddIffs [Nil_is_rev_conv];
    1.99  
   1.100 @@ -401,14 +401,14 @@
   1.101  Addsimps [concat_append];
   1.102  
   1.103  goal thy "(concat xss = []) = (!xs:set xss. xs=[])";
   1.104 -by(induct_tac "xss" 1);
   1.105 -by(ALLGOALS Asm_simp_tac);
   1.106 +by (induct_tac "xss" 1);
   1.107 +by (ALLGOALS Asm_simp_tac);
   1.108  qed "concat_eq_Nil_conv";
   1.109  AddIffs [concat_eq_Nil_conv];
   1.110  
   1.111  goal thy "([] = concat xss) = (!xs:set xss. xs=[])";
   1.112 -by(induct_tac "xss" 1);
   1.113 -by(ALLGOALS Asm_simp_tac);
   1.114 +by (induct_tac "xss" 1);
   1.115 +by (ALLGOALS Asm_simp_tac);
   1.116  qed "Nil_eq_concat_conv";
   1.117  AddIffs [Nil_eq_concat_conv];
   1.118  
   1.119 @@ -488,39 +488,39 @@
   1.120  (** last & butlast **)
   1.121  
   1.122  goal thy "last(xs@[x]) = x";
   1.123 -by(induct_tac "xs" 1);
   1.124 -by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   1.125 +by (induct_tac "xs" 1);
   1.126 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   1.127  qed "last_snoc";
   1.128  Addsimps [last_snoc];
   1.129  
   1.130  goal thy "butlast(xs@[x]) = xs";
   1.131 -by(induct_tac "xs" 1);
   1.132 -by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   1.133 +by (induct_tac "xs" 1);
   1.134 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   1.135  qed "butlast_snoc";
   1.136  Addsimps [butlast_snoc];
   1.137  
   1.138  goal thy
   1.139    "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
   1.140 -by(induct_tac "xs" 1);
   1.141 -by(ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   1.142 +by (induct_tac "xs" 1);
   1.143 +by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   1.144  qed_spec_mp "butlast_append";
   1.145  
   1.146  goal thy "x:set(butlast xs) --> x:set xs";
   1.147 -by(induct_tac "xs" 1);
   1.148 -by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   1.149 +by (induct_tac "xs" 1);
   1.150 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   1.151  qed_spec_mp "in_set_butlastD";
   1.152  
   1.153  goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
   1.154 -by(asm_simp_tac (simpset() addsimps [butlast_append]
   1.155 +by (asm_simp_tac (simpset() addsimps [butlast_append]
   1.156                            addsplits [expand_if]) 1);
   1.157 -by(blast_tac (claset() addDs [in_set_butlastD]) 1);
   1.158 +by (blast_tac (claset() addDs [in_set_butlastD]) 1);
   1.159  qed "in_set_butlast_appendI1";
   1.160  
   1.161  goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
   1.162 -by(asm_simp_tac (simpset() addsimps [butlast_append]
   1.163 +by (asm_simp_tac (simpset() addsimps [butlast_append]
   1.164                            addsplits [expand_if]) 1);
   1.165 -by(Clarify_tac 1);
   1.166 -by(Full_simp_tac 1);
   1.167 +by (Clarify_tac 1);
   1.168 +by (Full_simp_tac 1);
   1.169  qed "in_set_butlast_appendI2";
   1.170  
   1.171  (** take  & drop **)
   1.172 @@ -720,11 +720,11 @@
   1.173  section "replicate";
   1.174  
   1.175  goal thy "set(replicate (Suc n) x) = {x}";
   1.176 -by(induct_tac "n" 1);
   1.177 -by(ALLGOALS Asm_full_simp_tac);
   1.178 +by (induct_tac "n" 1);
   1.179 +by (ALLGOALS Asm_full_simp_tac);
   1.180  val lemma = result();
   1.181  
   1.182  goal thy "!!n. n ~= 0 ==> set(replicate n x) = {x}";
   1.183 -by(fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
   1.184 +by (fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
   1.185  qed "set_replicate";
   1.186  Addsimps [set_replicate];