Gergely Buday (Aug 18 2020 at 11:37): 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?
Mathias Fleury (Aug 18 2020 at 11:39):The ML command works at the same level as 'lemma'.
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...
Gergely Buday (Aug 18 2020 at 11:40):I see, thanks.
Manuel Eberl (Aug 18 2020 at 11:41):ML_prf
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.
Mathias Fleury (Aug 18 2020 at 11:43):ML_val works, but Manuel was faster
Manuel Eberl (Aug 18 2020 at 11:44):ML_valshould be stateless though.
Manuel Eberl (Aug 18 2020 at 11:46):Looks like a proof context is basically just a theory plus some extra generic data
Manuel Eberl (Aug 18 2020 at 11:47):don't think you can access that extra data directly
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.
Gergely Buday (Aug 18 2020 at 11:48):I see, @Mathias Fleury
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
Mathias Fleury (Aug 18 2020 at 11:52):But maybe Manuel knows a better way...
Manuel Eberl (Aug 18 2020 at 11:56):What do you mean by "manipulating contexts"?
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.
Mathias Fleury (Aug 18 2020 at 11:58):Context manipulation I did:
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.
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.
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…
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: Apr 19 2024 at 08:19 UTC