Email Gateway (Aug 19 2022 at 10:49): Email Gateway (Aug 19 2022 at 10:49):From: William Mansky <mansky1@illinois.edu>
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.
William
Email Gateway (Aug 19 2022 at 10:53):From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,
I've got the following situation:
locale abstract_graph =
fixes verts :: "'a set"
and edges :: "('a,'a) set"
assumes wf: "e : edges ==> fst e : verts & snd e : verts"
locale abstract_graphs:
fixes graphs :: "' c set"
and verts :: "'c => 'a set"
and edges :: "'c => ('a,'a) set"
and add_edge :: ...
and del_edge :: ...
assumes "!!g. g : graphs ==> abstract_graph (verts g) (edges g)"
and ...
Is there a way to get all lemmas from abstract_graph in abstract_graphs with
a) the locale_predicate replaced by the assumption "g : graphs" and
b) with the automation setup from abstract_graph (i.e. simp,
intro,elim, ...?
From the chapter about conditional interpretations in the locale
tutorial I gather that this is not possible?
Rationale: Most of the time, I only work with a fixed graph; so
abstract_graph would be the natural representation for that. However,
when I need to modify graphs, it would be a nicer not, if I would not
need to interpret every intermediate graph (in particular since the
operations on graphs preserve the membership and a therefore can be
proved trivially).
-- Lars
Last updated: Apr 26 2024 at 08:19 UTC