%Patch files loaded: patch2 version 1.2.2.133 \$\$\$fixed_points.pvs fixed_points [ T : TYPE ] : THEORY %------------------------------------------------------------------------ % % Fixed points of monotonic functions F: [set[T] -> set[T]] % % by Bruno Dutertre Queen Mary & Westfield College % edited by Rick Butler NASA Langley % % Version 1.0 last modified 2/6/97 % % Defines: % % monotonic?(F): bool = (FORALL X, Y: subset?(X, Y) % IMPLIES subset?(F(X), F(Y))) % % mu(G) : least fixed point of G % nu(G) : greatest fixed point of G % % dual(F) : [set[T] -> set[T]] = complement o F o complement % %------------------------------------------------------------------------ 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)) %----- Least 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) %------ Greatest 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(F: (monotonic?)) HAS_TYPE (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 NIL) (("1" (INST?) (("1" (ASSERT) (("1" (INST?) NIL))))) ("2" (INST?) (("2" (ASSERT) NIL))))) (|union_empty| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))) (|inter_lower_bound| "" (GRIND) NIL) (|inter_greatest_lower_bound| "" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) (("1" (INST? :IF-MATCH BEST) NIL))))) ("2" (INST? :IF-MATCH BEST) (("2" (ASSERT) 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))))))))))