[isabelle] Problems with multiple patterns in simproc_setup



Hello,

I am writing some simprocs and encountered a problem when using simproc_setup to install them. As you can see in the attached example, when multiple patterns for the simproc contain the same variable, the simproc isn't triggered for any of the given patterns. (I also encountered a case where the simproc was triggered for some, but not all given patterns)

The problem can be avoided by either using unique identifiers, calling simproc_setup multiple times or using Simplifier.make_simproc - note that for the latter the patterns work as expected. I also attached an example with working solutions.

Best regards,
Christoph
theory Simproc_Match_Not_Working
imports Main
begin

ML\<open>
fun sum_prod_simproc _ _ _ = 
let
  val _ = Pretty.writeln (Pretty.str "simproc triggered")
in
  NONE
end
\<close>

simproc_setup sum_prod ("prod f A" | "sum f B") = \<open>sum_prod_simproc\<close>

lemma "(\<Sum>i=1..3. i) = (\<Sum>i=0..2. i + 1)"
  apply simp
  sorry

lemma "(\<Prod>i=1..3. i) = (\<Prod>i=0..2. i + 1)"
  apply simp
  sorry



end
theory Simproc_Match_Working
imports Main
begin

ML\<open>
fun sum_prod_simproc _ _ _ = 
let
  val _ = Pretty.writeln (Pretty.str "simproc triggered")
in
  NONE
end
\<close>

(* 
  This simproc works as expected. However changing \<open>f'\<close> to \<open>f\<close> will break it
  (see Simproc_Match_Not_Working.thy). Changing the identifier for the set (here \<open>A\<close>)
  has no effect as far as I can tell, i.e. \<open>("prod f A" | "sum f B")\<close> does not 
  work either.
*)
simproc_setup sum_prod ("prod f A" | "sum f' A") = \<open>sum_prod_simproc\<close>

lemma "(\<Sum>i=1..3. i) = (\<Sum>i=0..2. i + 1)"
  apply simp
  sorry

lemma "(\<Prod>i=1..3. i) = (\<Prod>i=0..2. i + 1)"
  apply simp
  sorry

(*
  When not using \<open>simproc_setup\<close> this problem does not arise. In the following
  the exact same patterns are used which break the \<open>simproc_setup\<close> version,
  however in this case it works as expected.
*)
ML\<open>
val sum_prod' = Simplifier.make_simproc \<^context> "sum_prod_simproc"
  {lhss = [\<^term>\<open>prod f A\<close>, \<^term>\<open>sum f A\<close>], proc = sum_prod_simproc}
\<close>

lemma "(\<Sum>i=1..3. i) = (\<Sum>i=0..2. i + 1)"
  apply (tactic \<open>simp_tac ((put_simpset HOL_basic_ss \<^context>) addsimprocs [sum_prod']) 1\<close>)
  sorry

lemma "(\<Prod>i=1..3. i) = (\<Prod>i=0..2. i + 1)"
  apply (tactic \<open>simp_tac ((put_simpset HOL_basic_ss \<^context>) addsimprocs [sum_prod']) 1\<close>)
  sorry  



end


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.