1.1 --- a/src/HOL/List.ML	Thu Nov 11 11:29:11 1999 +0100
     1.2 +++ b/src/HOL/List.ML	Thu Nov 11 11:43:14 1999 +0100
     1.3 @@ -340,17 +340,44 @@
     1.4  bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
     1.5  
     1.6  Goal "(map f xs = []) = (xs = [])";
     1.7 -by (induct_tac "xs" 1);
     1.8 +by (exhaust_tac "xs" 1);
     1.9  by Auto_tac;
    1.10  qed "map_is_Nil_conv";
    1.11  AddIffs [map_is_Nil_conv];
    1.12  
    1.13  Goal "([] = map f xs) = (xs = [])";
    1.14 -by (induct_tac "xs" 1);
    1.15 +by (exhaust_tac "xs" 1);
    1.16  by Auto_tac;
    1.17  qed "Nil_is_map_conv";
    1.18  AddIffs [Nil_is_map_conv];
    1.19  
    1.20 +Goal "(map f xs = y#ys) = (? x xs'. xs = x#xs' & f x = y & map f xs' = ys)";
    1.21 +by (exhaust_tac "xs" 1);
    1.22 +by (ALLGOALS Asm_simp_tac);
    1.23 +qed "map_eq_Cons";
    1.24 +
    1.25 +Goal "!xs. map f xs = map f ys --> (!x y. f x = f y --> x=y) --> xs=ys";
    1.26 +by (induct_tac "ys" 1);
    1.27 + by (Asm_simp_tac 1);
    1.28 +by (fast_tac (claset() addss (simpset() addsimps [map_eq_Cons])) 1);
    1.29 +qed_spec_mp "map_injective";
    1.30 +
    1.31 +Goal "inj f ==> inj (map f)";
    1.32 +by(blast_tac (claset() addDs [map_injective,injD] addIs [injI]) 1);
    1.33 +qed "inj_mapI";
    1.34 +
    1.35 +Goalw [inj_on_def] "inj (map f) ==> inj f";
    1.36 +by(Clarify_tac 1);
    1.37 +by(eres_inst_tac [("x","[x]")] ballE 1);
    1.38 + by(eres_inst_tac [("x","[y]")] ballE 1);
    1.39 +  by(Asm_full_simp_tac 1);
    1.40 + by(Blast_tac 1);
    1.41 +by(Blast_tac 1);
    1.42 +qed "inj_mapD";
    1.43 +
    1.44 +Goal "inj (map f) = inj f";
    1.45 +by(blast_tac (claset() addDs [inj_mapD] addIs [inj_mapI]) 1);
    1.46 +qed "inj_map";
    1.47  
    1.48  (** rev **)
    1.49  
    1.50 @@ -450,13 +477,7 @@
    1.51  by Auto_tac;
    1.52  qed "set_filter";
    1.53  Addsimps [set_filter];
    1.54 -(*
    1.55 -Goal "(x : set (filter P xs)) = (x : set xs & P x)";
    1.56 -by (induct_tac "xs" 1);
    1.57 -by Auto_tac;
    1.58 -qed "in_set_filter";
    1.59 -Addsimps [in_set_filter];
    1.60 -*)
    1.61 +
    1.62  Goal "set[i..j(] = {k. i <= k & k < j}";
    1.63  by (induct_tac "j" 1);
    1.64  by Auto_tac;
    1.65 @@ -482,6 +503,7 @@
    1.66  by Auto_tac;
    1.67  qed "in_set_conv_decomp";
    1.68  
    1.69 +
    1.70  (* eliminate `lists' in favour of `set' *)
    1.71  
    1.72  Goal "(xs : lists A) = (!x : set xs. x : A)";
    1.73 @@ -642,19 +664,29 @@
    1.74  
    1.75  Goal "!n. n < length xs --> xs!n : set xs";
    1.76  by (induct_tac "xs" 1);
    1.77 -(* case [] *)
    1.78 -by (Simp_tac 1);
    1.79 -(* case x#xl *)
    1.80 + by (Simp_tac 1);
    1.81  by (rtac allI 1);
    1.82  by (induct_tac "n" 1);
    1.83 -(* case 0 *)
    1.84 -by (Asm_full_simp_tac 1);
    1.85 -(* case Suc x *)
    1.86 + by (Asm_full_simp_tac 1);
    1.87  by (Asm_full_simp_tac 1);
    1.88  qed_spec_mp "nth_mem";
    1.89  Addsimps [nth_mem];
    1.90  
    1.91  
    1.92 +Goal "(!i. i < length xs --> P(xs!i)) --> (!x : set xs. P x)";
    1.93 +by (induct_tac "xs" 1);
    1.94 + by (Asm_full_simp_tac 1);
    1.95 +by (simp_tac (simpset() addsplits [nat.split] addsimps [nth_Cons]) 1);
    1.96 +by (fast_tac (claset() addss simpset()) 1);
    1.97 +qed_spec_mp "all_nth_imp_all_set";
    1.98 +
    1.99 +Goal "(!x : set xs. P x) = (!i. i<length xs --> P (xs ! i))";
   1.100 +br iffI 1;
   1.101 + by (Asm_full_simp_tac 1);
   1.102 +be all_nth_imp_all_set 1;
   1.103 +qed_spec_mp "all_set_conv_all_nth";
   1.104 +
   1.105 +
   1.106  (** list update **)
   1.107  
   1.108  section "list update";
   1.109 @@ -686,6 +718,21 @@
   1.110  by (Blast_tac 1);
   1.111  qed_spec_mp "list_update_same_conv";
   1.112  
   1.113 +Goal "!i xy xs. length xs = length ys --> \
   1.114 +\     (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])";
   1.115 +by (induct_tac "ys" 1);
   1.116 + by Auto_tac;
   1.117 +by (exhaust_tac "xs" 1);
   1.118 + by (auto_tac (claset(), simpset() addsplits [nat.split]));
   1.119 +qed_spec_mp "update_zip";
   1.120 +
   1.121 +Goal "!i. set(xs[i:=x]) <= insert x (set xs)";
   1.122 +by (induct_tac "xs" 1);
   1.123 + by (asm_full_simp_tac (simpset() addsimps []) 1);
   1.124 +by (asm_full_simp_tac (simpset() addsplits [nat.split]) 1);
   1.125 +by (Fast_tac  1);
   1.126 +qed_spec_mp "set_update_subset";
   1.127 +
   1.128  
   1.129  (** last & butlast **)
   1.130  
   1.131 @@ -915,6 +962,61 @@
   1.132  
   1.133  Delsimps(tl (thms"zip.simps"));
   1.134  
   1.135 +Goal "!xs. length xs = length ys --> length (zip xs ys) = length ys";
   1.136 +by (induct_tac "ys" 1);
   1.137 + by (Simp_tac 1);
   1.138 +by (Clarify_tac 1);
   1.139 +by (exhaust_tac "xs" 1);
   1.140 + by(Auto_tac);
   1.141 +qed_spec_mp "length_zip";
   1.142 +Addsimps [length_zip];
   1.143 +
   1.144 +Goal
   1.145 +"!xs. length xs = length us --> length ys = length vs --> \
   1.146 +\     zip (xs@ys) (us@vs) = zip xs us @ zip ys vs";
   1.147 +by(induct_tac "us" 1);
   1.148 + by(Asm_full_simp_tac 1);
   1.149 +by(Asm_full_simp_tac 1);
   1.150 +by(Clarify_tac 1);
   1.151 +by(exhaust_tac "xs" 1);
   1.152 + by(Auto_tac);
   1.153 +qed_spec_mp "zip_append";
   1.154 +
   1.155 +Goal "!xs. length xs = length ys --> zip (rev xs) (rev ys) = rev (zip xs ys)";
   1.156 +by(induct_tac "ys" 1);
   1.157 + by(Asm_full_simp_tac 1);
   1.158 +by(Asm_full_simp_tac 1);
   1.159 +by(Clarify_tac 1);
   1.160 +by(exhaust_tac "xs" 1);
   1.161 + by(Auto_tac);
   1.162 +by (asm_full_simp_tac (simpset() addsimps [zip_append]) 1);
   1.163 +qed_spec_mp "zip_rev";
   1.164 +
   1.165 +Goal
   1.166 +"!i xs. i < length xs --> i < length ys --> (zip xs ys)!i = (xs!i, ys!i)";
   1.167 +by (induct_tac "ys" 1);
   1.168 + by (Simp_tac 1);
   1.169 +by (Clarify_tac 1);
   1.170 +by(exhaust_tac "xs" 1);
   1.171 + by(Auto_tac);
   1.172 +by (asm_full_simp_tac (simpset() addsimps (thms"nth.simps") addsplits [nat.split]) 1);
   1.173 +qed_spec_mp "nth_zip";
   1.174 +Addsimps [nth_zip];
   1.175 +
   1.176 +Goal
   1.177 + "length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]";
   1.178 +by(rtac sym 1);
   1.179 +by(asm_simp_tac (simpset() addsimps [update_zip]) 1);
   1.180 +qed_spec_mp "zip_update";
   1.181 +
   1.182 +Goal "!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)";
   1.183 +by (induct_tac "i" 1);
   1.184 + by(Auto_tac);
   1.185 +by (exhaust_tac "j" 1);
   1.186 + by(Auto_tac);
   1.187 +qed "zip_replicate";
   1.188 +Addsimps [zip_replicate];
   1.189 +
   1.190  
   1.191  (** foldl **)
   1.192  section "foldl";
   1.193 @@ -1102,6 +1204,11 @@
   1.194  qed "rev_replicate";
   1.195  Addsimps [rev_replicate];
   1.196  
   1.197 +Goal "replicate (n+m) x = replicate n x @ replicate m x";
   1.198 +by (induct_tac "n" 1);
   1.199 +by Auto_tac;
   1.200 +qed "replicate_add";
   1.201 +
   1.202  Goal"n ~= 0 --> hd(replicate n x) = x";
   1.203  by (induct_tac "n" 1);
   1.204  by Auto_tac;
   1.205 @@ -1137,10 +1244,14 @@
   1.206  qed "set_replicate";
   1.207  Addsimps [set_replicate];
   1.208  
   1.209 -Goal "replicate (n+m) x = replicate n x @ replicate m x";
   1.210 -by (induct_tac "n" 1);
   1.211 -by Auto_tac;
   1.212 -qed "replicate_add";
   1.213 +Goal "set(replicate n x) = (if n=0 then {} else {x})";
   1.214 +by(Auto_tac);
   1.215 +qed "set_replicate_conv_if";
   1.216 +
   1.217 +Goal "x : set(replicate n y) --> x=y";
   1.218 +by(asm_simp_tac (simpset() addsimps [set_replicate_conv_if]) 1);
   1.219 +qed_spec_mp "in_set_replicateD";
   1.220 +
   1.221  
   1.222  (*** Lexcicographic orderings on lists ***)
   1.223  section"Lexcicographic orderings on lists";