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


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
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)))))"
% ---------------------

Sven Schneider

Dr. Sven Schneider
Research Assistant

Campus Griebnitzsee | Universität Potsdam
Prof.-Dr.-Helmert-Straße 2 - 3 | 14482 Potsdam
Tel.: 0331 5509-353

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.