*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] SMT.thy*From*: Sascha Boehme <boehmes at in.tum.de>*Date*: Fri, 12 Feb 2010 10:03:59 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BC717707-6952-4CDF-B5DA-47A231EB1F0F@galois.com>*References*: <24F385E6-72CF-4EF8-A36A-F0E207B134C1@galois.com> <3B2608B8-207F-45A9-BA3F-F20457FA3685@galois.com> <20100211081503.GA1737@lapbroy158> <BC717707-6952-4CDF-B5DA-47A231EB1F0F@galois.com>*User-agent*: Mutt/1.5.20 (2009-06-14)

Hello John, Uninterpreted functions are supported by the smt method. In your case, there are two ways to prove the lemma: 1) Use a different SMT solver, i.e., lemma "(x::int) = y+1 --> f (x - 1) = f y" using [[smt_solver=cvc3]] by smt 2) Apply some magic. In this case, tweak the default SMT solver Z3 as follows: lemma "(x::int) = y+1 --> f (x - 1) = f y" using [[z3_options="AUTO_CONFIG=false"]] by smt Both ways also work for your third example. Thanks for bringing up this issue. In newer versions of Isabelle, providing this odd Z3 option will not be necessary anymore in such situations. Regards, Sascha John Matthews wrote: > Thanks Sascha. Since I'm working in HOLCF I tried your approach (2), > which worked fine. > > Another question: Does the smt proof method support uninterpreted > functions? I tried to prove the following three lemmas using smt, > but only the first one succeeded: > > 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 > >>> > >>> > >> > > > > >

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

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

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

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

- Previous by Date: Re: [isabelle] SMT.thy
- Next by Date: [isabelle] PLMMS 2010 Call for Papers
- Previous by Thread: Re: [isabelle] SMT.thy
- Next by Thread: [isabelle] updating code that calls add_locale_i
- 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