Re: [isabelle] Proving with Goal.prove


2010/10/1 Michael Chan <mchan at>:
>> Does the value prop not contain the goal of lem1? If not, how can the
>> goal for the current goal state be retrieved?
> John,
> I'm not sure myself, but it seems like the prop here is:
> EX (x::'a) y::'a. y < x ==> (EX (x::'a) y::'a. y < x)

Additionally there is a (hidden) prop marker that separates all the
remaining subgoals from
the original goal. Since 'auto' cannot deal with the prop-marker it
fails. So to make your code
work you may want to strip the assumptions and remove the prop marker.

The following does work:

  val {prop,...} = Thm.rep_thm st
  val t = Goal.prove ctxt [] [] (Logic.unprotect
(Logic.strip_assums_concl prop)) (fn _ => tac)

But the above is somehow very low-level, if you want to look at
subparts of the goal in a tactic
in a convenient way you may want to have a look at the Subgoal.FOCUS
family of combinators.


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