| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/complex/ (Beweissystem Isabelle Version 2025-1©) Datei vom 28.9.2014 mit Größe 3 kB |
|
SSL walks.pvs Sprache: PVS |
|||||||||
|
walks[T: TYPE]: THEORY
BEGIN IMPORTING digraphs[T], structures@seq_extras[T] 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 % ------------------------------------------------------------------------------- % Definitions % ------------------------------------------------------------------------------- prewalk: TYPE = {w: finseq[T] | length(w) > 0} s,ps,ww: VAR prewalk verts_in?(G,s): bool = (FORALL (i: below(length(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 < length(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)(length(ps) - 1) = v walk_from?(G,ps,u,v): bool = from?(ps,u,v) AND walk?(G,ps) Walk_from(G,u,v): TYPE = {w: prewalk | walk_from?(G,w,u,v)} set_walk_from(G, e): set[prewalk] = LET (u, v) = e IN {w: prewalk | walk_from?(G,w,u,v)} verts_of(ww: prewalk): finite_set[T] = {t: T | (EXISTS (i: below(length(ww))): ww(i) = t)} edges_of(ww): finite_set[edgetype[T]] = {e: edgetype[T] | EXISTS (i: below(length(ww)-1)): e = (ww(i),ww(i+1))} % ----------------------- Properties ----------------------- walk_from_l : LEMMA walk_from?(G,ps,u,v) AND u /= v IMPLIES length(ps) >= 2 verts_in?_concat: LEMMA FORALL (s1,s2: Seq(G)): verts_in?(G,s1 o s2) verts_in?_caret : LEMMA FORALL (j: below(length(ps))): i <= j IMPLIES verts_in?(G,ps) IMPLIES verts_in?(G,ps^(i,j)) vert_seq_lem : LEMMA FORALL (w: Seq(G)): n < length(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(length(ww)-1) AND length(ww) > 1 IMPLIES (EXISTS (i: below(length(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) = (# length := 1, seq := (LAMBDA (i: below(1)): u) #) gen_seq2(G, (u,v: (vert(G)))): Seq(G) = (# length := 2, seq := (LAMBDA (i: below(2)): IF i = 0 THEN u ELSE v ENDIF) #) Longprewalk: TYPE = {ps: prewalk | length(ps) >= 2} lWalk(G) : TYPE = {w: Longprewalk | walk?(G,w)} trunc1(p: Longprewalk ): prewalk = p^(0,length(p)-2) add1(ww,x): prewalk = (# length := length(ww) + 1, seq := (LAMBDA (ii: below(length(ww) + 1)): IF ii < length(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 < length(ps) AND walk?(G,ps) IMPLIES walk?(G,ps^(i,j)) l_trunc1 : LEMMA length(ww) > 1 IMPLIES length(trunc1(ww)) = length(ww)-1 walk?_add1 : LEMMA walk?(G,ww) AND vert(G)(x) AND edge?(G)(seq(ww)(length(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 length(w1) > 1 AND walk_from?(G, w1, u1, v) AND walk_from?(G, w2, v, u2) IMPLIES walk_from?(G, w1 ^ (0, length(w1) - 2) o w2,u1,u2) walk?_cut : LEMMA FORALL (i,j: below(length(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,length(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)) %******************************************************************************* % % Contributions from: % % Andréia Borges Avelar -- Universidade de Brasília - Brasil % Mauricio Ayala-Rincon -- Universidade de Brasília - Brasil % Cesar Muñoz -- NASA Langley Research Center - US % %******************************************************************************* % ------------------------------------------------------------------------------- % Definitions % ------------------------------------------------------------------------------- sub_walk?(G: digraph, w: Walk(G), ww): bool = EXISTS (i, j: below(length(w))): w^(i,j) = ww reachable?(G)( u, v : (vert(G)) ) : bool = (u = v OR EXISTS (w: prewalk) : walk_from?(G, w, u, v)) reord_prewalk(w: prewalk, i: posnat): prewalk = w ^ (i, length(w) - 1) o w ^ (0, i - 1) eq_prewalk?(w1, w2: prewalk): bool = w1 = w2 OR EXISTS (i: posnat): w2 = reord_prewalk(w1, i) % owalk(G: digraph, w1, w2: Walk(G) | last(w1) = first(w2)): Walk(G) = % w1 o rest(w2) % ------------------------------------------------------------------------------- % Properties % ------------------------------------------------------------------------------- eq_relation_eq_prewalk: LEMMA equivalence?(eq_prewalk?) eq_prewalk_length: LEMMA FORALL(w1, w2: prewalk): eq_prewalk?(w1, w2) IMPLIES length(w1) = length(w2) subwalk_is_walk : LEMMA FORALL (w: Walk(G)): sub_walk?(G, w, ww) IMPLIES walk?(G, ww) walk_o: LEMMA walk?(G, w1) AND walk?(G, w2) AND seq(w1)(length(w1) - 1) = seq(w2)(0) IMPLIES walk?(G, w1 o w2^(1, length(w2) - 1)) edges_o_walk: LEMMA walk?(G, w1) AND walk?(G, w2) AND last(w1) = first(w2) IMPLIES edges_of(w1 o rest(w2)) = union(edges_of(w1), edges_of(w2)) END walks ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28