*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] Failing simproc*From*: Brian Huffman <huffman at in.tum.de>*Date*: Sat, 21 Jul 2012 10:25:49 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50097B0D.7060904@in.tum.de>*References*: <50067A05.1040609@in.tum.de> <500682C0.2000407@in.tum.de> <CAAMXsiamg8P0NdVv16efsWYTKHnmSjuG7_rrDra8L2ZKN8g-Og@mail.gmail.com> <50097B0D.7060904@in.tum.de>

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! 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) Stepping through this proof with "show_sorts" enabled reveals the problem: The inserted "x" has type "?'b3" instead of "?'b1", because rule_tac automatically renames schematics in the rule to avoid clashes with schematics in the proof goal. > So you decided against the generic approach of importing the schematic > variables? Was it because of efficiency? I haven't looked at efficiency yet. The more serious problem is that simprocs that use this approach now are broken! The simprocs in Provers/Arith/cancel_numerals.ML already try to use Variable.import_terms and Variable.export to temporarily fix schematics. But on Dmitriy's original example, natless_cancel_numerals returns an equation that cannot be used by the simplifier because its schematic type variables are instantiated. 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 the Variable.import/export technique, at least not until we figure this out. - Brian

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

**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

- Previous by Date: Re: [isabelle] Automating the auto-tools
- Next by Date: Re: [isabelle] Automating the auto-tools
- 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