src/HOL/Numeral_Simprocs.thy
changeset 45463 9a588a835c1e
parent 45462 aba629d6cee5
child 45607 16b4f5774621
equal deleted inserted replaced
45462:aba629d6cee5 45463:9a588a835c1e
   228   ("((l::nat) + m) - n" | "(l::nat) - (m + n)" |
   228   ("((l::nat) + m) - n" | "(l::nat) - (m + n)" |
   229    "(l::nat) * m - n" | "(l::nat) - m * n" |
   229    "(l::nat) * m - n" | "(l::nat) - m * n" |
   230    "Suc m - n" | "m - Suc n") =
   230    "Suc m - n" | "m - Suc n") =
   231   {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *}
   231   {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *}
   232 
   232 
       
   233 simproc_setup nat_eq_cancel_numeral_factor
       
   234   ("(l::nat) * m = n" | "(l::nat) = m * n") =
       
   235   {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor *}
       
   236 
       
   237 simproc_setup nat_less_cancel_numeral_factor
       
   238   ("(l::nat) * m < n" | "(l::nat) < m * n") =
       
   239   {* fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor *}
       
   240 
       
   241 simproc_setup nat_le_cancel_numeral_factor
       
   242   ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
       
   243   {* fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor *}
       
   244 
       
   245 simproc_setup nat_div_cancel_numeral_factor
       
   246   ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
       
   247   {* fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor *}
       
   248 
       
   249 simproc_setup nat_dvd_cancel_numeral_factor
       
   250   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
       
   251   {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor *}
       
   252 
   233 simproc_setup nat_eq_cancel_factor
   253 simproc_setup nat_eq_cancel_factor
   234   ("(l::nat) * m = n" | "(l::nat) = m * n") =
   254   ("(l::nat) * m = n" | "(l::nat) = m * n") =
   235   {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *}
   255   {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *}
   236 
   256 
   237 simproc_setup nat_less_cancel_factor
   257 simproc_setup nat_less_cancel_factor
   240 
   260 
   241 simproc_setup nat_le_cancel_factor
   261 simproc_setup nat_le_cancel_factor
   242   ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
   262   ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
   243   {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *}
   263   {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *}
   244 
   264 
   245 simproc_setup nat_divide_cancel_factor
   265 simproc_setup nat_div_cancel_factor
   246   ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
   266   ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
   247   {* fn phi => Nat_Numeral_Simprocs.divide_cancel_factor *}
   267   {* fn phi => Nat_Numeral_Simprocs.div_cancel_factor *}
   248 
   268 
   249 simproc_setup nat_dvd_cancel_factor
   269 simproc_setup nat_dvd_cancel_factor
   250   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
   270   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
   251   {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
   271   {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
   252 
   272