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?

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

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

I see, thanks.

`ML_prf`

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.

ML_val works, but Manuel was faster

`ML_val`

should be stateless though.

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

don't think you can access that extra data directly

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

I see, @Mathias Fleury

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

But maybe Manuel knows a better way...

What do you mean by "manipulating contexts"?

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.

Context manipulation I did:

- At some point I tried to localise some simprocs
- Declaring assumptions, variables (currently extending Isabelle smt tactic to supports veriT)

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.

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

I mean you can do `print_context`

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

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