Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic? (fwd)

On Thu, 16 Feb 2012, Nils Jähnig wrote:

I did forget to reply.
it helped. with the name i found the tactic and its syntax. the right way
to use it is

res_inst_tac @{context} [ ( (x,0) , "A" ) ] exI 1

Is this going to be a generally abstracted tactic or proof method? If so, the compile-time @{context} needs to be passed as runtime parameter, typically as ctxt : Proof.context. You get the runtime value via the
normal method_setup syntax wrapping.

The static @{context} only makes sense for one-shot applications as in the proof method called "tactic", or certain ML commands in Isar.

which was convenient for me, as i don't have a term, but a string, which is easier to manipulate, if you're not yet on good terms with terms.

Again, it depends on the situation. Little can be done reliably with strings: accepting them from the end-user and passing them to certain other ML operations that expect such source input.

Composing "terms" in concrete syntax representation in general tactics breaks very quickly. Moreover, if the official source position markup is preserved, as is done by default by Args.term parsers etc. for Isar methods, any attempt to paste together such formal source will be rejected quickly. This is good because it makes such accidents immediately clear.


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