%% PVS Version 3.1 %% 6.2 [Linux (x86)] (Feb 14, 2003 18:42) \$\$\$zorn2.pvs zorn2 [ T: TYPE ] : THEORY BEGIN IMPORTING zorn X, Y: VAR set[T] A, B, C: VAR set[set[T]] chain?(A): bool = FORALL (X, Y: (A)): subset?(X, Y) or subset?(Y, X) %---------------------------------------- % Specializations of Zorn's Lemma % when order relation = set inclusion %----------------------------------------- zorn_subset: LEMMA (FORALL A: subset?(A, C) and chain?(A) IMPLIES EXISTS (X:(C)) : FORALL (Y: (A)): subset?(Y, X)) IMPLIES EXISTS (X: (C)): FORALL (Y: (C)): subset?(X, Y) IMPLIES Y=X zorn_subset2: LEMMA (FORALL A: subset?(A, C) AND chain?(A) IMPLIES C(union(A))) IMPLIES EXISTS (X: (C)): FORALL (Y: (C)): subset?(X, Y) IMPLIES Y=X END zorn2 \$\$\$zorn2.prf (zorn2 (zorn_subset 0 (zorn_subset-2 "removed Inst! from previous proof" 3236549652 3236549652 ("" (skosimp) (("" (lemma "zorn[(C!1), lambda (X, Y:(C!1)): subset?(X, Y)]") (("1" (ground) (("1" (delete -2) (("1" (reduce :if-match nil) (("1" (inst? +) (("1" (skosimp) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (skosimp) (("2" (inst - "{ X | C!1(X) AND A!1(X) }") (("2" (ground) (("1" (delete -2) (("1" (grind :exclude "subset?" :if-match nil) (("1" (inst? +) (("1" (skolem!) (("1" (inst? -) nil nil)) nil)) nil)) nil)) nil) ("2" (delete -1 2) (("2" (grind) nil nil)) nil) ("3" (delete 2) (("3" (grind :exclude "subset?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -1 2) (("2" (grind) (("2" (apply-extensionality :hide? t) (("2" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil) proved nil 239214 28660 t shostak) (zorn_subset-1 nil 3236549380 3236549395 ("" (skosimp) (("" (lemma "zorn[(C!1), lambda (X, Y:(C!1)): subset?(X, Y)]") (("1" (ground) (("1" (delete -2) (("1" (reduce :instantiator inst!) nil nil)) nil) ("2" (delete 2) (("2" (skosimp) (("2" (inst - "{ X | C!1(X) AND A!1(X) }") (("2" (ground) (("1" (delete -2) (("1" (grind :exclude "subset?" :instantiator inst!) nil nil)) nil) ("2" (delete -1 2) (("2" (grind) nil nil)) nil) ("3" (delete 2) (("3" (grind :exclude "subset?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -1 2) (("2" (grind) (("2" (apply-extensionality :hide? t) (("2" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((subset? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil zorn2 nil) (zorn formula-decl nil zorn nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (chain? const-decl "bool" zorn2 nil) (chain? const-decl "bool" zorn nil) (member const-decl "bool" sets nil) (bounded? const-decl "bool" zorn nil) (NOT const-decl "[bool -> bool]" booleans nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil)) 5299 360 nil nil)) (zorn_subset2 0 (zorn_subset2-2 "Remove inst! from zorn_subset2-1 proof" 3236549826 3236549826 ("" (auto-rewrite "union_upper_bound[T]") (("" (skosimp) (("" (rewrite "zorn_subset") (("" (delete 2) (("" (reduce :if-match nil) (("" (inst? -) (("" (assert) (("" (inst? +) (("" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved nil 112625 6510 t shostak) (zorn_subset2-1 nil 3236549380 nil ("" (auto-rewrite "union_upper_bound[T]") (("" (skosimp) (("" (rewrite "zorn_subset") (("" (delete 2) (("" (reduce :instantiator inst!) nil nil)) nil)) nil)) nil)) nil) proved ((union const-decl "set[T]" set_bounds nil) (union_upper_bound formula-decl nil set_bounds nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil zorn2 nil) (zorn_subset formula-decl nil zorn2 nil)) nil nil nil 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| "" (GRIND :IF-MATCH NIL) (("" (INST - "{x | x=x!1 OR x=y!1 OR x=z!1}") (("" (REDUCE :IF-MATCH ALL) NIL NIL)) NIL)) NIL) (|wo_irreflexive| "" (GRIND :IF-MATCH NIL) (("" (DELETE -2) (("" (INST - "{x | x=x!1}") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|wo_strict_total_order| "" (SKOLEM-TYPEPRED) (("" (AUTO-REWRITE-THEORIES "orders[T]" "relations[T]") (("" (ASSERT) (("" (PROP) (("1" (USE "wo_irreflexive" ("S" "S!1")) NIL NIL) ("2" (USE "wo_transitive" ("S" "S!1")) NIL NIL) ("3" (EXPAND "well_order?") (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL) (|subset_succ1| "" (GRIND :EXCLUDE "nonfull?") NIL NIL) (|subset_succ2| "" (SKOSIMP) (("" (AUTO-REWRITE "subset_succ1") (("" (USE "subset_transitive" ("c" "succ(E!1)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|subset_succ3| "" (GRIND :EXCLUDE "nonfull?" :IF-MATCH NIL) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("" (REDUCE :IF-MATCH ALL) NIL NIL)) NIL)) NIL)) NIL) (|ZM_smallest| "" (EXPAND "ZM") (("" (SKOSIMP) (("" (REWRITE "inter_lower_bound") NIL NIL)) NIL)) NIL) (|emptyset_in_ZM| "" (GRIND :EXCLUDE ("succ" "union")) NIL NIL) (|succ_in_ZM| "" (GRIND :EXCLUDE ("nonfull?" "succ" "union")) NIL 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ZM_is_chain| "" (GRIND :DEFS NIL :REWRITES ("Chain" "emptyset_in_ZM" "succ_in_ZM" "union_in_ZM")) NIL NIL) (|H_emptyset| "" (GRIND) NIL 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 NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (GROUND) (("1" (REWRITE "union_in_ZM") (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "subset_union") (("2" (REWRITE "union_least_upper_bound") (("2" (SKOLEM!) (("2" (INST? -) (("2" (GROUND) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|H_is_chain| "" (AUTO-REWRITE "H_emptyset" "H_succ" "H_union" "Chain") (("" (REDUCE :IF-MATCH NIL) NIL 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 NIL)) NIL)) NIL)) NIL) (|strict_order_on_ZM| "" (SKOSIMP) (("" (EXPAND "strict_subset?") (("" (USE "linear_order_on_ZM") (("" (GROUND) NIL NIL)) NIL)) NIL)) 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?) NIL NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (K_TCC1 "" (SKOLEM!) (("" (GROUND) (("1" (GRIND :EXCLUDE "ZM") (("1" (INST + "x!1") (("1" (SKOLEM!) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "union_in_ZM") (("2" (DELETE 2) (("2" (GRIND :EXCLUDE "ZM") NIL NIL)) NIL)) NIL)) NIL)) NIL) (K_TCC2 "" (SKOLEM-TYPEPRED) (("" (GROUND) (("1" (GRIND :EXCLUDE "ZM") NIL NIL) ("2" (REWRITE "union_in_ZM") (("2" (DELETE -1 2) (("2" (GRIND :EXCLUDE "ZM") NIL NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "disjoint?(C!1, K(C!1))") (("1" (GRIND :EXCLUDE "K" :IF-MATCH NIL) (("1" (INST - "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE 2 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|phi_K3| "" (SKOLEM!) (("" (ASSERT) (("" (USE "strict_order_on_ZM") (("" (GROUND) (("1" (FORWARD-CHAIN "strict_subset_succ") (("1" (REWRITE "phi_K1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "strict_subset_succ") (("2" (DELETE -1 -3 1) (("2" (NAME-REPLACE "x1" "phi(K(C!1))") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|trichotomous| "" (GRIND :DEFS NIL :REWRITES ("trichotomous?" "<")) (("" (USE "strict_order_on_ZM") (("" (GROUND) (("" (AUTO-REWRITE "phi_K1") (("" (CASE "phi(K(x!1)) = y!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "phi_K2") NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|well_order_exists| "" (INST + "<") (("" (EXPAND "well_order?") (("" (AUTO-REWRITE "well_founded" "trichotomous") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) \$\$\$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](<<) 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 %----------------- % Zorn's Lemma %----------------- C(x): RECURSIVE bool = FORALL (y | y << x): C(y) IMPLIES y <= x MEASURE x BY << C_is_chain: LEMMA chain?(C) zorn: PROPOSITION (FORALL A: chain?(A) IMPLIES bounded?(A)) IMPLIES EXISTS x : FORALL y : x <= y IMPLIES x = y %------------------------ % Maximal chains exist %------------------------ D(x): RECURSIVE bool = FORALL (y | y << x): D(y) IMPLIES x <= y OR y <= x MEASURE x BY << D_is_chain: LEMMA chain?(D) maximal_chain: PROPOSITION EXISTS A: chain?(A) AND FORALL B: chain?(B) AND subset?(A, B) IMPLIES B = A 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 NIL)) NIL)) NIL) (|total_order| "" (TYPEPRED "zorn.<<") (("" (EXPAND* "well_order?" "trichotomous?") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|reflexivity| "" (TYPEPRED "zorn.<=") (("" (EXPAND* "partial_order?" "preorder?" "reflexive?") (("" (GROUND) NIL NIL)) NIL)) NIL) (|transitivity| "" (TYPEPRED "zorn.<=") (("" (EXPAND* "partial_order?" "preorder?" "transitive?") (("" (GROUND) NIL NIL)) NIL)) NIL) (|antisymmetry| "" (TYPEPRED "zorn.<=") (("" (EXPAND* "partial_order?" "antisymmetric?") (("" (GROUND) NIL NIL)) NIL)) 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 NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL) ("3" (EXPAND "C" -2) (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|zorn| "" (AUTO-REWRITE "C_is_chain" "bounded?" "antisymmetry") (("" (SKOSIMP) (("" (INST - "C") (("" (ASSERT) (("" (SKOLEM!) (("" (INST? +) (("" (SKOSIMP) (("" (CASE "C(y!1)") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "C") (("2" (SKOSIMP) (("2" (INST?) (("2" (FORWARD-CHAIN "transitivity") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|D_is_chain| "" (EXPAND "chain?") (("" (SKOSIMP :PREDS? T) (("" (AUTO-REWRITE "reflexivity") (("" (LEMMA "total_order" ("x" "y!1" "y" "z!1")) (("" (GROUND) (("1" (EXPAND "D" -3) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL) ("3" (EXPAND "D" -2) (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|maximal_chain| "" (INST + "D") (("" (REWRITE "D_is_chain") (("" (REDUCE) (("" (REWRITE "subset_antisymmetric") (("" (EXPAND* "subset?" "member" "chain?") (("" (EXPAND "D" 1) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL))