src/HOL/Library/Extended_Nat.thy
changeset 51366 abdcf1a7cabf
parent 51301 6822aa82aafa
child 51717 9e7d1c139569
equal deleted inserted replaced
51365:6b5250100db8 51366:abdcf1a7cabf
   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))