walks[T: TYPE]: THEORY BEGIN IMPORTING digraphs[T], seq_def, finite_sets@finite_sets_eq, finite_sets_more G,GG: VAR digraph[T] n: VAR nat x,u,v,u1,u2,v1,v2,v3: VAR T e: VAR edgetype[T] i,j: VAR nat prewalk: TYPE = {w: finite_seq[T] | l(w) > 0} s,ps,ww: VAR prewalk verts_in?(G,s): bool = (FORALL (i: below(l(s))): vert(G)(seq(s)(i))) Seq(G): TYPE = {w: prewalk | verts_in?(G,w)} walk?(G,ps): bool = verts_in?(G,ps) AND (FORALL n: n < l(ps) - 1 IMPLIES edge?(G)(ps(n),ps(n+1))) Walk(G): TYPE = {w: prewalk | walk?(G,w)} from?(ps,u,v): bool = seq(ps)(0) = u AND seq(ps)(l(ps) - 1) = v walk_from?(G,ps,u,v): bool = seq(ps)(0) = u AND seq(ps)(l(ps) - 1) = v AND walk?(G,ps) Walk_from(G,u,v): TYPE = {w: prewalk | walk_from?(G,w,u,v)} walk_from_l : LEMMA walk_from?(G,ps,u,v) AND u /= v IMPLIES l(ps) >= 2 verts_of(ww: prewalk): finite_set[T] = {t: T | (EXISTS (i: below(l(ww))): ww(i) = t)} edges_of(ww): finite_set[edgetype[T]] = {e: edgetype[T] | EXISTS (i: below(l(ww)-1)): e = (ww(i),ww(i+1))} pre_circuit?(G: digraph[T], w: prewalk): bool = walk?(G,w) AND w(0) = w(l(w)-1) % ----------------------- Properties ----------------------- verts_in?_concat: LEMMA FORALL (s1,s2: Seq(G)): verts_in?(G,s1 o s2) verts_in?_caret : LEMMA FORALL (j: below(l(ps))): i <= j IMPLIES verts_in?(G,ps) IMPLIES verts_in?(G,ps^(i,j)) vert_seq_lem : LEMMA FORALL (w: Seq(G)): n < l(w) IMPLIES vert(G)(w(n)) verts_of_subset : LEMMA FORALL (w: Seq(G)): subset?(verts_of(w),vert(G)) edges_of_subset : LEMMA walk?(G,ww) IMPLIES subset?(edges_of(ww),edges(G)) walk_verts_in : LEMMA walk?(G,ps) IMPLIES verts_in?(G,ps) walk_from_vert : LEMMA FORALL (w: prewalk,v1,v2:T): walk_from?(G,w,v1,v2) IMPLIES vert(G)(v1) AND vert(G)(v2) walk_edge_in : LEMMA walk?(G,ww) AND subset?(edges_of(ww),edges(GG)) AND subset?(verts_of(ww),vert(GG)) IMPLIES walk?(GG,ww) prewalk_across: LEMMA ww(0) /= ww(l(ww)-1) AND l(ww) > 1 IMPLIES (EXISTS (i: below(l(ww)-1)): ww(i) = ww(0) AND ww(i+1) /= ww(0)) % ----------- operations and constructors for walks -------------------- gen_seq1(G, (u: (vert(G)))): Seq(G) = (# l := 1, seq := (LAMBDA (i: below(1)): u) #) gen_seq2(G, (u,v: (vert(G)))): Seq(G) = (# l := 2, seq := (LAMBDA (i: below(2)): IF i = 0 THEN u ELSE v ENDIF) #) Longprewalk: TYPE = {ps: prewalk | l(ps) >= 2} trunc1(p: Longprewalk ): prewalk = p^(0,l(p)-2) add1(ww,x): prewalk = (# l := l(ww) + 1, seq := (LAMBDA (ii: below(l(ww) + 1)): IF ii < l(ww) THEN seq(ww)(ii) ELSE x ENDIF) #) gen_seq1_is_walk: LEMMA vert(G)(x) IMPLIES walk?(G,gen_seq1(G,x)) edge_to_walk : LEMMA u /= v AND edges(G)((u, v)) IMPLIES walk?(G,gen_seq2(G,u,v)) w1,w2: VAR prewalk %%%%%%%%%%%%%%%%%%%%% NOT THEOREMS for directed graphs %%%%%%%%%%%%%% % % walk?_rev : LEMMA walk?(G,ps) IMPLIES walk?(G,rev(ps)) % % % % walk?_reverse : LEMMA walk_from?(G,w1,v1,v2) IMPLIES % (EXISTS (w: Walk(G)): walk_from?(G,w,v2,v1)) walk?_caret : LEMMA i <= j AND j < l(ps) AND walk?(G,ps) IMPLIES walk?(G,ps^(i,j)) l_trunc1 : LEMMA l(ww) > 1 IMPLIES l(trunc1(ww)) = l(ww)-1 walk?_add1 : LEMMA walk?(G,ww) AND vert(G)(x) AND edge?(G)(seq(ww)(l(ww)-1),x) IMPLIES walk?(G,add1(ww,x)) walk_concat_edge: LEMMA walk_from?(G, w1, u1, v1) AND walk_from?(G, w2, u2, v2) AND edge?(G)(v1,u2) IMPLIES walk_from?(G, w1 o w2,u1,v2) walk_concat: LEMMA l(w1) > 1 AND walk_from?(G, w1, u1, v) AND walk_from?(G, w2, v, u2) IMPLIES walk_from?(G, w1 ^ (0, l(w1) - 2) o w2,u1,u2) walk?_cut : LEMMA FORALL (i,j: below(l(ps))): i < j AND seq(ps)(i) = seq(ps)(j) AND walk_from?(G, ps, u, v) IMPLIES walk_from?(G, ps^(0,i) o ps^(j+1,l(ps)-1),u,v) yt: VAR T p1,p2: VAR prewalk walk_merge: LEMMA walk_from?(G, p1, u, yt) AND walk_from?(G, p2, yt, v ) IMPLIES (EXISTS (p: prewalk): walk_from?(G, p, u, v)) END walks