问题描述:

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`

Main

begin

typedecl node

record 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"

oops

end

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.)