Stream: Isabelle/ML

Topic: Differentiate hyps from context

view this post on Zulip Lukas Stevens (Sep 29 2021 at 16:06):

When I call Thm.hyps_of I get a list of open hypotheses of a theorem. Additionally, I may have a context that has the premises given by Assumption.all_prems_of. Is there an efficient way to determine whether all hypotheses of the theorem are also premises of the context and can therefore considered to be closed (w.r.t the context)?

view this post on Zulip Lukas Stevens (Sep 30 2021 at 16:10):

I think what I really need is to discharge those assumptions. Normally, the function Assumption.export seems to be the right tool for the job. However, I only have one context so what is the target context? Just the global context?

Last updated: Dec 07 2023 at 16:21 UTC