[isabelle-dev] simproc divide_cancel_factor produces error

[Lars Noschinski]

Hi everyone,

in the following snippet, applying the simplifier causes an error:

------------------------------------------
theory Scratch
   imports Complex_Main
begin

lemma
   shows "(3 / 2) * ln n = ((6 * k * ln n) / n) * ((1 / 2 * n / k) / 2)"
apply simp
------------------------------------------

outputs

------------------------------------------
Proof failed.
(if n = 0 then 0 else 6 * (k * ln n) / 1) * 2 / (4 * k) =
2 * (Numeral1 * (if n = 0 then 0 else 6 * (k * ln n) / 1)) / (2 * (2 * k))
  1. n ≠ Numeral0 ⟶ k * (ln n * (2 * 6)) / (k * 4) = k * (ln n * 12) / 
(k * 4)
1 unsolved goal(s)!
The error(s) above occurred for the goal statement:
(if n = 0 then 0 else 6 * (k * ln n) / 1) * 2 / (4 * k) =
2 * (Numeral1 * (if n = 0 then 0 else 6 * (k * ln n) / 1)) / (2 * (2 * k))
------------------------------------------

This is caused by the simproc divide_cancel_factor; when removing this 
simproc, the error goes away:

   apply (tactic {* simp_tac (Simplifier.delsimprocs (@{simpset},
     [nth Numeral_Simprocs.cancel_factors 6])) 1 *})

BTW: Is there a nicer way to remove one these old simprocs from the simpset?

   -- Lars