Stream: Beginner Questions

Topic: Inspecting context


view this post on Zulip Gergely Buday (Aug 18 2020 at 11:37):

I tried to inspect the context with

theorem "A ⟹ A"
proof -
ML ‹ val foo = @{context} ›

but the system pointed to the problem that

"Bad context for command "ML"⌂ -- using reset state "

What is wrong here with my ML code?

view this post on Zulip Mathias Fleury (Aug 18 2020 at 11:39):

The ML command works at the same level as 'lemma'.

view this post on Zulip Mathias Fleury (Aug 18 2020 at 11:40):

So ML does not work inside proofs, but I don't know how to call ML inside proofs...

view this post on Zulip Gergely Buday (Aug 18 2020 at 11:40):

I see, thanks.

view this post on Zulip Manuel Eberl (Aug 18 2020 at 11:41):

ML_prf

view this post on Zulip Gergely Buday (Aug 18 2020 at 11:42):

Indeed, @Manuel Eberl . Next question: Proof.context seems to be an abstract data type. Is there a function that shows its contents? I did not find one in the Isabelle Cookbook.

view this post on Zulip Mathias Fleury (Aug 18 2020 at 11:43):

ML_val works, but Manuel was faster

view this post on Zulip Manuel Eberl (Aug 18 2020 at 11:44):

ML_valshould be stateless though.

view this post on Zulip Manuel Eberl (Aug 18 2020 at 11:46):

Looks like a proof context is basically just a theory plus some extra generic data

view this post on Zulip Manuel Eberl (Aug 18 2020 at 11:47):

don't think you can access that extra data directly

view this post on Zulip Mathias Fleury (Aug 18 2020 at 11:47):

I am not convinced looking inside a context is a good idea. ASFAIK contexts are a nightmare that no-one really understands.

view this post on Zulip Gergely Buday (Aug 18 2020 at 11:48):

I see, @Mathias Fleury

view this post on Zulip Mathias Fleury (Aug 18 2020 at 11:51):

Basically, whenever I try manipulating contexts, I try to either (i) find an example somewhere in the ML files or (ii) find a email from Makarius where (he rants that whoever asks is doing it wrong and) gives the "correct" way to do it

view this post on Zulip Mathias Fleury (Aug 18 2020 at 11:52):

But maybe Manuel knows a better way...

view this post on Zulip Manuel Eberl (Aug 18 2020 at 11:56):

What do you mean by "manipulating contexts"?

view this post on Zulip Manuel Eberl (Aug 18 2020 at 11:57):

But yeah I haven't really understood how to work with contexts myself. There are still many things about them that I have no idea how to do because I never needed to do them, fortunately.

view this post on Zulip Mathias Fleury (Aug 18 2020 at 11:58):

Context manipulation I did:

view this post on Zulip Gergely Buday (Aug 18 2020 at 11:59):

My, probably failed idea was to understand better basic Isar primitives by looking at the Isar Virtual Machine state transitions. From your contribution it seems that this is not a doable way. I digged into the Isar codebase but it is hard to understand what is going on.

view this post on Zulip Mathias Fleury (Aug 18 2020 at 12:00):

That is way beyond what I ever tried to understand. I cannot really help you for that.

view this post on Zulip Manuel Eberl (Aug 18 2020 at 12:02):

I mean you can do print_context in Isar and that will at least show you the fixed variables and assumptions, I think…

view this post on Zulip Mathias Fleury (Aug 18 2020 at 12:02):

Jasmin once told me that Isar is basically mapping everything to the corresponding tactic (subgoal_tac) and hiding it nicely via keywords


Last updated: Feb 27 2024 at 08:17 UTC