*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Problems with multiple patterns in simproc_setup*From*: Christoph Madlener <madlener at in.tum.de>*Date*: Wed, 23 Oct 2019 09:54:07 +0200*User-agent*: Roundcube Webmail/1.3.3

Hello,

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

**Follow-Ups**:**Re: [isabelle] Problems with multiple patterns in simproc_setup***From:*Mathias Fleury

- Previous by Date: [isabelle] Probability P(x in M, Q) usage
- Next by Date: [isabelle] primrec
- Previous by Thread: [isabelle] Probability P(x in M, Q) usage
- Next by Thread: Re: [isabelle] Problems with multiple patterns in simproc_setup
- Cl-isabelle-users October 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list