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