Re: [isabelle] Pitfall with type-classes in Isar-Lemma format



> BTW, the thing given as arguments to the command 'by' is called "proof 
> method" or just "method" in Isar terminology.  
sorry for the confusion here.

> > An alternative would be to pass the lemmas as parameters to my tactic, 
> > which I have already (partially) implemented
> 
> This would indeed follow the standard convention: a method that accepts 
> implicit arguments via the context also allows the same as explicit 
> arguments on the spot.  

For my application, it has, however, the disadvantage that the setup has
to be repeated each time I apply a method. For example, I want to
support proofs like:

schematic_lemma 
  notes [refine_transfer] = some lengthy setup
  notes [...] = ...
  shows "?c <= a"
  apply (my_method)
  apply (some user-specified proof of subgoal, thereby instantiating
schematics on that the rest of the proof depends)
  apply (my_method)
  apply (some user-specified instantiation)
  apply (my_method)
  ...
  done

When I do the setup locally for the proof method, I have to repeat it
each time I apply the method. What I really want is to do the setup for
the whole proof.

Perhaps, what I'm doing here is an abuse of the original intention of
schematic_lemma ??

Peter







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