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



Thanks for your reply, Jasmin. As you say, the problem seems to be the
input Quickcheck and Nitpick are receiving and not what they are doing.
However, I'm not applying anything before trying the checkers. Strangely
enough, I got around it using Nitipick, but Quickcheck still fails. And
nitpick doesn't fail but it still behaves strangely, outputting something
that lets me know that it is processing that mysterious dummy term "TERM _"
before processing the real goal.

If we have a tactic "check_tac" that runs Nitpick before doing its thing,
shouldn't we get the same from this:
*****
lemma "0 = (1::nat)"
  ML_val{*
   val goal = #goal @{Isar.goal}
   val ctxt = #context @{Isar.goal}
   val t = check_tac ctxt goal
  *}
*****

and from this:
*****
lemma "0 = (1::nat)"
  apply (tactic "check_tac @{context}")
*****
?

Instead, the first one prints:
*****
Nitpicking goal:
  0 = 1.
Nitpick found a counterexample:

  Empty assignment
*****

as expected, but the second one prints:
*****
Nitpicking goal:
  TERM _.
Nitpick found no counterexample.
Nitpicking goal:
  0 = 1.
Nitpick found a counterexample:

  Empty assignment
*****

as if it is processing TERM _ before processing the term 0 = 1.

I'm attaching a minimalistic thy file just to showcase this behaviour. I
find it strange.

Daniel


>From this output, it would appear that the issue has nothing to do with
> Quickcheck and Nitpick, and everything to do with the string of tactics
> that were applied before you called those tools and that gave rise to "TERM
> _" (which I also don't know, but it looks like some dummy placeholder
> produced by some odd tactic).
>
> Regards,
>
> Jasmin
>
>

Attachment: dummyTERM.thy
Description: Binary data



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