[isabelle] Fwd: Using smt_tac from ML

[Matej Urbas]

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

[b***@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

Post by Matej Urbas
Dear all,
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})
(TRY
(SMT_Solver.smt_tac ctxt [] i))
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

[Thomas Sewell]

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.

Post by Matej Urbas
Dear all,
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})
(TRY
(SMT_Solver.smt_tac ctxt [] i))
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

[Matej Urbas]

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

Post by Thomas Sewell
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.

Post by Matej Urbas
Dear all,
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})
(TRY
(SMT_Solver.smt_tac ctxt [] i))
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