Email Gateway (Aug 18 2022 at 13:38): Email Gateway (Aug 18 2022 at 13:38):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Consider a representation of a kind of graph
theory graph
imports Main
begin
typedecl vcs ( type of vertices )
typedecl ll ( type of labels )
record lgraph =
vv :: "vcs set" ( set of vertices )
lbl :: "vcs \<Rightarrow> ll" ( labelling of vertices )
ee :: "vcs \<Rightarrow> vcs \<Rightarrow> bool" ( edge relation )
locale lgraph =
fixes GG::lgraph
assumes vvFin: "finite (vv GG)"
( ee^++ is a partial order )
and eePo: "order ((ee GG)^**) ((ee GG)^++)"
This is not completely satisfactory; e.g. I really intend lgraph
equality to depend only on lbl and ee restricted to (vv::vcs set).
Any suggestions on basic representation are appreciated, but leave
that aside for the moment.
The question is when I declare the locale of two lgraphs
locale subgraph =
H : lgraph + G : lgraph for H1 and G1 +
assumes "vv H \<subseteq> vv G"
assumes "vv H \<subseteq> vv G1"
assumes "vv H \<subseteq> vv GG"
What does "G" refer to, what does G1 refer to, and what does GG refer
to in the context of locale subgraph? I guess all three "assumes"
lines mean the same thing. But none of "G.vvFin", "G1.vvFin" nor
"GG.vvFin" are recognised in this context; how do I refer to the
"vvFin" property of the two constituent lgraphs of locale subgraph?
Also while
locale subgraph = H : lgraph + G : lgraph for H and G
locale subgraph = H : lgraph + GG : lgraph for H and G
are accepted,
locale subgraph = H : lgraph + G : lgraph for H and GG
is not accepted. HELP! The tutorial on locales (2009) doesn't
clarify these questions for me.
You will have observed that in this example I'm not using the
"(structure)" and \<index> notation that I see in many libraries.
Where can I read about how this works?
Thanks,
Randy
Email Gateway (Aug 18 2022 at 13:38):From: Clemens Ballarin <ballarin@in.tum.de>
Dear Randy,
This locale has the parameters GG, H1 and G1. H is a bound variable,
universally quantified for each assumption. You can obtain this
information by inspecting the locale
print_locale subgraph
and the definitions of the two locale predicates
thm subgraph_def
thm subgraph_axioms_def
Additionally, H and G are qualifiers prefixing all non-logical names
(theorem names, for example) of the respective locales (two times
lgraph, in this case).
Clearly, this is not what you had intended. The locale you most
likely had in mind is
locale subgraph =
H : lgraph H + G : lgraph G for H and G +
assumes "vv H \<subseteq> vv G"
In a locale expression, you may specify a parameter instantiation.
This is completely independent of the qualifiers. In this example, it
is the most convenient choice to qualify all (theorem) names of the
"H" instance of "lgraph" by H etc, but you also might choose to
qualify the "H" instance by "sub" leave the "G" instance unqualified.
In your declaration you omitted the parameter instantiation. In this
case, a parameter named after the particular parameter of that locale
is added automatically. This is mainly a convenience for situations
with simple inheritance situations like
locale monoid = fixes G assumes ...
locale group = monoid + assumes ...
and to provide backward compatibility with the previous locale
expressions, which were based on renaming.
I hope this helps you get started with your example.
Cheers,
Clemens
Last updated: May 03 2024 at 04:19 UTC