many new lemmas about take & drop, incl the famous take-lemma
authorpaulson
Thu Jun 10 10:41:36 1999 +0200 (1999-06-10)
changeset 6813bf90f86502b2
parent 6812 ac4c9707ae53
child 6814 d96d4977f94e
many new lemmas about take & drop, incl the famous take-lemma
Ran expandshort
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Thu Jun 10 10:40:57 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Jun 10 10:41:36 1999 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4  
     1.5  Goal "(length xs = Suc n) = (? y ys. xs = y#ys & length ys = n)";
     1.6  by (induct_tac "xs" 1);
     1.7 -by (Auto_tac);
     1.8 +by Auto_tac;
     1.9  qed "length_Suc_conv";
    1.10  
    1.11  (** @ - append **)
    1.12 @@ -435,8 +435,8 @@
    1.13  Addsimps [set_map];
    1.14  
    1.15  Goal "set(filter P xs) = {x. x : set xs & P x}";
    1.16 -by(induct_tac "xs" 1);
    1.17 -by(Auto_tac);
    1.18 +by (induct_tac "xs" 1);
    1.19 +by Auto_tac;
    1.20  qed "set_filter";
    1.21  Addsimps [set_filter];
    1.22  (*
    1.23 @@ -447,17 +447,17 @@
    1.24  Addsimps [in_set_filter];
    1.25  *)
    1.26  Goal "set[i..j(] = {k. i <= k & k < j}";
    1.27 -by(induct_tac "j" 1);
    1.28 -by(Auto_tac);
    1.29 -by(arith_tac 1);
    1.30 +by (induct_tac "j" 1);
    1.31 +by Auto_tac;
    1.32 +by (arith_tac 1);
    1.33  qed "set_upt";
    1.34  Addsimps [set_upt];
    1.35  
    1.36  Goal "!i < size xs. set(xs[i := x]) <= insert x (set xs)";
    1.37 -by(induct_tac "xs" 1);
    1.38 - by(Simp_tac 1);
    1.39 -by(asm_simp_tac (simpset() addsplits [nat.split]) 1);
    1.40 -by(Blast_tac 1);
    1.41 +by (induct_tac "xs" 1);
    1.42 + by (Simp_tac 1);
    1.43 +by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
    1.44 +by (Blast_tac 1);
    1.45  qed_spec_mp "set_list_update_subset";
    1.46  
    1.47  Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)";
    1.48 @@ -662,17 +662,17 @@
    1.49  qed_spec_mp "nth_list_update";
    1.50  
    1.51  Goal "!i. i < size xs --> xs[i:=x, i:=y] = xs[i:=y]";
    1.52 -by(induct_tac "xs" 1);
    1.53 - by(Simp_tac 1);
    1.54 -by(asm_simp_tac (simpset() addsplits [nat.split]) 1);
    1.55 +by (induct_tac "xs" 1);
    1.56 + by (Simp_tac 1);
    1.57 +by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
    1.58  qed_spec_mp "list_update_overwrite";
    1.59  Addsimps [list_update_overwrite];
    1.60  
    1.61  Goal "!i < length xs. (xs[i := x] = xs) = (xs!i = x)";
    1.62 -by(induct_tac "xs" 1);
    1.63 - by(Simp_tac 1);
    1.64 -by(simp_tac (simpset() addsplits [nat.split]) 1);
    1.65 -by(Blast_tac 1);
    1.66 +by (induct_tac "xs" 1);
    1.67 + by (Simp_tac 1);
    1.68 +by (simp_tac (simpset() addsplits [nat.split]) 1);
    1.69 +by (Blast_tac 1);
    1.70  qed_spec_mp "list_update_same_conv";
    1.71  
    1.72  
    1.73 @@ -806,6 +806,13 @@
    1.74   by Auto_tac;
    1.75  qed_spec_mp "take_drop";
    1.76  
    1.77 +Goal "!xs. take n xs @ drop n xs = xs";
    1.78 +by (induct_tac "n" 1);
    1.79 + by Auto_tac;
    1.80 +by (exhaust_tac "xs" 1);
    1.81 + by Auto_tac;
    1.82 +qed_spec_mp "append_take_drop_id";
    1.83 +
    1.84  Goal "!xs. take n (map f xs) = map f (take n xs)"; 
    1.85  by (induct_tac "n" 1);
    1.86   by Auto_tac;
    1.87 @@ -881,13 +888,13 @@
    1.88  section "zip";
    1.89  
    1.90  Goal "zip [] ys = []";
    1.91 -by(induct_tac "ys" 1);
    1.92 +by (induct_tac "ys" 1);
    1.93  by Auto_tac;
    1.94  qed "zip_Nil";
    1.95  Addsimps [zip_Nil];
    1.96  
    1.97  Goal "zip (x#xs) (y#ys) = (x,y)#zip xs ys";
    1.98 -by(Simp_tac 1);
    1.99 +by (Simp_tac 1);
   1.100  qed "zip_Cons_Cons";
   1.101  Addsimps [zip_Cons_Cons];
   1.102  
   1.103 @@ -966,42 +973,72 @@
   1.104  Addsimps [nth_upt];
   1.105  
   1.106  Goal "!i. i+m <= n --> take m [i..n(] = [i..i+m(]";
   1.107 -by(induct_tac "m" 1);
   1.108 - by(Simp_tac 1);
   1.109 -by(Clarify_tac 1);
   1.110 -by(stac upt_rec 1);
   1.111 -br sym 1;
   1.112 -by(stac upt_rec 1);
   1.113 -by(asm_simp_tac (simpset() delsimps (thms"upt.simps")) 1);
   1.114 +by (induct_tac "m" 1);
   1.115 + by (Simp_tac 1);
   1.116 +by (Clarify_tac 1);
   1.117 +by (stac upt_rec 1);
   1.118 +by (rtac sym 1);
   1.119 +by (stac upt_rec 1);
   1.120 +by (asm_simp_tac (simpset() delsimps (thms"upt.simps")) 1);
   1.121  qed_spec_mp "take_upt";
   1.122  Addsimps [take_upt];
   1.123  
   1.124  Goal "!m i. i < n-m --> (map f [m..n(]) ! i = f(m+i)";
   1.125 -by(induct_tac "n" 1);
   1.126 - by(Simp_tac 1);
   1.127 -by(Clarify_tac 1);
   1.128 -by(subgoal_tac "m < Suc n" 1);
   1.129 - by(arith_tac 2);
   1.130 -by(stac upt_rec 1);
   1.131 -by(asm_simp_tac (simpset() delsplits [split_if]) 1);
   1.132 -by(split_tac [split_if] 1);
   1.133 -br conjI 1;
   1.134 - by(simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
   1.135 - by(simp_tac (simpset() addsimps [nth_append] addsplits [nat.split]) 1);
   1.136 - by(Clarify_tac 1);
   1.137 - br conjI 1;
   1.138 -  by(Clarify_tac 1);
   1.139 -  by(subgoal_tac "Suc(m+nat) < n" 1);
   1.140 -   by(arith_tac 2);
   1.141 -  by(Asm_simp_tac 1);
   1.142 - by(Clarify_tac 1);
   1.143 - by(subgoal_tac "n = Suc(m+nat)" 1);
   1.144 -  by(arith_tac 2);
   1.145 - by(Asm_simp_tac 1);
   1.146 -by(simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
   1.147 -by(arith_tac 1);
   1.148 +by (induct_tac "n" 1);
   1.149 + by (Simp_tac 1);
   1.150 +by (Clarify_tac 1);
   1.151 +by (subgoal_tac "m < Suc n" 1);
   1.152 + by (arith_tac 2);
   1.153 +by (stac upt_rec 1);
   1.154 +by (asm_simp_tac (simpset() delsplits [split_if]) 1);
   1.155 +by (split_tac [split_if] 1);
   1.156 +by (rtac conjI 1);
   1.157 + by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
   1.158 + by (simp_tac (simpset() addsimps [nth_append] addsplits [nat.split]) 1);
   1.159 + by (Clarify_tac 1);
   1.160 + by (rtac conjI 1);
   1.161 +  by (Clarify_tac 1);
   1.162 +  by (subgoal_tac "Suc(m+nat) < n" 1);
   1.163 +   by (arith_tac 2);
   1.164 +  by (Asm_simp_tac 1);
   1.165 + by (Clarify_tac 1);
   1.166 + by (subgoal_tac "n = Suc(m+nat)" 1);
   1.167 +  by (arith_tac 2);
   1.168 + by (Asm_simp_tac 1);
   1.169 +by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
   1.170 +by (arith_tac 1);
   1.171  qed_spec_mp "nth_map_upt";
   1.172  
   1.173 +Goal "ALL xs ys. k <= length xs --> k <= length ys -->  \
   1.174 +\        (ALL i. i < k --> xs!i = ys!i)  \
   1.175 +\     --> take k xs = take k ys";
   1.176 +by (induct_tac "k" 1);
   1.177 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq_0_disj, 
   1.178 +						all_conj_distrib])));
   1.179 +by (Clarify_tac 1);
   1.180 +(*Both lists must be non-empty*)
   1.181 +by (exhaust_tac "xs" 1);
   1.182 +by (exhaust_tac "ys" 2);
   1.183 +by (ALLGOALS Clarify_tac);
   1.184 +(*prenexing's needed, not miniscoping*)
   1.185 +by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [sym])  
   1.186 +                                       delsimps (all_simps))));
   1.187 +by (Blast_tac 1);
   1.188 +qed_spec_mp "nth_take_lemma";
   1.189 +
   1.190 +Goal "[| length xs = length ys;  \
   1.191 +\        ALL i. i < length xs --> xs!i = ys!i |]  \
   1.192 +\     ==> xs = ys";
   1.193 +by (forward_tac [[le_refl, eq_imp_le] MRS nth_take_lemma] 1);
   1.194 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [take_all])));
   1.195 +qed_spec_mp "nth_equalityI";
   1.196 +
   1.197 +(*The famous take-lemma*)
   1.198 +Goal "(ALL i. take i xs = take i ys) ==> xs = ys";
   1.199 +by (dres_inst_tac [("x", "max (length xs) (length ys)")] spec 1);
   1.200 +by (full_simp_tac (simpset() addsimps [le_max_iff_disj, take_all]) 1);
   1.201 +qed_spec_mp "take_equalityI";
   1.202 +
   1.203  
   1.204  (** nodups & remdups **)
   1.205  section "nodups & remdups";
   1.206 @@ -1027,51 +1064,51 @@
   1.207  section "replicate";
   1.208  
   1.209  Goal "length(replicate n x) = n";
   1.210 -by(induct_tac "n" 1);
   1.211 -by(Auto_tac);
   1.212 +by (induct_tac "n" 1);
   1.213 +by Auto_tac;
   1.214  qed "length_replicate";
   1.215  Addsimps [length_replicate];
   1.216  
   1.217  Goal "map f (replicate n x) = replicate n (f x)";
   1.218  by (induct_tac "n" 1);
   1.219 -by(Auto_tac);
   1.220 +by Auto_tac;
   1.221  qed "map_replicate";
   1.222  Addsimps [map_replicate];
   1.223  
   1.224  Goal "(replicate n x) @ (x#xs) = x # replicate n x @ xs";
   1.225  by (induct_tac "n" 1);
   1.226 -by(Auto_tac);
   1.227 +by Auto_tac;
   1.228  qed "replicate_app_Cons_same";
   1.229  
   1.230  Goal "rev(replicate n x) = replicate n x";
   1.231  by (induct_tac "n" 1);
   1.232 - by(Simp_tac 1);
   1.233 + by (Simp_tac 1);
   1.234  by (asm_simp_tac (simpset() addsimps [replicate_app_Cons_same]) 1);
   1.235  qed "rev_replicate";
   1.236  Addsimps [rev_replicate];
   1.237  
   1.238  Goal"n ~= 0 --> hd(replicate n x) = x";
   1.239  by (induct_tac "n" 1);
   1.240 -by(Auto_tac);
   1.241 +by Auto_tac;
   1.242  qed_spec_mp "hd_replicate";
   1.243  Addsimps [hd_replicate];
   1.244  
   1.245  Goal "n ~= 0 --> tl(replicate n x) = replicate (n-1) x";
   1.246  by (induct_tac "n" 1);
   1.247 -by(Auto_tac);
   1.248 +by Auto_tac;
   1.249  qed_spec_mp "tl_replicate";
   1.250  Addsimps [tl_replicate];
   1.251  
   1.252  Goal "n ~= 0 --> last(replicate n x) = x";
   1.253  by (induct_tac "n" 1);
   1.254 -by(Auto_tac);
   1.255 +by Auto_tac;
   1.256  qed_spec_mp "last_replicate";
   1.257  Addsimps [last_replicate];
   1.258  
   1.259  Goal "!i. i<n --> (replicate n x)!i = x";
   1.260 -by(induct_tac "n" 1);
   1.261 - by(Simp_tac 1);
   1.262 -by(asm_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
   1.263 +by (induct_tac "n" 1);
   1.264 + by (Simp_tac 1);
   1.265 +by (asm_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
   1.266  qed_spec_mp "nth_replicate";
   1.267  Addsimps [nth_replicate];
   1.268  
   1.269 @@ -1101,12 +1138,12 @@
   1.270  by (rtac Int_lower1 2);
   1.271  by (rtac wf_prod_fun_image 1);
   1.272  by (rtac injI 2);
   1.273 -by (Auto_tac);
   1.274 +by Auto_tac;
   1.275  qed "wf_lexn";
   1.276  
   1.277  Goal "!xs ys. (xs,ys) : lexn r n --> length xs = n & length ys = n";
   1.278  by (induct_tac "n" 1);
   1.279 -by (Auto_tac);
   1.280 +by Auto_tac;
   1.281  qed_spec_mp "lexn_length";
   1.282  
   1.283  Goalw [lex_def] "wf r ==> wf(lex r)";