Email Gateway (Aug 19 2022 at 14:09): Email Gateway (Aug 19 2022 at 14:09):From: Thomas Sewell <thomas.sewell@nicta.com.au>
A note on ML tactics: the exception Option gets raised sometimes if a
tactic returned an empty result sequence and something tried to pull an
element out of the sequence anyway (Seq.pull).
So, it's possible nothing is wrong with the way smt_tac is being called
except that some tactic can't make progress.
Cheers,
Thomas.
Email Gateway (Aug 19 2022 at 14:11):From: Matej Urbas <matej.urbas@gmail.com>
Thank you very much for checking this example!
It took me a while, but I found the source of this error: I was importing
the smt_solver.ml file in my theory.
Best,
Matej
Email Gateway (Aug 19 2022 at 14:23):From: Matej Urbas <matej.urbas@gmail.com>
Dear all,
I would like to write a tactic that reproduces the following:
apply(simp add: subset_iff)
apply smt
I am applying this tactic to formulae like (EX s. C <= {s}) ⟹ (EX s. A Int
C <= {s})
So far, I got this:
(TRY
(full_simp_tac ((simpset_of ctxt) addsimps [@{thm subset_iff}]) i) THEN
(SMT_Solver.smt_tac ctxt [] i))
However, the smt_tac raises the following:
exception Option raised (line 81 of "General/basics.ML") At command
"apply"
I believe I am not using smt_tac correctly. Could I ask for advice on how
to use smt_tac?
I am using Isabelle 2012.
Thank you very much for your help.
Kindest,
Matej
Email Gateway (Aug 19 2022 at 14:24):From: boehmes@in.tum.de
Hi Matej,
Your tactic seems to work fine. I tried the following theory, using
Isabelle2012 and with enabled Z3, and I observed no problems:
theory Scratch
imports Main
begin
ML {*
fun tac ctxt i =
(TRY
(full_simp_tac ((simpset_of ctxt) addsimps [@{thm subset_iff}]) i) THEN
(SMT_Solver.smt_tac ctxt [] i))
*}
lemma "(EX s. C <= {s}) ⟹ (EX s. A Int C <= {s})"
apply (simp add: subset_iff)
apply smt
done
lemma "(EX s. C <= {s}) ⟹ (EX s. A Int C <= {s})"
apply (tactic {* HEADGOAL (tac @{context}) *})
done
end
Cheers,
Sascha
Last updated: Apr 25 2024 at 04:18 UTC