497 fun find_first_t _ _ [] = raise TERM("find_first_t", []) |
497 fun find_first_t _ _ [] = raise TERM("find_first_t", []) |
498 | find_first_t past u (t::terms) = |
498 | find_first_t past u (t::terms) = |
499 if u aconv t then (rev past @ terms) |
499 if u aconv t then (rev past @ terms) |
500 else find_first_t (t::past) u terms |
500 else find_first_t (t::past) u terms |
501 |
501 |
|
502 fun dest_summing (Const (@{const_name Groups.plus}, _) $ t $ u, ts) = |
|
503 dest_summing (t, dest_summing (u, ts)) |
|
504 | dest_summing (t, ts) = t :: ts |
|
505 |
502 val mk_sum = Arith_Data.long_mk_sum |
506 val mk_sum = Arith_Data.long_mk_sum |
503 val dest_sum = Arith_Data.dest_sum |
507 fun dest_sum t = dest_summing (t, []) |
504 val find_first = find_first_t [] |
508 val find_first = find_first_t [] |
505 val trans_tac = Numeral_Simprocs.trans_tac |
509 val trans_tac = Numeral_Simprocs.trans_tac |
506 val norm_ss = HOL_basic_ss addsimps |
510 val norm_ss = HOL_basic_ss addsimps |
507 @{thms add_ac add_0_left add_0_right} |
511 @{thms add_ac add_0_left add_0_right} |
508 fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) |
512 fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) |