I have made a record type called
graph, and I have defined a suitable "is a subgraph of" relation. I would like to show that the set of graphs together with the subgraph relation forms an order, i.e. is an instance of the
ord class. But I can't get it to work. Here is my minimal working example:
theory John imports
record graph =
nodes :: "node set"
edges :: "(node × node) set"
definition subgraph :: "graph ⇒ graph ⇒ bool"
(infix "⊑" 50)
"G ⊑ H ≡
nodes G ⊆ nodes H ∧ edges G ⊆ edges H"
lemma "(GREATEST H. H ⊑ G) = G"
I get the error:
Type unification failed: No type arity graph_ext :: ord"
I tried typing things like
instantiation graph :: ord and
instantiation graph_ext :: ord, but nothing seems to work. Any ideas?
When a record
graph is defined, behind the scenes a new type
'a graph_ext is actually created. This type is the same as your record type, but with an extra field that allows extra data to be tacked in (i.e., a new field with type
'a is added to your record definition, which can be used to add additional data into your records later on). The type
graph is simply an abbreviation for
This means that when you want to instantiate a
graph into a type class, you actually need to instantiate the underlying type
'a graph_ext. This could be done as follows:
instantiation graph_ext :: (type) ord begin instance .. end
Although you probably also want to provide some definitions for the
ord type, perhaps as follows:
instantiation graph_ext :: (type) ord begin definition "less_eq_graph_ext (G :: 'a graph_ext) (H :: 'a graph_ext) ≡ nodes G ⊆ nodes H ∧ edges G ⊆ edges H" definition "less_graph_ext (G :: 'a graph_ext) (H :: 'a graph_ext) ≡ (nodes G ⊆ nodes H ∧ edges G ⊆ edges H) ∧ ¬ (nodes H ⊆ nodes G ∧ edges H ⊆ edges G)" instance .. end
'a graph_ext has been instantiated into the class
ord, your final lemma type-checks (although to actually carry out the proof, you likely need to do a bit more work, such as instantiating
'a graph_ext into the