Email Gateway (Aug 22 2022 at 14:56): Email Gateway (Aug 22 2022 at 14:56):From: Christoph Dittmann <f-isabellelist@yozora.eu>
Hi,
I have a question about how to extend locales such as pre_digraph (from
the Graph_Theory AFP entry,
https://www.isa-afp.org/browser_info/current/AFP/Graph_Theory/Digraph.html
).
The definition in Graph_Theory/Digraph.thy goes like this:
record ('a,'b) pre_digraph =
verts :: "'a set"
arcs :: "'b set"
tail :: "'b ⇒ 'a"
head :: "'b ⇒ 'a"
locale pre_digraph =
fixes G :: "('a, 'b) pre_digraph" (structure)
Now I would like to use Graph_Theory as the basis for a theory about
games where each vertex has a priority. All definitions and lemmas
about vertex degrees, connectivity etc. are unaffected by this, so I
would like to import these in some way into my theory.
I tried to do it like this:
record ('a,'b) Game = "('a, 'b) pre_digraph" +
priority :: "'a ⇒ nat" ("ωı")
locale Game = pre_digraph G
for G :: "('a,'b,'c) Game_scheme" (structure) +
assumes priorities_finite: "finite (ω ` verts G)"
But this does not work because the locale pre_digraph does not accept
records of type "('a,'b,'c) Game_scheme" or of type "('a,'b) Game".
I would like to avoid giving the Game locale two parameters, because
this will end up very verbose in the the rest of the theory.
Another thing I tried was to change the definition in
Graph_Theory/Digraph.thy to:
locale pre_digraph =
fixes G :: "('a, 'b, 'c) pre_digraph_scheme" (structure)
and then define Game in my theory as:
locale Game = pre_digraph G
for G :: "('a, 'b, 'c) Game_scheme" (structure) +
assumes priorities_finite: "finite (ω ` verts G)"
This seems to work, but changing the locale pre_digraph like this breaks
a lot of lemmas in Graph_Theory and I do not know how much work it would
be to fix this or even if this is best practice at all.
What would be a good way to accomplish my use case?
Thanks,
Christoph
Email Gateway (Aug 22 2022 at 14:56):From: Christoph Dittmann <f-isabellelist@yozora.eu>
Hi,
I just had the idea to define a record
record GameVertex = priority :: nat
and then use
locale Game = pre_digraph G
for G :: "('a GameVertex_scheme, 'b) pre_digraph" (structure) +
assumes priorities_finite: "finite (priority ` verts G)"
I will try this in the next days and report back if this works for me.
Suggestions are still welcome. :)
Best,
Christoph
Email Gateway (Aug 22 2022 at 14:56):From: "Elsa L. Gunter" <egunter@illinois.edu>
Dear Christoph,
The path you are on for the interleaving of records and locales is
similar to an approach I have been taking. The fact the predigraph was
build from a record and not a record scheme makes it a bit awkward to
extend in a natural way, keeping up the interleaving of the record view
and the locale view. For predigraph in particular, I ended up creating
a structure that was mostly the same, but with more components, and
showed it interpreted predigraphs, thereby getting the predigraph
theory. Below I give a skeleton of an example development I have
interleaving records and locales, in case you find the methodology of use.
So I have been using records as the "signature" of the locale, by using
record schemes. As a bit of an example, I have
record ('instr,'dir) generalized_control_flow_graph_context =
Instructions :: "'instr set"
Directions :: "'dir set"
edgeTyping :: "'instr ⇒ ('dir ⇒ nat)set"
and then
locale GeneralizedControlFlowGraphContext =
fixes GCFG :: "('instr,'dir,'ext)
generalized_control_flow_graph_context_scheme"
assumes ...
then
record ('instr,'dir,'node) generalized_control_flow_graph =
"('instr,'dir) generalized_control_flow_graph_context" +
Nodes :: "'node set"
Edges :: "'node ⇒ ('dir × 'node)set"
labeling :: "'node ⇒ 'instr"
then
locale UnboundedGeneralizedControlFlowGraph =
GeneralizedControlFlowGraphContext
where GCFG = "GCFG :: ('instr,'dir,'node,'ext)
generalized_control_flow_graph_scheme"
for GCFG +
assumes ...
Note that just by making the type of GCFG be the more specific type of
('instr,'dir,'node,'ext) generalized_control_flow_graph_scheme, I can
get the extra fields "for free". Because I keep using a scheme at each
layer, I allow for the possibility of extension.
Then I can do
record
('instr,'dir,'node,'participant,'state)
generalized_control_flow_graph_interpretation =
"('instr,'dir,'node) generalized_control_flow_graph"
+
Participants :: " 'participant set"
Interpretation ::
"(('participant ⇒ 'node) × 'state) ⇒ 'dir ⇒ (('participant ⇒ 'node)
× 'state) ⇒ bool"
locale UnboundedGeneralizedControlFlowGraphInterpretation =
UnboundedGeneralizedControlFlowGraph
where GCFG =
"GCFG :: ('instr, 'dir, 'node, 'participant,'state,'ext)
generalized_control_flow_graph_interpretation_scheme"
for GCFG +
assumes ...
and
locale GeneralizedControlFlowGraph =
UnboundedGeneralizedControlFlowGraph
where GCFG =
"GCFG :: ('instr, 'dir, 'node,'ext)
generalized_control_flow_graph_scheme"
for GCFG +
assumes finite_nodes: "finite (Nodes GCFG)"
and finite_edges: "n ∈ Nodes GCFG ⟹ finite (Edges GCFG n)"
sublocale GeneralizedControlFlowGraph ⊆ fin_digraph
where G = "⦇ verts = Nodes GCFG,
arcs = {e. case e of (n,d,m) ⇒ n ∈ Nodes GCFG ∧
(d,m)∈Edges GCFG n},
tail = (λ e. case e of (n,d,m) ⇒ m),
head = (λ e. case e of (n,d,m) ⇒ n) ⦈"
by (unfold_locales, simp_all add: finite_nodes finite_edge_set)
Elsewhere I have
record ('block, 'region, 'val, 'thread)block_structure =
good_block ::"'block ⇒ bool"
good_region :: "'region ⇒ bool"
region_overlap::"'region ⇒ 'region ⇒ bool"
subblock::"'block ⇒ 'block ⇒ bool"
subregion :: "'region ⇒ 'region ⇒ bool"
region_get_block ::"'region ⇒ 'block"
block_as_region ::"'block ⇒ 'region"
value_fits_region :: "'val ⇒ 'region ⇒ bool"
region_fits_block ::"'region ⇒ 'block ⇒ bool"
does_not_modify_value :: "('thread, 'block, 'region,'val) block_access
⇒ 'region ⇒ bool"
does_not_modify_permissions :: "('thread, 'block, 'region,'val)
block_access
⇒ 'region ⇒ bool"
locale block_structure =
fixes BlkSt :: "('block, 'region, 'val, 'thread,
'ext)block_structure_scheme"*
Some definitions ... and then a model for block_structure
definition memory_machine_block_structure where
"memory_machine_block_structure GMMA rest ≡
⦇good_block = good_block_mm GMMA ,
good_region = good_region_mm GMMA ,
region_overlap = region_overlap_mm GMMA ,
subblock = subblock_mm GMMA ,
subregion = subregion_mm GMMA ,
region_get_block = region_get_block_mm GMMA ,
block_as_region = block_as_region_mm GMMA ,
value_fits_region = value_fits_region_mm GMMA ,
region_fits_block = region_fits_block_mm GMMA ,
does_not_modify_value = does_not_modify_value_mm GMMA ,
does_not_modify_permissions = does_not_modify_permissions_mm GMMA ,
… = rest⦈"
interpretation block_structure
"memory_machine_block_structure GMMA rest"
proof ... qed
record ('block, 'region, 'val, 'thread, 'addr, 'byte)
block_structure_addresses =
"('block, 'region, 'val, 'thread)block_structure" +
allowed_addresses:: "'addr set"
region_to_addresses:: "'region ⇒ 'addr set"
value_byte_check::
"'region ⇒ 'val ⇒ ('addr ⇒ 'byte option) ⇒ bool"
locale block_structure_addresses =
fixes BlkStAddr ::
"('block, 'region, 'val, 'thread, 'addr, 'byte,
'ext)block_structure_addresses_scheme"
assumes ...
And then we can extend our memory machine model for block_structure to
one for block_structure_addresses with
definition memory_machine_block_structure_addresses where
"memory_machine_block_structure_addresses
(GMMA:: ('byte list,'byte,'extmem)gen_memory_with_address_scheme) rest ≡
(memory_machine_block_structure GMMA
⦇allowed_addresses = {i. (MinAddress GMMA ≤ i) ∧ (i ≤ MaxAddress GMMA)},
region_to_addresses = (λ r. (case r of ((j,k),B) ⇒ {i. j ≤ i ∧ i ≤ k})),
value_byte_check = (λ r v m. case r of ((j,k),B) ⇒ v = intmap m j k),
… = rest ⦈
::((int * int), (int × int) × int × int, 'byte list, 'thread, int,
'byte, 'extblk)
block_structure_addresses_scheme)"
and then we can prove the extended model is indeed a model of the
extended local
interpretation block_structure_addresses
"memory_machine_block_structure_addresses
(GMMA:: ('byte list,'byte,'ext)gen_memory_with_address_scheme) rest "
apply (simp add: memory_machine_block_structure_addresses_def
memory_machine_block_structure_def)
apply (unfold_locales, simp_all)
...
This method has some kinks to it. It gets a bit twisted up if you try
to extend the union of two locales with a common ancestor. It is
generally best not to make definitions inside contexts, but pass the
extra argument(s) explicitly. There may be some more limitations, but
on the whole I have found it a useful way to use locals and records
together so that I can work inside the locale to prove facts about the
general theory, and then use records and predicates when I am using
instances of the theory. Anyway, I hope it gives you some useful ideas.
---Elsa
Email Gateway (Aug 22 2022 at 14:57):From: Christoph Dittmann <f-isabellelist@yozora.eu>
Hello Elsa,
thank you for this suggestion. I hadn't thought about using
interpretations.
For now, I am satisfied with showing that my Digraph locale and the
nomulti_digraph locale from Graph_Theory interpret each other:
https://devel.isa-afp.org/browser_info/current/AFP/Parity_Game/Graph_TheoryCompatibility.html
This does not allow me to use the theorems of nomulti_digraph as easily
as I would like, but it shows at least that the locales are somehow
compatible.
Best,
Christoph
Last updated: Apr 23 2024 at 16:19 UTC