%Patch files loaded: patch2 version 2.417 % patch2-test version 1.789 $$$zorn.pvs zorn [ T: TYPE, <=:(partial_order?[T]) ] : THEORY BEGIN IMPORTING well_ordering_principle[T] x, y, z: VAR T A, B: VAR set[T] P: VAR [T -> bool] %----------------------- % well ordering on T %----------------------- <<: (well_order?[T]) well_founded_relation: LEMMA well_founded?[T](<<) induction: LEMMA (FORALL x: (FORALL y: y << x IMPLIES P(y)) IMPLIES P(x)) IMPLIES (FORALL x: P(x)) total_order: LEMMA x << y OR x = y OR y << x %-------------------- % properties of <= %-------------------- reflexivity: LEMMA x <= x transitivity: LEMMA x <= y AND y <= z IMPLIES x <= z antisymmetry: LEMMA x <= y AND y <= x IMPLIES x = y %------------------------------------- % Chains: totally orderd sets by <= %------------------------------------- chain?(A): bool = FORALL (y, z: (A)): y <= z OR z <= y bounded?(A): bool = EXISTS x : FORALL (y: (A)): y <= x %---------------------- % C: a maximal chain %---------------------- C(x): RECURSIVE bool = FORALL (y | y << x): C(y) IMPLIES y <= x MEASURE x BY << C_is_chain: LEMMA chain?(C) %------------------------ % Maximality principle %------------------------ maximality: PROPOSITION (FORALL A: chain?(A) IMPLIES bounded?(A)) IMPLIES EXISTS x : FORALL y : x <= y IMPLIES x = y END zorn $$$zorn.prf (|zorn| (|doublelessp_TCC1| "" (LEMMA "well_order_exists") (("" (SKOLEM!) (("" (INST + "R!1") NIL))))) (|well_founded_relation| "" (TYPEPRED "zorn.<<") (("" (EXPAND "well_order?") (("" (GROUND) NIL))))) (|induction| "" (AUTO-REWRITE "well_founded_relation") (("" (LEMMA "wf_induction[T, <<]") (("" (PROPAX) NIL))))) (|total_order| "" (TYPEPRED "zorn.<<") (("" (EXPAND* "well_order?" "trichotomous?") (("" (GROUND) (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL))))))))))) (|reflexivity| "" (TYPEPRED "zorn.<=") (("" (EXPAND* "partial_order?" "preorder?" "reflexive?") (("" (GROUND) NIL))))) (|transitivity| "" (TYPEPRED "zorn.<=") (("" (EXPAND* "partial_order?" "preorder?" "transitive?") (("" (GROUND) NIL))))) (|antisymmetry| "" (TYPEPRED "zorn.<=") (("" (EXPAND* "partial_order?" "antisymmetric?") (("" (GROUND) NIL))))) (C_TCC1 "" (REPLACE-ETA "zorn.<<") (("" (REWRITE "well_founded_relation") NIL))) (C_TCC2 "" (SKOLEM!) (("" (ASSERT) NIL))) (|C_is_chain| "" (EXPAND "chain?") (("" (SKOSIMP :PREDS? T) (("" (AUTO-REWRITE "reflexivity") (("" (LEMMA "total_order" ("x" "y!1" "y" "z!1")) (("" (GROUND) (("1" (EXPAND "C" -3) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (REPLACE*) (("2" (ASSERT) NIL))) ("3" (EXPAND "C" -2) (("3" (INST?) (("3" (ASSERT) NIL))))))))))))))) (|maximality| "" (AUTO-REWRITE "C_is_chain" "bounded?" "antisymmetry") (("" (SKOSIMP) (("" (INST - "C") (("" (ASSERT) (("" (SKOLEM!) (("" (INST? +) (("" (SKOSIMP) (("" (CASE "C(y!1)") (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (EXPAND "C") (("2" (SKOSIMP) (("2" (INST?) (("2" (FORWARD-CHAIN "transitivity") NIL)))))))))))))))))))))))) $$$well_ordering.pvs well_ordering [ T : TYPE ] : THEORY BEGIN R : VAR [T, T -> bool] x, y, z : VAR T %------------------------------- % Definition of well ordering %------------------------------- well_order?(R) : bool = well_founded?(R) AND trichotomous?(R); %------------------------------------------ % a well ordering is a strict total order %------------------------------------------ S : VAR (well_order?) wo_transitive : LEMMA S(x, y) AND S(y, z) IMPLIES S(x, z) wo_irreflexive : LEMMA NOT S(x, x) wo_strict_total_order : LEMMA strict_total_order?(S) END well_ordering $$$well_ordering.prf (|well_ordering| (|wo_transitive| "" (SKOSIMP :PREDS? T) (("" (EXPAND* "well_order?" "trichotomous?[T]" "well_founded?[T]") (("" (FLATTEN) (("" (INST - "{x | x=x!1 OR x=y!1 OR x=z!1}") (("" (REDUCE :IF-MATCH ALL) NIL))))))))) (|wo_irreflexive| "" (SKOSIMP :PREDS? T) (("" (AUTO-REWRITE "well_order?" "trichotomous?[T]" "well_founded?[T]") (("" (ASSERT) (("" (FLATTEN) (("" (DELETE -2) (("" (INST - "{x | x=x!1}") (("" (REDUCE :IF-MATCH ALL) NIL))))))))))))) (|wo_strict_total_order| "" (SKOLEM-TYPEPRED) (("" (AUTO-REWRITE-THEORIES "orders[T]" "relations[T]") (("" (ASSERT) (("" (PROP) (("1" (USE "wo_irreflexive" ("S" "S!1")) NIL) ("2" (USE "wo_transitive" ("S" "S!1")) NIL) ("3" (EXPAND "well_order?") (("3" (GROUND) NIL)))))))))))) $$$set_bounds.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Arbitrary unions and intersections % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% set_bounds [ T : TYPE ] : THEORY BEGIN A, B : VAR set[set[T]] X, Y, Z : VAR set[T] x : VAR T %------------------ % Infinite union %------------------ union(A) : set[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) subset_union : LEMMA (EXISTS (X:(A)): subset?(Y, X)) IMPLIES subset?(Y, union(A)) union_empty : LEMMA union(emptyset[set[T]]) = emptyset %---------------- % Intersection %---------------- inter(A) : set[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) subset_inter : LEMMA (EXISTS (X : (A)): subset?(X, Y)) IMPLIES subset?(inter(A), Y) inter_empty : LEMMA inter(emptyset[set[T]]) = fullset %----------------- % pairs of sets %----------------- pair(X, Y) : (nonempty?[set[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_bounds $$$set_bounds.prf (|set_bounds| (|union_upper_bound| "" (GRIND) NIL) (|union_least_upper_bound| "" (GRIND :IF-MATCH NIL) (("1" (REDUCE) NIL) ("2" (REDUCE) NIL))) (|subset_union| "" (GRIND) NIL) (|union_empty| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))) (|inter_lower_bound| "" (GRIND) NIL) (|inter_greatest_lower_bound| "" (GRIND :IF-MATCH NIL) (("1" (REDUCE :IF-MATCH BEST) NIL) ("2" (REDUCE :IF-MATCH BEST) NIL))) (|subset_inter| "" (GRIND) 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)))))))))) $$$well_ordering_principle.pvs well_ordering_principle [T : TYPE] : THEORY BEGIN IMPORTING set_bounds, well_ordering A, B : VAR set[T] C : VAR (nonempty?[T]) M, N : VAR set[set[T]] x, y, z : VAR T %----------------- % Non full sets %----------------- nonfull?(A) : bool = EXISTS x : not A(x) E, E1, E2 : VAR (nonfull?) %----------------------------------- % Variant of the choice function %----------------------------------- phi(E) : { x | not E(x) } succ(E) : (nonempty?[T]) = add(phi(E), E) subset_succ1: LEMMA subset?(E, succ(E)) subset_succ2: LEMMA subset?(A, E) IMPLIES subset?(A, succ(E)) subset_succ3: LEMMA subset?(E, A) AND subset?(A, succ(E)) IMPLIES A = E OR A = succ(E) %---------- % Chains %---------- Chain(M): bool = M(emptyset) AND (FORALL E : M(E) IMPLIES M(succ(E))) AND (FORALL N : subset?(N, M) IMPLIES M(union(N))) %-------------------------- % ZM: the smallest chain %-------------------------- ZM : set[set[T]] = inter(Chain) ZM_smallest : LEMMA Chain(M) IMPLIES subset?(ZM, M) emptyset_in_ZM : LEMMA ZM(emptyset) succ_in_ZM : LEMMA ZM(E) IMPLIES ZM(succ(E)) union_in_ZM : LEMMA subset?(M, ZM) IMPLIES ZM(union(M)) ZM_is_chain : LEMMA Chain(ZM) X, Y, Z : VAR (ZM) %--------------- % Main lemmas %--------------- H : set[set[T]] = { A | FORALL X: subset?(X, A) or subset?(A, X) } H_emptyset : LEMMA H(emptyset) H_succ : LEMMA H(E) IMPLIES H(succ(E)) H_union : LEMMA subset?(M, H) IMPLIES H(union(M)) H_is_chain: PROPOSITION Chain(H) %-------------------------------------------------------------- % Consequence: ZM is totally ordered by the subset? relation %-------------------------------------------------------------- linear_order_on_ZM : PROPOSITION subset?(X, Y) OR subset?(Y, X) strict_order_on_ZM : PROPOSITION strict_subset?(X, Y) OR X=Y OR strict_subset?(Y, X) strict_subset_succ : LEMMA strict_subset?(X, Y) IMPLIES nonfull?(X) AND Y(phi(X)) %----------------- % Ordering on T %----------------- K(x): { E | ZM(E) } = union({ B | ZM(B) AND not B(x) }) K(C): { E | ZM(E) } = union({ B | ZM(B) AND disjoint?(C, B) }) phi_K1: LEMMA phi(K(x)) = x phi_K2: LEMMA C(phi(K(C))) phi_K3: LEMMA K(phi(K(C))) = K(C); <(x, y): bool = strict_subset?(K(x), K(y)) trichotomous: LEMMA trichotomous?(<) well_founded: LEMMA well_founded?(<) %--------------- % Main result %--------------- R : VAR [T, T -> bool] well_order_exists : THEOREM EXISTS R : well_order?(R) END well_ordering_principle $$$well_ordering_principle.prf (|well_ordering_principle| (|phi_TCC1| "" (INST + "lambda E : epsilon! (x: T | NOT E(x)) : true") (("" (GRIND) NIL))) (|succ_TCC1| "" (GRIND) NIL) (|subset_succ1| "" (GRIND :EXCLUDE "nonfull?") NIL) (|subset_succ2| "" (SKOSIMP) (("" (AUTO-REWRITE "subset_succ1") (("" (USE "subset_transitive" ("c" "succ(E!1)")) (("" (ASSERT) NIL))))))) (|subset_succ3| "" (GRIND :EXCLUDE "nonfull?" :IF-MATCH NIL) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("" (IFF) (("" (REDUCE :IF-MATCH ALL) NIL))))))))) (|ZM_smallest| "" (EXPAND "ZM") (("" (SKOSIMP) (("" (REWRITE "inter_lower_bound") NIL))))) (|emptyset_in_ZM| "" (GRIND :EXCLUDE ("succ" "union")) NIL) (|succ_in_ZM| "" (GRIND :EXCLUDE ("nonfull?" "succ" "union")) NIL) (|union_in_ZM| "" (SKOSIMP) (("" (EXPAND "ZM" +) (("" (EXPAND "inter") (("" (SKOLEM-TYPEPRED) (("" (FORWARD-CHAIN "ZM_smallest") (("" (EXPAND "Chain") (("" (PROP) (("" (INST? -4) (("" (ASSERT) (("" (USE "subset_transitive" ("a" "M!1")) (("" (ASSERT) NIL))))))))))))))))))))) (|ZM_is_chain| "" (GRIND :DEFS NIL :REWRITES ("Chain" "emptyset_in_ZM" "succ_in_ZM" "union_in_ZM")) NIL) (|H_emptyset| "" (GRIND) NIL) (|H_succ| "" (SKOSIMP) (("" (CASE "Chain({ B | ZM(B) and (subset?(B, E!1) or subset?(succ(E!1), B)) })") (("1" (FORWARD-CHAIN "ZM_smallest") (("1" (DELETE -2 -3) (("1" (GRIND :DEFS NIL :REWRITES ("H" "subset?[set[T]]" "member[set[T]]" "subset_succ1" "subset_succ2") :IF-MATCH NIL) (("1" (INST?) (("1" (GROUND) NIL))))))))) ("2" (DELETE 2) (("2" (EXPAND "Chain") (("2" (AUTO-REWRITE "H" "emptyset_in_ZM" "succ_in_ZM" "subset_emptyset[T]" "subset_reflexive[T]" "subset_succ1" "subset_succ2" "subset?[set[T]]" "member[set[T]]") (("2" (GROUND) (("1" (SKOSIMP) (("1" (ASSERT) (("1" (INST - "succ(E!2)") (("1" (GROUND) (("1" (FORWARD-CHAIN "subset_succ3") (("1" (REPLACE*) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL))))))))))) ("2" (SKOSIMP) (("2" (GROUND) (("1" (REWRITE "union_in_ZM") (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL))))))) ("2" (REWRITE "subset_union") (("2" (REWRITE "union_least_upper_bound") (("2" (SKOLEM!) (("2" (INST? -) (("2" (GROUND) (("2" (INST?) NIL))))))))))))))))))))))))))) (|H_union| "" (AUTO-REWRITE "H" "subset?[set[T]]" "member[set[T]]") (("" (REDUCE :IF-MATCH NIL) (("" (REWRITE "subset_union") (("" (REWRITE "union_least_upper_bound") (("" (SKOLEM!) (("" (INST - "X!2") (("" (ASSERT) (("" (INST? -) (("" (ASSERT) (("" (INST?) NIL))))))))))))))))))) (|H_is_chain| "" (AUTO-REWRITE "H_emptyset" "H_succ" "H_union" "Chain") (("" (REDUCE :IF-MATCH NIL) NIL))) (|linear_order_on_ZM| "" (SKOSIMP) (("" (USE "H_is_chain") (("" (FORWARD-CHAIN "ZM_smallest") (("" (GRIND :DEFS NIL :REWRITES ("member[set[T]]" "subset?[set[T]]" "H")) NIL))))))) (|strict_order_on_ZM| "" (SKOSIMP) (("" (EXPAND "strict_subset?") (("" (GROUND) (("" (USE "linear_order_on_ZM") (("" (ASSERT) NIL))))))))) (|strict_subset_succ| "" (SKOSIMP) (("" (CASE "nonfull?(X!1)") (("1" (ASSERT) (("1" (AUTO-REWRITE "succ_in_ZM") (("1" (USE "linear_order_on_ZM" ("X" "succ(X!1)" "Y" "Y!1")) (("1" (GRIND :EXCLUDE "nonfull?" :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (IFF) (("2" (INST?) (("2" (INST?) (("2" (GROUND) NIL))))))))))))))))) ("2" (DELETE 2) (("2" (GRIND) (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("2" (IFF) (("2" (INST?) (("2" (INST?) (("2" (GROUND) NIL))))))))))))))))) (K_TCC1 "" (SKOLEM!) (("" (GROUND) (("1" (GRIND :EXCLUDE "ZM") (("1" (INST + "x!1") (("1" (SKOLEM!) (("1" (ASSERT) NIL))))))) ("2" (REWRITE "union_in_ZM") (("2" (DELETE 2) (("2" (GRIND :EXCLUDE "ZM") NIL))))))))) (K_TCC2 "" (SKOLEM-TYPEPRED) (("" (GROUND) (("1" (GRIND :EXCLUDE "ZM") NIL) ("2" (REWRITE "union_in_ZM") (("2" (DELETE -1 2) (("2" (GRIND :EXCLUDE "ZM") NIL))))))))) (|phi_K1| "" (SKOLEM!) (("" (AUTO-REWRITE "succ_in_ZM") (("" (ASSERT) (("" (USE "union_upper_bound" ("A" "{ B | ZM(B) AND not B(x!1) }" "X" "succ(K(x!1))")) (("1" (REWRITE "K" :DIR RL) (("1" (DELETE +) (("1" (GRIND :EXCLUDE "K" :IF-MATCH NIL) (("1" (INST - "phi(K(x!1))") (("1" (ASSERT) NIL))))))))) ("2" (GRIND) NIL))))))))) (|phi_K2| "" (SKOLEM!) (("" (AUTO-REWRITE "succ_in_ZM") (("" (ASSERT) (("" (USE "union_upper_bound" ("A" "{ B | ZM(B) AND disjoint?(C!1, B) }" "X" "succ(K(C!1))")) (("1" (REWRITE "K" :DIR RL) (("1" (DELETE +) (("1" (GRIND :EXCLUDE "K" :IF-MATCH NIL) (("1" (INST - "phi(K(C!1))") (("1" (ASSERT) NIL))))))))) ("2" (CASE "disjoint?(C!1, K(C!1))") (("1" (GRIND :EXCLUDE "K" :IF-MATCH NIL) (("1" (INST - "x!1") (("1" (ASSERT) NIL))))) ("2" (DELETE 2 3) (("2" (GRIND) NIL))))))))))))) (|phi_K3| "" (SKOLEM!) (("" (ASSERT) (("" (USE "strict_order_on_ZM") (("" (GROUND) (("1" (FORWARD-CHAIN "strict_subset_succ") (("1" (REWRITE "phi_K1") (("1" (ASSERT) NIL))))) ("2" (FORWARD-CHAIN "strict_subset_succ") (("2" (DELETE -1 -3 1) (("2" (NAME-REPLACE "x1" "phi(K(C!1))") (("2" (GRIND) NIL))))))))))))))) (|trichotomous| "" (EXPAND "trichotomous?") (("" (SKOSIMP) (("" (EXPAND "<") (("" (ASSERT) (("" (USE "strict_order_on_ZM") (("" (GROUND) (("" (AUTO-REWRITE "phi_K1") (("" (CASE "phi(K(x!1)) = y!1") (("1" (ASSERT) NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL))))))))))))))))))) (|well_founded| "" (EXPAND "well_founded?") (("" (SKOSIMP) (("" (CASE "nonempty?(p!1)") (("1" (ASSERT) (("1" (DELETE -) (("1" (INST + "phi(K(p!1))") (("1" (AUTO-REWRITE "phi_K1" "phi_K3") (("1" (SKOLEM-TYPEPRED) (("1" (EXPAND "<") (("1" (ASSERT) (("1" (FORWARD-CHAIN "strict_subset_succ") (("1" (ASSERT) (("1" (DELETE -1 -4) (("1" (GRIND) NIL))))))))))))))) ("2" (REWRITE "phi_K2") NIL))))))) ("2" (DELETE 2) (("2" (GRIND) NIL))))))))) (|well_order_exists| "" (INST + "<") (("" (EXPAND "well_order?") (("" (AUTO-REWRITE "well_founded" "trichotomous") (("" (ASSERT) NIL))))))))