isabelle - Establishing that a record type belongs to a given class -

i have made record type called graph, , have defined suitable "is subgraph of" relation. show set of graphs subgraph relation forms order, i.e. instance of ord class. can't work. here 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)   "g ⊑ h ≡    nodes g ⊆ nodes h ∧ edges g ⊆ edges h"  lemma "(greatest h. h ⊑ g) = g" oops  end 

i error:

type unification failed: no type arity graph_ext :: ord"

i tried typing things instantiation graph :: ord , instantiation graph_ext :: ord, nothing seems work. ideas?

when record graph defined, behind scenes new type 'a graph_ext created. type same record type, field allows data tacked in (i.e., new field type 'a added record definition, can used add additional data records later on). type graph abbreviation unit graph_ext.

this means when want instantiate graph type class, need instantiate underlying type 'a graph_ext. done follows:

instantiation graph_ext :: (type) ord begin   instance .. end 

although want provide definitions ord type, perhaps 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 class ord, final lemma type-checks (although carry out proof, need bit more work, such instantiating 'a graph_ext preorder or order classes.)