446 |
446 |
447 |
447 |
448 val [] = Goal "(Alls u:A. P u) = (!n. n < length A --> P(nth n A))"; |
448 val [] = Goal "(Alls u:A. P u) = (!n. n < length A --> P(nth n A))"; |
449 by (induct_thm_tac list_induct "A" 1); |
449 by (induct_thm_tac list_induct "A" 1); |
450 by (ALLGOALS Asm_simp_tac); |
450 by (ALLGOALS Asm_simp_tac); |
451 br trans 1; |
451 by (rtac trans 1); |
452 br (nat_case_dist RS sym) 2; |
452 by (rtac (nat_case_dist RS sym) 2); |
453 by (ALLGOALS Asm_simp_tac); |
453 by (ALLGOALS Asm_simp_tac); |
454 qed "alls_P_eq_P_nth"; |
454 qed "alls_P_eq_P_nth"; |
455 |
455 |
456 |
456 |
457 Goal "[| !x. P x --> Q x; (Alls x:xs. P(x)) |] ==> (Alls x:xs. Q(x))"; |
457 Goal "[| !x. P x --> Q x; (Alls x:xs. P(x)) |] ==> (Alls x:xs. Q(x))"; |
499 by (ALLGOALS Asm_simp_tac); |
499 by (ALLGOALS Asm_simp_tac); |
500 by (case_tac "f xa = x" 1); |
500 by (case_tac "f xa = x" 1); |
501 by (ALLGOALS Asm_simp_tac); |
501 by (ALLGOALS Asm_simp_tac); |
502 by (res_inst_tac [("x","xa")] exI 1); |
502 by (res_inst_tac [("x","xa")] exI 1); |
503 by (ALLGOALS Asm_simp_tac); |
503 by (ALLGOALS Asm_simp_tac); |
504 br impI 1; |
504 by (rtac impI 1); |
505 by (rotate_tac 1 1); |
505 by (rotate_tac 1 1); |
506 by (ALLGOALS Asm_full_simp_tac); |
506 by (ALLGOALS Asm_full_simp_tac); |
507 be exE 1; be conjE 1; |
507 by (etac exE 1); by (etac conjE 1); |
508 by (res_inst_tac [("x","y")] exI 1); |
508 by (res_inst_tac [("x","y")] exI 1); |
509 by (asm_simp_tac (HOL_ss addsimps [if_cancel]) 1); |
509 by (asm_simp_tac (HOL_ss addsimps [if_cancel]) 1); |
510 qed "mem_map_aux1"; |
510 qed "mem_map_aux1"; |
511 |
511 |
512 Goal |
512 Goal |
513 "(? y. y mem q & x = f y) --> x mem (map f q)"; |
513 "(? y. y mem q & x = f y) --> x mem (map f q)"; |
514 by (induct_thm_tac list_induct "q" 1); |
514 by (induct_thm_tac list_induct "q" 1); |
515 by (Asm_simp_tac 1); |
515 by (Asm_simp_tac 1); |
516 br impI 1; |
516 by (rtac impI 1); |
517 be exE 1; |
517 by (etac exE 1); |
518 be conjE 1; |
518 by (etac conjE 1); |
519 by (ALLGOALS Asm_simp_tac); |
519 by (ALLGOALS Asm_simp_tac); |
520 by (case_tac "xa = y" 1); |
520 by (case_tac "xa = y" 1); |
521 by (rotate_tac 2 1); |
521 by (rotate_tac 2 1); |
522 by (asm_full_simp_tac (HOL_ss addsimps [if_cancel]) 1); |
522 by (asm_full_simp_tac (HOL_ss addsimps [if_cancel]) 1); |
523 be impE 1; |
523 by (etac impE 1); |
524 by (asm_simp_tac (HOL_ss addsimps [if_cancel]) 1); |
524 by (asm_simp_tac (HOL_ss addsimps [if_cancel]) 1); |
525 by (case_tac "f xa = f y" 2); |
525 by (case_tac "f xa = f y" 2); |
526 by (res_inst_tac [("x","y")] exI 1); |
526 by (res_inst_tac [("x","y")] exI 1); |
527 by (asm_simp_tac (HOL_ss addsimps [if_cancel]) 1); |
527 by (asm_simp_tac (HOL_ss addsimps [if_cancel]) 1); |
528 by (Auto_tac); |
528 by (Auto_tac); |
529 qed "mem_map_aux2"; |
529 qed "mem_map_aux2"; |
530 |
530 |
531 |
531 |
532 Goal |
532 Goal |
533 "x mem (map f q) = (? y. y mem q & x = f y)"; |
533 "x mem (map f q) = (? y. y mem q & x = f y)"; |
534 br iffI 1; |
534 by (rtac iffI 1); |
535 br (mem_map_aux1 RS mp) 1; |
535 by (rtac (mem_map_aux1 RS mp) 1); |
536 br (mem_map_aux2 RS mp) 2; |
536 by (rtac (mem_map_aux2 RS mp) 2); |
537 by (ALLGOALS atac); |
537 by (ALLGOALS atac); |
538 qed "mem_map"; |
538 qed "mem_map"; |
539 |
539 |
540 Goal "A ~= [] --> hd(A @ B) = hd(A)"; |
540 Goal "A ~= [] --> hd(A @ B) = hd(A)"; |
541 by (induct_thm_tac list_induct "A" 1); |
541 by (induct_thm_tac list_induct "A" 1); |
683 |
683 |
684 (* SQUIGGOL LEMMAS *) |
684 (* SQUIGGOL LEMMAS *) |
685 |
685 |
686 |
686 |
687 Goalw [o_def] "map(f o g) = ((map f) o (map g))"; |
687 Goalw [o_def] "map(f o g) = ((map f) o (map g))"; |
688 br ext 1; |
688 by (rtac ext 1); |
689 by (simp_tac (HOL_ss addsimps [map_compose RS sym,o_def]) 1); |
689 by (simp_tac (HOL_ss addsimps [map_compose RS sym,o_def]) 1); |
690 qed "map_compose_ext"; |
690 qed "map_compose_ext"; |
691 |
691 |
692 Goal "map f (flat S) = flat(map (map f) S)"; |
692 Goal "map f (flat S) = flat(map (map f) S)"; |
693 by (induct_thm_tac list_induct "S" 1); |
693 by (induct_thm_tac list_induct "S" 1); |
837 qed "length_take_drop"; |
837 qed "length_take_drop"; |
838 |
838 |
839 |
839 |
840 Goal "ALL A. length(A) = n --> take(A@B) n = A"; |
840 Goal "ALL A. length(A) = n --> take(A@B) n = A"; |
841 by (induct_tac "n" 1); |
841 by (induct_tac "n" 1); |
842 br allI 1; |
842 by (rtac allI 1); |
843 br allI 2; |
843 by (rtac allI 2); |
844 by (induct_thm_tac list_induct "A" 1); |
844 by (induct_thm_tac list_induct "A" 1); |
845 by (induct_thm_tac list_induct "A" 3); |
845 by (induct_thm_tac list_induct "A" 3); |
846 by (ALLGOALS Asm_full_simp_tac); |
846 by (ALLGOALS Asm_full_simp_tac); |
847 qed_spec_mp "take_append"; |
847 qed_spec_mp "take_append"; |
848 |
848 |
849 Goal "ALL A. length(A) = n --> take(A@B) (n+k) = A@take B k"; |
849 Goal "ALL A. length(A) = n --> take(A@B) (n+k) = A@take B k"; |
850 by (induct_tac "n" 1); |
850 by (induct_tac "n" 1); |
851 br allI 1; |
851 by (rtac allI 1); |
852 br allI 2; |
852 by (rtac allI 2); |
853 by (induct_thm_tac list_induct "A" 1); |
853 by (induct_thm_tac list_induct "A" 1); |
854 by (induct_thm_tac list_induct "A" 3); |
854 by (induct_thm_tac list_induct "A" 3); |
855 by (ALLGOALS Asm_full_simp_tac); |
855 by (ALLGOALS Asm_full_simp_tac); |
856 qed_spec_mp "take_append2"; |
856 qed_spec_mp "take_append2"; |
857 |
857 |
863 by (ALLGOALS Asm_simp_tac); |
863 by (ALLGOALS Asm_simp_tac); |
864 qed_spec_mp "take_map"; |
864 qed_spec_mp "take_map"; |
865 |
865 |
866 Goal "ALL A. length(A) = n --> drop(A@B)n = B"; |
866 Goal "ALL A. length(A) = n --> drop(A@B)n = B"; |
867 by (induct_tac "n" 1); |
867 by (induct_tac "n" 1); |
868 br allI 1; |
868 by (rtac allI 1); |
869 br allI 2; |
869 by (rtac allI 2); |
870 by (induct_thm_tac list_induct "A" 1); |
870 by (induct_thm_tac list_induct "A" 1); |
871 by (induct_thm_tac list_induct "A" 3); |
871 by (induct_thm_tac list_induct "A" 3); |
872 by (ALLGOALS Asm_full_simp_tac); |
872 by (ALLGOALS Asm_full_simp_tac); |
873 qed_spec_mp "drop_append"; |
873 qed_spec_mp "drop_append"; |
874 |
874 |
875 Goal "ALL A. length(A) = n --> drop(A@B)(n+k) = drop B k"; |
875 Goal "ALL A. length(A) = n --> drop(A@B)(n+k) = drop B k"; |
876 by (induct_tac "n" 1); |
876 by (induct_tac "n" 1); |
877 br allI 1; |
877 by (rtac allI 1); |
878 br allI 2; |
878 by (rtac allI 2); |
879 by (induct_thm_tac list_induct "A" 1); |
879 by (induct_thm_tac list_induct "A" 1); |
880 by (induct_thm_tac list_induct "A" 3); |
880 by (induct_thm_tac list_induct "A" 3); |
881 by (ALLGOALS Asm_full_simp_tac); |
881 by (ALLGOALS Asm_full_simp_tac); |
882 qed_spec_mp "drop_append2"; |
882 qed_spec_mp "drop_append2"; |
883 |
883 |
884 |
884 |
885 Goal "ALL A. length(A) = n --> drop A n = []"; |
885 Goal "ALL A. length(A) = n --> drop A n = []"; |
886 by (induct_tac "n" 1); |
886 by (induct_tac "n" 1); |
887 br allI 1; |
887 by (rtac allI 1); |
888 br allI 2; |
888 by (rtac allI 2); |
889 by (induct_thm_tac list_induct "A" 1); |
889 by (induct_thm_tac list_induct "A" 1); |
890 by (induct_thm_tac list_induct "A" 3); |
890 by (induct_thm_tac list_induct "A" 3); |
891 by Auto_tac; |
891 by Auto_tac; |
892 qed_spec_mp "drop_all"; |
892 qed_spec_mp "drop_all"; |
893 |
893 |
900 qed_spec_mp "drop_map"; |
900 qed_spec_mp "drop_map"; |
901 |
901 |
902 |
902 |
903 Goal "ALL A. length(A) = n --> take A n = A"; |
903 Goal "ALL A. length(A) = n --> take A n = A"; |
904 by (induct_tac "n" 1); |
904 by (induct_tac "n" 1); |
905 br allI 1; |
905 by (rtac allI 1); |
906 br allI 2; |
906 by (rtac allI 2); |
907 by (induct_thm_tac list_induct "A" 1); |
907 by (induct_thm_tac list_induct "A" 1); |
908 by (induct_thm_tac list_induct "A" 3); |
908 by (induct_thm_tac list_induct "A" 3); |
909 by (ALLGOALS (simp_tac (simpset()))); |
909 by (ALLGOALS (simp_tac (simpset()))); |
910 by (asm_simp_tac ((simpset()) addsimps [le_eq_less_or_eq]) 1); |
910 by (asm_simp_tac ((simpset()) addsimps [le_eq_less_or_eq]) 1); |
911 qed_spec_mp "take_all"; |
911 qed_spec_mp "take_all"; |
947 |
947 |
948 Goal |
948 Goal |
949 "[| !a. f a e = a; !a. f e a = a; \ |
949 "[| !a. f a e = a; !a. f e a = a; \ |
950 \ !a b c. f a (f b c) = f(f a b) c |] \ |
950 \ !a b c. f a (f b c) = f(f a b) c |] \ |
951 \ ==> foldl f e (A @ B) = f(foldl f e A)(foldl f e B)"; |
951 \ ==> foldl f e (A @ B) = f(foldl f e A)(foldl f e B)"; |
952 br trans 1; |
952 by (rtac trans 1); |
953 br foldl_append 1; |
953 by (rtac foldl_append 1); |
954 br (foldl_neutr_distr) 1; |
954 by (rtac (foldl_neutr_distr) 1); |
955 by Auto_tac; |
955 by Auto_tac; |
956 qed "foldl_append_sym"; |
956 qed "foldl_append_sym"; |
957 |
957 |
958 Goal "ALL a. foldr f a (A @ B) = foldr f (foldr f a B) A"; |
958 Goal "ALL a. foldr f a (A @ B) = foldr f (foldr f a B) A"; |
959 by (induct_thm_tac list_induct "A" 1); |
959 by (induct_thm_tac list_induct "A" 1); |
1018 |
1018 |
1019 |
1019 |
1020 Goal "ALL i. i < length(A) --> nth i (map f A) = f(nth i A)"; |
1020 Goal "ALL i. i < length(A) --> nth i (map f A) = f(nth i A)"; |
1021 by (induct_thm_tac list_induct "A" 1); |
1021 by (induct_thm_tac list_induct "A" 1); |
1022 by (ALLGOALS(asm_simp_tac (simpset() delsimps [less_Suc_eq]))); |
1022 by (ALLGOALS(asm_simp_tac (simpset() delsimps [less_Suc_eq]))); |
1023 br allI 1; |
1023 by (rtac allI 1); |
1024 by (induct_tac "i" 1); |
1024 by (induct_tac "i" 1); |
1025 by (ALLGOALS(asm_simp_tac (simpset() addsimps [nth_0,nth_Suc]))); |
1025 by (ALLGOALS(asm_simp_tac (simpset() addsimps [nth_0,nth_Suc]))); |
1026 qed_spec_mp "nth_map"; |
1026 qed_spec_mp "nth_map"; |
1027 |
1027 |
1028 Goal "ALL i. i < length(A) --> nth i(A@B) = nth i A"; |
1028 Goal "ALL i. i < length(A) --> nth i(A@B) = nth i A"; |
1029 by (induct_thm_tac list_induct "A" 1); |
1029 by (induct_thm_tac list_induct "A" 1); |
1030 by (ALLGOALS(asm_simp_tac (simpset() delsimps [less_Suc_eq]))); |
1030 by (ALLGOALS(asm_simp_tac (simpset() delsimps [less_Suc_eq]))); |
1031 br allI 1; |
1031 by (rtac allI 1); |
1032 by (induct_tac "i" 1); |
1032 by (induct_tac "i" 1); |
1033 by (ALLGOALS(asm_simp_tac (simpset() addsimps [nth_0,nth_Suc]))); |
1033 by (ALLGOALS(asm_simp_tac (simpset() addsimps [nth_0,nth_Suc]))); |
1034 qed_spec_mp "nth_app_cancel_right"; |
1034 qed_spec_mp "nth_app_cancel_right"; |
1035 |
1035 |
1036 |
1036 |