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



> Is this just an exercise in driving the system into an unspecified / 
> uninhabitable state, or does it have some practical significance?

I have distilled that from a practical example, that went like this:

schematic_lemma 
  notes [refine_transfer] = <Some lemmas that only makes sense for this
particular refinement proof>
  shows "?concrete_program <= abstract_program"
  by (tactic that uses lemmas declared with attribute 
	"refine_transfer" (which is a NamedThms structure)

As I do not know how to refer to the schematic
variable ?concrete_program when I do 
  proof - note [refine_transfer] = ... show "xxx" ...
   (For xxx, neither ?thesis nor "?concrete_program <= abstract_program"
works),
I used the notes-syntax.

An alternative would be to pass the lemmas as parameters to my tactic,
which I have already (partially) implemented (after writing the first
mail ;) ).

  
Peter







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