*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] Failing simproc*From*: Makarius <makarius at sketis.net>*Date*: Sat, 21 Jul 2012 20:19:42 +0200 (CEST)*Cc*: Lars Noschinski <noschinl at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAMXsiZKw=w73Dkik_yTsjHF0qtO9++Sqgmd6fwzQAUYJ02mMg@mail.gmail.com>*References*: <50067A05.1040609@in.tum.de> <500682C0.2000407@in.tum.de> <CAAMXsiamg8P0NdVv16efsWYTKHnmSjuG7_rrDra8L2ZKN8g-Og@mail.gmail.com> <50097B0D.7060904@in.tum.de> <CAAMXsiZKw=w73Dkik_yTsjHF0qtO9++Sqgmd6fwzQAUYJ02mMg@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Sat, 21 Jul 2012, Brian Huffman wrote:

On Fri, Jul 20, 2012 at 5:36 PM, Lars Noschinski <noschinl at in.tum.de> wrote:On 20.07.2012 15:06, Brian Huffman wrote: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.)Perhaps I can explain this better. Here's how the Nat_Arith cancellation simprocs worked before yesterday's rev. 868dc809c8a2 -- note that this technique is *wrong* and simproc writers must avoid it!

What is wrong, fixed, broken now? I am confused.

The idea is to prove e.g. "(a + x + b < c + x + d) = (a + b < c + d)" by inserting "x" on the right, and then doing ac rewriting. The simproc does the same steps as this proof script: schematic_lemma "(a + size (x::?'b1::size) + b < c + size (x::?'b1::size) + d) = (a + b < c + d)" apply (rule_tac ?k.1 = "size x" in nat_add_left_cancel_less [THEN subst_equals]) apply (simp only: add_ac)

I'm not sure, but there might be a bug in Variable.export and related functions. For example: ML_val {* let val ctxt = @{context} val ts1 = [Thm.term_of @{cpat "size (x::?'a::size)"}] val (ts2, ctxt') = Variable.import_terms true ts1 ctxt val ts3 = Variable.export_terms ctxt' ctxt ts2 in (ts1, ts2, ts3) end *} val it = ([Const ("Nat.size_class.size", "?'a \<Rightarrow> nat") $ Free ("x", "?'a")], [Const ("Nat.size_class.size", "'a \<Rightarrow> nat") $ Free ("x", "'a")], [Const ("Nat.size_class.size", "'a \<Rightarrow> nat") $ Free ("x", "'a")]): term list * term list * term list The export_terms step does nothing at all! (This example actually works correctly if we replace "x" with "?x" in the input term.)I'm afraid we can't recommend simproc writers to use theVariable.import/export technique, at least not until we figure this out.

Makarius

**Follow-Ups**:**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

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

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

- Previous by Date: Re: [isabelle] Failing simproc
- Next by Date: Re: [isabelle] Schematic vars or universal bound vars in 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