问题描述:

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?

随机阅读：

- 夏季炎热的午后，伴随着轻柔的音乐，勤劳的环卫工人驾驶着洒水车以8km/h的速度匀速行驶在美丽的河滨路上．若这段公路全长2km，，求：（1）洒水车驶过这段公路需要多少时
- html - jquery slide toggle divs without creating multiple classes, functions, etc... ui accordion
- 如图是“研究电磁铁磁性强弱”的一组学生实验图，图A、B、C三个线圈匝数相同，D线圈的匝数比A、B、C线圈的匝数多，已知通过的电流I2＞I1，则下列分析错误的是A.比较
- php - What's the "correct way" to organize this project?

**推荐内容**-

**热点内容**