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

(* graph theory *)

theory Path

6 7
  type graph

8 9
  type vertex

Andrei Paskevich's avatar
Andrei Paskevich committed
10
  predicate 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.
Andrei Paskevich's avatar
Andrei Paskevich committed
17
      path g src v1 -> edge g v1 v2 -> path g v2 dst ->
18
      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
theory SimplePath

  use import list.List
  use import list.Mem

  type graph

  type vertex

Andrei Paskevich's avatar
Andrei Paskevich committed
39
  predicate edge graph vertex vertex
Jean-Christophe's avatar
Jean-Christophe committed
40

Andrei Paskevich's avatar
Andrei Paskevich committed
41
  (* [simple_path g src [x1;...;xn] dst] is a path
Jean-Christophe's avatar
Jean-Christophe committed
42
     src --> x1 --> x2 --> ... --> xn --> dst without repetition. *)
43
  inductive simple_path graph vertex (list vertex) vertex =
Andrei Paskevich's avatar
Andrei Paskevich committed
44
  | Path_empty :
45
      forall g:graph, v:vertex. simple_path g v (Nil : list vertex) v
Andrei Paskevich's avatar
Andrei Paskevich committed
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

Andrei Paskevich's avatar
Andrei Paskevich committed
52 53
  predicate simple_cycle (g : graph) (v : vertex) =
    exists l : list vertex. l <> Nil /\ simple_path g v l v
54

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