[isabelle] Easily using built-in tactics at the ML level (and/or using a method as a tactic)



Hi all,

In an Isabelle theory file, I can write simple one-line tactics such as
the following:

    apply (clarsimp simp: split_def split: prod.splits)

I find, however, when I start writing ML code to automate proofs,
producing a ML tactic object is far more verbose:

  clarsimp_tac (Context.proof_map (
      Simplifier.map_ss (fold Splitter.add_split @{thms prod.splits})
      #> Simplifier.map_ss (fn ss => ss addsimps [ at {thm split_def}]))
    @{context}) 1

The background is that I am writing tools[1] to automatically convert
C code into an abstract(ish) monadic form with the goal of easing
reasoning. As part of this, I frequently need to write ML code that
dynamically generates theorems and then proceeds to prove them. A simple
way of writing tactics such as the one above would be helpful both in
quick-and-dirty prototyping of ML proof procedures, but ideally would
also be clean enough for "production quality code".

Does anyone have any hints or tips?

(This discussion was originally started at StackOverflow[2], but it was
suggested that I move it over here when the discussion became a little
more involved. It is also part of long-running bigger question as to
"what is the best way to interact with Isabelle at the ML level?", but
perhaps it is better to address this concrete issue for now.)

  [1]: http://ssrg.nicta.com.au/projects/TS/autocorres/
  [2]: http://stackoverflow.com/questions/15217009/how-can-i-easily-write-simple-tactics-at-the-ml-level-of-isabelle

Thanks so much,
David

--


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.





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