Re: [isabelle] Proving with Goal.prove



I want to add that I know foo could just be auto_tac (clasimpset_of
ctxt) and proves lem1, but I'm experimenting with Goal.prove.
Specifically, I want to see why Goal.prove fails.

Thanks

John

On Thu, Sep 30, 2010 at 2:00 AM, John Munroe <munddr at gmail.com> wrote:
> Hello again,
>
> I'm trying another example with Goal.prove, but it can't seem to
> discharge the proof goal. I must have done something wrong:
>
> ML {*
>
> fun foo ctxt st =
>  let
>    val {prop,...} = Thm.rep_thm st
>    val tac = auto_tac (clasimpset_of ctxt)
>    val t = Goal.prove ctxt [] [] prop
>      (fn _ => tac)
>  in
>    tac st
>  end;
>
> *}
>
> lemma lem1: "EX x y. x = y"
> apply (tactic {* foo @{context} *})
>
> Does the value prop not contain the goal of lem1? If not, how can the
> goal for the current goal state be retrieved?
>
> Thanks again!
>
> John
>





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