Hi,

so-far I have used a record like (node\edge are type_synonyms to nat)

```
record ('a,'v,'e) graph =
nodes :: "node set"
edges :: "edge set"
src :: "edge ⇒ node"
trg :: "edge ⇒ node"
...
```

to describe a graph. Checking the well-formedness was performed by `(∀ x ∈ (edges gr) . src gr x ∈ nodes gr ∧ trg gr x ∈ nodes gr) ...`

.

When specifying a concrete graph, I tried naively tried

```
⦇nodes = {1,2}, edges={1},
src = [1 ↦ 1],
trg = [1 ↦ 1],
...
```

which forces `src\trg`

to be of type `edge => node option`

.

I read about underspecifying https://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total%2C_sometimes_undefined and thought, this is ok for my usage but now I"m not sure if I fully understood the topic.

Does it make sense for `src\trg`

to map to `'a option`

if a well-formed graph permits this case?

(deleted)

the `[1 ↦ 1]`

syntax models partiality explicitly with the `option`

datatype. If you want to define a function by specifying its values at specific points and leaving the rest undefined, you could use `(%x. undefined)(1 := 1)`

(this is called the functional update syntax; the `%`

is the ASCII symbol for lambda which I don't have a way of typing here)

As for what makes sense for modeling a graph, I'd probably use `edges :: "(node, node) set"`

(or a multiset, depends on the requirement)

thank you for the fast reply. I will check both approaches :-)

Btw. there is already a similar graph library: https://www.isa-afp.org/entries/Graph_Theory.html

Furthermore, @Mohammad Abdulaziz is currently working on a graph library which aims to unify the different representations that currently exist in Isabelle: https://github.com/wimmers/archive-of-graph-formalizations/pull/1

this is good to know, thank you for pointing me to it.

Last updated: Sep 09 2024 at 08:25 UTC