### no message

parent 1a659308
source/graphs.mmt 0 → 100644
 namespace http://data.mathhub.info/schemas❚ /T Nodes on formalizing graphs from scratch made during Primož Potočnik's visit in May 2019. This was a quick exercise to get a feel for the system and still has lots of errors.❚ theory BackgroundMath : ur:?LF = set: type❙ prop: type❙ in : set ⟶ set ⟶ prop❘# 1 ∈ 2 prec 50❙ eq : set ⟶ set ⟶ prop❘# 1 = 2 prec 50❙ elem : set ⟶ type❘# elem 1 prec -5❙ elemeq : {A} elem A ⟶ elem A ⟶ prop❘# 2 == 3 prec 50❙ list : set ⟶ set❙ power : set ⟶ set❘# ℘ 1❙ image : {A} (elem A ⟶ set) ⟶ set❙ those : {A} (elem A ⟶ prop) ⟶ elem ℘ A❙ ❚ theory DiGraph1 : ?BackgroundMath = node: set❙ edge: set❙ source: elem edge ⟶ elem node❙ target: elem edge ⟶ elem node❙ ❚ theory Graph1 : ?BackgroundMath = node: set❙ edge: set❙ endpoints : elem edge ⟶ those [P : elem ℘ node] #P == 2❙ ❚ theory DartGraph : ?BackgroundMath = node: set❙ dart: set❙ beg: elem dart ⟶ elem node❙ inv: elem dart ⟶ elem dart❙ inv_inv : {d} ⊦ inv (inv d) == d❙ edge : type❘= image [d] uop d (inv d)❙ ❚ theory Graph2 : ?BackgroundMath = include ?DartGraph❙ no_semiedges : {d} ¬ inv d == d❙ ❚ view V : ?DartGraph -> ?Graph1 = node = node❙ dart = those [x: node*edge] x.1 ∈ endpoints x.2❙ beg = [d] d.1❙ inv = [d] (the (endpoints d.2 ∖ d.1), d.2)❙ inv_inv = sketch"..."❙ ❚ view W : ?Graph2 -> ?Graph1 = include V❙ no_semiedges = [d] sketch"..."❙ ❚ view W2 : ?Graph1 -> ?Graph2 = node = node❙ edge = edge❙ endpoints = [e] e❙ ❚ theory DiGraph3 : ?BackgroundMath = node: set❙ edge: elem node ⟶ elem node ⟶ prop❙ ❚ theory DiGraph4 : ?BackgroundMath = node: set❙ edges: elem list (node * node)❙ ❚ theory CodecExamples = PairAsArray : {A,B,c} codec A c ⟶ codec B c ⟶ codec (A*B) (array c)❙ FinSetAsArray : {A,a} codec A a ⟶ codec (FinSet A) (array a)❙ ❚ theory DiGraphIsoType : ?BackgroundMath = order: ℕ❘ meta codec NatAsInt❙ nodes: type❘= upto order❙ edges: FinSet (nodes*nodes)❘ meta codec FinSetAsArray (PairAsArray NatAsInt NatAsInt)❙ ❚ \ No newline at end of file
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