Re: [isabelle] Telling auto to use an eisbach method



Dear Larry,

indeed, that seems to be the right way into the machinery!

I have something that seems to work, but raises a few questions about
Isabelle/ML-level programming.

Here is my code so far:

theory Auto_Method
imports
 Main
 "~~/src/HOL/Eisbach/Eisbach"
keywords "auto_method" :: thy_decl
begin

ML â
 fun auto_method method_text = (fn ctxt =>
ÂÂÂÂctxt addSbefore ("TODO", fn ctxt => fn _ =>
ÂÂÂÂÂÂlet val method = Method.evaluate method_text ctxt
ÂÂÂÂÂÂinÂÂMethod.NO_CONTEXT_TACTIC ctxt (method [])
ÂÂÂÂÂÂend
ÂÂÂ));

 fun auto_method_cmd method_text lthy =Â
ÂÂÂÂlet (* val ctxt = Local_Theory.target_of lthy
ÂÂÂÂÂÂÂÂÂÂÂval method = Method.evaluate method_text ctxt *)
ÂÂÂÂin Local_Theory.background_theory (map_theory_claset (auto_method method_text)) lthy
ÂÂÂÂend;

 Outer_Syntax.local_theory @{command_keyword "auto_method"}Â
ÂÂÂÂ"adds a method invocation to the classical reasoner"
ÂÂÂÂ(Method.parse >> (fn (method_text, _) => auto_method_cmd method_text))
â

And this actually works:

    consts P :: boolÂ
    consts Q :: bool
    lemma H1: "P â Q" and H2: P sorry
    method Q_method methods m = (match conclusion in "Q" â ârule H1; mâ)
    auto_method (Q_method ârule H2â)
    lemma Q by auto

So far so good. But I noticed that if I make a mistake in auto_method,
i.e. by writing

    auto_method (Q_method ârule does_not_existâ)

then the error about does_not_exist is raised in the application of
auto, _not_ the invocation of auto_method, where it should be.

I concluded that this is due to the executing Method.evaluate in the
context of the wrapper invocation, not in the context of the
local_theory command. When I try doing it there (see the commented-out-
code) I get the proper error message. But actually using the wrapper
causes the error message

    exception CONTEXT
    Â Â("Cannot transfer: not a super theory", [], [], ["Q â (Q)"],

What am I doing wrong?

Thanks,
Joachim




-- 
Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

I have left Karlsruhe and joined the
University of Pennsylvania.
Please use joachim at cis.upenn.eduÂinstead.

Attachment: signature.asc
Description: This is a digitally signed message part



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