Commit 0db711e4 authored by Michael Kohlhase's avatar Michael Kohlhase

adding graph order

parent d4b95b29
......@@ -52,10 +52,19 @@ theory emptyGraph : base:?Logic =
edges := ([x : A,y : A] false)
'] ❙
theory GraphDegree : base:?Logic =
theory GraphOrderSize : base:?Logic =
include ?Graphs ❙
include ts:?FiniteCardinality ❙
order : dgraph ⟶ ℕ ❘ = [g] | nodesOf g | ❘ # | 1 | ❙
// TODO: we would need to convert a relation into a set of pairs and count that ❙
//size : dgraph ⟶ ℕ ❘ = [g] | dedgesOf g | ❘ # || 1 || ❙
theory GraphDegree : base:?Logic =
include ?Graphs ❙
include ts:?FiniteCardinality ❙
// indegree : {g : dgraph} (g.nodes) ⟶ ℕ ❘ = [g,n] | ⟪ dedgesOf g | [e] π2 e ≐n ⟫ | ❘ indeg 2❙
// outdegree : {g : dgraph} (g.nodes) ⟶ ℕ ❘ = [g,n] | ⟪ dedgesOf g | [e] π1 e ≐n ⟫ | ❘ outdeg 2❙
// degree : {g : ugraph} (g.nodes) ⟶ ℕ ❘ = [g,n] | ⟪ dedgesOf g | [e] π1 e ≐n ⟫ | ❘ degree 2❙
......@@ -67,3 +76,4 @@ theory InitialTerminal : base:?Logic =
// terminal : {g : dgraph} (g.nodes) ⟶ bool ❘ = [g,n] ¬∃[e] e ∈ (g.edges) ∧ ∃[m] e n m ❘ # terminal 2 ❙
// sets =/= types ❙
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment