Re: [isabelle] Why does unfold fail to work?



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.