433 by Auto_tac; |
433 by Auto_tac; |
434 qed "set_map"; |
434 qed "set_map"; |
435 Addsimps [set_map]; |
435 Addsimps [set_map]; |
436 |
436 |
437 Goal "set(filter P xs) = {x. x : set xs & P x}"; |
437 Goal "set(filter P xs) = {x. x : set xs & P x}"; |
438 by(induct_tac "xs" 1); |
438 by (induct_tac "xs" 1); |
439 by(Auto_tac); |
439 by Auto_tac; |
440 qed "set_filter"; |
440 qed "set_filter"; |
441 Addsimps [set_filter]; |
441 Addsimps [set_filter]; |
442 (* |
442 (* |
443 Goal "(x : set (filter P xs)) = (x : set xs & P x)"; |
443 Goal "(x : set (filter P xs)) = (x : set xs & P x)"; |
444 by (induct_tac "xs" 1); |
444 by (induct_tac "xs" 1); |
445 by Auto_tac; |
445 by Auto_tac; |
446 qed "in_set_filter"; |
446 qed "in_set_filter"; |
447 Addsimps [in_set_filter]; |
447 Addsimps [in_set_filter]; |
448 *) |
448 *) |
449 Goal "set[i..j(] = {k. i <= k & k < j}"; |
449 Goal "set[i..j(] = {k. i <= k & k < j}"; |
450 by(induct_tac "j" 1); |
450 by (induct_tac "j" 1); |
451 by(Auto_tac); |
451 by Auto_tac; |
452 by(arith_tac 1); |
452 by (arith_tac 1); |
453 qed "set_upt"; |
453 qed "set_upt"; |
454 Addsimps [set_upt]; |
454 Addsimps [set_upt]; |
455 |
455 |
456 Goal "!i < size xs. set(xs[i := x]) <= insert x (set xs)"; |
456 Goal "!i < size xs. set(xs[i := x]) <= insert x (set xs)"; |
457 by(induct_tac "xs" 1); |
457 by (induct_tac "xs" 1); |
458 by(Simp_tac 1); |
458 by (Simp_tac 1); |
459 by(asm_simp_tac (simpset() addsplits [nat.split]) 1); |
459 by (asm_simp_tac (simpset() addsplits [nat.split]) 1); |
460 by(Blast_tac 1); |
460 by (Blast_tac 1); |
461 qed_spec_mp "set_list_update_subset"; |
461 qed_spec_mp "set_list_update_subset"; |
462 |
462 |
463 Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)"; |
463 Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)"; |
464 by (induct_tac "xs" 1); |
464 by (induct_tac "xs" 1); |
465 by (Simp_tac 1); |
465 by (Simp_tac 1); |
660 by (Simp_tac 1); |
660 by (Simp_tac 1); |
661 by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split])); |
661 by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split])); |
662 qed_spec_mp "nth_list_update"; |
662 qed_spec_mp "nth_list_update"; |
663 |
663 |
664 Goal "!i. i < size xs --> xs[i:=x, i:=y] = xs[i:=y]"; |
664 Goal "!i. i < size xs --> xs[i:=x, i:=y] = xs[i:=y]"; |
665 by(induct_tac "xs" 1); |
665 by (induct_tac "xs" 1); |
666 by(Simp_tac 1); |
666 by (Simp_tac 1); |
667 by(asm_simp_tac (simpset() addsplits [nat.split]) 1); |
667 by (asm_simp_tac (simpset() addsplits [nat.split]) 1); |
668 qed_spec_mp "list_update_overwrite"; |
668 qed_spec_mp "list_update_overwrite"; |
669 Addsimps [list_update_overwrite]; |
669 Addsimps [list_update_overwrite]; |
670 |
670 |
671 Goal "!i < length xs. (xs[i := x] = xs) = (xs!i = x)"; |
671 Goal "!i < length xs. (xs[i := x] = xs) = (xs!i = x)"; |
672 by(induct_tac "xs" 1); |
672 by (induct_tac "xs" 1); |
673 by(Simp_tac 1); |
673 by (Simp_tac 1); |
674 by(simp_tac (simpset() addsplits [nat.split]) 1); |
674 by (simp_tac (simpset() addsplits [nat.split]) 1); |
675 by(Blast_tac 1); |
675 by (Blast_tac 1); |
676 qed_spec_mp "list_update_same_conv"; |
676 qed_spec_mp "list_update_same_conv"; |
677 |
677 |
678 |
678 |
679 (** last & butlast **) |
679 (** last & butlast **) |
680 |
680 |
964 by (Asm_simp_tac 1); |
971 by (Asm_simp_tac 1); |
965 qed_spec_mp "nth_upt"; |
972 qed_spec_mp "nth_upt"; |
966 Addsimps [nth_upt]; |
973 Addsimps [nth_upt]; |
967 |
974 |
968 Goal "!i. i+m <= n --> take m [i..n(] = [i..i+m(]"; |
975 Goal "!i. i+m <= n --> take m [i..n(] = [i..i+m(]"; |
969 by(induct_tac "m" 1); |
976 by (induct_tac "m" 1); |
970 by(Simp_tac 1); |
977 by (Simp_tac 1); |
971 by(Clarify_tac 1); |
978 by (Clarify_tac 1); |
972 by(stac upt_rec 1); |
979 by (stac upt_rec 1); |
973 br sym 1; |
980 by (rtac sym 1); |
974 by(stac upt_rec 1); |
981 by (stac upt_rec 1); |
975 by(asm_simp_tac (simpset() delsimps (thms"upt.simps")) 1); |
982 by (asm_simp_tac (simpset() delsimps (thms"upt.simps")) 1); |
976 qed_spec_mp "take_upt"; |
983 qed_spec_mp "take_upt"; |
977 Addsimps [take_upt]; |
984 Addsimps [take_upt]; |
978 |
985 |
979 Goal "!m i. i < n-m --> (map f [m..n(]) ! i = f(m+i)"; |
986 Goal "!m i. i < n-m --> (map f [m..n(]) ! i = f(m+i)"; |
980 by(induct_tac "n" 1); |
987 by (induct_tac "n" 1); |
981 by(Simp_tac 1); |
988 by (Simp_tac 1); |
982 by(Clarify_tac 1); |
989 by (Clarify_tac 1); |
983 by(subgoal_tac "m < Suc n" 1); |
990 by (subgoal_tac "m < Suc n" 1); |
984 by(arith_tac 2); |
991 by (arith_tac 2); |
985 by(stac upt_rec 1); |
992 by (stac upt_rec 1); |
986 by(asm_simp_tac (simpset() delsplits [split_if]) 1); |
993 by (asm_simp_tac (simpset() delsplits [split_if]) 1); |
987 by(split_tac [split_if] 1); |
994 by (split_tac [split_if] 1); |
988 br conjI 1; |
995 by (rtac conjI 1); |
989 by(simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); |
996 by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); |
990 by(simp_tac (simpset() addsimps [nth_append] addsplits [nat.split]) 1); |
997 by (simp_tac (simpset() addsimps [nth_append] addsplits [nat.split]) 1); |
991 by(Clarify_tac 1); |
998 by (Clarify_tac 1); |
992 br conjI 1; |
999 by (rtac conjI 1); |
993 by(Clarify_tac 1); |
1000 by (Clarify_tac 1); |
994 by(subgoal_tac "Suc(m+nat) < n" 1); |
1001 by (subgoal_tac "Suc(m+nat) < n" 1); |
995 by(arith_tac 2); |
1002 by (arith_tac 2); |
996 by(Asm_simp_tac 1); |
1003 by (Asm_simp_tac 1); |
997 by(Clarify_tac 1); |
1004 by (Clarify_tac 1); |
998 by(subgoal_tac "n = Suc(m+nat)" 1); |
1005 by (subgoal_tac "n = Suc(m+nat)" 1); |
999 by(arith_tac 2); |
1006 by (arith_tac 2); |
1000 by(Asm_simp_tac 1); |
1007 by (Asm_simp_tac 1); |
1001 by(simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); |
1008 by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); |
1002 by(arith_tac 1); |
1009 by (arith_tac 1); |
1003 qed_spec_mp "nth_map_upt"; |
1010 qed_spec_mp "nth_map_upt"; |
|
1011 |
|
1012 Goal "ALL xs ys. k <= length xs --> k <= length ys --> \ |
|
1013 \ (ALL i. i < k --> xs!i = ys!i) \ |
|
1014 \ --> take k xs = take k ys"; |
|
1015 by (induct_tac "k" 1); |
|
1016 by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq_0_disj, |
|
1017 all_conj_distrib]))); |
|
1018 by (Clarify_tac 1); |
|
1019 (*Both lists must be non-empty*) |
|
1020 by (exhaust_tac "xs" 1); |
|
1021 by (exhaust_tac "ys" 2); |
|
1022 by (ALLGOALS Clarify_tac); |
|
1023 (*prenexing's needed, not miniscoping*) |
|
1024 by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [sym]) |
|
1025 delsimps (all_simps)))); |
|
1026 by (Blast_tac 1); |
|
1027 qed_spec_mp "nth_take_lemma"; |
|
1028 |
|
1029 Goal "[| length xs = length ys; \ |
|
1030 \ ALL i. i < length xs --> xs!i = ys!i |] \ |
|
1031 \ ==> xs = ys"; |
|
1032 by (forward_tac [[le_refl, eq_imp_le] MRS nth_take_lemma] 1); |
|
1033 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [take_all]))); |
|
1034 qed_spec_mp "nth_equalityI"; |
|
1035 |
|
1036 (*The famous take-lemma*) |
|
1037 Goal "(ALL i. take i xs = take i ys) ==> xs = ys"; |
|
1038 by (dres_inst_tac [("x", "max (length xs) (length ys)")] spec 1); |
|
1039 by (full_simp_tac (simpset() addsimps [le_max_iff_disj, take_all]) 1); |
|
1040 qed_spec_mp "take_equalityI"; |
1004 |
1041 |
1005 |
1042 |
1006 (** nodups & remdups **) |
1043 (** nodups & remdups **) |
1007 section "nodups & remdups"; |
1044 section "nodups & remdups"; |
1008 |
1045 |
1025 |
1062 |
1026 (** replicate **) |
1063 (** replicate **) |
1027 section "replicate"; |
1064 section "replicate"; |
1028 |
1065 |
1029 Goal "length(replicate n x) = n"; |
1066 Goal "length(replicate n x) = n"; |
1030 by(induct_tac "n" 1); |
1067 by (induct_tac "n" 1); |
1031 by(Auto_tac); |
1068 by Auto_tac; |
1032 qed "length_replicate"; |
1069 qed "length_replicate"; |
1033 Addsimps [length_replicate]; |
1070 Addsimps [length_replicate]; |
1034 |
1071 |
1035 Goal "map f (replicate n x) = replicate n (f x)"; |
1072 Goal "map f (replicate n x) = replicate n (f x)"; |
1036 by (induct_tac "n" 1); |
1073 by (induct_tac "n" 1); |
1037 by(Auto_tac); |
1074 by Auto_tac; |
1038 qed "map_replicate"; |
1075 qed "map_replicate"; |
1039 Addsimps [map_replicate]; |
1076 Addsimps [map_replicate]; |
1040 |
1077 |
1041 Goal "(replicate n x) @ (x#xs) = x # replicate n x @ xs"; |
1078 Goal "(replicate n x) @ (x#xs) = x # replicate n x @ xs"; |
1042 by (induct_tac "n" 1); |
1079 by (induct_tac "n" 1); |
1043 by(Auto_tac); |
1080 by Auto_tac; |
1044 qed "replicate_app_Cons_same"; |
1081 qed "replicate_app_Cons_same"; |
1045 |
1082 |
1046 Goal "rev(replicate n x) = replicate n x"; |
1083 Goal "rev(replicate n x) = replicate n x"; |
1047 by (induct_tac "n" 1); |
1084 by (induct_tac "n" 1); |
1048 by(Simp_tac 1); |
1085 by (Simp_tac 1); |
1049 by (asm_simp_tac (simpset() addsimps [replicate_app_Cons_same]) 1); |
1086 by (asm_simp_tac (simpset() addsimps [replicate_app_Cons_same]) 1); |
1050 qed "rev_replicate"; |
1087 qed "rev_replicate"; |
1051 Addsimps [rev_replicate]; |
1088 Addsimps [rev_replicate]; |
1052 |
1089 |
1053 Goal"n ~= 0 --> hd(replicate n x) = x"; |
1090 Goal"n ~= 0 --> hd(replicate n x) = x"; |
1054 by (induct_tac "n" 1); |
1091 by (induct_tac "n" 1); |
1055 by(Auto_tac); |
1092 by Auto_tac; |
1056 qed_spec_mp "hd_replicate"; |
1093 qed_spec_mp "hd_replicate"; |
1057 Addsimps [hd_replicate]; |
1094 Addsimps [hd_replicate]; |
1058 |
1095 |
1059 Goal "n ~= 0 --> tl(replicate n x) = replicate (n-1) x"; |
1096 Goal "n ~= 0 --> tl(replicate n x) = replicate (n-1) x"; |
1060 by (induct_tac "n" 1); |
1097 by (induct_tac "n" 1); |
1061 by(Auto_tac); |
1098 by Auto_tac; |
1062 qed_spec_mp "tl_replicate"; |
1099 qed_spec_mp "tl_replicate"; |
1063 Addsimps [tl_replicate]; |
1100 Addsimps [tl_replicate]; |
1064 |
1101 |
1065 Goal "n ~= 0 --> last(replicate n x) = x"; |
1102 Goal "n ~= 0 --> last(replicate n x) = x"; |
1066 by (induct_tac "n" 1); |
1103 by (induct_tac "n" 1); |
1067 by(Auto_tac); |
1104 by Auto_tac; |
1068 qed_spec_mp "last_replicate"; |
1105 qed_spec_mp "last_replicate"; |
1069 Addsimps [last_replicate]; |
1106 Addsimps [last_replicate]; |
1070 |
1107 |
1071 Goal "!i. i<n --> (replicate n x)!i = x"; |
1108 Goal "!i. i<n --> (replicate n x)!i = x"; |
1072 by(induct_tac "n" 1); |
1109 by (induct_tac "n" 1); |
1073 by(Simp_tac 1); |
1110 by (Simp_tac 1); |
1074 by(asm_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); |
1111 by (asm_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); |
1075 qed_spec_mp "nth_replicate"; |
1112 qed_spec_mp "nth_replicate"; |
1076 Addsimps [nth_replicate]; |
1113 Addsimps [nth_replicate]; |
1077 |
1114 |
1078 Goal "set(replicate (Suc n) x) = {x}"; |
1115 Goal "set(replicate (Suc n) x) = {x}"; |
1079 by (induct_tac "n" 1); |
1116 by (induct_tac "n" 1); |
1099 by (Simp_tac 1); |
1136 by (Simp_tac 1); |
1100 by (rtac wf_subset 1); |
1137 by (rtac wf_subset 1); |
1101 by (rtac Int_lower1 2); |
1138 by (rtac Int_lower1 2); |
1102 by (rtac wf_prod_fun_image 1); |
1139 by (rtac wf_prod_fun_image 1); |
1103 by (rtac injI 2); |
1140 by (rtac injI 2); |
1104 by (Auto_tac); |
1141 by Auto_tac; |
1105 qed "wf_lexn"; |
1142 qed "wf_lexn"; |
1106 |
1143 |
1107 Goal "!xs ys. (xs,ys) : lexn r n --> length xs = n & length ys = n"; |
1144 Goal "!xs ys. (xs,ys) : lexn r n --> length xs = n & length ys = n"; |
1108 by (induct_tac "n" 1); |
1145 by (induct_tac "n" 1); |
1109 by (Auto_tac); |
1146 by Auto_tac; |
1110 qed_spec_mp "lexn_length"; |
1147 qed_spec_mp "lexn_length"; |
1111 |
1148 |
1112 Goalw [lex_def] "wf r ==> wf(lex r)"; |
1149 Goalw [lex_def] "wf r ==> wf(lex r)"; |
1113 by (rtac wf_UN 1); |
1150 by (rtac wf_UN 1); |
1114 by (blast_tac (claset() addIs [wf_lexn]) 1); |
1151 by (blast_tac (claset() addIs [wf_lexn]) 1); |