Re: [isabelle] Fwd: Using smt_tac from ML



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
On 23 Apr 2014 02:12, "Thomas Sewell" <thomas.sewell at nicta.com.au> wrote:

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