Stream: Isabelle/ML

Topic: Using facts proved in Isabelle/ML

view this post on Zulip Ciarán Dunne (Apr 24 2022 at 16:39):

Dear Isabelle users,

I have successfully proved a list of facts using a combination of List.foldl
and Proof.theorem to yield a new context ctxt with these theorems available.

I then want to prove some more facts, using the facts now available in ctxt
in the thm list given to Proof.unfolding.

  1. What is the best way for me to access the proved theorems?
    I'm currently using Global_Theory.get_thm and coercing the
    lthy : local_theory into a theory to retrieve them by name, which feels sloppy.
    Is there a version of Proof.theorem which returns a thm and Proof.context?

  2. When I try to proof my new facts using those available in ctxt, the proof fails.
    I have been able to successfully emulate what I'm trying to do in toplevel Isar,
    using ML and local_setup keywords. But trying to do this within one ML function
    has proved difficult.

I assume that I am handling my contexts in a poor fashion. Any advice?

Thanks,
Ciaran

view this post on Zulip Ciarán Dunne (Apr 25 2022 at 11:48):

Got it! I was building my new goal using the wrong term :rolling_eyes:, so my other facts didn't work.

Last updated: Jul 15 2022 at 23:21 UTC