From: Sven Schneider <email@example.com>
I would like to use Isabelle as an external tool to simplify terms.
My terms currently contain only real valued variables, linear
arithmetic, and quantification for some of these variables (i.e., there
are some free variables).
The terms I consider are often greatly simplified using clarsimp already.
Is there a way to execute Isabelle in batch mode to obtain that
I could imagine to generate the following file, to execute Isabelle
somehow on that file, and to retrieve the simplified term from "result.txt".
lemma foo1 [simp]: "((x::real) ≤ y & y=x) = (y=x)"
lemma foo2 [simp]: "Ex ((≤) (y::real)) = True"
(∃(x::real). (x ≥ y)∧ ((∃(x::real). (x ≥ y)∧ ((y ≥ 4) ∧ (y = 4)))))"
From: Makarius <firstname.lastname@example.org>
In principle you can use the Isabelle server, as documented in the "system"
manual chapter 4: you submit theory sources via a protocol message and get
results eventually (regular messages, warnings, errors etc.).
Often it is better to do it the other way round: assume a running Isabelle
application and invoke your tool from an existing theory context. There are
various possibilities to do this, e.g. as a Scala function from ML ("system
manual section 5.2), or as a TCP server from ML (like Isabelle/Naproche does).
All this works both in the Prover IDE (Isabelle/jEdit) and in batch mode
In contrast, invoking Isabelle as a whole in batch mode is going the be very
slow: it basically means to run a certain "isabelle build" process each time.
The remaining question: What is your tool? How is it used?
Last updated: Dec 08 2021 at 09:20 UTC