\$\$\$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 % % Adapted to PVS 2.3 by Paul Y Gloess % on march 20, 2001: % - adaptation of "dual JUDGEMENT" to suit PVS 2.3 syntax; % - renamings (to avoid clashes with "mucalculus" prelude theory): % "monotonic?" -> "bmonotonic?" % "mu" -> "bmu"; % "nu" -> "bnu" % also applied to lemma names (e.g., "closure_mu" -> "closure_bmu"). % % % Defines: % % bmonotonic?(F): bool = (FORALL X, Y: subset?(X, Y) % IMPLIES subset?(F(X), F(Y))) % % bmu(G) : least fixed point of G % bnu(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 set_inf_unions[T] %----- Monotonic functions ---------- bmonotonic?(F) : bool = FORALL X, Y : subset?(X, Y) IMPLIES subset?(F(X), F(Y)) %----- Least fixed point of a monotonic function ----- G : VAR (bmonotonic?) bmu(G) : setof[T] = inter({ X | subset?(G(X), X) }) closure_bmu : LEMMA subset?(G(bmu(G)), bmu(G)) smallest_closed : LEMMA subset?(G(X), X) IMPLIES subset?(bmu(G), X) fixed_point_bmu : LEMMA G(bmu(G)) = bmu(G) least_fixed_point : LEMMA G(X) = X IMPLIES subset?(bmu(G), X) %------ Greatest fixed point of a monotonic function ----- bnu(G) : setof[T] = union({ X | subset?(X, G(X)) }) closure_bnu : LEMMA subset?(bnu(G), G(bnu(G))) largest_closed : LEMMA subset?(X, G(X)) IMPLIES subset?(X, bnu(G)) fixed_point_bnu : LEMMA G(bnu(G)) = bnu(G) greatest_fixed_point : LEMMA G(X) = X IMPLIES subset?(X, bnu(G)) %------ Dual of F ----- dual(F) : [setof[T] -> setof[T]] = complement o F o complement %% PVS 2.3 syntax: JUDGEMENT dual(F: (bmonotonic?)) HAS_TYPE (bmonotonic?) 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 bmu(dual(G)) = complement(bnu(G)) greatest_fixed_point_dual : LEMMA bnu(dual(G)) = complement(bmu(G)) END fixed_points \$\$\$fixed_points.prf (|fixed_points| (|closure_bmu| "" (AUTO-REWRITE "inter_lower_bound" "inter_greatest_lower_bound" "bmu" "bmonotonic?") (("" (REDUCE :IF-MATCH NIL) (("" (INST - "bmu(G!1)" "X!1") (("" (ASSERT) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|smallest_closed| "" (AUTO-REWRITE "bmu" "inter_lower_bound") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|fixed_point_bmu| "" (AUTO-REWRITE "closure_bmu" "bmonotonic?") (("" (SKOLEM-TYPEPRED) (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (EXPAND "bmu" 1 1) (("" (REWRITE "inter_lower_bound") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|least_fixed_point| "" (SKOSIMP) (("" (REWRITE "smallest_closed") (("" (REPLACE*) (("" (REWRITE "subset_reflexive") NIL NIL)) NIL)) NIL)) NIL) (|closure_bnu| "" (AUTO-REWRITE "union_upper_bound" "union_least_upper_bound" "bnu" "bmonotonic?") (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (SKOLEM-TYPEPRED) (("" (INST - "X!1" "bnu(G!1)") (("" (ASSERT) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|largest_closed| "" (AUTO-REWRITE "bnu" "union_upper_bound") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|fixed_point_bnu| "" (SKOLEM-TYPEPRED) (("" (USE "closure_bnu") (("" (CASE "subset?(G!1(bnu(G!1)), bnu(G!1))") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND :EXCLUDE ("bmonotonic?" "bnu")) NIL NIL)) NIL) ("2" (EXPAND "bmonotonic?") (("2" (EXPAND "bnu" 1 2) (("2" (REWRITE "union_upper_bound") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|greatest_fixed_point| "" (SKOSIMP) (("" (REWRITE "largest_closed") (("" (REPLACE*) (("" (REWRITE "subset_reflexive") NIL NIL)) NIL)) NIL)) NIL) (|dual_TCC1| "" (GRIND :IF-MATCH NIL) (("" (INST - "complement(Y!1)" "complement(X!1)") (("" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|dual_dual| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :REWRITES ("complement_complement[T]")) NIL NIL)) NIL)) NIL) (|dual_inclusion1| "" (GRIND) NIL NIL) (|dual_inclusion2| "" (GRIND) NIL NIL) (|least_fixed_point_dual| "" (SKOLEM!) (("" (CASE "subset?(bmu(dual(G!1)), complement(bnu(G!1))) AND subset?(complement(bmu(dual(G!1))), bnu(G!1))") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND :EXCLUDE ("bmu" "bnu" "dual")) NIL NIL)) NIL) ("2" (AUTO-REWRITE "dual_inclusion1" "dual_inclusion2" "dual_dual" "smallest_closed" "largest_closed" "closure_bnu" "closure_bmu") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|greatest_fixed_point_dual| "" (SKOLEM!) (("" (CASE "subset?(complement(bmu(G!1)), bnu(dual(G!1))) AND subset?(bmu(G!1), complement(bnu(dual(G!1))))") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND :EXCLUDE ("bmu" "bnu" "dual")) NIL NIL)) NIL) ("2" (AUTO-REWRITE "dual_inclusion1" "dual_inclusion2" "dual_dual" "smallest_closed" "largest_closed" "closure_bnu" "closure_bmu") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) \$\$\$set_inf_unions.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Arbitrary union and intersections % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% set_inf_unions [ 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 set_inf_unions \$\$\$set_inf_unions.prf (|set_inf_unions| (|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))))))))))