*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] Failing simproc*From*: Brian Huffman <huffman at in.tum.de>*Date*: Fri, 20 Jul 2012 15:06:41 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <500682C0.2000407@in.tum.de>*References*: <50067A05.1040609@in.tum.de> <500682C0.2000407@in.tum.de>

On Wed, Jul 18, 2012 at 11:32 AM, Lars Noschinski <noschinl at in.tum.de> wrote: > On 18.07.2012 10:55, Dmitriy Traytel wrote: >> >> Hi *, >> >> I stumbled upon some funny behaviour which prevents the simplifier in >> proving "True" in Isabelle2012 (also in 8a1ef12f7e6d). The reduced >> example is attached. > > > This exception is thrown by the simproc natless_cancel_sums (in > Nat_Arith.nat_cancel_sums), as the following succeeds: > > notepad > begin > ML_prf {* Delsimprocs [nth Nat_Arith.nat_cancel_sums 1] *} > have "(\<And>ys zs. length ys < Suc (length zs + length ys))" by simp > hence True > by simp > > The other simprocs in Nat_Arith also seem to be affected. For the record: This problem was caused by an interaction between simprocs and schematic type variables. More specifically, some internal proofs done by Nat_Arith simprocs would fail on terms that contain schematics. The problem is now fixed in revision 868dc809c8a2. Authors of simprocs should take note: The simplifier may run simprocs on terms containing schematics (type and/or term variables) and it is the responsibility of the simproc to handle this situation properly. A simproc must never instantiate any schematic variable. Some guidelines for simproc writers: Internal proofs should use the simplifier only in "safe" mode, i.e. only using the "safe" solvers, which avoid instantiating schematics. Also, avoid instantiating rules with terms from the input and then using those rules with rtac, because schematic variables in a rule are not preserved when the rule is applied. (The Nat_Arith simprocs failed to follow either of these guidelines.) - Brian

**Follow-Ups**:**Re: [isabelle] Failing simproc***From:*Lars Noschinski

**References**:**[isabelle] Failing simproc***From:*Dmitriy Traytel

**Re: [isabelle] Failing simproc***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] provers used by sledgehammer
- Next by Date: Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem
- Previous by Thread: Re: [isabelle] Failing simproc
- Next by Thread: Re: [isabelle] Failing simproc
- Cl-isabelle-users July 2012 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