Email Gateway (Aug 19 2022 at 14:53): Email Gateway (Aug 19 2022 at 14:53):From: Holden Lee <hl422@cam.ac.uk>
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):
length l - 1 ≤ deg R (ring.coeff_list_to_poly R l)
*)
apply (unfold deg_def bound_def)
(* Unfolds successfully.
goal (1 subgoal):
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)"
Email Gateway (Aug 19 2022 at 14:54):From: Brian Huffman <huffman.brian.c@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,
Last updated: Apr 25 2024 at 20:15 UTC