794 val ss2 = |
794 val ss2 = |
795 simpset_of (\<^context> addsimps |
795 simpset_of (\<^context> addsimps |
796 [@{thm plus_vec_def}, @{thm times_vec_def}, |
796 [@{thm plus_vec_def}, @{thm times_vec_def}, |
797 @{thm minus_vec_def}, @{thm uminus_vec_def}, |
797 @{thm minus_vec_def}, @{thm uminus_vec_def}, |
798 @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def}, |
798 @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def}, |
799 @{thm scaleR_vec_def}, |
799 @{thm scaleR_vec_def}, @{thm vector_scalar_mult_def}]) |
800 @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}]) |
|
801 fun vector_arith_tac ctxt ths = |
800 fun vector_arith_tac ctxt ths = |
802 simp_tac (put_simpset ss1 ctxt) |
801 simp_tac (put_simpset ss1 ctxt) |
803 THEN' (fn i => resolve_tac ctxt @{thms Finite_Cartesian_Product.sum_cong_aux} i |
802 THEN' (fn i => resolve_tac ctxt @{thms Finite_Cartesian_Product.sum_cong_aux} i |
804 ORELSE resolve_tac ctxt @{thms sum.neutral} i |
803 ORELSE resolve_tac ctxt @{thms sum.neutral} i |
805 ORELSE simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm vec_eq_iff}]) i) |
804 ORELSE simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm vec_eq_iff}]) i) |