More lemmas.
authornipkow
Wed Jan 12 15:58:01 2000 +0100 (2000-01-12)
changeset 8118746c5cf09bde
parent 8117 0a6173c9b2d0
child 8119 60b606eddec8
More lemmas.
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Mon Jan 10 17:08:41 2000 +0100
     1.2 +++ b/src/HOL/List.ML	Wed Jan 12 15:58:01 2000 +0100
     1.3 @@ -643,47 +643,48 @@
     1.4  
     1.5  Goal "!n. n < length xs --> (map f xs)!n = f(xs!n)";
     1.6  by (induct_tac "xs" 1);
     1.7 -(* case [] *)
     1.8 -by (Asm_full_simp_tac 1);
     1.9 -(* case x#xl *)
    1.10 + by (Asm_full_simp_tac 1);
    1.11  by (rtac allI 1);
    1.12  by (induct_tac "n" 1);
    1.13  by Auto_tac;
    1.14  qed_spec_mp "nth_map";
    1.15  Addsimps [nth_map];
    1.16  
    1.17 -Goal "!n. n < length xs --> Ball (set xs) P --> P(xs!n)";
    1.18 +Goal "set xs = {xs!i |i. i < length xs}";
    1.19  by (induct_tac "xs" 1);
    1.20 -(* case [] *)
    1.21 -by (Simp_tac 1);
    1.22 -(* case x#xl *)
    1.23 -by (rtac allI 1);
    1.24 -by (induct_tac "n" 1);
    1.25 -by Auto_tac;
    1.26 + by (Simp_tac 1);
    1.27 +by(Asm_simp_tac 1);
    1.28 +by(Safe_tac);
    1.29 +  by(res_inst_tac [("x","0")] exI 1);
    1.30 +  by (Simp_tac 1);
    1.31 + by(res_inst_tac [("x","Suc i")] exI 1);
    1.32 + by(Asm_simp_tac 1);
    1.33 +by(exhaust_tac "i" 1);
    1.34 + by(Asm_full_simp_tac 1);
    1.35 +by(rename_tac "j" 1);
    1.36 + by(res_inst_tac [("x","j")] exI 1);
    1.37 +by(Asm_simp_tac 1);
    1.38 +qed "set_conv_nth";
    1.39 +
    1.40 +Goal "n < length xs ==> Ball (set xs) P --> P(xs!n)";
    1.41 +by (simp_tac (simpset() addsimps [set_conv_nth]) 1);
    1.42 +by(Blast_tac 1);
    1.43  qed_spec_mp "list_ball_nth";
    1.44  
    1.45 -Goal "!n. n < length xs --> xs!n : set xs";
    1.46 -by (induct_tac "xs" 1);
    1.47 - by (Simp_tac 1);
    1.48 -by (rtac allI 1);
    1.49 -by (induct_tac "n" 1);
    1.50 - by (Asm_full_simp_tac 1);
    1.51 -by (Asm_full_simp_tac 1);
    1.52 +Goal "n < length xs ==> xs!n : set xs";
    1.53 +by (simp_tac (simpset() addsimps [set_conv_nth]) 1);
    1.54 +by(Blast_tac 1);
    1.55  qed_spec_mp "nth_mem";
    1.56  Addsimps [nth_mem];
    1.57  
    1.58 -
    1.59  Goal "(!i. i < length xs --> P(xs!i)) --> (!x : set xs. P x)";
    1.60 -by (induct_tac "xs" 1);
    1.61 - by (Asm_full_simp_tac 1);
    1.62 -by (simp_tac (simpset() addsplits [nat.split] addsimps [nth_Cons]) 1);
    1.63 -by (fast_tac (claset() addss simpset()) 1);
    1.64 +by (simp_tac (simpset() addsimps [set_conv_nth]) 1);
    1.65 +by(Blast_tac 1);
    1.66  qed_spec_mp "all_nth_imp_all_set";
    1.67  
    1.68  Goal "(!x : set xs. P x) = (!i. i<length xs --> P (xs ! i))";
    1.69 -by (rtac iffI 1);
    1.70 - by (Asm_full_simp_tac 1);
    1.71 -by (etac all_nth_imp_all_set 1);
    1.72 +by (simp_tac (simpset() addsimps [set_conv_nth]) 1);
    1.73 +by(Blast_tac 1);
    1.74  qed_spec_mp "all_set_conv_all_nth";
    1.75  
    1.76  
    1.77 @@ -761,6 +762,12 @@
    1.78  by Auto_tac;
    1.79  qed_spec_mp "butlast_append";
    1.80  
    1.81 +Goal "xs ~= [] --> butlast xs @ [last xs] = xs";
    1.82 +by(induct_tac "xs" 1);
    1.83 +by(ALLGOALS Asm_simp_tac);
    1.84 +qed_spec_mp "append_butlast_last_id";
    1.85 +Addsimps [append_butlast_last_id];
    1.86 +
    1.87  Goal "x:set(butlast xs) --> x:set xs";
    1.88  by (induct_tac "xs" 1);
    1.89  by Auto_tac;
    1.90 @@ -874,6 +881,7 @@
    1.91  by (exhaust_tac "xs" 1);
    1.92   by Auto_tac;
    1.93  qed_spec_mp "append_take_drop_id";
    1.94 +Addsimps [append_take_drop_id];
    1.95  
    1.96  Goal "!xs. take n (map f xs) = map f (take n xs)"; 
    1.97  by (induct_tac "n" 1);
    1.98 @@ -907,6 +915,17 @@
    1.99  qed_spec_mp "nth_drop";
   1.100  Addsimps [nth_drop];
   1.101  
   1.102 +
   1.103 +Goal
   1.104 + "!zs. (xs@ys = zs) = (xs = take (length xs) zs & ys = drop (length xs) zs)";
   1.105 +by(induct_tac "xs" 1);
   1.106 + by(Simp_tac 1);
   1.107 +by(Asm_full_simp_tac 1);
   1.108 +by(Clarify_tac 1);
   1.109 +by(exhaust_tac "zs" 1);
   1.110 +by(Auto_tac);
   1.111 +qed_spec_mp "append_eq_conv_conj";
   1.112 +
   1.113  (** takeWhile & dropWhile **)
   1.114  
   1.115  section "takeWhile & dropWhile";
   1.116 @@ -962,7 +981,7 @@
   1.117  
   1.118  Delsimps(tl (thms"zip.simps"));
   1.119  
   1.120 -Goal "!xs. length xs = length ys --> length (zip xs ys) = length ys";
   1.121 +Goal "!xs. length (zip xs ys) = min (length xs) (length ys)";
   1.122  by (induct_tac "ys" 1);
   1.123   by (Simp_tac 1);
   1.124  by (Clarify_tac 1);
   1.125 @@ -972,15 +991,33 @@
   1.126  Addsimps [length_zip];
   1.127  
   1.128  Goal
   1.129 -"!xs. length xs = length us --> length ys = length vs --> \
   1.130 -\     zip (xs@ys) (us@vs) = zip xs us @ zip ys vs";
   1.131 -by (induct_tac "us" 1);
   1.132 - by (Asm_full_simp_tac 1);
   1.133 -by (Asm_full_simp_tac 1);
   1.134 + "!xs. zip (xs@ys) zs = \
   1.135 +\      zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)";
   1.136 +by(induct_tac "zs" 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 +by(exhaust_tac "xs" 1);
   1.142 + by(Asm_simp_tac 1);
   1.143 +by(Asm_simp_tac 1);
   1.144 +qed_spec_mp "zip_append1";
   1.145 +
   1.146 +Goal
   1.147 + "!ys. zip xs (ys@zs) = \
   1.148 +\      zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs";
   1.149 +by(induct_tac "xs" 1);
   1.150 + by(Simp_tac 1);
   1.151 +by (Clarify_tac 1);
   1.152 +by(exhaust_tac "ys" 1);
   1.153 + by(Asm_simp_tac 1);
   1.154 +by(Asm_simp_tac 1);
   1.155 +qed_spec_mp "zip_append2";
   1.156 +
   1.157 +Goal
   1.158 + "[| length xs = length us; length ys = length vs |] ==> \
   1.159 +\ zip (xs@ys) (us@vs) = zip xs us @ zip ys vs";
   1.160 +by(asm_simp_tac (simpset() addsimps [zip_append1]) 1);
   1.161  qed_spec_mp "zip_append";
   1.162 +Addsimps [zip_append];
   1.163  
   1.164  Goal "!xs. length xs = length ys --> zip (rev xs) (rev ys) = rev (zip xs ys)";
   1.165  by (induct_tac "ys" 1);
   1.166 @@ -989,19 +1026,8 @@
   1.167  by (Clarify_tac 1);
   1.168  by (exhaust_tac "xs" 1);
   1.169   by (Auto_tac);
   1.170 -by (asm_full_simp_tac (simpset() addsimps [zip_append]) 1);
   1.171  qed_spec_mp "zip_rev";
   1.172  
   1.173 -Goal
   1.174 - "!ys. set(zip xs ys) = {(xs!i,ys!i) |i. i < min (length xs) (length ys)}";
   1.175 -by(induct_tac "xs" 1);
   1.176 - by (Simp_tac 1);
   1.177 -br allI 1;
   1.178 -by(exhaust_tac "ys" 1);
   1.179 - by(Asm_simp_tac 1);
   1.180 -by(auto_tac (claset(),
   1.181 -           simpset() addsimps [nth_Cons,gr0_conv_Suc] addsplits [nat.split]));
   1.182 -qed_spec_mp "set_zip";
   1.183  
   1.184  Goal
   1.185  "!i xs. i < length xs --> i < length ys --> (zip xs ys)!i = (xs!i, ys!i)";
   1.186 @@ -1014,6 +1040,10 @@
   1.187  qed_spec_mp "nth_zip";
   1.188  Addsimps [nth_zip];
   1.189  
   1.190 +Goal "set(zip xs ys) = {(xs!i,ys!i) |i. i < min (length xs) (length ys)}";
   1.191 +by (simp_tac (simpset() addsimps [set_conv_nth]addcongs [rev_conj_cong]) 1);
   1.192 +qed_spec_mp "set_zip";
   1.193 +
   1.194  Goal
   1.195   "length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]";
   1.196  by (rtac sym 1);
   1.197 @@ -1052,6 +1082,44 @@
   1.198  AddIffs[list_all2_Cons];
   1.199  
   1.200  Goalw [list_all2_def]
   1.201 + "list_all2 P (x#xs) ys = (? z zs. ys = z#zs & P x z & list_all2 P xs zs)";
   1.202 +by(exhaust_tac "ys" 1);
   1.203 +by(Auto_tac);
   1.204 +qed "list_all2_Cons1";
   1.205 +
   1.206 +Goalw [list_all2_def]
   1.207 + "list_all2 P xs (y#ys) = (? z zs. xs = z#zs & P z y & list_all2 P zs ys)";
   1.208 +by(exhaust_tac "xs" 1);
   1.209 +by(Auto_tac);
   1.210 +qed "list_all2_Cons2";
   1.211 +
   1.212 +Goalw [list_all2_def]
   1.213 + "list_all2 P (xs@ys) zs = \
   1.214 +\ (EX us vs. zs = us@vs & length us = length xs & length vs = length ys & \
   1.215 +\            list_all2 P xs us & list_all2 P ys vs)";
   1.216 +by(simp_tac (simpset() addsimps [zip_append1]) 1);
   1.217 +br iffI 1;
   1.218 + by(res_inst_tac [("x","take (length xs) zs")] exI 1);
   1.219 + by(res_inst_tac [("x","drop (length xs) zs")] exI 1);
   1.220 + by(asm_full_simp_tac (simpset() addsimps [min_def,eq_sym_conv]) 1);
   1.221 +by (Clarify_tac 1);
   1.222 +by(asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
   1.223 +qed "list_all2_append1";
   1.224 +
   1.225 +Goalw [list_all2_def]
   1.226 + "list_all2 P xs (ys@zs) = \
   1.227 +\ (EX us vs. xs = us@vs & length us = length ys & length vs = length zs & \
   1.228 +\            list_all2 P us ys & list_all2 P vs zs)";
   1.229 +by(simp_tac (simpset() addsimps [zip_append2]) 1);
   1.230 +br iffI 1;
   1.231 + by(res_inst_tac [("x","take (length ys) xs")] exI 1);
   1.232 + by(res_inst_tac [("x","drop (length ys) xs")] exI 1);
   1.233 + by(asm_full_simp_tac (simpset() addsimps [min_def,eq_sym_conv]) 1);
   1.234 +by (Clarify_tac 1);
   1.235 +by(asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
   1.236 +qed "list_all2_append2";
   1.237 +
   1.238 +Goalw [list_all2_def]
   1.239    "list_all2 P xs ys = \
   1.240  \  (length xs = length ys & (!i<length xs. P (xs!i) (ys!i)))";
   1.241  by(force_tac (claset(), simpset() addsimps [set_zip]) 1);