%Patch files loaded: (patch2) version 2.394 \$\$\$simple_ctl.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % The CTL modal operators % % using inductive definitions % % % % Parameters describe a simple state machine % % The non empty Event type ensures that % % infinite trajectories exist % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% simple_ctl [ State : TYPE, Event : NONEMPTY_TYPE, delta : [State, Event -> State]] : THEORY BEGIN x, y : VAR State a, b : VAR Event n, i, j : VAR nat P, Q, X : VAR pred[State] %----------------------------- % Propositional combinators %----------------------------- or(P, Q)(x) : bool = P(x) or Q(x); and(P, Q)(x) : bool = P(x) and Q(x); not(P)(x) : bool = not P(x); ff(x) : bool = false tt(x) : bool = true not_not : LEMMA (not not P) = P %-------- % Next %-------- EX(P)(x) : bool = EXISTS a : P(delta(x, a)) AX(P)(x) : bool = FORALL a : P(delta(x, a)) %-------------- % Eventually %-------------- EF(P)(x) : INDUCTIVE bool = P(x) OR EXISTS a : EF(P)(delta(x, a)) AF(P)(x) : INDUCTIVE bool = P(x) OR FORALL a : AF(P)(delta(x, a)) %--------- % Until %--------- EU(P, Q)(x) : INDUCTIVE bool = Q(x) OR (P(x) AND EXISTS a : EU(P, Q)(delta(x, a))) AU(P, Q)(x) : INDUCTIVE bool = Q(x) OR (P(x) AND FORALL a : AU(P, Q)(delta(x, a))); %---------- % Always %---------- EG(P)(x) : bool = not AF(not P)(x) AG(P)(x) : bool = not EF(not P)(x) %------------------------ % Tests : fixed points %------------------------ fix_EF : LEMMA EF(P) = ( P or EX(EF(P)) ) fix_AF : LEMMA AF(P) = ( P or AX(AF(P)) ) fix_EU : LEMMA EU(P, Q) = ( Q or P and EX(EU(P, Q)) ) fix_AU : LEMMA AU(P, Q) = ( Q or P and AX(AU(P, Q)) ) fix_EG : LEMMA EG(P) = ( P and EX(EG(P)) ) fix_AG : LEMMA AG(P) = ( P and AX(AG(P)) ) IMPORTING fixed_points[State] least_fix_EF : LEMMA EF(P) = mu! X : P or EX(X) least_fix_AF : LEMMA AF(P) = mu! X : P or AX(X) greatest_fix_EG : LEMMA EG(P) = nu! X : P and EX(X) greatest_fix_AG : LEMMA AG(P) = nu! X : P and AX(X) %---------------------- % Other equivalences %---------------------- eventually_until1 : LEMMA EF(P) = EU(tt, P) eventually_until2 : LEMMA AF(P) = AU(tt, P) %------------------------------------- % Modal operators and trajectories %------------------------------------- IMPORTING trajectories[State, Event, delta] s : VAR Trajectory test1 : LEMMA EF(P)(x) IFF EXISTS (s | s(0) = x) : EXISTS n : P(s(n)) test2 : LEMMA AF(P)(x) IFF FORALL (s | s(0) = x) : EXISTS n : P(s(n)) test3 : LEMMA EG(P)(x) IFF EXISTS (s | s(0) = x) : FORALL n : P(s(n)) test4 : LEMMA AG(P)(x) IFF FORALL (s | s(0) = x) : FORALL n : P(s(n)) END simple_ctl \$\$\$simple_ctl.prf (|simple_ctl| (|not_not| "" (SKOLEM!) (("" (AUTO-REWRITE "not") (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))) (|fix_EF| "" (SKOLEM!) (("" (AUTO-REWRITE "EX" "AX" "OR" "AND" "NOT") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "EF" 1 1) (("" (PROPAX) NIL))))))))) (|fix_AF| "" (SKOLEM!) (("" (AUTO-REWRITE "EX" "AX" "OR" "AND" "NOT") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "AF" 1 1) (("" (PROPAX) NIL))))))))) (|fix_EU| "" (SKOLEM!) (("" (AUTO-REWRITE "EX" "AX" "OR" "AND" "NOT") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "EU" 1 1) (("" (PROPAX) NIL))))))))) (|fix_AU| "" (SKOLEM!) (("" (AUTO-REWRITE "EX" "AX" "OR" "AND" "NOT") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "AU" 1 1) (("" (PROPAX) NIL))))))))) (|fix_EG| "" (SKOLEM!) (("" (AUTO-REWRITE "EG" "EX" "AX" "OR" "AND" "NOT") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "AF" 1 1) (("" (GRIND :DEFS NIL) NIL))))))))) (|fix_AG| "" (SKOLEM!) (("" (AUTO-REWRITE "AG" "EX" "AX" "OR" "AND" "NOT") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "EF" 1 1) (("" (GRIND :DEFS NIL) NIL))))))))) (|least_fix_EF_TCC1| "" (GRIND :IF-MATCH NIL) (("" (INST?) (("" (ASSERT) (("" (INST?) NIL))))))) (|least_fix_EF| "" (SKOLEM!) (("" (AUTO-REWRITE "least_fix_EF_TCC1" "subset?" "member") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (PROP) (("1" (LEMMA "EF_weak_induction") (("1" (INST - "P!1" "lambda P : mu! (X: pred[State]): P or EX(X)") (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (USE "closure_mu") (("2" (EXPAND "OR" -1 1) (("2" (EXPAND "EX" -1 1) (("2" (ASSERT) NIL))))))))))))) ("2" (CASE "subset?(mu! (X: pred[State]): P!1 OR EX(X), EF(P!1))") (("1" (GRIND :DEFS NIL) NIL) ("2" (REWRITE "least_fixed_point") (("2" (USE "fix_EF") (("2" (ASSERT) NIL))))))))))))))))) (|least_fix_AF_TCC1| "" (GRIND) NIL) (|least_fix_AF| "" (SKOLEM!) (("" (AUTO-REWRITE "least_fix_AF_TCC1" "subset?" "member") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (PROP) (("1" (LEMMA "AF_weak_induction") (("1" (INST - "P!1" "lambda P : mu! (X: pred[State]): P or AX(X)") (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (USE "closure_mu") (("2" (EXPAND "OR" -1 1) (("2" (EXPAND "AX" -1 1) (("2" (ASSERT) NIL))))))))))))) ("2" (CASE "subset?(mu! (X: pred[State]): P!1 OR AX(X), AF(P!1))") (("1" (GRIND :DEFS NIL) NIL) ("2" (REWRITE "least_fixed_point") (("2" (USE "fix_AF") (("2" (ASSERT) NIL))))))))))))))))) (|greatest_fix_EG_TCC1| "" (GRIND) NIL) (|greatest_fix_EG| "" (SKOLEM!) (("" (CASE-REPLACE "(lambda (X: pred[State]): P!1 AND EX(X)) = dual(lambda X : not P!1 or AX(X))") (("1" (AUTO-REWRITE "least_fix_AF_TCC1") (("1" (REWRITE "greatest_fixed_point_dual") (("1" (CASE-REPLACE "EG(P!1) = complement(AF(not P!1))") (("1" (REWRITE "least_fix_AF") NIL) ("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND :EXCLUDE ("AF")) NIL))))))))))) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL))))))))))) (|greatest_fix_AG_TCC1| "" (GRIND :IF-MATCH NIL) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL))))))) (|greatest_fix_AG| "" (SKOLEM!) (("" (CASE-REPLACE "(lambda (X: pred[State]): P!1 AND AX(X)) = dual(lambda X : not P!1 or EX(X))") (("1" (AUTO-REWRITE "least_fix_EF_TCC1") (("1" (REWRITE "greatest_fixed_point_dual") (("1" (CASE-REPLACE "AG(P!1) = complement(EF(not P!1))") (("1" (REWRITE "least_fix_EF") NIL) ("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND :EXCLUDE ("EF")) NIL))))))))))) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL))))))))))) (|eventually_until1| "" (SKOLEM!) (("" (AUTO-REWRITE "tt") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (PROP) (("1" (LEMMA "EF_weak_induction") (("1" (INST -1 "P!1" "lambda P : EU(tt, P)") (("1" (GRIND :DEFS NIL) (("1" (EXPAND "EU") (("1" (PROPAX) NIL))) ("2" (EXPAND "EU" +) (("2" (GROUND) (("2" (INST? 2) NIL))))))))))) ("2" (LEMMA "EU_weak_induction") (("2" (INST -1 "tt" "lambda P, Q : EF(Q)" "P!1") (("2" (GRIND :DEFS NIL) (("1" (EXPAND "EF") (("1" (PROPAX) NIL))) ("2" (EXPAND "EF" +) (("2" (GROUND) (("2" (INST?) NIL))))))))))))))))))))) (|eventually_until2| "" (SKOLEM!) (("" (AUTO-REWRITE "tt") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (PROP) (("1" (LEMMA "AF_weak_induction") (("1" (INST -1 "P!1" "lambda P : AU(tt, P)") (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (DELETE -1 2) (("2" (EXPAND "AU" 1 2) (("2" (SKOLEM!) (("2" (GROUND) NIL))))))))))))) ("2" (LEMMA "AU_weak_induction") (("2" (INST -1 "tt" "lambda P, Q : AF(Q)" "P!1") (("2" (GROUND) (("1" (GRIND :DEFS NIL) NIL) ("2" (DELETE -1 2) (("2" (EXPAND "AF" 1 2) (("2" (SKOLEM!) (("2" (GROUND) NIL))))))))))))))))))))))) (|test1| "" (AUTO-REWRITE "cons" "traj" "tail" "seq") (("" (APPLY (THEN (SKOLEM!) (PROP))) (("1" (LEMMA "EF_weak_induction") (("1" (INST - "P!1" "lambda P : lambda x : EXISTS (s | s(0) = x ) :EXISTS n : P(s(n))") (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (DELETE -1 2) (("2" (APPLY (THEN (SKOLEM!) (PROP))) (("1" (INST + "traj(x!2)") (("1" (INST + "0") (("1" (ASSERT) NIL))))) ("2" (SKOSIMP*) (("2" (INST + "cons(x!2, a!1, s!1)") (("2" (INST + "n!1+1") (("2" (ASSERT) NIL))))))))))))))))) ("2" (CASE "FORALL n, x : (EXISTS (s | s(0) = x) : P!1(s(n))) IMPLIES EF(P!1)(x)") (("1" (SKOSIMP*) (("1" (INST - "n!1" "x!1") (("1" (ASSERT) (("1" (INST?) NIL))))))) ("2" (DELETE -1 2) (("2" (INDUCT "n") (("1" (SKOSIMP*) (("1" (EXPAND "EF") (("1" (ASSERT) NIL))))) ("2" (SKOSIMP* :PREDS? T) (("2" (EXPAND "EF" +) (("2" (GROUND) (("2" (INST - "0") (("2" (SKOLEM!) (("2" (INST? +) (("2" (INST?) (("2" (ASSERT) (("2" (INST + "tail(s!1)") (("2" (ASSERT) NIL))))))))))))))))))))))))))))) (|test2| "" (SKOLEM!) (("" (PROP) (("1" (LEMMA "AF_weak_induction") (("1" (INST - "P!1" "lambda P : lambda x : FORALL (s | s(0) = x) : EXISTS n : P(s(n))") (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (DELETE -1 2) (("2" (SKOSIMP*) (("2" (GROUND) (("1" (INST + "0") (("1" (ASSERT) NIL))) ("2" (AUTO-REWRITE "tail") (("2" (TYPEPRED "s!1") (("2" (INST - "0") (("2" (SKOLEM!) (("2" (INST - "a!1") (("2" (INST - "tail(s!1)") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST?) NIL))))) ("2" (ASSERT) NIL))))))))))))))))))))))))) ("2" (LEMMA "tree_induction2") (("2" (INST - "lambda (z : wf) : (FORALL (s | s(0) = root(z)) : P!1(s(mark(z)(s)))) IMPLIES AF(P!1)(root(z))") (("2" (GROUND) (("1" (INST - "(# root:=x!1, mark := lambda (s | s(0) = x!1) : epsilon! n : P!1(s(n)) #)") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST?) (("1" (LEMMA "epsilon_ax" ("p" "lambda n : P!1(s!1(n))")) (("1" (ASSERT) NIL))))))))))) ("2" (DELETE -1 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST? -3) (("2" (EXPAND "AF") (("2" (ASSERT) NIL))))))))) ("3" (DELETE -1 2) (("3" (GRIND :IF-MATCH NIL) (("3" (EXPAND "AF" +) (("3" (REDUCE) NIL))))))))))))))))) (|test3| "" (AUTO-REWRITE "EG" "test2" "not") (("" (SKOLEM!) (("" (APPLY (THEN (GROUND) (REPEAT* (THEN (SKOLEM!) (INST?))))) NIL))))) (|test4| "" (SKOLEM!) (("" (GRIND :EXCLUDE ("EF") :REWRITES ("test1")) NIL)))) \$\$\$fixed_points.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Fixed points of functions F : [setof[T] -> setof[T]] % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% fixed_points [ T : TYPE ] : THEORY BEGIN X, Y, Z : VAR setof[T] F : VAR [setof[T] -> setof[T]] A, B, C : VAR setof[setof[T]] IMPORTING sets_bounds[T] %------------------------- % Monotonic functions %------------------------- monotonic?(F) : bool = FORALL X, Y : subset?(X, Y) IMPLIES subset?(F(X), F(Y)) %------------------------------------------------ % Smallest fixed point of a monotonic function %------------------------------------------------ G : VAR (monotonic?) mu(G) : setof[T] = inter({ X | subset?(G(X), X) }) closure_mu : LEMMA subset?(G(mu(G)), mu(G)) smallest_closed : LEMMA subset?(G(X), X) IMPLIES subset?(mu(G), X) fixed_point_mu : LEMMA G(mu(G)) = mu(G) least_fixed_point : LEMMA G(X) = X IMPLIES subset?(mu(G), X) %------------------------------------------------- % Largest fixed point of a monotonic function %------------------------------------------------- nu(G) : setof[T] = union({ X | subset?(X, G(X)) }) closure_nu : LEMMA subset?(nu(G), G(nu(G))) largest_closed : LEMMA subset?(X, G(X)) IMPLIES subset?(X, nu(G)) fixed_point_nu : LEMMA G(nu(G)) = nu(G) greatest_fixed_point : LEMMA G(X) = X IMPLIES subset?(X, nu(G)) %------------- % Dual of F %------------- dual(F) : [setof[T] -> setof[T]] = complement o F o complement JUDGEMENT dual HAS_TYPE [ (monotonic?) -> (monotonic?) ] dual_dual : LEMMA dual(dual(F)) = F dual_inclusion1 : LEMMA subset?(F(complement(X)), complement(X)) IFF subset?(X, dual(F)(X)) dual_inclusion2 : LEMMA subset?(complement(X), F(complement(X))) IFF subset?(dual(F)(X), X) least_fixed_point_dual : LEMMA mu(dual(G)) = complement(nu(G)) greatest_fixed_point_dual : LEMMA nu(dual(G)) = complement(mu(G)) END fixed_points \$\$\$fixed_points.prf (|fixed_points| (|closure_mu| "" (AUTO-REWRITE "inter_lower_bound" "inter_greatest_lower_bound" "mu" "monotonic?") (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (SKOLEM-TYPEPRED) (("" (INST - "mu(G!1)" "X!1") (("" (ASSERT) (("" (GRIND) NIL))))))))))))) (|smallest_closed| "" (AUTO-REWRITE "mu" "inter_lower_bound") (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|fixed_point_mu| "" (SKOLEM!) (("" (USE "closure_mu") (("" (CASE "subset?(mu(G!1), G!1(mu(G!1)))") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND :EXCLUDE "mu") NIL))) ("2" (DELETE 2) (("2" (TYPEPRED "G!1") (("2" (EXPAND "monotonic?") (("2" (EXPAND "mu" 1 1) (("2" (REWRITE "inter_lower_bound") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))) (|least_fixed_point| "" (SKOSIMP) (("" (REWRITE "smallest_closed") (("" (REPLACE*) (("" (REWRITE "subset_reflexive") NIL))))))) (|closure_nu| "" (AUTO-REWRITE "union_upper_bound" "union_least_upper_bound" "nu" "monotonic?") (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (SKOLEM-TYPEPRED) (("" (INST - "X!1" "nu(G!1)") (("" (ASSERT) (("" (GRIND) NIL))))))))))))) (|largest_closed| "" (AUTO-REWRITE "nu" "union_upper_bound") (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|fixed_point_nu| "" (SKOLEM-TYPEPRED) (("" (USE "closure_nu") (("" (CASE "subset?(G!1(nu(G!1)), nu(G!1))") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND :EXCLUDE ("monotonic?" "nu")) NIL))) ("2" (EXPAND "monotonic?") (("2" (EXPAND "nu" 1 2) (("2" (REWRITE "union_upper_bound") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))) (|greatest_fixed_point| "" (SKOSIMP) (("" (REWRITE "largest_closed") (("" (REPLACE*) (("" (REWRITE "subset_reflexive") NIL))))))) (|dual_TCC1| "" (GRIND :IF-MATCH NIL) (("" (INST - "complement(Y!1)" "complement(X!1)") (("" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL))))))))))) (|dual_dual| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :REWRITES ("complement_complement[T]")) NIL))))) (|dual_inclusion1| "" (GRIND) NIL) (|dual_inclusion2| "" (GRIND) NIL) (|least_fixed_point_dual| "" (SKOLEM!) (("" (CASE "subset?(mu(dual(G!1)), complement(nu(G!1))) AND subset?(complement(mu(dual(G!1))), nu(G!1))") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND :EXCLUDE ("mu" "nu" "dual")) NIL))) ("2" (AUTO-REWRITE "dual_inclusion1" "dual_inclusion2" "dual_dual" "smallest_closed" "largest_closed" "closure_nu" "closure_mu") (("2" (GROUND) NIL))))))) (|greatest_fixed_point_dual| "" (SKOLEM!) (("" (CASE "subset?(complement(mu(G!1)), nu(dual(G!1))) AND subset?(mu(G!1), complement(nu(dual(G!1))))") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND :EXCLUDE ("mu" "nu" "dual")) NIL))) ("2" (AUTO-REWRITE "dual_inclusion1" "dual_inclusion2" "dual_dual" "smallest_closed" "largest_closed" "closure_nu" "closure_mu") (("2" (GROUND) NIL)))))))) \$\$\$sets_bounds.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Arbitrary union and intersections % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% sets_bounds [ T : TYPE ] : THEORY BEGIN A, B : VAR setof[setof[T]] X, Y, Z : VAR setof[T] x : VAR T %------------------ % Infinite union %------------------ union(A) : setof[T] = { x | EXISTS (X : (A)) : X(x) } union_upper_bound : LEMMA FORALL (X : (A)) : subset?(X, union(A)) union_least_upper_bound : LEMMA subset?(union(A), Y) IFF FORALL (X : (A)) : subset?(X, Y) union_empty : LEMMA union(emptyset[setof[T]]) = emptyset %---------------- % Intersection %---------------- inter(A) : setof[T] = { x | FORALL (X : (A)) : X(x) } inter_lower_bound : LEMMA FORALL (X : (A)) : subset?(inter(A), X) inter_greatest_lower_bound : LEMMA subset?(Y, inter(A)) IFF FORALL (X : (A)) : subset?(Y, X) inter_empty : LEMMA inter(emptyset[setof[T]]) = fullset %----------------- % pairs of sets %----------------- pair(X, Y) : (nonempty?[setof[T]]) = { Z | Z = X or Z = Y } union_pair : LEMMA union(pair(X, Y)) = union(X, Y) inter_pair : LEMMA inter(pair(X, Y)) = intersection(X, Y) %----------- % Duality %----------- inter_complement : LEMMA inter(image(complement, A)) = complement(union(A)) union_complement : LEMMA union(image(complement, A)) = complement(inter(A)) END sets_bounds \$\$\$sets_bounds.prf (|sets_bounds| (|union_upper_bound| "" (GRIND) NIL) (|union_least_upper_bound| "" (GRIND :IF-MATCH BEST) NIL) (|union_empty| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))) (|inter_lower_bound| "" (GRIND) NIL) (|inter_greatest_lower_bound| "" (GRIND :IF-MATCH BEST) NIL) (|inter_empty| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))) (|pair_TCC1| "" (GRIND) NIL) (|union_pair| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))))) (|inter_pair| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))))) (|inter_complement| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :IF-MATCH NIL) (("1" (INST - "complement(X!1)") (("1" (ASSERT) NIL) ("2" (INST?) NIL))) ("2" (INST?) NIL))))))) (|union_complement| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :IF-MATCH NIL) (("1" (INST?) NIL) ("2" (INST + "complement(X!1)") (("1" (ASSERT) NIL) ("2" (INST?) NIL)))))))))) \$\$\$trajectories.pvs trajectories [ State : TYPE, Event : NONEMPTY_TYPE, delta : [State, Event -> State]] : THEORY BEGIN x : VAR State a : VAR Event n, m, i : VAR nat alpha : Event %----------------------------------------------- % Trajectories: infinite sequences of states %----------------------------------------------- u : VAR sequence[State] Trajectory : TYPE = { u | FORALL n : EXISTS a : u(n + 1) = delta(u(n), a) } s : VAR Trajectory %--- Operations on trajectories ---% seq(x, a)(n) : RECURSIVE State = IF n = 0 THEN x ELSE delta(seq(x, a)(n-1), a) ENDIF MEASURE n traj(x) : Trajectory = seq(x, alpha) tail(s) : Trajectory = LAMBDA n : s(n+1) cons(x, a, (s | s(0) = delta(x, a))) : Trajectory = LAMBDA n : IF n = 0 THEN x ELSE s(n-1) ENDIF suffix(s, n) : Trajectory = LAMBDA i : s(i+n) suffix_suffix : LEMMA suffix(suffix(s, n), m) = suffix(s, n + m) tail_suffix : LEMMA tail(s) = suffix(s, 1) full_suffix : LEMMA suffix(s, 0) = s %------------------------------------------------- % Structure for well founded induction on trees: % - a node x (root of a tree) % - a function gives a finite prefix for all % the trajectories of origin x %------------------------------------------------- wf : TYPE = [# root : State, mark : [ {s | s(0) = root} -> nat ] #] t1, t2 : VAR wf IMPORTING wf_props %--- well founded relation on these structures ---% <(t1, t2) : bool = (EXISTS a : root(t1) = delta(root(t2), a)) AND (FORALL (s | s(0) = root(t2) AND s(1) = root(t1)) : mark(t1)(tail(s)) < mark(t2)(s)) wf_relation : LEMMA well_founded?[wf](<) %--- shift wf to one successor of root(wf) ---% shiftable(t1) : bool = FORALL (s | s(0) = root(t1)) : mark(t1)(s) > 0 t : VAR (shiftable) shift(t, a) : wf = (# root := delta(root(t), a), mark := lambda (s | s(0) = delta(root(t), a)) : mark(t)(cons(root(t), a, s)) - 1 #) shift_wf : LEMMA shift(t, a) < t %--- induction rules ---% P : VAR pred[wf] tree_induction1 : LEMMA (FORALL t1 : (FORALL t2 : t2 < t1 IMPLIES P(t2)) IMPLIES P(t1)) IMPLIES (FORALL t1 : P(t1)) tree_induction2 : LEMMA (FORALL (t1 | not shiftable(t1)) : P(t1)) AND (FORALL t : (FORALL a : P(shift(t, a))) IMPLIES P(t)) IMPLIES (FORALL t1 : P(t1)) END trajectories \$\$\$trajectories.prf (|trajectories| (|seq_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|seq_TCC2| "" (APPLY (THEN (SKOSIMP) (ASSERT))) NIL) (|traj_TCC1| "" (GRIND) NIL) (|tail_TCC1| "" (GRIND) NIL) (|cons_TCC1| "" (APPLY (THEN (SKOSIMP) (ASSERT))) NIL) (|cons_TCC2| "" (GRIND :IF-MATCH NIL) (("1" (INST? +) NIL) ("2" (INST?) (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL))))))))) (|suffix_TCC1| "" (GRIND) NIL) (|suffix_suffix| "" (APPLY (THEN (SKOLEM!) (APPLY-EXTENSIONALITY) (GRIND))) NIL) (|tail_suffix| "" (AUTO-REWRITE "tail" "suffix") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))) (|full_suffix| "" (SKOLEM!) (("" (EXPAND "suffix") (("" (APPLY-ETA "s!1") NIL))))) (|lessp_TCC1| "" (GRIND :DEFS NIL :REWRITES ("tail")) NIL) (|lessp_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|wf_relation| "" (AUTO-REWRITE "suffix_suffix" "tail_suffix" "full_suffix") (("" (LEMMA "wf_nat") (("" (REWRITE "well_founded_equiv") (("" (REWRITE "well_founded_equiv") (("" (SKOLEM!) (("" (CASE "EXISTS s : FORALL i : s(i) = root(u!1(i))") (("1" (SKOLEM!) (("1" (INST + "lambda i : mark(u!1(i))(suffix(s!1, i))") (("1" (GRIND :EXCLUDE ("suffix") :IF-MATCH NIL) (("1" (INST? -3) (("1" (FLATTEN) (("1" (INST? -4) (("1" (ASSERT) NIL) ("2" (DELETE -3 2) (("2" (GRIND) NIL))))))))))) ("2" (DELETE -2) (("2" (GRIND) NIL))))))) ("2" (DELETE 2) (("2" (INST + "lambda i : root(u!1(i))") (("1" (ASSERT) NIL) ("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (FLATTEN) (("2" (PROPAX) NIL))))))))))))))))))))))) (|shift_TCC1| "" (GRIND) NIL) (|shift_TCC2| "" (GRIND) NIL) (|shift_wf| "" (GRIND) (("" (CASE-REPLACE "cons(root(t!1), a!1, tail(s!1)) = s!1") (("1" (ASSERT) NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL))))))))) (|tree_induction1| "" (AUTO-REWRITE "wf_relation") (("" (LEMMA "wf_induction[wf, <]") (("" (PROPAX) NIL))))) (|tree_induction2| "" (SKOSIMP) (("" (LEMMA "wf_induction[wf, lambda t1, t2 : shiftable(t2) AND (EXISTS a : t1 = shift(t2, a))]") (("1" (INST?) (("1" (GROUND) (("1" (DELETE 2) (("1" (SKOSIMP*) (("1" (INST? -2) (("1" (INST -3 "x!1") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST? :WHERE 2) (("1" (ASSERT) (("1" (INST?) NIL))))))))))))))))))))) ("2" (DELETE -1 -2 2) (("2" (LEMMA "wf_relation") (("2" (USE "well_founded_subrelation" ("R1" "LAMBDA t1, t2: shiftable(t2) AND (EXISTS a: t1 = shift(t2, a))")) (("2" (GROUND) (("2" (EXPAND "subrel?") (("2" (SKOSIMP*) (("2" (REPLACE*) (("2" (REWRITE "shift_wf") NIL)))))))))))))))))))) \$\$\$wf_props.pvs wf_props [ T : TYPE ] : THEORY BEGIN < : VAR pred[[T, T]] u : VAR sequence[T] i, n : VAR nat %--------------------------------------------------------------- % Necessary and sufficient condition for < to be well founded %--------------------------------------------------------------- E : VAR (nonempty?[T]) seq(<, E)(n) : RECURSIVE (E) = IF n=0 THEN epsilon! (x : (E)) : true ELSE epsilon! (x : (E)) : x < seq(<, E)(n - 1) ENDIF MEASURE n well_founded_equiv : THEOREM well_founded?(<) IFF not (EXISTS u : FORALL i : u(i+1) < u(i)) %---------------------------------------------------------- % Subrelation of a well founded relation is well founded %---------------------------------------------------------- R1, R2 : VAR pred[[T, T]] x, y : VAR T %--- subrel? easier to use than subset? ---% subrel?(R1, R2) : bool = FORALL x, y : R1(x, y) IMPLIES R2(x, y) well_founded_subrelation : THEOREM well_founded?(R2) and subrel?(R1, R2) IMPLIES well_founded?(R1) END wf_props \$\$\$wf_props.prf (|wf_props| (|seq_TCC1| "" (GRIND) (("" (INST + "x!1") NIL))) (|seq_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|seq_TCC3| "" (ASSERT) NIL) (|well_founded_equiv| "" (GRIND :IF-MATCH NIL) (("1" (INST - "lambda (x : T) : EXISTS i : u!1(i) = x") (("1" (GROUND) (("1" (SKOSIMP* :PREDS? T) (("1" (INST - "u!1(i!1 + 1)") (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (INST + "1+i!1") NIL))))) ("2" (INST + "u!1(0)") (("2" (INST?) NIL))))))) ("2" (CASE "nonempty?(p!1)") (("1" (ASSERT) (("1" (DELETE -) (("1" (INST 2 "seq(lessp!1, p!1)") (("1" (GRIND :IF-MATCH NIL) (("1" (NAME-REPLACE "zz" "seq(lessp!1, p!1)(i!1)") (("1" (INST + "zz") (("1" (SKOLEM!) (("1" (LEMMA "epsilon_ax" ("p" "lambda (x : (p!1)) : lessp!1(x, zz)")) (("1" (ASSERT) (("1" (INST?) NIL))) ("2" (INST + "y!1") NIL))))))))))))))))) ("2" (DELETE 2 3) (("2" (GRIND) NIL))))))) (|well_founded_subrelation| "" (GRIND :IF-MATCH NIL) (("" (INST?) (("" (PROP) (("1" (SKOLEM!) (("1" (INST? +) (("1" (SKOLEM!) (("1" (INST - "x!1") (("1" (INST?) (("1" (ASSERT) NIL))))))))))) ("2" (INST?) NIL))))))))