Re: [isabelle] Interpretations with assumptions?
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Interpretations with assumptions?
- From: William Mansky <mansky1 at illinois.edu>
- Date: Thu, 04 Apr 2013 09:12:09 -0500
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:17.0) Gecko/20130307 Thunderbird/17.0.4
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
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