*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Thu, 19 Jul 2012 10:06:53 -0500*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

First, I ask a straightforward question. If I declare a type, such as typedecl sT,

NITPICK STUFF

Jasmine Blanchette rates these SAT solvers like this:

nitpick[verbose,user_axioms,sat_solver=MiniSat_JNI] nitpick[verbose,user_axioms,sat_solver=CryptoMiniSat_JNI] nitpick[verbose,user_axioms,sat_solver=Lingeling_JNI] nitpick[verbose,user_axioms,sat_solver=SAT4J] nitpick[verbose,user_axioms,sat_solver=SAT4J_Light] SLEDGEHAMMER STUFF

SLEDGEHAMMER YICES

NITPICK'S COUNTERX: PENCIL & PAPER LOGIC vs. ISABELLE'S LOGIC

Some responses, whether sent or thought, might be:

Regards, GB theory sTs_Empty_Exist_Nitpick imports Main begin declare[[show_brackets=true]] typedecl sT consts emS::sT consts inS::"sT => sT => bool" (infixl "IN" 55) axiomatization where eeA:"!x. ¬(x IN emS)" theorem emS_is_unique1: "!u. (!x. ~(x IN u)) --> u = emS" nitpick[verbose,user_axioms] oops axiomatization where exA: "!u. !v. ((!x. x IN u <-> x IN v) --> u = v)" theorem emS_is_unique2: "!u. (!x. ~(x IN u)) --> u = emS" by (metis eeA exA) end

theory sTs_Empty_Exist_Nitpick imports Main begin declare[[show_brackets=true]] typedecl sT consts emS::sT consts inS::"sT => sT => bool" (infixl "IN" 55) axiomatization where eeA:"!x. \<not>(x IN emS)" theorem emS_is_unique1: "!u. (!x. ~(x IN u)) --> u = emS" nitpick[verbose,user_axioms] oops axiomatization where exA: "!u. !v. ((!x. x IN u <-> x IN v) --> u = v)" theorem emS_is_unique2: "!u. (!x. ~(x IN u)) --> u = emS" by (metis eeA exA) end

**Follow-Ups**:**Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Gottfried Barrow

**Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Date: Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem
- Previous by Thread: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Thread: Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem
- 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