Re: [isabelle] Fwd: Using smt_tac from ML



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 [ at {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



Am .04.2014, 11:58 Uhr, schrieb Matej Urbas <matej.urbas at 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 [ 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.