[isabelle] usage of Isabelle as a simplifier in batch mode



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

--
Dr. Sven Schneider
Research Assistant

Hasso-Plattner-Institut
Campus Griebnitzsee | Universität Potsdam
Prof.-Dr.-Helmert-Straße 2 - 3 | 14482 Potsdam
Tel.: 0331 5509-353
www.hpi.de

Folgen Sie uns auch auf:
www.hpi.de/facebook | www.hpi.de/twitter
www.hpi.de/youtube | www.hpi.de/linkedin

Hasso-Plattner-Institut für Digital Engineering gGmbH
Sitz: Potsdam
Registergericht: AG Potsdam, HRB 12184 P
Geschäftsführer: Prof. Dr. Christoph Meinel (CEO), Dr. Marcus Kölling (CFO)

Design IT. Create Knowledge.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.