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 importsMainbegintypedecl noderecord graph =nodes :: "node set"edges :: "(node × node) set"definition subgraph :: "graph ⇒ graph ⇒ bool"(infix "⊑" 50)where"G ⊑ H ≡nodes G ⊆ nodes H ∧ edges G ⊆ edges H"lemma "(GREATEST H. H ⊑ G) = G"oopsend``

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 `unit graph_ext`.

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
``````

Once `'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 `preorder` or `order` classes.)

Top