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

On Thu, 20 Nov 2014, Daniel Raggi wrote:

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 =
  val term = concl_of thm
  case  Quickcheck.test_terms ctxt (true, true) [] [(term, [])] of
    NONE => Seq.single thm
    | _ => Seq.empty

This ML snipped looks non-canonical in various ways, so it is no surprise that it does not work at all.

The "implementation" manual is the main source of information for proper use of Isabelle/ML, including important naming conventions that direct the reader/writer in the right direction what things actually mean. Static types do not necessarily carry a meaning in ML, especially at the bottom of the LCF kernel.

E.g. a goal state should not be called "thm", but "st"; concl_of a goal state is its main conclusion, but that is private property of the system as pointed out in the manual. It is actually very rare that you access the goal state directly like above: there are combinators to put together tactics without exposing the state directly.

Here is a more standard way to do it:

ML ‹
fun check_counter_tac ctxt =
  SUBGOAL (fn (goal, _) =>
    if is_none (Quickcheck.test_terms ctxt (true, true) [] [(goal, [])])
    then all_tac else no_tac)

lemma "0 = (1::nat)"
  apply (tactic ‹check_counter_tac @{context} 1›)

See especially "implementation" manual section 4.2 Tactics, maybe also section 7.2 Proof methods. All of what is written there is important.

(This thread has nothing to do with quickcheck or nitpick in particular.)


          944,730 people so far

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