[isabelle] Why does unfold fail to work?



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.