Email Gateway (Aug 03 2022 at 12:50): Email Gateway (Aug 03 2022 at 12:50):From: Gebistorf Cedric <gecedric@student.ethz.ch>
Hello everyone,
I am currently trying to automate some stuff in Isabelle/ML but I am running into a problem. Unfortunately I the code base is rather big and I cannot seem to produce a small example where the same problem is occurring. Therefore I try to explain the problem on an abstract level:
I have two functions "contextChangingFunction1" and "contextChangingFunction2" which, as the name suggests, are functions from local_theory to local_theory. Here "contextChangingFunction1" defines some function in the current context using "Function_Fun.add_fun" and then "contextChangingFunction2" proofs a lemma which uses the "eresolve_tac" with the ".elims" theorem of the newly defined function.
At the moment I can use these two functions with the "local_setup"-Isar command to change my context like in VERSION 1 (below). Unfortunately if I chain them together as in VERSION 2 (also below) I get an error because the proof of the lemma fails. I cannot seem to work out an explanation for my problem as I had the impression that "local_setup" only executes the function given to change the current context. But if that would be the case, then VERSION 1 and VERSION 2 would have an equivalent result.
Does anyone know what the reason for this could be? Or is this a problem that can only be narrowed down considering the whole code-base?
Cheers and thanks for your help,
Cedric
VERSION 1 (works):
local_setup \<open>
contextChangingFunction1
\<close>
local_setup \<open>
contextChangingFunction2
\<close>
VERSION 2 (does not work):
local_setup \<open>
contextChangingFunction1
#> contextChangingFunction2
\<close>
ML-MOCKUP OF THE TWO FUNCTIONS CORE FUNCTIONALITY:
ML \<open>
fun contextChangingFunction1 (ctxt: local_theory) =
Function_Fun.add_fun [(Binding.name funcName, ...)] ...;
fun contextChangingFunction2 (ctxt: local_theory) =
let
val proof =
Goal.prove ctxt [] [] someGoal
(fn _ => ...
THEN (eresolve_tac ctxt [Proof_Context.get_thm ctxt "funcName.elims")] 1)
... );
in
(Local_Theory.note ((Binding.name lemmaName, ...), [proof]) #> snd) ctxt
end;
\<close>
Last updated: Apr 19 2024 at 12:27 UTC