Email Gateway (Aug 18 2022 at 16:23): Email Gateway (Aug 18 2022 at 16:23):From: Steve W <s.wong.731@gmail.com>
Hello,
I'm trying to experiment with Goal.prove on a very simple lemma:
ML {*
let
val trm = @{term "EX x. x = 0"}
val ctxt = @{context}
in
Goal.prove ctxt [] [] trm (K (auto_tac (clasimpset_of ctxt)))
end;
*}
Unfortunately, I get an exception saying "instantiate: type conflict". Does
anyone know what I'm doing wrong? I know I could write it as a tactic and
apply it in Isar, but I'm just trying to experiment with Goal.prove.
Regards,
Steve
Email Gateway (Aug 18 2022 at 16:23):From: Sascha Boehme <boehmes@in.tum.de>
Hello Steve,
Try using the prop antiquotation, i.e.,
val t = @{prop "EX x. x = 0"}
The background is that HOL is a logic embedded in Isabelle's
metalogic, and every HOL property needs to be coerced into a meta
justification, for example by using the prop antiquotation. A more
explicit way to express this would be as follows:
val t = HOLogic.mk_Trueprop @{term "EX x. x = 0"}
Regards,
Sascha
Steve W wrote:
Last updated: Apr 20 2024 at 12:26 UTC