*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Sledgehammer and Nitpick from the command line?*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Thu, 26 Jul 2012 08:50:50 -0500*In-reply-to*: <16675520-E312-468F-B925-2D6E0EAB040C@gmail.com>*References*: <5010A92E.4030909@gmx.com> <16675520-E312-468F-B925-2D6E0EAB040C@gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/26/2012 4:36 AM, Jasmin Blanchette wrote:

The "system.pdf" manual explains how to process Isabelle theories onthe command line. I never remember the exact syntaxes and have to lookit up each time, but look for the "isabelle usedir" tool. (There mightbe other tools as well.) This is nothing specific to Sledgehammer.Regards, Jasmin

I'll try using i3p: http://pu.inf.uni-tuebingen.de/i3p/

DETAILS

Building z0 ...

With no sledgehammer command in, usedir work as expected.

Here is the theory with sledgehammer: theory z0 imports z0i begin sledgehammer_params[verbose=true,isar_proof=false,timeout=120,provers=" z3 e spass z3_tptp cvc3 "] theorem emS_is_unique_Sn: "~(\<forall>u. (\<forall>x. x nIN u) \<longrightarrow> u = emS)" apply(auto) sledgehammer oops end Here is the file it imports: theory z0i imports Main begin typedecl --"The primitive set type: everything is a set." sT consts --"Set membership predicate: to be axiomatized by subsequent axioms." inS::"sT \<Rightarrow> sT \<Rightarrow> bool" (infixl "IN" 55) abbreviation

consts --"The empty set: naively named as a constant." emS::sT axiomatization --"Axiom of existence: the empty set is empty." where eeA:"\<forall>x. \<not>(x IN emS)" axiomatization --"Axiom of extention: set equality." where

theorem emS_is_unique --"The empty set is unique.": "\<forall>u. (\<forall>x. x nIN u) \<longrightarrow> u = emS" by (metis eeA exA) end Here is ROOT.ML (* no_document use_thy "ThisTheory"; use_thy "ThatTheory"; *) use_thy "z0"; Here is the usedir command: isabelle usedir -b HOL z0 Here are my usedir etc/settings

Regards, GB

**Attachment:
120726__sledge_with_usedir.zip**

**References**:**[isabelle] Sledgehammer and Nitpick from the command line?***From:*Gottfried Barrow

**Re: [isabelle] Sledgehammer and Nitpick from the command line?***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] Uniqueness quantification
- Next by Date: Re: [isabelle] HOLCF equality type class
- Previous by Thread: Re: [isabelle] Sledgehammer and Nitpick from the command line?
- Next by Thread: Re: [isabelle] Sledgehammer and Nitpick from the command line?
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list