*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] Failing simproc*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Fri, 20 Jul 2012 17:36:45 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAMXsiamg8P0NdVv16efsWYTKHnmSjuG7_rrDra8L2ZKN8g-Og@mail.gmail.com>*References*: <50067A05.1040609@in.tum.de> <500682C0.2000407@in.tum.de> <CAAMXsiamg8P0NdVv16efsWYTKHnmSjuG7_rrDra8L2ZKN8g-Og@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.3) Gecko/20120329 Icedove/10.0.3

On 20.07.2012 15:06, Brian Huffman wrote:

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.

$ zgrep 'IGNORED result of simproc' * | cut -d\" -f2 | sort | uniq -c 45 Cfun.beta_cfun_proc 86 equal 2 Numeral_Simprocs.inteq_cancel_numerals 941 perm_simproc_fun 24814 record_eq_simp (src/HOL make all)

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.)

-- Lars

**Follow-Ups**:**Re: [isabelle] Failing simproc***From:*Florian Haftmann

**Re: [isabelle] Failing simproc***From:*Brian Huffman

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

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

**Re: [isabelle] Failing simproc***From:*Brian Huffman

- Previous by Date: Re: [isabelle] provers used by sledgehammer
- Next by Date: Re: [isabelle] provers used by sledgehammer
- 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