namespace http://mathhub.info/MitM/core/graphs❚
import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/core/typedsets ❚
import num http://mathhub.info/MitM/core/arithmetics ❚

theory Graphs : base:?Logic =
    include ☞ts:?AllSets ❙
	include ☞ts:?Relations ❙
	include ☞ts:?Union ❙
	include ☞num:?NaturalArithmetics ❙
    include ☞ts:?SetQuantifiers ❙

	nodetype : type ❙
	
	theory dgraph_theory : base:?Logic =
	    nodes : set nodetype ❙
	    edges : relation nodetype nodetype ❙

	    successors : nodetype ⟶ set nodetype ❘
	        = [a] ⟪ nodes | ([x] edges a x) ⟫ ❙

	    predecessors : nodetype ⟶ set nodetype ❘
	        = [a] ⟪ nodes | ([x] edges x a) ⟫ ❙

	    neighbours : nodetype ⟶ set nodetype ❘
	        = [a] (successors a) ∪ (predecessors a)  ❙

    	n_regular : ℕ ⟶ prop ❘ = [n] ∀ ∈ nodes . [a] ∃= n ∈ (neighbours a) . [b] TRUE ❙
	❚

	theory ugraph_theory : base:?Logic = 
		include ☞?Graphs/dgraph_theory ❙
		undirected_edges : ⊦ symmetric edges ❙
	❚

	theory finite_dgraph_theory : base:?Logic =
    	include ☞?Graphs/dgraph_theory ❙
    	finite : ⊦ nodes finite ❙
    ❚

    theory finite_ugraph_theory : base:?Logic =
        include ☞?Graphs/ugraph_theory ❙
        include ☞?Graphs/finite_dgraph_theory ❙
    ❚

	dgraph : kind ❘ = Mod ☞?Graphs/dgraph_theory ❘ role abbreviation ❙
	ugraph : kind ❘ = Mod ☞?Graphs/ugraph_theory ❘ role abbreviation ❙

	finite_dgraph : kind ❘ = Mod ☞?Graphs/finite_dgraph_theory ❘ role abbreviation ❙
	finite_ugraph : kind ❘ = Mod ☞?Graphs/finite_ugraph_theory ❘ role abbreviation ❙
	
 	include ☞ts:?RelationClosure ❙
	
	nodesOf : {g: dgraph}set nodetype ❘ = [g] (g.nodes) ❘ # nodes 1❙
	dEdgesOf : {g: dgraph}relOn nodetype ❘ = [g] (g.edges) ❘ # edgesOf 1❙
	uEdgesOf : {g: ugraph}relOn nodetype ❘ = [g] symmetric_closure (g.edges) ❘ # edgesOf 1 ❙

	order : finite_dgraph ⟶ ℕ ❘ = [g] | nodesOf g | ❙

	include ☞base:?InformalProofs ❙
	
	inducedUGraph : dgraph ⟶ ugraph ❘ = [d : dgraph] ['
		nodes := d.nodes , 
		edges := symmetric_closure (d.edges) ,
		undirected_edges := trivial
	'] ❙
	    
❚

theory emptyGraph : base:?Logic = 
  include ?Graphs ❙
  graphEmpty : dgraph ⟶ bool ❘ = [g] empty (g.nodes) ❙
  emptyGraph : dgraph ❘ = ['
	  nodes := emptySet nodetype ,
	  edges := ([x : nodetype,y : nodetype] false)
	'] ❘ # ∅ ❙
	
	graphEdgeless : dgraph ⟶ bool ❘ = [g] (g.edges) ≐ [x,y] false ❙
	edgelessGraph : set nodetype ⟶ dgraph ❘ = [S] ['
      nodes := S ,
      edges := ([x : nodetype,y : nodetype] false)
      '] ❙
	❚

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❙
❚
  
theory InitialTerminal : base:?Logic = 
   include ?Graphs ❙
   // initial : {g : dgraph} (g.nodes) ⟶ bool ❘ = [g,n] ¬∃[e] e ∈ (g.edges) ∧ ∃[m] e m n ❘ # initial 2 ❙
   // terminal : {g : dgraph} (g.nodes) ⟶ bool ❘ = [g,n] ¬∃[e] e ∈ (g.edges) ∧ ∃[m] e n m ❘ # terminal 2 ❙
   // sets =/= types ❙
❚

theory GraphMorphisms :base:?Logic =
    include ?Graphs ❙

    theory graphMorphism_theory > g1 : ugraph, g2 : ugraph ❘ =
        fun : nodetype ⟶ nodetype ❙

        morphism_property : ⊦ ∀ ∈ (g1.nodes) . [n1] ∀ ∈ (g1.nodes) . [n2] (g1.edges) n1 n2 ⇒ (g2.edges) (fun n1) (fun n2) ❙
    ❚
❚