Establishing that a record type belongs to a given class

Question

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?

Answer 1

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