Re: [isabelle] Fwd: Using smt_tac from ML



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.

On 21/04/14 19:58, Matej Urbas wrote:
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 [ at {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





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