问题描述:

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

您可能感兴趣的文章：

- c# - How to access child object's properties using ASP.NET ReportViewer?
- javascript - Actions on a collection (sorting, limiting, searching, etc.)
- c++ - Is it bad manners to return a heap allocated pointer from a function?
- php - Post JSON data cross site using jquery
- wordpress - Combining CSS files into a single cached one
- php - Reading a specific line from a text file
- clr - Any implementation of an Unrolled Linked List in C#?
- Finding Hudson Log Files
- Forward to a payment-gateway together with POST data using cURL (or any other PHP server side solution)
- WCF in Winforms app - is it always single-threaded?

随机阅读：

**推荐内容**-

**热点内容**