*To*: Holden Lee <hl422 at cam.ac.uk>*Subject*: Re: [isabelle] Why does unfold fail to work?*From*: Brian Huffman <huffman.brian.c at gmail.com>*Date*: Wed, 16 Jul 2014 10:02:12 -0700*Cc*: Isabelle Users ML <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAKSvo_bMq58=_Rg8oKMXG+ZNkSsGP+ZfX5OEyri_JEU3-uGUYw@mail.gmail.com>*References*: <CAKSvo_bMq58=_Rg8oKMXG+ZNkSsGP+ZfX5OEyri_JEU3-uGUYw@mail.gmail.com>

Hi Holden, Try typing thm ring.coeff_list_to_poly_def and see whether the definition has a side condition attached to it (i.e. does it have the form "_ ==> _ = _" rather than just "_ = _"). When "definition" is used to define a constant within a locale context, the exported theorem <locale-name>.foo_def typically has the locale predicate attached as an extra assumption. This will cause problems when you try to unfold it. If you have an appropriate fact like "ring R" available in your proof, you could try something like unfold ring.coeff_list_to_poly_def [OF `ring R`] to get an unconditional theorem. However, the best-supported way to reason about constants defined in a locale context is to state all your lemmas in the same locale, and then use the locale version of the _def rule (i.e. the one without the "ring" qualifier). lemma (in ring) "..." unfolding coeff_list_to_poly_def Hope this helps, - Brian On Wed, Jul 16, 2014 at 2:19 AM, Holden Lee <hl422 at cam.ac.uk> wrote: > Here's a snippet from a proof. How can I force Isabelle to unfold the > definition? > > from a2 have "deg R (ring.coeff_list_to_poly R l) ≥ (length l) - 1" > (* > goal (1 subgoal): > 1. length l - 1 ≤ deg R (ring.coeff_list_to_poly R l) > *) > apply (unfold deg_def bound_def) > (* Unfolds successfully. > goal (1 subgoal): > 1. l ! (length l - 1) ≠ \zero > length l - 1 ≤ (LEAST n. ∀m>n. coeff (UP R) (*ring.coeff_list_to_poly* > R l) m = \zero) > *) > apply (unfold *ring.coeff_list_to_poly_def*) > (*Failed to apply proof method*) > > For reference: > > definition (in ring) *coeff_list_to_poly*::"'a list ⇒ 'a polytype" > where "coeff_list_to_poly l = (λn. if (n < length l) then (l ! n) else > \zero)"

**References**:**[isabelle] Why does unfold fail to work?***From:*Holden Lee

- Previous by Date: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Next by Date: [isabelle] Record for module?
- Previous by Thread: [isabelle] Why does unfold fail to work?
- Next by Thread: [isabelle] Isabelle2014-RC0: Computations with rational numbers
- Cl-isabelle-users July 2014 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