graph.why 1.27 KB
Newer Older
1 2 3 4 5

(* graph theory *)

theory Path

6 7
  type graph

8 9
  type vertex

10
  logic edge graph vertex vertex
11

12
  inductive path graph vertex vertex =
13
  | Path_empty :
14
      forall g : graph, v : vertex. path g v v
15
  | Path_append:
16
      forall g : graph, v1 v2 src dst : vertex.
17 18
      path g src v1 -> edge g v1 v2 -> path g v2 dst -> 
      path g src dst
19

Jean-Christophe's avatar
Jean-Christophe committed
20 21 22 23 24 25 26 27
  lemma path_left_extension :
    forall g : graph, v1 v2 v3 : vertex.
    edge g v1 v2 -> path g v2 v3 -> path g v1 v3

  lemma path_right_extension :
    forall g : graph, v1 v2 v3 : vertex.
    path g v1 v2 -> edge g v2 v3 -> path g v1 v3

28 29
end

Jean-Christophe's avatar
Jean-Christophe committed
30 31 32 33 34 35 36 37 38 39 40 41 42
theory SimplePath

  use import list.List
  use import list.Mem

  type graph

  type vertex

  logic edge graph vertex vertex

  (* [simple_path g src [x1;...;xn] dst] is a path 
     src --> x1 --> x2 --> ... --> xn --> dst without repetition. *)
43
  inductive simple_path graph vertex (list vertex) vertex =
44
  | Path_empty : 
45
      forall g:graph, v:vertex. simple_path g v (Nil : list vertex) v
46
  | Path_cons  : 
47
      forall g:graph, src v dst : vertex, l : list vertex.
Jean-Christophe's avatar
Jean-Christophe committed
48 49
      edge g src v -> src <> v ->
      simple_path g v l dst -> not mem src l ->
50
      simple_path g src (Cons v l) dst
51

Jean-Christophe's avatar
Jean-Christophe committed
52
  logic simple_cycle (g : graph) (v : vertex) =
53
    exists l : list vertex. l <> Nil and simple_path g v l v
54

Jean-Christophe's avatar
Jean-Christophe committed
55
end