[isabelle] emergence of "TERM _" (using quickcheck and nitpick)



I'm getting exceptions and having other kinds of problems when using
quickcheck or nitpick inside tactics.  I define a tactic that should fail
when quickcheck finds a counterexample and shouldn't do anything otherwise,
as follows:

fun check_counter_tac ctxt thm =
  let
   val term = concl_of thm
  in
   case  Quickcheck.test_terms ctxt (true, true) [] [(term, [])] of
     NONE => Seq.single thm
     | _ => Seq.empty
  end;

Then I try to run the tactic in a proof, like this:
lemma "0=(1::nat)" apply (tactic "check_counter_tac @{context}")
but I get the following exception:

exception TYPE raised (line 273 of "sign.ML"):
  Type error in application: incompatible operand type

  Operator:  If :: bool => (bool × term list) option => (bool × term list)
option => (bool × term list) option
  Operand:   TERM _ :: prop
  bool => (bool × term list) option => (bool × term list) option => (bool ×
term list) option
  prop
  If
  TERM _


The function Quickcheck.test_terms works fine otherwise, e.g., if I feed it
a term manually, or if I feed it the goal directly inside ML_val{**}.

I'm having the same problem when trying to use nitpick inside a tactic. I
don't get the exception, but it seems that the tactic is feeding the
nitpick function the same dummy term TERM _, and nitpick will never find a
counterexample. It writes:

Nitpicking goal:
  TERM _.

and finds nothing.

Does anyone know what this is about?

Thanks,
Daniel



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