Re: [isabelle] Interpretations with assumptions?

I would very much like to be able to do that too (I have a similar setup with control-flow graphs and structures made of sets of graphs). The only way I've found so far is to use the "lemmas" keyword to produce each lemma, and explicitly declare them to have the desired attributes. For instance, if you have an assumption like

assumes graphs_are_graphs: "!!g. g : graphs ==> abstract_graph (verts g) (edges g)"

you could write in that locale

lemmas graphs_elim_rule = abstract_graph.graph_elim_rule [OF graphs_are_graphs]
declare graphs_elim_rule [elim]

It would be nice if there was a simpler solution.


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