Re: [isabelle] tactic being executed twice



Hi Lars,

Thanks - I'm afraid I don't get it. I guess that the focus type is somehow related to the current proof state, or, if the int argument is a subgoal, then I guess the focus is somehow related to the particular subgoal in the current proof state, but I can't guess, beyond that, is there some explanation in the documentation that you can point to? Or some examples?

Thanks

Jeremy


On 06/06/2018 07:30 PM, Lars Hupel wrote:
Also, using CSUBGOAL works.  I couldn't understand
what "Subgoal.FOCUS" does.  CSUBGOAL is similar to SUBGOAL which is
described clearly in the old Reference Manual.

Subgoal.FOCUS is a very useful combinator. It allows you to destructure
a goal such that you can get your hands on the premises and fixed
variables easily. I found that its type is quite self-explanatory:

   type focus =
    {context: Proof.context, params: (string * cterm) list,
     prems: thm list, asms: cterm list,
     concl: cterm,
     schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) *
cterm) list}

   val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic

I use it for almost all of my custom ML tactics.

Cheers
Lars





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