summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/List.ML

changeset 4935 | 1694e2daef8f |

parent 4911 | 6195e4468c54 |

child 5043 | 3fdc881e8ff9 |

1.1 --- a/src/HOL/List.ML Fri May 15 11:35:56 1998 +0200 1.2 +++ b/src/HOL/List.ML Mon May 18 17:31:49 1998 +0200 1.3 @@ -6,21 +6,21 @@ 1.4 List lemmas 1.5 *) 1.6 1.7 -goal thy "!x. xs ~= x#xs"; 1.8 +Goal "!x. xs ~= x#xs"; 1.9 by (induct_tac "xs" 1); 1.10 by (ALLGOALS Asm_simp_tac); 1.11 qed_spec_mp "not_Cons_self"; 1.12 bind_thm("not_Cons_self2",not_Cons_self RS not_sym); 1.13 Addsimps [not_Cons_self,not_Cons_self2]; 1.14 1.15 -goal thy "(xs ~= []) = (? y ys. xs = y#ys)"; 1.16 +Goal "(xs ~= []) = (? y ys. xs = y#ys)"; 1.17 by (induct_tac "xs" 1); 1.18 by (Simp_tac 1); 1.19 by (Asm_simp_tac 1); 1.20 qed "neq_Nil_conv"; 1.21 1.22 (* Induction over the length of a list: *) 1.23 -val [prem] = goal thy 1.24 +val [prem] = Goal 1.25 "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)"; 1.26 by(rtac measure_induct 1 THEN etac prem 1); 1.27 qed "length_induct"; 1.28 @@ -28,7 +28,7 @@ 1.29 1.30 (** "lists": the list-forming operator over sets **) 1.31 1.32 -goalw thy lists.defs "!!A B. A<=B ==> lists A <= lists B"; 1.33 +Goalw lists.defs "!!A B. A<=B ==> lists A <= lists B"; 1.34 by (rtac lfp_mono 1); 1.35 by (REPEAT (ares_tac basic_monos 1)); 1.36 qed "lists_mono"; 1.37 @@ -37,12 +37,12 @@ 1.38 AddSEs [listsE]; 1.39 AddSIs lists.intrs; 1.40 1.41 -goal thy "!!l. l: lists A ==> l: lists B --> l: lists (A Int B)"; 1.42 +Goal "!!l. l: lists A ==> l: lists B --> l: lists (A Int B)"; 1.43 by (etac lists.induct 1); 1.44 by (ALLGOALS Blast_tac); 1.45 qed_spec_mp "lists_IntI"; 1.46 1.47 -goal thy "lists (A Int B) = lists A Int lists B"; 1.48 +Goal "lists (A Int B) = lists A Int lists B"; 1.49 by (rtac (mono_Int RS equalityI) 1); 1.50 by (simp_tac (simpset() addsimps [mono_def, lists_mono]) 1); 1.51 by (blast_tac (claset() addSIs [lists_IntI]) 1); 1.52 @@ -53,12 +53,12 @@ 1.53 (** Case analysis **) 1.54 section "Case analysis"; 1.55 1.56 -val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)"; 1.57 +val prems = Goal "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)"; 1.58 by (induct_tac "xs" 1); 1.59 by (REPEAT(resolve_tac prems 1)); 1.60 qed "list_cases"; 1.61 1.62 -goal thy "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)"; 1.63 +Goal "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)"; 1.64 by (induct_tac "xs" 1); 1.65 by (Blast_tac 1); 1.66 by (Blast_tac 1); 1.67 @@ -70,43 +70,43 @@ 1.68 1.69 section "length"; 1.70 1.71 -goal thy "length(xs@ys) = length(xs)+length(ys)"; 1.72 +Goal "length(xs@ys) = length(xs)+length(ys)"; 1.73 by (induct_tac "xs" 1); 1.74 by (ALLGOALS Asm_simp_tac); 1.75 qed"length_append"; 1.76 Addsimps [length_append]; 1.77 1.78 -goal thy "length (map f l) = length l"; 1.79 +Goal "length (map f l) = length l"; 1.80 by (induct_tac "l" 1); 1.81 by (ALLGOALS Simp_tac); 1.82 qed "length_map"; 1.83 Addsimps [length_map]; 1.84 1.85 -goal thy "length(rev xs) = length(xs)"; 1.86 +Goal "length(rev xs) = length(xs)"; 1.87 by (induct_tac "xs" 1); 1.88 by (ALLGOALS Asm_simp_tac); 1.89 qed "length_rev"; 1.90 Addsimps [length_rev]; 1.91 1.92 -goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = (length xs) - 1"; 1.93 +Goal "!!xs. xs ~= [] ==> length(tl xs) = (length xs) - 1"; 1.94 by (exhaust_tac "xs" 1); 1.95 by (ALLGOALS Asm_full_simp_tac); 1.96 qed "length_tl"; 1.97 Addsimps [length_tl]; 1.98 1.99 -goal thy "(length xs = 0) = (xs = [])"; 1.100 +Goal "(length xs = 0) = (xs = [])"; 1.101 by (induct_tac "xs" 1); 1.102 by (ALLGOALS Asm_simp_tac); 1.103 qed "length_0_conv"; 1.104 AddIffs [length_0_conv]; 1.105 1.106 -goal thy "(0 = length xs) = (xs = [])"; 1.107 +Goal "(0 = length xs) = (xs = [])"; 1.108 by (induct_tac "xs" 1); 1.109 by (ALLGOALS Asm_simp_tac); 1.110 qed "zero_length_conv"; 1.111 AddIffs [zero_length_conv]; 1.112 1.113 -goal thy "(0 < length xs) = (xs ~= [])"; 1.114 +Goal "(0 < length xs) = (xs ~= [])"; 1.115 by (induct_tac "xs" 1); 1.116 by (ALLGOALS Asm_simp_tac); 1.117 qed "length_greater_0_conv"; 1.118 @@ -116,44 +116,44 @@ 1.119 1.120 section "@ - append"; 1.121 1.122 -goal thy "(xs@ys)@zs = xs@(ys@zs)"; 1.123 +Goal "(xs@ys)@zs = xs@(ys@zs)"; 1.124 by (induct_tac "xs" 1); 1.125 by (ALLGOALS Asm_simp_tac); 1.126 qed "append_assoc"; 1.127 Addsimps [append_assoc]; 1.128 1.129 -goal thy "xs @ [] = xs"; 1.130 +Goal "xs @ [] = xs"; 1.131 by (induct_tac "xs" 1); 1.132 by (ALLGOALS Asm_simp_tac); 1.133 qed "append_Nil2"; 1.134 Addsimps [append_Nil2]; 1.135 1.136 -goal thy "(xs@ys = []) = (xs=[] & ys=[])"; 1.137 +Goal "(xs@ys = []) = (xs=[] & ys=[])"; 1.138 by (induct_tac "xs" 1); 1.139 by (ALLGOALS Asm_simp_tac); 1.140 qed "append_is_Nil_conv"; 1.141 AddIffs [append_is_Nil_conv]; 1.142 1.143 -goal thy "([] = xs@ys) = (xs=[] & ys=[])"; 1.144 +Goal "([] = xs@ys) = (xs=[] & ys=[])"; 1.145 by (induct_tac "xs" 1); 1.146 by (ALLGOALS Asm_simp_tac); 1.147 by (Blast_tac 1); 1.148 qed "Nil_is_append_conv"; 1.149 AddIffs [Nil_is_append_conv]; 1.150 1.151 -goal thy "(xs @ ys = xs) = (ys=[])"; 1.152 +Goal "(xs @ ys = xs) = (ys=[])"; 1.153 by (induct_tac "xs" 1); 1.154 by (ALLGOALS Asm_simp_tac); 1.155 qed "append_self_conv"; 1.156 1.157 -goal thy "(xs = xs @ ys) = (ys=[])"; 1.158 +Goal "(xs = xs @ ys) = (ys=[])"; 1.159 by (induct_tac "xs" 1); 1.160 by (ALLGOALS Asm_simp_tac); 1.161 by (Blast_tac 1); 1.162 qed "self_append_conv"; 1.163 AddIffs [append_self_conv,self_append_conv]; 1.164 1.165 -goal thy "!ys. length xs = length ys | length us = length vs \ 1.166 +Goal "!ys. length xs = length ys | length us = length vs \ 1.167 \ --> (xs@us = ys@vs) = (xs=ys & us=vs)"; 1.168 by (induct_tac "xs" 1); 1.169 by (rtac allI 1); 1.170 @@ -169,15 +169,15 @@ 1.171 qed_spec_mp "append_eq_append_conv"; 1.172 Addsimps [append_eq_append_conv]; 1.173 1.174 -goal thy "(xs @ ys = xs @ zs) = (ys=zs)"; 1.175 +Goal "(xs @ ys = xs @ zs) = (ys=zs)"; 1.176 by (Simp_tac 1); 1.177 qed "same_append_eq"; 1.178 1.179 -goal thy "(xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 1.180 +Goal "(xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 1.181 by (Simp_tac 1); 1.182 qed "append1_eq_conv"; 1.183 1.184 -goal thy "(ys @ xs = zs @ xs) = (ys=zs)"; 1.185 +Goal "(ys @ xs = zs @ xs) = (ys=zs)"; 1.186 by (Simp_tac 1); 1.187 qed "append_same_eq"; 1.188 1.189 @@ -186,115 +186,82 @@ 1.190 AddSDs 1.191 [same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1]; 1.192 1.193 -goal thy "(xs @ ys = ys) = (xs=[])"; 1.194 +Goal "(xs @ ys = ys) = (xs=[])"; 1.195 by(cut_inst_tac [("zs","[]")] append_same_eq 1); 1.196 by(Asm_full_simp_tac 1); 1.197 qed "append_self_conv2"; 1.198 1.199 -goal thy "(ys = xs @ ys) = (xs=[])"; 1.200 +Goal "(ys = xs @ ys) = (xs=[])"; 1.201 by(simp_tac (simpset() addsimps 1.202 [simplify (simpset()) (read_instantiate[("ys","[]")]append_same_eq)]) 1); 1.203 by(Blast_tac 1); 1.204 qed "self_append_conv2"; 1.205 AddIffs [append_self_conv2,self_append_conv2]; 1.206 1.207 -goal thy "xs ~= [] --> hd xs # tl xs = xs"; 1.208 +Goal "xs ~= [] --> hd xs # tl xs = xs"; 1.209 by (induct_tac "xs" 1); 1.210 by (ALLGOALS Asm_simp_tac); 1.211 qed_spec_mp "hd_Cons_tl"; 1.212 Addsimps [hd_Cons_tl]; 1.213 1.214 -goal thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)"; 1.215 +Goal "hd(xs@ys) = (if xs=[] then hd ys else hd xs)"; 1.216 by (induct_tac "xs" 1); 1.217 by (ALLGOALS Asm_simp_tac); 1.218 qed "hd_append"; 1.219 1.220 -goal thy "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs"; 1.221 +Goal "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs"; 1.222 by (asm_simp_tac (simpset() addsimps [hd_append] 1.223 addsplits [split_list_case]) 1); 1.224 qed "hd_append2"; 1.225 Addsimps [hd_append2]; 1.226 1.227 -goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)"; 1.228 +Goal "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)"; 1.229 by (simp_tac (simpset() addsplits [split_list_case]) 1); 1.230 qed "tl_append"; 1.231 1.232 -goal thy "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys"; 1.233 +Goal "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys"; 1.234 by (asm_simp_tac (simpset() addsimps [tl_append] 1.235 addsplits [split_list_case]) 1); 1.236 qed "tl_append2"; 1.237 Addsimps [tl_append2]; 1.238 1.239 1.240 -(** Snoc exhaustion and induction **) 1.241 -section "Snoc exhaustion and induction"; 1.242 - 1.243 -goal thy "xs ~= [] --> (? ys y. xs = ys@[y])"; 1.244 -by(induct_tac "xs" 1); 1.245 -by(Simp_tac 1); 1.246 -by(exhaust_tac "list" 1); 1.247 - by(Asm_simp_tac 1); 1.248 - by(res_inst_tac [("x","[]")] exI 1); 1.249 - by(Simp_tac 1); 1.250 -by(Asm_full_simp_tac 1); 1.251 -by(Clarify_tac 1); 1.252 -by(res_inst_tac [("x","a#ys")] exI 1); 1.253 -by(Asm_simp_tac 1); 1.254 -val lemma = result(); 1.255 - 1.256 -goal thy "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P"; 1.257 -by(cut_facts_tac [lemma] 1); 1.258 -by(Blast_tac 1); 1.259 -bind_thm ("snoc_exhaust", 1.260 - impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp))))); 1.261 - 1.262 -val prems = goal thy "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs"; 1.263 -by(res_inst_tac [("xs","xs")] length_induct 1); 1.264 -by(res_inst_tac [("xs","xs")] snoc_exhaust 1); 1.265 - by(Clarify_tac 1); 1.266 - brs prems 1; 1.267 -by(Clarify_tac 1); 1.268 -brs prems 1; 1.269 -auto(); 1.270 -qed "snoc_induct"; 1.271 - 1.272 - 1.273 (** map **) 1.274 1.275 section "map"; 1.276 1.277 -goal thy 1.278 +Goal 1.279 "(!x. x : set xs --> f x = g x) --> map f xs = map g xs"; 1.280 by (induct_tac "xs" 1); 1.281 by (ALLGOALS Asm_simp_tac); 1.282 bind_thm("map_ext", impI RS (allI RS (result() RS mp))); 1.283 1.284 -goal thy "map (%x. x) = (%xs. xs)"; 1.285 +Goal "map (%x. x) = (%xs. xs)"; 1.286 by (rtac ext 1); 1.287 by (induct_tac "xs" 1); 1.288 by (ALLGOALS Asm_simp_tac); 1.289 qed "map_ident"; 1.290 Addsimps[map_ident]; 1.291 1.292 -goal thy "map f (xs@ys) = map f xs @ map f ys"; 1.293 +Goal "map f (xs@ys) = map f xs @ map f ys"; 1.294 by (induct_tac "xs" 1); 1.295 by (ALLGOALS Asm_simp_tac); 1.296 qed "map_append"; 1.297 Addsimps[map_append]; 1.298 1.299 -goalw thy [o_def] "map (f o g) xs = map f (map g xs)"; 1.300 +Goalw [o_def] "map (f o g) xs = map f (map g xs)"; 1.301 by (induct_tac "xs" 1); 1.302 by (ALLGOALS Asm_simp_tac); 1.303 qed "map_compose"; 1.304 Addsimps[map_compose]; 1.305 1.306 -goal thy "rev(map f xs) = map f (rev xs)"; 1.307 +Goal "rev(map f xs) = map f (rev xs)"; 1.308 by (induct_tac "xs" 1); 1.309 by (ALLGOALS Asm_simp_tac); 1.310 qed "rev_map"; 1.311 1.312 (* a congruence rule for map: *) 1.313 -goal thy 1.314 +Goal 1.315 "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys"; 1.316 by (rtac impI 1); 1.317 by (hyp_subst_tac 1); 1.318 @@ -303,13 +270,13 @@ 1.319 val lemma = result(); 1.320 bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp))); 1.321 1.322 -goal List.thy "(map f xs = []) = (xs = [])"; 1.323 +Goal "(map f xs = []) = (xs = [])"; 1.324 by (induct_tac "xs" 1); 1.325 by (ALLGOALS Asm_simp_tac); 1.326 qed "map_is_Nil_conv"; 1.327 AddIffs [map_is_Nil_conv]; 1.328 1.329 -goal List.thy "([] = map f xs) = (xs = [])"; 1.330 +Goal "([] = map f xs) = (xs = [])"; 1.331 by (induct_tac "xs" 1); 1.332 by (ALLGOALS Asm_simp_tac); 1.333 qed "Nil_is_map_conv"; 1.334 @@ -320,42 +287,56 @@ 1.335 1.336 section "rev"; 1.337 1.338 -goal thy "rev(xs@ys) = rev(ys) @ rev(xs)"; 1.339 +Goal "rev(xs@ys) = rev(ys) @ rev(xs)"; 1.340 by (induct_tac "xs" 1); 1.341 by (ALLGOALS Asm_simp_tac); 1.342 qed "rev_append"; 1.343 Addsimps[rev_append]; 1.344 1.345 -goal thy "rev(rev l) = l"; 1.346 +Goal "rev(rev l) = l"; 1.347 by (induct_tac "l" 1); 1.348 by (ALLGOALS Asm_simp_tac); 1.349 qed "rev_rev_ident"; 1.350 Addsimps[rev_rev_ident]; 1.351 1.352 -goal thy "(rev xs = []) = (xs = [])"; 1.353 +Goal "(rev xs = []) = (xs = [])"; 1.354 by (induct_tac "xs" 1); 1.355 by (ALLGOALS Asm_simp_tac); 1.356 qed "rev_is_Nil_conv"; 1.357 AddIffs [rev_is_Nil_conv]; 1.358 1.359 -goal thy "([] = rev xs) = (xs = [])"; 1.360 +Goal "([] = rev xs) = (xs = [])"; 1.361 by (induct_tac "xs" 1); 1.362 by (ALLGOALS Asm_simp_tac); 1.363 qed "Nil_is_rev_conv"; 1.364 AddIffs [Nil_is_rev_conv]; 1.365 1.366 +val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs"; 1.367 +by(stac (rev_rev_ident RS sym) 1); 1.368 +br(read_instantiate [("P","%xs. ?P(rev xs)")]list.induct)1; 1.369 +by(ALLGOALS Simp_tac); 1.370 +brs prems 1; 1.371 +bes prems 1; 1.372 +qed "rev_induct"; 1.373 + 1.374 +Goal "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P"; 1.375 +by(res_inst_tac [("xs","xs")] rev_induct 1); 1.376 +by(ALLGOALS Asm_simp_tac); 1.377 +bind_thm ("rev_exhaust", 1.378 + impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp))))); 1.379 + 1.380 1.381 (** mem **) 1.382 1.383 section "mem"; 1.384 1.385 -goal thy "x mem (xs@ys) = (x mem xs | x mem ys)"; 1.386 +Goal "x mem (xs@ys) = (x mem xs | x mem ys)"; 1.387 by (induct_tac "xs" 1); 1.388 by (ALLGOALS Asm_simp_tac); 1.389 qed "mem_append"; 1.390 Addsimps[mem_append]; 1.391 1.392 -goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))"; 1.393 +Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))"; 1.394 by (induct_tac "xs" 1); 1.395 by (ALLGOALS Asm_simp_tac); 1.396 qed "mem_filter"; 1.397 @@ -365,48 +346,48 @@ 1.398 1.399 section "set"; 1.400 1.401 -goal thy "set (xs@ys) = (set xs Un set ys)"; 1.402 +Goal "set (xs@ys) = (set xs Un set ys)"; 1.403 by (induct_tac "xs" 1); 1.404 by (ALLGOALS Asm_simp_tac); 1.405 qed "set_append"; 1.406 Addsimps[set_append]; 1.407 1.408 -goal thy "(x mem xs) = (x: set xs)"; 1.409 +Goal "(x mem xs) = (x: set xs)"; 1.410 by (induct_tac "xs" 1); 1.411 by (ALLGOALS Asm_simp_tac); 1.412 by (Blast_tac 1); 1.413 qed "set_mem_eq"; 1.414 1.415 -goal thy "set l <= set (x#l)"; 1.416 +Goal "set l <= set (x#l)"; 1.417 by (Simp_tac 1); 1.418 by (Blast_tac 1); 1.419 qed "set_subset_Cons"; 1.420 1.421 -goal thy "(set xs = {}) = (xs = [])"; 1.422 +Goal "(set xs = {}) = (xs = [])"; 1.423 by (induct_tac "xs" 1); 1.424 by (ALLGOALS Asm_simp_tac); 1.425 qed "set_empty"; 1.426 Addsimps [set_empty]; 1.427 1.428 -goal thy "set(rev xs) = set(xs)"; 1.429 +Goal "set(rev xs) = set(xs)"; 1.430 by (induct_tac "xs" 1); 1.431 by (ALLGOALS Asm_simp_tac); 1.432 qed "set_rev"; 1.433 Addsimps [set_rev]; 1.434 1.435 -goal thy "set(map f xs) = f``(set xs)"; 1.436 +Goal "set(map f xs) = f``(set xs)"; 1.437 by (induct_tac "xs" 1); 1.438 by (ALLGOALS Asm_simp_tac); 1.439 qed "set_map"; 1.440 Addsimps [set_map]; 1.441 1.442 -goal thy "set(map f xs) = f``(set xs)"; 1.443 +Goal "set(map f xs) = f``(set xs)"; 1.444 by (induct_tac "xs" 1); 1.445 by (ALLGOALS Asm_simp_tac); 1.446 qed "set_map"; 1.447 Addsimps [set_map]; 1.448 1.449 -goal thy "(x : set(filter P xs)) = (x : set xs & P x)"; 1.450 +Goal "(x : set(filter P xs)) = (x : set xs & P x)"; 1.451 by (induct_tac "xs" 1); 1.452 by (ALLGOALS Asm_simp_tac); 1.453 by(Blast_tac 1); 1.454 @@ -418,19 +399,19 @@ 1.455 1.456 section "list_all"; 1.457 1.458 -goal thy "list_all (%x. True) xs = True"; 1.459 +Goal "list_all (%x. True) xs = True"; 1.460 by (induct_tac "xs" 1); 1.461 by (ALLGOALS Asm_simp_tac); 1.462 qed "list_all_True"; 1.463 Addsimps [list_all_True]; 1.464 1.465 -goal thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; 1.466 +Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; 1.467 by (induct_tac "xs" 1); 1.468 by (ALLGOALS Asm_simp_tac); 1.469 qed "list_all_append"; 1.470 Addsimps [list_all_append]; 1.471 1.472 -goal thy "list_all P xs = (!x. x mem xs --> P(x))"; 1.473 +Goal "list_all P xs = (!x. x mem xs --> P(x))"; 1.474 by (induct_tac "xs" 1); 1.475 by (ALLGOALS Asm_simp_tac); 1.476 by (Blast_tac 1); 1.477 @@ -441,25 +422,25 @@ 1.478 1.479 section "filter"; 1.480 1.481 -goal thy "filter P (xs@ys) = filter P xs @ filter P ys"; 1.482 +Goal "filter P (xs@ys) = filter P xs @ filter P ys"; 1.483 by (induct_tac "xs" 1); 1.484 by (ALLGOALS Asm_simp_tac); 1.485 qed "filter_append"; 1.486 Addsimps [filter_append]; 1.487 1.488 -goal thy "filter (%x. True) xs = xs"; 1.489 +Goal "filter (%x. True) xs = xs"; 1.490 by (induct_tac "xs" 1); 1.491 by (ALLGOALS Asm_simp_tac); 1.492 qed "filter_True"; 1.493 Addsimps [filter_True]; 1.494 1.495 -goal thy "filter (%x. False) xs = []"; 1.496 +Goal "filter (%x. False) xs = []"; 1.497 by (induct_tac "xs" 1); 1.498 by (ALLGOALS Asm_simp_tac); 1.499 qed "filter_False"; 1.500 Addsimps [filter_False]; 1.501 1.502 -goal thy "length (filter P xs) <= length xs"; 1.503 +Goal "length (filter P xs) <= length xs"; 1.504 by (induct_tac "xs" 1); 1.505 by (ALLGOALS Asm_simp_tac); 1.506 qed "length_filter"; 1.507 @@ -469,41 +450,41 @@ 1.508 1.509 section "concat"; 1.510 1.511 -goal thy "concat(xs@ys) = concat(xs)@concat(ys)"; 1.512 +Goal "concat(xs@ys) = concat(xs)@concat(ys)"; 1.513 by (induct_tac "xs" 1); 1.514 by (ALLGOALS Asm_simp_tac); 1.515 qed"concat_append"; 1.516 Addsimps [concat_append]; 1.517 1.518 -goal thy "(concat xss = []) = (!xs:set xss. xs=[])"; 1.519 +Goal "(concat xss = []) = (!xs:set xss. xs=[])"; 1.520 by (induct_tac "xss" 1); 1.521 by (ALLGOALS Asm_simp_tac); 1.522 qed "concat_eq_Nil_conv"; 1.523 AddIffs [concat_eq_Nil_conv]; 1.524 1.525 -goal thy "([] = concat xss) = (!xs:set xss. xs=[])"; 1.526 +Goal "([] = concat xss) = (!xs:set xss. xs=[])"; 1.527 by (induct_tac "xss" 1); 1.528 by (ALLGOALS Asm_simp_tac); 1.529 qed "Nil_eq_concat_conv"; 1.530 AddIffs [Nil_eq_concat_conv]; 1.531 1.532 -goal thy "set(concat xs) = Union(set `` set xs)"; 1.533 +Goal "set(concat xs) = Union(set `` set xs)"; 1.534 by (induct_tac "xs" 1); 1.535 by (ALLGOALS Asm_simp_tac); 1.536 qed"set_concat"; 1.537 Addsimps [set_concat]; 1.538 1.539 -goal thy "map f (concat xs) = concat (map (map f) xs)"; 1.540 +Goal "map f (concat xs) = concat (map (map f) xs)"; 1.541 by (induct_tac "xs" 1); 1.542 by (ALLGOALS Asm_simp_tac); 1.543 qed "map_concat"; 1.544 1.545 -goal thy "filter p (concat xs) = concat (map (filter p) xs)"; 1.546 +Goal "filter p (concat xs) = concat (map (filter p) xs)"; 1.547 by (induct_tac "xs" 1); 1.548 by (ALLGOALS Asm_simp_tac); 1.549 qed"filter_concat"; 1.550 1.551 -goal thy "rev(concat xs) = concat (map rev (rev xs))"; 1.552 +Goal "rev(concat xs) = concat (map rev (rev xs))"; 1.553 by (induct_tac "xs" 1); 1.554 by (ALLGOALS Asm_simp_tac); 1.555 qed "rev_concat"; 1.556 @@ -512,7 +493,7 @@ 1.557 1.558 section "nth"; 1.559 1.560 -goal thy 1.561 +Goal 1.562 "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"; 1.563 by (nat_ind_tac "n" 1); 1.564 by (Asm_simp_tac 1); 1.565 @@ -521,7 +502,7 @@ 1.566 by (ALLGOALS Asm_simp_tac); 1.567 qed_spec_mp "nth_append"; 1.568 1.569 -goal thy "!n. n < length xs --> (map f xs)!n = f(xs!n)"; 1.570 +Goal "!n. n < length xs --> (map f xs)!n = f(xs!n)"; 1.571 by (induct_tac "xs" 1); 1.572 (* case [] *) 1.573 by (Asm_full_simp_tac 1); 1.574 @@ -532,7 +513,7 @@ 1.575 qed_spec_mp "nth_map"; 1.576 Addsimps [nth_map]; 1.577 1.578 -goal thy "!n. n < length xs --> list_all P xs --> P(xs!n)"; 1.579 +Goal "!n. n < length xs --> list_all P xs --> P(xs!n)"; 1.580 by (induct_tac "xs" 1); 1.581 (* case [] *) 1.582 by (Simp_tac 1); 1.583 @@ -542,7 +523,7 @@ 1.584 by (ALLGOALS Asm_full_simp_tac); 1.585 qed_spec_mp "list_all_nth"; 1.586 1.587 -goal thy "!n. n < length xs --> xs!n mem xs"; 1.588 +Goal "!n. n < length xs --> xs!n mem xs"; 1.589 by (induct_tac "xs" 1); 1.590 (* case [] *) 1.591 by (Simp_tac 1); 1.592 @@ -556,83 +537,43 @@ 1.593 qed_spec_mp "nth_mem"; 1.594 Addsimps [nth_mem]; 1.595 1.596 -(** More case analysis and induction **) 1.597 -section "More case analysis and induction"; 1.598 - 1.599 -goal thy "xs ~= [] --> (? ys y. xs = ys@[y])"; 1.600 -by(res_inst_tac [("xs","xs")] length_induct 1); 1.601 -by(Clarify_tac 1); 1.602 -bd (neq_Nil_conv RS iffD1) 1; 1.603 -by(Clarify_tac 1); 1.604 -by(rename_tac "ys" 1); 1.605 -by(case_tac "ys = []" 1); 1.606 - by(res_inst_tac [("x","[]")] exI 1); 1.607 - by(Asm_full_simp_tac 1); 1.608 -by(eres_inst_tac [("x","ys")] allE 1); 1.609 -by(Asm_full_simp_tac 1); 1.610 -by(REPEAT(etac exE 1)); 1.611 -by(rename_tac "zs z" 1); 1.612 -by(hyp_subst_tac 1); 1.613 -by(res_inst_tac [("x","y#zs")] exI 1); 1.614 -by(Simp_tac 1); 1.615 -qed_spec_mp "neq_Nil_snocD"; 1.616 - 1.617 -val prems = goal thy 1.618 - "[| xs=[] ==> P []; !!ys y. xs=ys@[y] ==> P(ys@[y]) |] ==> P xs"; 1.619 -by(case_tac "xs = []" 1); 1.620 - by(Asm_simp_tac 1); 1.621 - bes prems 1; 1.622 -bd neq_Nil_snocD 1; 1.623 -by(REPEAT(etac exE 1)); 1.624 -by(Asm_simp_tac 1); 1.625 -bes prems 1; 1.626 -qed "snoc_eq_cases"; 1.627 - 1.628 -val prems = goal thy 1.629 - "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P(xs)"; 1.630 -by(res_inst_tac [("xs","xs")] length_induct 1); 1.631 -by(res_inst_tac [("xs","xs")] snoc_eq_cases 1); 1.632 - brs prems 1; 1.633 -by(fast_tac (claset() addIs prems addss simpset()) 1); 1.634 -qed "snoc_induct"; 1.635 - 1.636 (** last & butlast **) 1.637 1.638 -goal thy "last(xs@[x]) = x"; 1.639 +Goal "last(xs@[x]) = x"; 1.640 by (induct_tac "xs" 1); 1.641 by (ALLGOALS Asm_simp_tac); 1.642 qed "last_snoc"; 1.643 Addsimps [last_snoc]; 1.644 1.645 -goal thy "butlast(xs@[x]) = xs"; 1.646 +Goal "butlast(xs@[x]) = xs"; 1.647 by (induct_tac "xs" 1); 1.648 by (ALLGOALS Asm_simp_tac); 1.649 qed "butlast_snoc"; 1.650 Addsimps [butlast_snoc]; 1.651 1.652 -goal thy "length(butlast xs) = length xs - 1"; 1.653 -by (res_inst_tac [("xs","xs")] snoc_induct 1); 1.654 +Goal "length(butlast xs) = length xs - 1"; 1.655 +by (res_inst_tac [("xs","xs")] rev_induct 1); 1.656 by (ALLGOALS Asm_simp_tac); 1.657 qed "length_butlast"; 1.658 Addsimps [length_butlast]; 1.659 1.660 -goal thy 1.661 +Goal 1.662 "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)"; 1.663 by (induct_tac "xs" 1); 1.664 by (ALLGOALS Asm_simp_tac); 1.665 qed_spec_mp "butlast_append"; 1.666 1.667 -goal thy "x:set(butlast xs) --> x:set xs"; 1.668 +Goal "x:set(butlast xs) --> x:set xs"; 1.669 by (induct_tac "xs" 1); 1.670 by (ALLGOALS Asm_simp_tac); 1.671 qed_spec_mp "in_set_butlastD"; 1.672 1.673 -goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))"; 1.674 +Goal "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))"; 1.675 by (asm_simp_tac (simpset() addsimps [butlast_append]) 1); 1.676 by (blast_tac (claset() addDs [in_set_butlastD]) 1); 1.677 qed "in_set_butlast_appendI1"; 1.678 1.679 -goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))"; 1.680 +Goal "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))"; 1.681 by (asm_simp_tac (simpset() addsimps [butlast_append]) 1); 1.682 by (Clarify_tac 1); 1.683 by (Full_simp_tac 1); 1.684 @@ -641,28 +582,28 @@ 1.685 (** take & drop **) 1.686 section "take & drop"; 1.687 1.688 -goal thy "take 0 xs = []"; 1.689 +Goal "take 0 xs = []"; 1.690 by (induct_tac "xs" 1); 1.691 by (ALLGOALS Asm_simp_tac); 1.692 qed "take_0"; 1.693 1.694 -goal thy "drop 0 xs = xs"; 1.695 +Goal "drop 0 xs = xs"; 1.696 by (induct_tac "xs" 1); 1.697 by (ALLGOALS Asm_simp_tac); 1.698 qed "drop_0"; 1.699 1.700 -goal thy "take (Suc n) (x#xs) = x # take n xs"; 1.701 +Goal "take (Suc n) (x#xs) = x # take n xs"; 1.702 by (Simp_tac 1); 1.703 qed "take_Suc_Cons"; 1.704 1.705 -goal thy "drop (Suc n) (x#xs) = drop n xs"; 1.706 +Goal "drop (Suc n) (x#xs) = drop n xs"; 1.707 by (Simp_tac 1); 1.708 qed "drop_Suc_Cons"; 1.709 1.710 Delsimps [take_Cons,drop_Cons]; 1.711 Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons]; 1.712 1.713 -goal thy "!xs. length(take n xs) = min (length xs) n"; 1.714 +Goal "!xs. length(take n xs) = min (length xs) n"; 1.715 by (nat_ind_tac "n" 1); 1.716 by (ALLGOALS Asm_simp_tac); 1.717 by (rtac allI 1); 1.718 @@ -671,7 +612,7 @@ 1.719 qed_spec_mp "length_take"; 1.720 Addsimps [length_take]; 1.721 1.722 -goal thy "!xs. length(drop n xs) = (length xs - n)"; 1.723 +Goal "!xs. length(drop n xs) = (length xs - n)"; 1.724 by (nat_ind_tac "n" 1); 1.725 by (ALLGOALS Asm_simp_tac); 1.726 by (rtac allI 1); 1.727 @@ -680,7 +621,7 @@ 1.728 qed_spec_mp "length_drop"; 1.729 Addsimps [length_drop]; 1.730 1.731 -goal thy "!xs. length xs <= n --> take n xs = xs"; 1.732 +Goal "!xs. length xs <= n --> take n xs = xs"; 1.733 by (nat_ind_tac "n" 1); 1.734 by (ALLGOALS Asm_simp_tac); 1.735 by (rtac allI 1); 1.736 @@ -688,7 +629,7 @@ 1.737 by (ALLGOALS Asm_simp_tac); 1.738 qed_spec_mp "take_all"; 1.739 1.740 -goal thy "!xs. length xs <= n --> drop n xs = []"; 1.741 +Goal "!xs. length xs <= n --> drop n xs = []"; 1.742 by (nat_ind_tac "n" 1); 1.743 by (ALLGOALS Asm_simp_tac); 1.744 by (rtac allI 1); 1.745 @@ -696,7 +637,7 @@ 1.746 by (ALLGOALS Asm_simp_tac); 1.747 qed_spec_mp "drop_all"; 1.748 1.749 -goal thy 1.750 +Goal 1.751 "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"; 1.752 by (nat_ind_tac "n" 1); 1.753 by (ALLGOALS Asm_simp_tac); 1.754 @@ -706,7 +647,7 @@ 1.755 qed_spec_mp "take_append"; 1.756 Addsimps [take_append]; 1.757 1.758 -goal thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 1.759 +Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 1.760 by (nat_ind_tac "n" 1); 1.761 by (ALLGOALS Asm_simp_tac); 1.762 by (rtac allI 1); 1.763 @@ -715,7 +656,7 @@ 1.764 qed_spec_mp "drop_append"; 1.765 Addsimps [drop_append]; 1.766 1.767 -goal thy "!xs n. take n (take m xs) = take (min n m) xs"; 1.768 +Goal "!xs n. take n (take m xs) = take (min n m) xs"; 1.769 by (nat_ind_tac "m" 1); 1.770 by (ALLGOALS Asm_simp_tac); 1.771 by (rtac allI 1); 1.772 @@ -726,7 +667,7 @@ 1.773 by (ALLGOALS Asm_simp_tac); 1.774 qed_spec_mp "take_take"; 1.775 1.776 -goal thy "!xs. drop n (drop m xs) = drop (n + m) xs"; 1.777 +Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 1.778 by (nat_ind_tac "m" 1); 1.779 by (ALLGOALS Asm_simp_tac); 1.780 by (rtac allI 1); 1.781 @@ -734,7 +675,7 @@ 1.782 by (ALLGOALS Asm_simp_tac); 1.783 qed_spec_mp "drop_drop"; 1.784 1.785 -goal thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 1.786 +Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 1.787 by (nat_ind_tac "m" 1); 1.788 by (ALLGOALS Asm_simp_tac); 1.789 by (rtac allI 1); 1.790 @@ -742,7 +683,7 @@ 1.791 by (ALLGOALS Asm_simp_tac); 1.792 qed_spec_mp "take_drop"; 1.793 1.794 -goal thy "!xs. take n (map f xs) = map f (take n xs)"; 1.795 +Goal "!xs. take n (map f xs) = map f (take n xs)"; 1.796 by (nat_ind_tac "n" 1); 1.797 by (ALLGOALS Asm_simp_tac); 1.798 by (rtac allI 1); 1.799 @@ -750,7 +691,7 @@ 1.800 by (ALLGOALS Asm_simp_tac); 1.801 qed_spec_mp "take_map"; 1.802 1.803 -goal thy "!xs. drop n (map f xs) = map f (drop n xs)"; 1.804 +Goal "!xs. drop n (map f xs) = map f (drop n xs)"; 1.805 by (nat_ind_tac "n" 1); 1.806 by (ALLGOALS Asm_simp_tac); 1.807 by (rtac allI 1); 1.808 @@ -758,7 +699,7 @@ 1.809 by (ALLGOALS Asm_simp_tac); 1.810 qed_spec_mp "drop_map"; 1.811 1.812 -goal thy "!n i. i < n --> (take n xs)!i = xs!i"; 1.813 +Goal "!n i. i < n --> (take n xs)!i = xs!i"; 1.814 by (induct_tac "xs" 1); 1.815 by (ALLGOALS Asm_simp_tac); 1.816 by (Clarify_tac 1); 1.817 @@ -769,7 +710,7 @@ 1.818 qed_spec_mp "nth_take"; 1.819 Addsimps [nth_take]; 1.820 1.821 -goal thy "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)"; 1.822 +Goal "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)"; 1.823 by (nat_ind_tac "n" 1); 1.824 by (ALLGOALS Asm_simp_tac); 1.825 by (rtac allI 1); 1.826 @@ -782,42 +723,39 @@ 1.827 1.828 section "takeWhile & dropWhile"; 1.829 1.830 -goal thy "takeWhile P xs @ dropWhile P xs = xs"; 1.831 +Goal "takeWhile P xs @ dropWhile P xs = xs"; 1.832 by (induct_tac "xs" 1); 1.833 by (ALLGOALS Asm_full_simp_tac); 1.834 qed "takeWhile_dropWhile_id"; 1.835 Addsimps [takeWhile_dropWhile_id]; 1.836 1.837 -goal thy "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs"; 1.838 +Goal "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs"; 1.839 by (induct_tac "xs" 1); 1.840 by (ALLGOALS Asm_full_simp_tac); 1.841 by (Blast_tac 1); 1.842 bind_thm("takeWhile_append1", conjI RS (result() RS mp)); 1.843 Addsimps [takeWhile_append1]; 1.844 1.845 -goal thy 1.846 - "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys"; 1.847 +Goal "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys"; 1.848 by (induct_tac "xs" 1); 1.849 by (ALLGOALS Asm_full_simp_tac); 1.850 bind_thm("takeWhile_append2", ballI RS (result() RS mp)); 1.851 Addsimps [takeWhile_append2]; 1.852 1.853 -goal thy 1.854 - "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"; 1.855 +Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"; 1.856 by (induct_tac "xs" 1); 1.857 by (ALLGOALS Asm_full_simp_tac); 1.858 by (Blast_tac 1); 1.859 bind_thm("dropWhile_append1", conjI RS (result() RS mp)); 1.860 Addsimps [dropWhile_append1]; 1.861 1.862 -goal thy 1.863 - "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys"; 1.864 +Goal "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys"; 1.865 by (induct_tac "xs" 1); 1.866 by (ALLGOALS Asm_full_simp_tac); 1.867 bind_thm("dropWhile_append2", ballI RS (result() RS mp)); 1.868 Addsimps [dropWhile_append2]; 1.869 1.870 -goal thy "x:set(takeWhile P xs) --> x:set xs & P x"; 1.871 +Goal "x:set(takeWhile P xs) --> x:set xs & P x"; 1.872 by (induct_tac "xs" 1); 1.873 by (ALLGOALS Asm_full_simp_tac); 1.874 qed_spec_mp"set_take_whileD"; 1.875 @@ -829,19 +767,19 @@ 1.876 (** nodups & remdups **) 1.877 section "nodups & remdups"; 1.878 1.879 -goal thy "set(remdups xs) = set xs"; 1.880 +Goal "set(remdups xs) = set xs"; 1.881 by (induct_tac "xs" 1); 1.882 by (Simp_tac 1); 1.883 by (asm_full_simp_tac (simpset() addsimps [insert_absorb]) 1); 1.884 qed "set_remdups"; 1.885 Addsimps [set_remdups]; 1.886 1.887 -goal thy "nodups(remdups xs)"; 1.888 +Goal "nodups(remdups xs)"; 1.889 by (induct_tac "xs" 1); 1.890 by (ALLGOALS Asm_full_simp_tac); 1.891 qed "nodups_remdups"; 1.892 1.893 -goal thy "nodups xs --> nodups (filter P xs)"; 1.894 +Goal "nodups xs --> nodups (filter P xs)"; 1.895 by (induct_tac "xs" 1); 1.896 by (ALLGOALS Asm_full_simp_tac); 1.897 qed_spec_mp "nodups_filter"; 1.898 @@ -849,12 +787,12 @@ 1.899 (** replicate **) 1.900 section "replicate"; 1.901 1.902 -goal thy "set(replicate (Suc n) x) = {x}"; 1.903 +Goal "set(replicate (Suc n) x) = {x}"; 1.904 by (induct_tac "n" 1); 1.905 by (ALLGOALS Asm_full_simp_tac); 1.906 val lemma = result(); 1.907 1.908 -goal thy "!!n. n ~= 0 ==> set(replicate n x) = {x}"; 1.909 +Goal "!!n. n ~= 0 ==> set(replicate n x) = {x}"; 1.910 by (fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1); 1.911 qed "set_replicate"; 1.912 Addsimps [set_replicate];