*To*: Sascha Boehme <boehmes at in.tum.de>*Subject*: Re: [isabelle] SMT.thy*From*: John Matthews <matthews at galois.com>*Date*: Thu, 11 Feb 2010 14:29:41 -0800*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <20100211081503.GA1737@lapbroy158>*References*: <24F385E6-72CF-4EF8-A36A-F0E207B134C1@galois.com> <3B2608B8-207F-45A9-BA3F-F20457FA3685@galois.com> <20100211081503.GA1737@lapbroy158>

lemma "(x::int) = y+1 --> abs (x - 1) = abs y" by smt consts f :: "int => int" lemma "(x::int) = y+1 --> f (x - 1) = f y" oops lemma "(x::int) = y+1 --> g (x - 1) = g y" oops Thanks, -john On Feb 11, 2010, at 12:15 AM, Sascha Boehme wrote:

Hello John, Thanks for reporting this bug; it will be fixed in newer versions of Isabelle. As for Isabelle2009-1, there are two possible workarounds (the first one is the recommended way): 1) Build the HOL-SMT image by (at the Isabelle2009-1 directory): ./build -m HOL-SMT HOL and load this when using SMT instead of the default HOL image. With this method, you may drop the path to the SMT theory; the import line may thus read "imports SMT". 2) Manually modify the file "~~/src/HOL/SMT/SMT_Base.thy", i.e., change the line starting with "imports" into imports Real "~~/src/HOL/Word/Word" "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Note that in any case "Main" does not need to be imported, because it is already contained in SMT. Regards, Sascha John Matthews wrote:Actually, I'm trying to use this import statement: imports Main "~~/src/HOL/SMT/SMT" Thanks, -john On Feb 10, 2010, at 3:44 PM, John Matthews wrote:Hello, I'm trying to use the new "smt" proof method in Isabelle2009-1. Here's my theory header: theory test imports Main "~~/SMT/SMT" begin However, Isabelle reports the following error when trying to load the SMT theory:*** Theory loader: failed to load "SMT" (unresolved "Z3","SMT_Base")*** Theory loader: failed to load "Z3" (unresolved "SMT_Base") *** Undeclared class: "len" *** At command "definition" (line 67 of "/Applications/Isabelle/ Isabelle/src/HOL/SMT/SMT_Base.thy"). *** At command "theory". Should I be loading SMT.thy some other way? Thanks, -john

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] SMT.thy***From:*Sascha Boehme

**References**:**[isabelle] SMT.thy***From:*John Matthews

**Re: [isabelle] SMT.thy***From:*John Matthews

**Re: [isabelle] SMT.thy***From:*Sascha Boehme

- Previous by Date: Re: [isabelle] updating code that calls add_locale_i
- Next by Date: Re: [isabelle] SMT.thy
- Previous by Thread: Re: [isabelle] SMT.thy
- Next by Thread: Re: [isabelle] SMT.thy
- Cl-isabelle-users February 2010 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