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.

view this post on Zulip Notification Bot (Apr 28 2022 at 08:55):

Ciarán Dunne has marked this topic as resolved.

Last updated: Nov 01 2025 at 01:47 UTC