$$$pvs-strategies ;; ;; Proof rules for CSP ;; ;; Each rule corresponds to a step in a proof of A # R |> RankUser(rho) ;; ;; initialisation: install all the automatic rules ;; is assumes that the events are of type ;; "event[id, msg]" (defstep init-csp (id msg) (let ((rank-user-stop (format nil "rank_user_stop[~A,~A]" id msg)) (rank-user-input (format nil "rank_user_input[~A,~A]" id msg)) (rank-user-output (format nil "rank_user_output[~A,~A]" id msg)) (restriction-stop (format nil "restriction_stop[event[~A,~A]]" id msg))) (auto-rewrite rank-user-stop rank-user-input rank-user-output restriction-stop)) "Installs the automatic CSP rules" "Installing CSP rules") ;; choice: applies the simple choice rule (defstep choice () (try (rewrite "restriction_choice") (then (rewrite "rank_user_choice") (ground)) (skip-msg "No change")) "CSP rule for (P1 \/ P2) # R |> RankUser(rho)." "Applying choice rule") ;; choice2: same thing for unbounded choice (defstep choice2 () (try (rewrite "restriction_choice2") (then (rewrite "rank_user_choice2") (skolem!)) (skip-msg "No change")) "CSP rule for Choice(SP) # R |> RankUser(rho)" "Applying choice rule") ;; choice3: parametric choice (defstep choice3 () (try (rewrite "restriction_choice3") (then (rewrite "rank_user_choice3") (skolem!)) (skip-msg "No change")) "CSP rule for Choice! i : P(i) # R |> RankUser(rho)" "Applying choice rule") ;; prefix (defstep prefix () (try (rewrite "restriction_pref") (then* (lift-if) (assert) (prop)) (skip-msg "No change")) "CSP rule for (a >> P) # R |> RankUser(rho)" "Applying prefix rule") ;; parallel composition with synchro (defstep parallel () (try (rewrite "restriction_par") (then (rewrite "rank_user_par")(prop)) (skip-msg "No change")) "CSP rule for Par(A)(P1, P2) # R |> RankUser(rho)" "Applying parallel rule") ;; free parallel composition (defstep interleaving () (try (rewrite "restriction_free_par") (then (rewrite "rank_user_free_par")(prop)) (skip-msg "No change")) "CSP rule for (P1 // P2) # R |> RankUser(rho)" "Applying interleaving rule") ;; multiple parallel composition (defstep parallel2 () (try (rewrite "restriction_par2") (then (rewrite "rank_rule_par2")(skolem!)) (skip-msg "No change")) "CSP rule for Par(A)(lambda i : P(i)) # R |> RankUser(rho)" "Applying parallel rule") ;; multiple interleaving (defstep interleaving2 () (try (rewrite "restriction_free_par2") (then (rewrite "rank_user_free_par2")(skolem!)) (skip-msg "No change")) "CSP rule for (P1 // P2) # R |> RankUser(rho)" "Applying interleaving rule") $$$csp_traces.pvs % % Includes all the basic theories for CSP % trace semantics % csp_traces : THEORY BEGIN IMPORTING processes, parametric_choice, multipar, satisfaction, satisfaction2, satisfaction3, fixed_points, fixed_points2, process_rules END csp_traces $$$fixed_points2.pvs % % Theory for non-parametic fixed points % i.e. of monotonic functions F : [process[T] -> process[T]] % fixed_points2 [ T : TYPE ] : THEORY BEGIN IMPORTING fixed_points F : VAR [process[T] -> process[T]] X, Y : VAR process[T] %----------------------- % Monotonic functions %----------------------- monotonic?(F) : bool = FORALL X, Y : subset?(X, Y) IMPLIES subset?(F(X), F(Y)) G : VAR (monotonic?) %----------------------------------------------------------- % short cut: everything translated to the parametric case %----------------------------------------------------------- dummy : NONEMPTY_TYPE rep : dummy x : VAR dummy H : VAR [dummy -> process[T]] ext(F)(H) : [dummy -> process[T]] = lambda x : F(H(x)) mu(G) : process[T] = mu(ext(G))(rep) closure_mu2 : LEMMA subset?(G(mu(G)), mu(G)) smallest_closed2 : LEMMA subset?(G(X), X) IMPLIES subset?(mu(G), X) fixed_point2 : LEMMA G(mu(G)) = mu(G) least_fixed_point2 : LEMMA G(X) = X IMPLIES subset?(mu(G), X) %--------------------- % Induction rules %--------------------- E : VAR set[trace[T]] induction : PROPOSITION Stop[T] |> E AND (FORALL X : X |> E IMPLIES G(X) |> E) IMPLIES mu(G) |> E induction2 : PROPOSITION E(null) AND (FORALL X : X |> E IMPLIES G(X) |> E) IMPLIES mu(G) |> E END fixed_points2 $$$fixed_points2.prf (|fixed_points2| (|mu_TCC1| "" (GRIND :IF-MATCH NIL) (("" (INST - "X!1(x!1)" "Y!1(x!1)") (("" (REDUCE) NIL))))) (|closure_mu2| "" (SKOLEM!) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (EXPAND "mu") (("" (USE "closure_mu" ("G" "ext(G!1)")) (("" (ASSERT) (("" (INST?) NIL))))))))))) (|smallest_closed2| "" (SKOSIMP) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (EXPAND "mu") (("" (USE "smallest_closed" ("G" "ext(G!1)" "X" "lambda x : X!1")) (("" (GROUND) (("1" (INST?) NIL) ("2" (SKOLEM!) NIL))))))))))) (|fixed_point2| "" (SKOLEM!) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (USE "fixed_point" ("G" "ext(G!1)")) (("" (EXPAND "mu" 1 2) (("" (REPLACE -1 + RL) (("" (ASSERT) (("" (EXPAND "mu" 1 1) (("" (PROPAX) NIL))))))))))))))) (|least_fixed_point2| "" (SKOSIMP) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (EXPAND "mu") (("" (USE "least_fixed_point" ("G" "ext(G!1)" "X" "lambda x : X!1")) (("" (GROUND) (("1" (INST?) NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))) (|induction| "" (SKOSIMP) (("" (AUTO-REWRITE "mu_TCC1" "ext") (("" (EXPAND "mu") (("" (USE "param_induction" ("G" "ext(G!1)" "E" "lambda x : E!1")) (("" (GROUND) (("1" (INST?) NIL) ("2" (SKOLEM!) NIL) ("3" (SKOSIMP*) (("3" (INST?) (("3" (INST?) (("3" (ASSERT) NIL))))))))))))))))) (|induction2| "" (SKOSIMP) (("" (USE "induction") (("" (GROUND) (("" (DELETE -2 2) (("" (GRIND) NIL)))))))))) $$$fixed_points.pvs fixed_points [ U, T : TYPE ] : THEORY BEGIN IMPORTING processes, satisfaction x, x1, x2 : VAR U X, Y, Z : VAR [U -> process[T]]; t : VAR trace[T] Q : VAR process[T] %================================================= % Fixed points of a monotonic function F % F : [[U -> process[T]] -> [U -> process[T]]] %================================================= %-------------------------------------- % Order between parametric processes %-------------------------------------- <=(X, Y) : bool = FORALL x : subset?(X(x), Y(x)) reflexive : LEMMA X <= X antisymmetric : LEMMA X <= Y AND Y <= X IMPLIES X = Y transitive : LEMMA X <= Y AND Y <= Z IMPLIES X <= Z %------------------------ % greater lower bounds %------------------------ SX : VAR set[[U -> process[T]]] glb(SX)(x) : process[T] = { t | FORALL (X : (SX)) : X(x)(t) } glb_is_bound : LEMMA FORALL (X : (SX)) : glb(SX) <= X glb_is_inf : LEMMA (FORALL (X : (SX)) : Y <= X) IMPLIES Y <= glb(SX) %--------------- % Fixed point %--------------- F : VAR [[U -> process[T]] -> [U -> process[T]]] monotonic?(F) : bool = FORALL X, Y : X <= Y IMPLIES F(X) <= F(Y) G : VAR (monotonic?) mu(G) : [U -> process[T]] = glb({X | G(X) <= X}) closure_mu : LEMMA G(mu(G)) <= mu(G) smallest_closed : LEMMA G(X) <= X IMPLIES mu(G) <= X fixed_point : LEMMA G(mu(G)) = mu(G) least_fixed_point : LEMMA G(X) = X IMPLIES mu(G) <= X %------------------- % Induction rule %------------------- E : VAR [ U -> pred[trace[T]] ] <(X, E) : bool = FORALL x : X(x) |> E(x) pseudo_transitive : LEMMA X <= Y AND Y < E IMPLIES X < E SY : VAR { SX | not empty?(SX) } lub(SY)(x) : process[T] = { t | EXISTS (X : (SY)) : X(x)(t) } lub_is_bound : LEMMA FORALL (X : (SY)) : X <= lub(SY) lub_is_sup : LEMMA (FORALL (X : (SY)) : X < E) IMPLIES lub(SY) < E induction_aux : LEMMA (EXISTS X : X < E) AND (FORALL X : X < E implies G(X) < E) IMPLIES mu(G) < E param_induction0 : PROPOSITION (FORALL x : EXISTS Q : Q |> E(x)) AND (FORALL X : (FORALL x : X(x) |> E(x)) => (FORALL x : G(X)(x) |> E(x))) IMPLIES (FORALL x : mu(G)(x) |> E(x)) param_induction : PROPOSITION (FORALL x : Stop[T] |> E(x)) AND (FORALL X : (FORALL x : X(x) |> E(x)) => (FORALL x : G(X)(x) |> E(x))) IMPLIES (FORALL x : mu(G)(x) |> E(x)) param_induction2 : PROPOSITION (FORALL x : E(x)(null)) AND (FORALL X : (FORALL x : X(x) |> E(x)) => (FORALL x : G(X)(x) |> E(x))) IMPLIES (FORALL x : mu(G)(x) |> E(x)) END fixed_points $$$fixed_points.prf (|fixed_points| (|reflexive| "" (GRIND) NIL NIL) (|antisymmetric| "" (GRIND :IF-MATCH NIL) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (INST?) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (INST?) (("" (BDDSIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|transitive| "" (GRIND) NIL NIL) (|glb_TCC1| "" (GRIND :IF-MATCH NIL :EXCLUDE "prefix") (("" (INST?) (("" (TYPEPRED "X!1(x!1)") (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|glb_is_bound| "" (GRIND) NIL NIL) (|glb_is_inf| "" (GRIND :IF-MATCH BEST) NIL NIL) (|closure_mu| "" (AUTO-REWRITE "glb_is_bound" "mu" "monotonic?") (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (REWRITE "glb_is_inf") (("" (SKOLEM-TYPEPRED) (("" (INST - "mu(G!1)" "X!1") (("" (ASSERT) (("" (USE "transitive" ("X" "G!1(mu(G!1))" "Y" "G!1(X!1)" "Z" "X!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|smallest_closed| "" (AUTO-REWRITE "mu" "glb_is_bound") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|fixed_point| "" (AUTO-REWRITE "monotonic?") (("" (SKOLEM-TYPEPRED) (("" (USE* "closure_mu" "antisymmetric") (("" (ASSERT) (("" (DELETE 2) (("" (EXPAND "mu" 1 1) (("" (REWRITE "glb_is_bound") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|least_fixed_point| "" (SKOSIMP) (("" (REWRITE "smallest_closed") (("" (REPLACE*) (("" (REWRITE "reflexive") NIL NIL)) NIL)) NIL)) NIL) (|pseudo_transitive| "" (GRIND) NIL NIL) (|lub_TCC1| "" (GRIND :EXCLUDE ("prefix")) (("" (TYPEPRED "X!1(x!1)") (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|lub_is_bound| "" (GRIND) NIL NIL) (|lub_is_sup| "" (GRIND) NIL NIL) (|induction_aux| "" (SKOSIMP) (("" (CASE "empty?({ X | X < E!1})") (("1" (DELETE -3 1) (("1" (GRIND :EXCLUDE ("<" "prefix_closed") :IF-MATCH NIL) (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (DELETE -1 1) (("2" (NAME "Z!1" "lub({X | X < E!1})") (("2" (USE "lub_is_sup" ("E" "E!1")) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) (("2" (USE "lub_is_bound" ("SY" "{X | X < E!1}" "X" "G!1(Z!1)")) (("2" (REPLACE*) (("2" (FORWARD-CHAIN "smallest_closed") (("2" (FORWARD-CHAIN "pseudo_transitive") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|param_induction0| "" (SKOSIMP) (("" (USE "induction_aux") (("" (EXPAND "<") (("" (GROUND) (("" (DELETE -2 2) (("" (INST + "lambda x : epsilon! Q : Q |> E!1(x)") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (USE "epsilon_ax" ("p" "lambda Q : Q |> E!1(x!1)")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|param_induction| "" (SKOSIMP) (("" (REWRITE "param_induction0") (("" (DELETE -2 2) (("" (SKOLEM!) (("" (INST? -) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|param_induction2| "" (SKOSIMP) (("" (REWRITE "param_induction") (("" (DELETE -2 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) $$$satisfaction3.pvs % % Properties of sat and unbounded interleave % satisfaction3 [U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING satisfaction, multipar P : VAR [U -> process[T]] x : VAR U E : VAR set[trace[T]] sat_free_par3 : LEMMA Interleave(P) |> E IMPLIES P(x) |> E END satisfaction3 $$$satisfaction3.prf (|satisfaction3| (|sat_free_par3| "" (SKOSIMP) (("" (USE "interleave_subset3[U, T]") (("" (REWRITE "|>" :DIR RL) (("" (FORWARD-CHAIN "sat_transitive1") NIL)))))))) $$$satisfaction2.pvs satisfaction2 [ T : TYPE, U : TYPE ] : THEORY BEGIN IMPORTING satisfaction, parametric_choice P : VAR [U -> process[T]] x : VAR U E : VAR set[trace[T]] sat_choice3 : LEMMA Choice(P) |> E IFF Stop[T] |> E AND (FORALL x : P(x) |> E) END satisfaction2 $$$satisfaction2.prf (|satisfaction2| (|sat_choice3| "" (GRIND :EXCLUDE ("prefix_closed")) NIL)) $$$satisfaction.pvs % % Definition of the satisfaction relation % - if P is a process, E a trace predicate % P |> E means "P sat E" % - if E is also a process, % P |> E can mean "P is a refinement of E" % satisfaction [T : TYPE ] : THEORY BEGIN IMPORTING processes, process_rules P, Q : VAR process[T] E, F : VAR pred[trace[T]] SP : VAR set[process[T]] |> (P, E) : bool = subset?(P, E) sat_idempotent : LEMMA P |> P sat_transitive1 : LEMMA (P |> Q) AND (Q |> E) IMPLIES (P |> E) sat_transitive2 : LEMMA (P |> E) AND subset?(E, F) IMPLIES (P |> F) sat_choice1 : LEMMA (P \/ Q) |> E IFF P |> E AND Q |> E sat_choice2 : LEMMA Choice(SP) |> E IFF Stop[T] |> E AND (FORALL (P : (SP)) : P |> E ) sat_free_par1 : LEMMA (P // Q) |> E IMPLIES P |> E sat_free_par2 : LEMMA (P // Q) |> E IMPLIES Q |> E END satisfaction $$$satisfaction.prf (|satisfaction| (|sat_idempotent| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL) (|sat_transitive1| "" (SKOSIMP) (("" (GRIND) NIL NIL)) NIL) (|sat_transitive2| "" (SKOSIMP) (("" (GRIND) NIL NIL)) NIL) (|sat_choice1| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL) (|sat_choice2| "" (GRIND :EXCLUDE ("prefix_closed") :IF-MATCH NIL) (("1" (INST?) (("1" (GROUND) (("1" (INST + "P!1") NIL NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST - "P!1" "x!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL) (|sat_free_par1| "" (SKOSIMP) (("" (USE "interleaves_subset1[T]") (("" (REWRITE "|>" :DIR RL) (("" (FORWARD-CHAIN "sat_transitive1") NIL NIL)) NIL)) NIL)) NIL) (|sat_free_par2| "" (SKOSIMP) (("" (USE "interleaves_subset2[T]") (("" (REWRITE "|>" :DIR RL) (("" (FORWARD-CHAIN "sat_transitive1") NIL NIL)) NIL)) NIL)) NIL)) $$$multiprod.pvs % % products of a non-empty family of traces % multiprod [ U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING traces, parametric_sets t, t1, t2 : VAR [U -> trace[T]] u, v : VAR trace[T] i, j, k : VAR U A, B, C : VAR set[T] S : VAR [U -> set[T]] %---------------------------------------------------------------- % prod(A)(t, u) : "u is a product of the traces {t(i) | i in U} % with synchronisations on A %---------------------------------------------------------------- prod(A)(t, u) : RECURSIVE bool = CASES u OF null: (FORALL i : t(i) = null), cons(x, y): IF A(x) THEN (FORALL i : cons?(t(i)) AND car(t(i)) = x) AND prod(A)(lambda j : cdr(t(j)), y) ELSE EXISTS i : cons?(t(i)) AND car(t(i)) = x AND prod(A)(t with [(i) := cdr(t(i))], y) ENDIF ENDCASES MEASURE length(u) proj_multiprod : LEMMA prod(A)(t, u) IMPLIES FORALL i : proj(t(i), A) = proj(u, A) prefix_multiprod : LEMMA prod(A)(t, u) AND prefix(v, u) IMPLIES EXISTS t1 : prod(A)(t1, v) AND FORALL i : prefix(t1(i), t(i)) multiprod_fullset : LEMMA prod(fullset)(t, u) IFF (FORALL i : t(i) = u) free_multiprod : LEMMA prod(emptyset)((lambda i : null[T]) WITH [(j) := u], u) sigma_multiprod : LEMMA prod(A)(t, u) IMPLIES sigma(u) = union! i : sigma(t(i)) sigma_multiprod_inter : LEMMA prod(A)(t, u) IMPLIES intersection(sigma(t(i)), A) = intersection(sigma(u), A) %---------------------------------------------------------------- % Interleaving when the traces have mutually disjoint alphabets %---------------------------------------------------------------- sub_alphabet(t, S) : bool = FORALL i : subset?(sigma(t(i)), S(i)) disj_alphabet(S) : bool = FORALL i, j : i /= j IMPLIES disjoint?(S(i), S(j)) inter_disjoint : LEMMA disj_alphabet(S) AND sub_alphabet(t, S) AND prod(emptyset)(t, u) IMPLIES FORALL i : t(i) = proj(u, S(i)) %--------------------------------------- % Projections/restrictions %----------------------------------------- inter_proj : LEMMA prod(emptyset)(t, u) IMPLIES prod(emptyset)(lambda i : proj(t(i), B), proj(u, B)) null_proj_multiprod : LEMMA prod(A)(t, u) IMPLIES (proj(u, B) = null IFF FORALL i : proj(t(i), B) = null) null_proj_multiprod2 : LEMMA prod(A)(t, u) AND subset?(B, A) AND proj(t(i), B) = null IMPLIES proj(u, B) = null null_inter_proj : LEMMA prod(emptyset)(t, u) IMPLIES (proj(u, B) = null IFF FORALL i : proj(t(i), B) = null) END multiprod $$$multiprod.prf (|multiprod| (|prod_TCC1| "" (SKOSIMP*) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_TCC2| "" (TERMINATION-TCC) NIL NIL) (|prod_TCC3| "" (TERMINATION-TCC) NIL NIL) (|proj_multiprod| "" (AUTO-REWRITE-DEFS) (("" (SKOLEM + ("A!1" _ _)) (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (CASE "A!1(cons1_var!1)") (("1" (REDUCE) NIL NIL) ("2" (ASSERT) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (INST?) (("2" (GROUND) (("2" (INST - "i!1") (("2" (CASE "i!1 = i!2") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_multiprod| "" (AUTO-REWRITE "prefix_null[T]" "null_prefix[T]") (("" (SKOLEM + ("A!1" _ _ _)) (("" (INDUCT "u") (("1" (AUTO-REWRITE "prod") (("1" (SKOSIMP) (("1" (INST + "lambda i : null") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (REWRITE "prefix_equiv") (("2" (GROUND) (("1" (AUTO-REWRITE "prod") (("1" (INST + "lambda i : null") (("1" (DELETE -2 -3) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "prod") (("2" (CASE "A!1(cons1_var!1)") (("1" (ASSERT) (("1" (GROUND) (("1" (INST - "LAMBDA (i: U): cdr(t!1(i))" "cdr(v!1)") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "lambda i : cons(cons1_var!1, t1!1(i))") (("1" (GROUND) (("1" (LEMMA "eta[U, trace[T]]") (("1" (INST - "t1!1") (("1" (REPLACE -1) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST?) (("2" (INST?) (("2" (REWRITE "prefix_equiv" +) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (INST - "t!1 WITH [(i!1) := cdr(t!1(i!1))]" "cdr(v!1)") (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "t1!1 with [(i!1) := cons(cons1_var!1, t1!1(i!1))]") (("2" (GROUND) (("1" (INST + "i!1") (("1" (ASSERT) (("1" (CASE-REPLACE "t1!1 WITH [(i!1):= cons(cons1_var!1, t1!1(i!1)), (i!1) := t1!1(i!1)] = t1!1") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (CASE "x!1 = i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST - "i!2") (("2" (CASE "i!1 = i!2") (("1" (ASSERT) (("1" (REWRITE "prefix_equiv" +) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|multiprod_fullset| "" (AUTO-REWRITE "fullset" "prod") (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (GROUND) (("1" (INST? -3) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST?) (("1" (INST?) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -2 2) (("2" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST?) (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (INST? -2) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST?) (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|free_multiprod| "" (INDUCT-AND-SIMPLIFY "u") NIL NIL) (|sigma_multiprod| "" (INDUCT-AND-SIMPLIFY "u") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (REDUCE) NIL NIL)) NIL) ("2" (REPLACE*) (("2" (DELETE -1 -4) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (REDUCE) (("1" (INST + "epsilon! i : true") (("1" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (DELETE -1 -4) (("3" (APPLY-EXTENSIONALITY :HIDE? T) (("3" (IFF) (("3" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOLEM!) (("2" (INST + "i!2") (("2" (SMASH) NIL NIL)) NIL)) NIL) ("3" (SKOLEM!) (("3" (INST?) (("3" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_multiprod_inter| "" (SKOSIMP) (("" (FORWARD-CHAIN "proj_multiprod") (("" (INST?) (("" (REWRITE "sigma_proj" :DIR RL) (("" (REWRITE "sigma_proj" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inter_disjoint| "" (AUTO-REWRITE "prod" "emptyset" "proj" "filter") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (SKOLEM + ("A!1" _ _)) (("" (INDUCT "u") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL) ("2" (AUTO-REWRITE "sub_alphabet" "disj_alphabet" "sigma" "list2set") (("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST - "t!1 WITH [(i!1) := cdr(t!1(i!1))]") (("2" (GROUND) (("1" (INST? -3) (("1" (INST -3 "cons1_var!1") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST?) (("1" (CASE "i!1 = i!2") (("1" (ASSERT) (("1" (APPLY-EXTENSIONALITY) NIL NIL)) NIL) ("2" (INST - "i!1" "i!2") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -5 2) (("2" (SKOLEM!) (("2" (INST - "i!2") (("2" (CASE "i!1 = i!2") (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inter_proj| "" (AUTO-REWRITE "prod" "emptyset" "proj" "filter") (("" (SKOLEM + ("A!1" _ _)) (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST? :WHERE -4) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) (("1" (CASE-REPLACE "(LAMBDA i : filter(t!1(i), A!1)) WITH [(i!1) := filter(cdr(t!1(i!1)), A!1)] = (LAMBDA i : filter(t!1 WITH [(i!1) := cdr(t!1(i!1))](i), A!1))") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (CASE "x!1 = i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE-REPLACE "(LAMBDA i : filter(t!1(i), A!1)) = LAMBDA i : filter(t!1 WITH [(i!1) := cdr(t!1(i!1))](i), A!1)") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (CASE "x!1 = i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_multiprod| "" (SKOSIMP) (("" (AUTO-REWRITE "null_proj_equiv[T]") (("" (ASSERT) (("" (FORWARD-CHAIN "sigma_multiprod") (("" (REPLACE*) (("" (DELETE -) (("" (EXPAND "union") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_multiprod2| "" (SKOSIMP) (("" (AUTO-REWRITE "null_proj_equiv[T]") (("" (ASSERT) (("" (USE "sigma_multiprod_inter") (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) (("" (CASE "intersection(sigma(t!1(i!1)), A!1)(x!1)") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_inter_proj| "" (SKOSIMP) (("" (USE "null_proj_multiprod") (("" (ASSERT) NIL NIL)) NIL)) NIL)) $$$multipar.pvs % % Parallel composition of a non-empty family of processes % % T : event type % U : parameter type % multipar [ U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING processes, multiprod, process_rules P : VAR [U -> process[T]] A : VAR set[T] S : VAR [U -> set[T]] u : VAR trace[T] i, j : VAR U %-------------------------------------------------- % Parallel composition with synchronisation on A %-------------------------------------------------- Par(A)(P) : process[T] = { u | EXISTS (t : [i:U -> (P(i))]) : prod(A)(t, u) } %---------------- % Interleaving %---------------- Interleave(P) : process[T] = Par(emptyset)(P) %-------------- % Properties %-------------- sigma_par2 : LEMMA subset?(sigma(Par(A)(P)), union! i : sigma(P(i))) sigma_free_par2 : LEMMA sigma(Interleave(P)) = union! i : sigma(P(i)) par_full2 : LEMMA Par(fullset)(P) = intersection! i : P(i) interleave_subset3 : LEMMA subset?(P(i), Interleave(P)) %-------------------------------------------------------- % Interleaving when processes have disjoint interfaces %-------------------------------------------------------- interleave_disjoint : LEMMA (FORALL i : subset?(sigma(P(i)), S(i))) AND (FORALL i, j : i /= j IMPLIES disjoint?(S(i), S(j))) IMPLIES subset?(Interleave(P), { u | FORALL i : P(i)(proj(u, S(i))) }) END multipar $$$multipar.prf (|multipar| (|Par_TCC1| "" (SKOLEM!) (("" (GROUND) (("1" (INST + "lambda i : null") (("1" (EXPAND "prod") (("1" (PROPAX) NIL))) ("2" (REDUCE) NIL))) ("2" (AUTO-REWRITE "prefix_closed") (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (FORWARD-CHAIN "prefix_multiprod") (("2" (SKOSIMP) (("2" (INST + "t1!2") (("2" (SKOLEM!) (("2" (INST?) (("2" (TYPEPRED "P!1(x1!1)") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))))) (|sigma_par2| "" (EXPAND "Par") (("" (EXPAND "sigma") (("" (GRIND :DEFS NIL :THEORIES ("sets[T]" "sets[trace[T]]") :IF-MATCH NIL) (("" (FORWARD-CHAIN "sigma_multiprod") (("" (REPLACE -1) (("" (EXPAND "union") (("" (SKOLEM!) (("" (INST + "i!1") (("" (INST?) NIL))))))))))))))))) (|sigma_free_par2| "" (EXPAND "Interleave") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (USE "sigma_par2") (("1" (EXPAND "subset?") (("1" (EXPAND "member") (("1" (INST?) (("1" (ASSERT) NIL))))))))) ("2" (EXPAND "union") (("2" (EXPAND "Par") (("2" (EXPAND "sigma") (("2" (SKOSIMP* :PREDS? T) (("2" (INST?) (("2" (INST + "lambda i : IF i = i!1 THEN t!1 ELSE null[T] ENDIF") (("1" (LEMMA "free_multiprod" ("j" "i!1" "u" "t!1")) (("1" (CASE-REPLACE "(LAMBDA i: IF i = i!1 THEN t!1 ELSE null[T] ENDIF) = ((LAMBDA i: null[T]) WITH [(i!1) := t!1])") (("1" (DELETE -1 -3 2) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (SMASH) NIL))))))))) ("2" (SKOSIMP) (("2" (ASSERT) NIL))) ("3" (SKOSIMP) (("3" (ASSERT) NIL))))))))))))))))))))))))) (|par_full2| "" (AUTO-REWRITE "Par" "intersection") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (SKOLEM!) (("1" (REWRITE "multiprod_fullset") (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL))))))))) ("2" (INST + "lambda i : x!1") (("2" (REWRITE "multiprod_fullset") NIL))))))))))))) (|interleave_subset3| "" (GRIND :EXCLUDE ("prod")) (("" (USE "free_multiprod[U, T]") (("" (INST + "lambda i : IF i = i!1 THEN x!1 ELSE null[T] ENDIF") (("1" (CASE-REPLACE "(LAMBDA i: IF i = i!1 THEN x!1 ELSE null[T] ENDIF) = (LAMBDA i: null[T]) WITH [(i!1) := x!1]") (("1" (DELETE -1 2) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (REDUCE) NIL))))))) ("2" (SKOSIMP) (("2" (ASSERT) NIL))) ("3" (SKOSIMP) (("3" (ASSERT) NIL))))))))) (|interleave_disjoint| "" (GRIND :EXCLUDE ("proj" "sigma" "disjoint?") :REWRITES ("disj_alphabet[U, T]" "sub_alphabet[U, T]") :IF-MATCH NIL) (("" (USE "inter_disjoint[U, T]" ("t" "t!1")) (("" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (REWRITE "sub_alphabet") (("2" (SKOSIMP*) (("2" (INST?) (("2" (ASSERT) (("2" (DELETE -2 -3 1 3) (("2" (USE "sigma_subset" ("P" "P!1(i!2)")) (("2" (REDUCE) NIL)))))))))))))))))))) $$$parametric_sets.pvs % % union and intersection of a family of sets % % T : element type % U : index type % parametric_sets [ U, T : TYPE ] : THEORY BEGIN A : VAR [U -> set[T]] i : VAR U x : VAR T S : VAR set[T] %--------------- % Definitions %--------------- union(A) : set[T] = { x | EXISTS i : A(i)(x) } intersection(A) : set[T] = { x | FORALL i : A(i)(x) } %-------------- % Properties %-------------- union_is_bound : LEMMA subset?(A(i), union(A)) union_is_lub : LEMMA (FORALL i : subset?(A(i), S)) IMPLIES subset?(union(A), S) inter_is_bound : LEMMA subset?(intersection(A), A(i)) inter_is_glb : LEMMA (FORALL i : subset?(S, A(i))) IMPLIES subset?(S, intersection(A)) END parametric_sets $$$parametric_sets.prf (|parametric_sets| (|union_is_bound| "" (GRIND) NIL) (|union_is_lub| "" (GRIND) NIL) (|inter_is_bound| "" (GRIND) NIL) (|inter_is_glb| "" (GRIND) NIL)) $$$process_rules.pvs process_rules [ T : TYPE ] : THEORY BEGIN IMPORTING processes, parametric_sets P, P1, P2, P3, P4 : VAR process[T] SP, SP1, SP2 : VAR set[process[T]] a, b, c : VAR T A, B, C : VAR set[T] t : VAR trace[T] %------------------ % Prefix closure %------------------ process_add : LEMMA P(add(t, a)) IMPLIES P(t) %------------------- % Rules for sigma %------------------- sigma_stop : LEMMA sigma(Stop[T]) = emptyset sigma_choice : LEMMA sigma(P1 \/ P2) = union(sigma(P1), sigma(P2)) sigma_choice2 : LEMMA sigma(Choice(SP)) = union! (P : (SP)) : sigma(P) sigma_pref : LEMMA sigma(a >> P) = add(a, sigma(P)) sigma_par : LEMMA subset?(sigma(Par(A)(P1, P2)), union(sigma(P1), sigma(P2))) sigma_free_par : LEMMA sigma(P1 // P2) = union(sigma(P1), sigma(P2)) sigma_empty : LEMMA sigma(P) = emptyset IFF P = Stop[T] sigma_union : LEMMA sigma(P) = union! (t : (P)) : sigma(t) sigma_subset : LEMMA FORALL (t : (P)) : subset?(sigma(t), sigma(P)) %-------------------------------- % Stop is the smallest process %-------------------------------- stop_subset : LEMMA subset?(Stop[T], P) stop_smallest : LEMMA subset?(P, Stop[T]) IFF P = Stop[T] %---------------------------- % Rules for bounded choice %---------------------------- choice_commutes : LEMMA (P1 \/ P2) = (P2 \/ P1) choice_assoc : LEMMA (P1 \/ (P2 \/ P3)) = ((P1 \/ P2) \/ P3) choice_idempotent : LEMMA (P \/ P) = P choice_subset1 : LEMMA subset?(P1, P1 \/ P2) choice_subset2 : LEMMA subset?(P2, P1 \/ P2) choice_stop1 : LEMMA (P \/ Stop[T]) = P choice_stop2 : LEMMA (Stop[T] \/ P) = P choice_stop3 : LEMMA (P1 \/ P2) = Stop[T] IFF P1 = Stop[T] AND P2 = Stop[T] %------------------------------ % Rules for unbounded choice %------------------------------ choice_empty : LEMMA Choice(emptyset[process[T]]) = Stop[T] choice_add : LEMMA Choice(add(P, SP)) = (P \/ Choice(SP)) choice_singleton : LEMMA Choice(singleton(P)) = P choice_union : LEMMA Choice(union(SP1, SP2)) = (Choice(SP1) \/ Choice(SP2)) choice_member : LEMMA FORALL (P : (SP)) : subset?(P, Choice(SP)) %---------------------------------- % Rules for parallel composition %---------------------------------- par_commutes : LEMMA Par(A)(P1, P2) = Par(A)(P2, P1) par_assoc : LEMMA Par(A)(P1, Par(A)(P2, P3)) = Par(A)(Par(A)(P1, P2), P3) par_stop : LEMMA Par(A)(P, Stop) = { t | P(t) AND proj(t, A) = null } par_full : LEMMA Par(fullset)(P1, P2) = intersection(P1, P2) %--------------------------- % Rules for interleaving %--------------------------- interleaves_commutes : LEMMA P1 // P2 = P2 // P1 interleaves_assoc : LEMMA (P1 // P2) // P3 = P1 // (P2 // P3) interleaves_subset1 : LEMMA subset?(P1, P1 // P2) interleaves_subset2 : LEMMA subset?(P2, P1 // P2) interleaves_stop1 : LEMMA P // Stop[T] = P interleaves_stop2 : LEMMA Stop[T] // P = P END process_rules $$$process_rules.prf (|process_rules| (|process_add| "" (AUTO-REWRITE "prefix_closed[T]" "prefix[T]" "add[T]") (("" (SKOSIMP :PREDS? T) (("" (ASSERT) (("" (INST - "t!1" "add(t!1, a!1)") (("" (ASSERT) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_stop| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL) (|sigma_choice| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :DEFS NIL :REWRITES ("sigma" "Choice" "\\/") :THEORIES ("sets[T]" "sets[trace[T]]")) NIL NIL)) NIL)) NIL) (|sigma_choice2| "" (AUTO-REWRITE "sigma" "Choice" "union" "emptyset" "list2set") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (SKOLEM-TYPEPRED) (("1" (ASSERT) (("1" (GROUND) (("1" (SKOLEM!) (("1" (INST + "P!1") (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST?) (("2" (FLATTEN) (("2" (INST + "i!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_pref| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :IF-MATCH NIL) (("1" (INST?) NIL NIL) ("2" (INST + "(: a!1 :)") (("1" (ASSERT) NIL NIL) ("2" (INST?) NIL NIL)) NIL) ("3" (INST + "cons(a!1, t!1)") (("1" (ASSERT) NIL NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_par| "" (EXPAND "Par") (("" (EXPAND "sigma") (("" (GRIND :DEFS NIL :THEORIES ("sets[T]" "sets[trace[T]]") :IF-MATCH NIL) (("" (FORWARD-CHAIN "sigma_prod") (("" (REPLACE*) (("" (ASSERT) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_free_par| "" (SKOLEM!) (("" (EXPAND "//") (("" (USE "sigma_par") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (IFF) (("" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE -2) (("2" (GRIND :DEFS NIL :REWRITES ("Par" "sigma" "free_prod_left[T]" "free_prod_right[T]") :IF-MATCH NIL) (("1" (INST?) (("1" (INST + "t!1" "null") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST?) (("2" (INST + "null" "t!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_empty| "" (SKOLEM!) (("" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (EXPAND "Stop") (("1" (REWRITE "emptyset_is_empty?" :DIR RL) (("1" (GRIND) (("1" (INST - "car(x!1)") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (REWRITE "sigma_stop") NIL NIL)) NIL)) NIL)) NIL) (|sigma_union| "" (EXPAND "sigma" 1 1) (("" (EXPAND "union") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|sigma_subset| "" (SKOLEM!) (("" (REWRITE "sigma_union") (("" (USE "union_is_bound" ("A" "lambda (t: (P!1)): sigma(t)")) NIL NIL)) NIL)) NIL) (|stop_subset| "" (GRIND :EXCLUDE "prefix_closed") NIL NIL) (|stop_smallest| "" (GRIND :EXCLUDE "prefix_closed" :IF-MATCH NIL) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (IFF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|choice_commutes| "" (GRIND :EXCLUDE "prefix_closed") (("" (REWRITE "union_commutative") NIL NIL)) NIL) (|choice_assoc| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "union_associative") NIL NIL)) NIL)) NIL)) NIL) (|choice_idempotent| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "union_idempotent") NIL NIL)) NIL)) NIL)) NIL) (|choice_subset1| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "union_subset1") NIL NIL)) NIL)) NIL)) NIL) (|choice_subset2| "" (SKOLEM!) (("" (REWRITE "choice_commutes") (("" (REWRITE "choice_subset1") NIL NIL)) NIL)) NIL) (|choice_stop1| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|choice_stop2| "" (SKOLEM!) (("" (REWRITE "choice_commutes") (("" (REWRITE "choice_stop1") NIL NIL)) NIL)) NIL) (|choice_stop3| "" (AUTO-REWRITE "choice_idempotent" "stop_smallest") (("" (SKOLEM!) (("" (GROUND) (("1" (USE "choice_subset1") (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (USE "choice_subset2") (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|choice_empty| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL) (|choice_add| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE "prefix_closed" :IF-MATCH NIL) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL) ("3" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|choice_singleton| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE "prefix_closed") NIL NIL)) NIL)) NIL) (|choice_union| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE "prefix_closed") NIL NIL)) NIL)) NIL) (|choice_member| "" (GRIND :EXCLUDE "prefix_closed") NIL NIL) (|par_commutes| "" (SKOLEM!) (("" (EXPAND "Par") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (SKOSIMP) (("1" (REWRITE "prod_commutes") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (REWRITE "prod_commutes") (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|par_assoc| "" (SKOLEM!) (("" (EXPAND "Par") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE :IF-MATCH NIL) (("1" (USE "prod_assoc2" ("u" "t2!1")) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "u1!1" "t2!2") (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "prod_assoc1" ("u" "t1!1")) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "t1!2" "u1!1") (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|par_stop| "" (AUTO-REWRITE "Par" "Stop") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (PROP) (("1" (SKOLEM-TYPEPRED) (("1" (ASSERT) (("1" (REPLACE*) (("1" (FORWARD-CHAIN "prod_null1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM-TYPEPRED) (("2" (ASSERT) (("2" (REPLACE*) (("2" (FORWARD-CHAIN "proj_prod2") (("2" (AUTO-REWRITE "proj") (("2" (AUTO-REWRITE "proj" "filter") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (FORWARD-CHAIN "prod_null3") (("3" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|par_full| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE ("prod") :REWRITES ("prod_fullset[T]")) NIL NIL)) NIL)) NIL) (|interleaves_commutes| "" (EXPAND "//") (("" (SKOLEM!) (("" (REWRITE "par_commutes") NIL NIL)) NIL)) NIL) (|interleaves_assoc| "" (SKOLEM!) (("" (EXPAND "//") (("" (REWRITE "par_assoc") NIL NIL)) NIL)) NIL) (|interleaves_subset1| "" (GRIND :EXCLUDE ("prefix_closed" "prod") :IF-MATCH NIL) (("" (INST + "x!1" "null") (("" (REWRITE "free_prod_left") NIL NIL)) NIL)) NIL) (|interleaves_subset2| "" (GRIND :EXCLUDE ("prefix_closed" "prod") :IF-MATCH NIL) (("" (INST + "null" "x!1") (("" (REWRITE "free_prod_right") NIL NIL)) NIL)) NIL) (|interleaves_stop1| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE ("prod" "prefix_closed") :IF-MATCH NIL) (("1" (USE "prod_null1" ("t1" "t1!1" "t" "x!1")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "x!1" "null") (("2" (REWRITE "free_prod_left") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|interleaves_stop2| "" (SKOLEM!) (("" (REWRITE "interleaves_commutes") (("" (REWRITE "interleaves_stop1") NIL NIL)) NIL)) NIL)) $$$parametric_choice.pvs % % Unbounded choice of a family {P(i) | i in U} % % T = event type % U = parameter type % parametric_choice [ U, T : TYPE] : THEORY BEGIN IMPORTING processes, process_rules P : VAR [U -> process[T]] Q : VAR process[T] t : VAR trace[T] i : VAR U %-------------- % Definition %-------------- Choice(P) : process[T] = { t | null?(t) OR EXISTS i : P(i)(t) } %----------------- % Various rules %----------------- choice_equiv : LEMMA Choice(P) = Choice({ Q | EXISTS i : Q = P(i)}) choice_nonempty_param : LEMMA (EXISTS i : true) IMPLIES Choice(P) = union! i : P(i) choice_empty_param : LEMMA (FORALL i : false) IMPLIES Choice(P) = Stop sigma_choice3 : LEMMA sigma(Choice(P)) = union! i : sigma(P(i)) choice_member2 : LEMMA subset?(P(i), Choice(P)) END parametric_choice $$$parametric_choice.prf (|parametric_choice| (|Choice_TCC1| "" (GRIND :IF-MATCH NIL :EXCLUDE ("prefix")) (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (INST?) (("2" (TYPEPRED "P!1(i!1)") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|choice_equiv| "" (SKOLEM!) (("" (EXPAND "Choice") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (DELETE 1) (("1" (REDUCE) NIL NIL)) NIL) ("2" (DELETE 1) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|choice_nonempty_param| "" (SKOSIMP*) (("" (TYPEPRED "P!1(i!1)") (("" (DELETE -2) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|choice_empty_param| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|sigma_choice3| "" (SKOLEM!) (("" (REWRITE "choice_equiv") (("" (REWRITE "sigma_choice2") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "union") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|choice_member2| "" (SKOLEM!) (("" (REWRITE "choice_nonempty_param") (("1" (USE "union_is_bound" ("A" "lambda i : P!1(i)")) NIL NIL) ("2" (INST + "i!1") NIL NIL)) NIL)) NIL)) $$$more_list_props.pvs % % Extension of the pre-defined operations on lists % and extra properties % more_list_props [ T : TYPE] : THEORY BEGIN l, l1, l2 : VAR list[T] cons_l, cons_l1, cons_l2 : VAR (cons?[T]) a, b, c : VAR T P : VAR [list[T] -> bool] %---------------------------------------- % add(l, a) : append a at the end of l %---------------------------------------- add(l, a) : (cons?[T]) = append(l, cons(a, null)) add_null : LEMMA add(null, a) = (: a :) add_cons : LEMMA add(cons(a, l), b) = cons(a, add(l, b)) %------------------------ % Properties of length %------------------------ length_append : LEMMA length(append(l1, l2)) = length(l1) + length(l2) length_add : LEMMA length(add(l, a)) = length(l) + 1 length_reverse : LEMMA length(reverse(l)) = length(l) length_cdr : LEMMA length(cdr(cons_l)) = length(cons_l) - 1 length_zero : LEMMA length(l) = 0 IFF l = null length_non_zero : LEMMA length(l) > 0 IFF cons?(l) %----------------------- % Induction using add %----------------------- cons_to_add : LEMMA FORALL cons_l : EXISTS a, l : cons_l = add(l, a) add_induction : PROPOSITION P(null) AND (FORALL l, a : P(l) IMPLIES P(add(l, a))) IMPLIES (FORALL l : P(l)) END more_list_props $$$more_list_props.prf (|more_list_props| (|add_TCC1| "" (SKOLEM!) (("" (EXPAND "append") (("" (LIFT-IF) (("" (ASSERT) NIL))))))) (|add_null| "" (GRIND) NIL) (|add_cons| "" (GRIND) NIL) (|length_append| "" (SKOLEM + (_ "l2!1")) (("" (INDUCT-AND-SIMPLIFY "l1") NIL))) (|length_add| "" (AUTO-REWRITE "length" "add" "length_append") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|length_reverse| "" (INDUCT-AND-SIMPLIFY "l" :REWRITES ("length_append")) NIL) (|length_cdr| "" (AUTO-REWRITE "length") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|length_zero| "" (GRIND) NIL) (|length_non_zero| "" (GRIND) NIL) (|cons_to_add| "" (AUTO-REWRITE "add_null" "add_cons") (("" (INDUCT "cons_l") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (SKOSIMP) (("3" (GROUND) (("1" (SKOLEM!) (("1" (INST + "a!1" "cons(cons1_var!1, l!1)") (("1" (ASSERT) NIL))))) ("2" (INST + "cons1_var!1" "null") (("2" (ASSERT) (("2" (ASSERT) NIL))))))))))))) (|add_induction| "" (SKOSIMP) (("" (CASE "FORALL (n : nat), l : length(l) = n IMPLIES P!1(l)") (("1" (SKOLEM!) (("1" (INST - "length(l!1)" "l!1") (("1" (ASSERT) NIL))))) ("2" (DELETE 2) (("2" (AUTO-REWRITE "length_zero" "length_add") (("2" (INDUCT "n") (("1" (SKOSIMP) (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (USE "length_non_zero" ("l" "l!1")) (("2" (ASSERT) (("2" (USE "cons_to_add" ("cons_l" "l!1")) (("2" (SKOLEM!) (("2" (REPLACE -1) (("2" (INST - "l!2") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))))))))) $$$traces.pvs % % Traces over events of type T % defines operators specific to PVS % % Functions defined in the prelude: % length(t) : nat % member(a, t) : bool % nth(t, i) : T (i : below[length(t)]) % append(t1, t2) : trace % reverse(t) : trace % cons(a, t) : trace % null : trace % car(t) : T % cdr(t) : trace % % filter(t, S) : trace % filter(S)(t) : trace % list2set(t) : set[T] % % Defined in more_list_props % add(t, a) : trace % % Defined in trace % prefix(t1, t2) : bool % proj(t, S) : trace % prod(S)(t1, t2, t) : bool % sigma(t) : set[T] % traces [ T : TYPE ] : THEORY BEGIN IMPORTING more_list_props trace : TYPE = list[T] a, b, c : VAR T A, B, C : VAR setof[T] t, t1, t2, t3 : VAR trace u, u1, u2 : VAR trace %----------- % Prefix %----------- prefix(t1, t2) : bool = EXISTS t : t2 = append(t1, t) prefix_equiv : LEMMA prefix(t1, t2) IFF null?(t1) OR (cons?(t1) AND cons?(t2) AND car(t1) = car(t2) AND prefix(cdr(t1), cdr(t2))) null_prefix : LEMMA prefix(null, t) prefix_null : LEMMA prefix(t, null) IFF t = null cons_prefix : LEMMA prefix(cons(a, t1), cons(b, t2)) IFF a = b AND prefix(t1, t2) prefix_append1 : LEMMA prefix(t1, t2) IMPLIES prefix(t1, append(t2, t3)) prefix_append2 : LEMMA prefix(t1, t2) IMPLIES prefix(append(t, t1), append(t, t2)) prefix_add1 : LEMMA prefix(t, add(t, a)) prefix_add2 : LEMMA prefix(t1, t2) IMPLIES prefix(t1, add(t2, a)) length_prefix : LEMMA prefix(t1, t2) IMPLIES length(t1) <= length(t2) prefix_reflexive : LEMMA prefix(t, t) prefix_transitive : LEMMA prefix(t1, t2) AND prefix(t2, t3) IMPLIES prefix(t1, t3) prefix_antisymmetric : LEMMA prefix(t1, t2) AND prefix(t2, t1) IMPLIES t1 = t2 %-------------- % Projection %-------------- proj : [trace, set[T] -> trace] = filter proj_null : LEMMA proj(null, A) = null proj_cons : LEMMA proj(cons(a, t), A) = IF A(a) THEN cons(a, proj(t, A)) ELSE proj(t, A) ENDIF proj_append : LEMMA proj(append(t1, t2), A) = append(proj(t1, A), proj(t2, A)) proj_add : LEMMA proj(add(t, a), A) = IF A(a) THEN add(proj(t, A), a) ELSE proj(t, A) ENDIF proj_prefix : LEMMA prefix(t1, t2) IMPLIES prefix(proj(t1, A), proj(t2, A)) proj_reverse : LEMMA proj(reverse(t), A) = reverse(proj(t, A)) prefix_of_proj : LEMMA prefix(t1, proj(t, A)) IMPLIES EXISTS t2 : prefix(t2, t) AND t1 = proj(t2, A) prefix_of_proj2 : LEMMA prefix(t1, proj(t, A)) IFF EXISTS t2 : prefix(t2, t) AND t1 = proj(t2, A) proj_twice : LEMMA proj(proj(t, A), B) = proj(t, intersection(A, B)) %------------------------------------------------ % product: for parallel composition % -> prod(A)(t1, t2, t) holds if % % t is a possible interleaving of t1 and t2 % with events in A synchronized %------------------------------------------------- prod(A)(t1, t2, t) : RECURSIVE bool = CASES t OF null : null?(t1) AND null?(t2), cons(x, y) : IF A(x) THEN cons?(t1) AND cons?(t2) AND car(t1) = x AND car(t2) = x AND prod(A)(cdr(t1), cdr(t2), y) ELSE (cons?(t1) AND car(t1) = x AND prod(A)(cdr(t1), t2, y)) OR (cons?(t2) AND car(t2) = x AND prod(A)(t1, cdr(t2), y)) ENDIF ENDCASES MEASURE length(t) prod_commutes : LEMMA prod(A)(t1, t2, t) IFF prod(A)(t2, t1, t) proj_prod1 : LEMMA prod(A)(t1, t2, t) IMPLIES proj(t1, A) = proj(t, A) proj_prod2 : LEMMA prod(A)(t1, t2, t) IMPLIES proj(t2, A) = proj(t, A) prod_null1 : LEMMA prod(A)(t1, null, t) IMPLIES t1 = t prod_null2 : LEMMA prod(A)(null, t2, t) IMPLIES t2 = t prod_null3 : LEMMA proj(t, A) = null IMPLIES prod(A)(t, null, t) prod_null4 : LEMMA proj(t, A) = null IMPLIES prod(A)(null, t, t) prefix_prod : LEMMA prod(A)(t1, t2, t) AND prefix(u, t) IMPLIES EXISTS u1, u2 : prefix(u1, t1) AND prefix(u2, t2) AND prod(A)(u1, u2, u) prod_assoc1 : LEMMA prod(A)(t1, t2, u) AND prod(A)(u, t3, t) IMPLIES EXISTS u1 : prod(A)(t1, u1, t) AND prod(A)(t2, t3, u1) prod_assoc2 : LEMMA prod(A)(t1, u, t) AND prod(A)(t2, t3, u) IMPLIES EXISTS u1 : prod(A)(t1, t2, u1) AND prod(A)(u1, t3, t) prod_assoc : LEMMA (EXISTS u : prod(A)(t1, t2, u) AND prod(A)(u, t3, t)) IFF (EXISTS u : prod(A)(t1, u, t) AND prod(A)(t2, t3, u)) prod_fullset : LEMMA prod(fullset)(t1, t2, u) IFF t1 = u AND t2 = u free_prod_left : LEMMA prod(emptyset)(t, null, t) free_prod_right : LEMMA prod(emptyset)(null, t, t) %--------------------------- % sigma(t) : events of t %-------------------------- sigma : [trace -> set[T]] = list2set sigma_equiv : LEMMA sigma(t) = { a | member(a, t) } sigma_null : LEMMA sigma(null) = emptyset sigma_cons : LEMMA sigma(cons(a, t)) = add(a, sigma(t)) sigma_empty : LEMMA empty?(sigma(t)) IFF t = null sigma_append : LEMMA sigma(append(t1, t2)) = union(sigma(t1), sigma(t2)) sigma_add : LEMMA sigma(add(t, a)) = add(a, sigma(t)) sigma_prefix : LEMMA prefix(t1, t2) IMPLIES subset?(sigma(t1), sigma(t2)) sigma_proj : LEMMA sigma(proj(t, A)) = intersection(sigma(t), A) sigma_prod : LEMMA prod(A)(t1, t2, t) IMPLIES sigma(t) = union(sigma(t1), sigma(t2)) sigma_prod_inter1 : LEMMA prod(A)(t1, t2, t) IMPLIES intersection(sigma(t), A) = intersection(sigma(t1), A) sigma_prod_inter2 : LEMMA prod(A)(t1, t2, t) IMPLIES intersection(sigma(t), A) = intersection(sigma(t2), A) %---------------------- % Empty projections %---------------------- null_proj_equiv : LEMMA proj(t, B) = null IFF disjoint?(sigma(t), B) null_proj_subset : LEMMA subset?(A, B) AND proj(t, B) = null IMPLIES proj(t, A) = null null_proj_union : LEMMA proj(t, union(A, B)) = null IFF proj(t, A) = null AND proj(t, B) = null null_proj_prod : LEMMA prod(A)(t1, t2, t) IMPLIES (proj(t, B) = null IFF proj(t1, B) = null AND proj(t2, B) = null) null_proj_prod1 : LEMMA prod(A)(t1, t2, t) AND proj(t, B) = null IMPLIES proj(t1, B) = null null_proj_prod2 : LEMMA prod(A)(t1, t2, t) AND proj(t, B) = null IMPLIES proj(t2, B) = null null_proj_prod3 : LEMMA prod(A)(t1, t2, t) AND subset?(B, A) AND proj(t1, B) = null IMPLIES proj(t, B) = null null_proj_prod4 : LEMMA prod(A)(t1, t2, t) AND subset?(B, A) AND proj(t2, B) = null IMPLIES proj(t, B) = null END traces $$$traces.prf (|traces| (|prefix_equiv| "" (AUTO-REWRITE "prefix" "append") (("" (SKOLEM!) (("" (GROUND) (("1" (SKOLEM!) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOLEM!) (("3" (INST + "t!1") (("3" (REPLACE*) (("3" (EXPAND "append" 1 1) (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOLEM!) (("4" (INST + "t!1") (("4" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_prefix| "" (SKOLEM!) (("" (REWRITE "prefix_equiv") NIL NIL)) NIL) (|prefix_null| "" (SKOLEM!) (("" (REWRITE "prefix_equiv") (("" (GROUND) NIL NIL)) NIL)) NIL) (|cons_prefix| "" (SKOLEM!) (("" (GROUND) (("1" (REWRITE "prefix_equiv") NIL NIL) ("2" (REWRITE "prefix_equiv" -) NIL NIL) ("3" (REWRITE "prefix_equiv" +) NIL NIL)) NIL)) NIL) (|prefix_append1| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (REPLACE*) (("" (INST + "append(t!1, t3!1)") (("" (REWRITE "append_assoc") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_append2| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (REPLACE*) (("" (INST + "t!2") (("" (REWRITE "append_assoc") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_add1| "" (AUTO-REWRITE "add" "prefix") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|prefix_add2| "" (AUTO-REWRITE "add" "prefix_append1") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|length_prefix| "" (GRIND :DEFS NIL :REWRITES ("prefix" "length_append[T]")) NIL NIL) (|prefix_reflexive| "" (AUTO-REWRITE "append_null" "prefix") (("" (AUTO-REWRITE "append_null[T]" "prefix") (("" (SKOLEM!) (("" (ASSERT) (("" (INST + "null") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_transitive| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (REPLACE*) (("" (INST + "append(t!1, t!2)") (("" (REWRITE "append_assoc") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_antisymmetric| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (AUTO-REWRITE "length_zero[T]" "append_null[T]") (("" (CASE "length(t!1) = 0") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (USE "length_append[T]") (("2" (USE "length_append[T]" ("l1" "t2!1")) (("2" (STOP-REWRITE "length_zero[T]") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|proj_null| "" (GRIND) NIL NIL) (|proj_cons| "" (AUTO-REWRITE "proj" "filter[T]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|proj_append| "" (SKOLEM 1 ("A!1" _ "t!2")) (("" (INDUCT-AND-SIMPLIFY "t1") NIL NIL)) NIL) (|proj_add| "" (AUTO-REWRITE "proj_append" "add") (("" (SKOLEM!) (("" (ASSERT) (("" (AUTO-REWRITE "proj" "filter" "append_null[T]") (("" (LIFT-IF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|proj_prefix| "" (GRIND :EXCLUDE ("append" "proj") :REWRITES ("proj_append")) NIL NIL) (|proj_reverse| "" (INDUCT "t") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP*) (("2" (AUTO-REWRITE "reverse" "proj_append") (("2" (ASSERT) (("2" (AUTO-REWRITE "proj" "filter" "append_null[T]") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_of_proj| "" (SKOLEM + ("A!1" _ _)) (("" (AUTO-REWRITE "proj" "filter" "prefix_null" "null_prefix" "cons_prefix") (("" (INDUCT "t") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (GROUND) (("1" (REWRITE "prefix_equiv") (("1" (GROUND) (("1" (INST + "null") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, t2!1)") (("2" (ASSERT) (("2" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, t2!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_of_proj2| "" (GRIND :DEFS NIL :IF-MATCH NIL :REWRITES ("prefix_of_proj" "proj_prefix")) NIL NIL) (|proj_twice| "" (SKOLEM 1 ("A!1" "B!1" _)) (("" (INDUCT-AND-SIMPLIFY "t") NIL NIL)) NIL) (|prod_TCC1| "" (GRIND) NIL NIL) (|prod_TCC2| "" (GRIND) NIL NIL) (|prod_TCC3| "" (GRIND) NIL NIL) (|prod_commutes| "" (SKOLEM!) (("" (CASE "FORALL t1, t2, t : prod(A!1)(t1, t2, t) IMPLIES prod(A!1)(t2, t1, t)") (("1" (GRIND :IF-MATCH ALL) NIL NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "prod" "proj" "filter") (("2" (INDUCT "t") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE "A!1(cons1_var!1)") (("1" (ASSERT) (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (SPLIT -) (("1" (FLATTEN) (("1" (INST? - :WHERE 3) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (INST? - :WHERE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|proj_prod1| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|proj_prod2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "proj_prod1") NIL NIL)) NIL)) NIL) (|prod_null1| "" (INDUCT-AND-SIMPLIFY "t") (("" (APPLY-EXTENSIONALITY) NIL NIL)) NIL) (|prod_null2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "prod_null1") NIL NIL)) NIL)) NIL) (|prod_null3| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|prod_null4| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (REWRITE "prod_null3") NIL NIL)) NIL)) NIL) (|prefix_prod| "" (SKOLEM + ("A!1" _ _ _ _)) (("" (AUTO-REWRITE "prod" "prefix_null" "null_prefix") (("" (INDUCT "t") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (INST + "null" "null") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE "null?(u!1)") (("1" (DELETE -2 -3) (("1" (INST + "null" "null") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "prefix_equiv") (("2" (ASSERT) (("2" (GROUND) (("1" (INST? -) (("1" (INST? -) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "cons(cons1_var!1, u1!1)" "cons(cons1_var!1, u2!1)") (("1" (ASSERT) (("1" (AUTO-REWRITE "prefix_equiv") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? -) (("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, u1!1)" "u2!1") (("2" (ASSERT) (("2" (REWRITE "prefix_equiv" +) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST? -) (("3" (INST? -) (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST + "u1!1" "cons(cons1_var!1, u2!1)") (("3" (ASSERT) (("3" (REWRITE "prefix_equiv" +) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_assoc1| "" (SKOLEM 1 ("A!1" _ _ _ _ _)) (("" (AUTO-REWRITE "prod") (("" (INDUCT "t") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (REDUCE :IF-MATCH NIL) (("1" (INST?) (("1" (INST?) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "cons(cons1_var!1, u1!1)") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? -) (("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST? -) (("3" (INST? -) (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST + "cons(cons1_var!1, u1!1)") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (INST? -) (("4" (INST? -) (("4" (ASSERT) (("4" (SKOSIMP) (("4" (INST + "cons(cons1_var!1, u1!1)") (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_assoc2| "" (SKOLEM 1 ("A!1" _ _ _ _ _)) (("" (AUTO-REWRITE "prod") (("" (INDUCT "t") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (REDUCE :IF-MATCH NIL) (("1" (INST - "cdr(t1!1)" "cdr(t2!1)" "cdr(t3!1)" "cdr(u!1)") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "cons(cons1_var!1, u1!1)") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "cdr(t1!1)" "t2!1" "t3!1" "u!1") (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, u1!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST - "t1!1" "cdr(t2!1)" "t3!1" "cdr(u!1)") (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST + "cons(cons1_var!1, u1!1)") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (INST - "t1!1" "t2!1" "cdr(t3!1)" "cdr(u!1)") (("4" (ASSERT) (("4" (SKOSIMP) (("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_assoc| "" (REDUCE :IF-MATCH NIL) (("1" (USE "prod_assoc1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "prod_assoc2") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_fullset| "" (AUTO-REWRITE "fullset" "prod") (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (INST?) (("1" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) (("2" (INST?) (("2" (REPLACE*) (("2" (DELETE -) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|free_prod_left| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|free_prod_right| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|sigma_equiv| "" (INDUCT-AND-SIMPLIFY "t") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|sigma_null| "" (GRIND) NIL NIL) (|sigma_cons| "" (GRIND) NIL NIL) (|sigma_empty| "" (GRIND) NIL NIL) (|sigma_append| "" (INDUCT-AND-SIMPLIFY "t1") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|sigma_add| "" (EXPAND "add" 1 1) (("" (SKOLEM!) (("" (REWRITE "sigma_append") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_prefix| "" (AUTO-REWRITE "prefix" "sigma_append") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|sigma_proj| "" (INDUCT-AND-SIMPLIFY "t") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (APPLY-EXTENSIONALITY :HIDE? T) (("3" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|sigma_prod| "" (INDUCT-AND-SIMPLIFY "t") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (IFF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (APPLY-EXTENSIONALITY :HIDE? T) (("3" (IFF) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (REPLACE*) (("4" (APPLY-EXTENSIONALITY :HIDE? T) (("4" (IFF) (("4" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_prod_inter1| "" (SKOSIMP) (("" (FORWARD-CHAIN "proj_prod1") (("" (REWRITE "sigma_proj" :DIR RL) (("" (REWRITE "sigma_proj" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_prod_inter2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "sigma_prod_inter1") NIL NIL)) NIL)) NIL) (|null_proj_equiv| "" (SKOLEM + ("B!1" _)) (("" (INDUCT-AND-SIMPLIFY "t") NIL NIL)) NIL) (|null_proj_subset| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_union| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOLEM!) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_prod| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOSIMP) (("" (ASSERT) (("" (FORWARD-CHAIN "sigma_prod") (("" (REPLACE*) (("" (DELETE -) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_prod1| "" (SKOSIMP) (("" (USE "null_proj_prod") (("" (GROUND) NIL NIL)) NIL)) NIL) (|null_proj_prod2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "null_proj_prod1") NIL NIL)) NIL)) NIL) (|null_proj_prod3| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOSIMP) (("" (ASSERT) (("" (FORWARD-CHAIN "sigma_prod_inter1") (("" (DELETE -2) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) (("" (CASE "intersection(sigma(t!1), A!1)(x!1)") (("1" (REPLACE -2) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_prod4| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "null_proj_prod3") NIL NIL)) NIL)) NIL)) $$$processes.pvs % % Processes with alphabet T % (trace semantics) % processes [ T : TYPE ] : THEORY BEGIN IMPORTING traces S : VAR setof[trace[T]] A : VAR setof[T] t, t1, t2 : VAR trace[T] %=================================================== % process: non-empty, prefix closed set of traces %=================================================== prefix_closed(S) : bool = FORALL t1, t2 : prefix(t1, t2) AND S(t2) IMPLIES S(t1) process : TYPE = { S | S(null) AND prefix_closed(S) } P, P1, P2 : VAR process SP : VAR set[process] a : VAR T %=================== % Process algebra %=================== %----------- % Stop[T] %----------- Stop : process = { t | t = null }; %------------------ % Bounded choice %------------------ \/(P1, P2) : process = union(P1, P2) %--------------------- % Unbounded choice %--------------------- Choice(SP) : process = { t | null?(t) OR EXISTS (P : (SP)) : P(t) }; %----------- % a >> P %----------- >> (a, P) : process = { t | null?(t) OR EXISTS (t1 : (P)) : t = cons(a, t1) } %------------------------ % Parallel composition %------------------------ Par(A)(P1, P2) : process = { t | EXISTS (t1 : (P1)), (t2 : (P2)) : prod(A)(t1, t2, t) }; %---------------- % Interleaving %---------------- //(P1, P2) : process = Par(emptyset)(P1, P2) %========================== % sigma(P) = events of P %========================== sigma(P) : setof[T] = { a | EXISTS (t : (P)) : sigma(t)(a) } END processes $$$processes.prf (|processes| (|Stop_TCC1| "" (GRIND :EXCLUDE ("prefix") :REWRITES ("prefix_null[T]")) NIL NIL) (|vee_TCC1| "" (GRIND :EXCLUDE ("prefix")) NIL NIL) (|Choice_TCC1| "" (GRIND :EXCLUDE "prefix" :IF-MATCH NIL) (("1" (DELETE 2) (("1" (EXPAND "prefix") (("1" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (REDUCE) NIL NIL)) NIL) (|doublegreaterp_TCC1| "" (GRIND :DEFS NIL :REWRITES ("prefix_closed") :IF-MATCH NIL) (("1" (REWRITE "prefix_equiv") NIL NIL) ("2" (REWRITE "prefix_equiv") (("2" (GROUND) (("2" (INST? -) (("2" (ASSERT) (("2" (INST + "cdr(t1!1)") (("2" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Par_TCC1| "" (SKOLEM-TYPEPRED) (("" (PROP) (("1" (EXPAND "prod") (("1" (INST + "null" "null") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (EXPAND "prefix_closed") (("2" (SKOSIMP*) (("2" (FORWARD-CHAIN "prefix_prod") (("2" (SKOSIMP) (("2" (INST? - :WHERE -1) (("2" (INST? - :WHERE -2) (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL))