Email Gateway (Oct 12 2021 at 10:06): Email Gateway (Oct 12 2021 at 10:06):From: Sven Schneider <sven.schneider@hpi.de>
Hi,
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
simplified term?
I could imagine to generate the following file, to execute Isabelle
somehow on that file, and to retrieve the simplified term from "result.txt".
% ---------------------
theory Scratch
imports HOL.Real
begin
lemma foo1 [simp]: "((x::real) ≤ y & y=x) = (y=x)"
by force
lemma foo2 [simp]: "Ex ((≤) (y::real)) = True"
by force
lemma "
(∃(x::real). (x ≥ y)∧ ((∃(x::real). (x ≥ y)∧ ((y ≥ 4) ∧ (y = 4)))))"
apply(clarsimp)
export_first_goal("result.txt")
% ---------------------
Best,
Sven Schneider
Email Gateway (Oct 12 2021 at 15:33):From: Makarius <makarius@sketis.net>
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
(isabelle build).
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?
Makarius
Last updated: Apr 19 2024 at 20:15 UTC