Re: [isabelle] SMT.thy



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
> >>>
> >>>
> >>
> >
> >
> 







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