Re: [isabelle] Printing instantiations



Thanks. I have another question which may require working at the ML level:
If some lemma can be proved at the Isar level, are there ways to extract out
the instantiations of each term in the lemma? Does the proof of the lemma
need to be at the ML level as well?

Thanks
Steve

On Tue, Jun 15, 2010 at 9:17 AM, Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de> wrote:

> Hi Steve,
>
> > I was wondering whether it's possible to print out the instantiations
> > returned by Thm.first_order_match. Since it returns the type (ctyp *
> ctyp)
> > list * (cterm * cterm) list, is there a way to convert this type to a
> > string? I just want to test it to see what the instantiations look like.
> > Should I actually bother?
>
> for explorative purpose the ML function PolyML.makestring does a good
> job.  Any serious printing of logical entities requires weaving the
> desired appearance on the ML level, e.g.
>
>  fn ts => commas (map (Syntax.string_of_term @{context}) ts)
>
> for printing a list of terms as string.  In the system those string
> conversions are used rarely, more likely output is assembled by means of
> pretty printer entities (type Pretty.T).
>
>  fn ts => Pretty.commas (map (Syntax.pretty_term @{context}) ts)
>
> See the pretty.ML, library.ML, and syntax.ML modules for available
> combinators.
>

Thanks.

>
> Hope this helps,
>        Florian
>
> --
>
> Home:
> http://www.in.tum.de/~haftmann
>
> PGP available:
>
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>




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