Re: [isabelle] SMT.thy

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"

lemma "(x::int) = y+1 --> g (x - 1) = g y"


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"

Note that in any case "Main" does not need to be imported, because it
is already contained in SMT.


John Matthews wrote:
Actually, I'm trying to use this import statement:

  imports Main "~~/src/HOL/SMT/SMT"


On Feb 10, 2010, at 3:44 PM, John Matthews wrote:


I'm trying to use the new "smt" proof method in Isabelle2009-1.
Here's my theory header:

theory test
imports Main "~~/SMT/SMT"

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/
*** At command "theory".

Should I be loading SMT.thy some other way?


Attachment: smime.p7s
Description: S/MIME cryptographic signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.