(* Parameter the "174b78e53fc239e8c2aab4ab5a996a27e3e5741e88070dad186e05fb13f275e5" *) Parameter the : (set->prop)->set. Definition True : prop := forall p:prop, p -> p. Definition False : prop := forall p:prop, p. Definition not : prop -> prop := fun A:prop => A -> False. Definition and : prop -> prop -> prop := fun A B:prop => forall p:prop, (A -> B -> p) -> p. Definition or : prop -> prop -> prop := fun A B:prop => forall p:prop, (A -> p) -> (B -> p) -> p. Definition iff : prop -> prop -> prop := fun A B:prop => and (A -> B) (B -> A). (* Unicode ~ "00ac" *) Prefix ~ 700 := not. Section Eq. Variable A:SType. Definition eq : A->A->prop := fun x y:A => forall Q:A->A->prop, Q x y -> Q y x. Definition neq : A->A->prop := fun x y:A => ~ eq x y. End Eq. Infix = 502 := eq. (* Unicode <> "2260" *) Infix <> 502 := neq. Section FE. Variable A B : SType. Axiom func_ext : forall f g : A -> B , (forall x : A , f x = g x) -> f = g. End FE. Section Ex. Variable A:SType. Definition ex : (A->prop)->prop := fun Q:A->prop => forall P:prop, (forall x:A, Q x -> P) -> P. End Ex. (* Unicode exists "2203" *) Binder+ exists , := ex. Axiom prop_ext : forall p q:prop, iff p q -> p = q. (* Parameter If_i "8c8f550868df4fdc93407b979afa60092db4b1bb96087bc3c2f17fadf3f35cbf" "b8ff52f838d0ff97beb955ee0b26fad79602e1529f8a2854bda0ecd4193a8a3c" *) Parameter If_i : prop->set->set->set. Notation IfThenElse If_i. Parameter In:set->set->prop. Definition Subq : set -> set -> prop := fun A B => forall x :e A, x :e B. Definition nSubq : set->set->prop := fun X Y => ~Subq X Y. (* Unicode /c= "2288" *) Infix /c= 502 := nSubq. Binder+ exists , := ex; and. (* Parameter UPair "f55f90f052decfc17a366f12be0ad237becf63db26be5d163bf4594af99f943a" "e2a83319facad3a3d8ff453f4ef821d9da495e56a623695546bb7d7ac333f3fe" *) Parameter UPair : set -> set -> set. (* Parameter Sing "ee0b09fbfbda76156511ec03a1fc7c909693103f062263776c2c98a655837c92" "ec9394dc0cd84355682ca93f9e80c8aa367ef9c3479874f5f04da125c87db1f1" *) Parameter Sing : set -> set. (* Unicode Union "22C3" *) Parameter Union : set->set. Axiom the_ax : forall P:set->prop, forall x:set, P x -> P (the P). Axiom setext : forall X Y:set, (forall x, iff (x :e X) (x :e Y)) -> X = Y. (* Unicode /\ "2227" *) Infix /\ 780 left := and. (* Unicode \/ "2228" *) Infix \/ 785 left := or. (* Unicode <-> "2194" *) Infix <-> 805 := iff. Axiom FalseE : False -> forall p:prop, p. Axiom TrueI : True. Axiom notI : forall A:prop, (A -> False) -> ~A. Axiom notE : forall A:prop, ~A -> A -> False. Axiom andI : forall (A B : prop), A -> B -> A /\ B. Axiom andEL : forall (A B : prop), A /\ B -> A. Axiom andER : forall (A B : prop), A /\ B -> B. Axiom orIL : forall (A B : prop), A -> A \/ B. Axiom orIR : forall (A B : prop), B -> A \/ B. Axiom orE : forall (A B C:prop), (A -> C) -> (B -> C) -> A \/ B -> C. Axiom iffEL : forall A B:prop, (A <-> B) -> A -> B. Axiom iffER : forall A B:prop, (A <-> B) -> B -> A. Axiom iffI : forall A B:prop, (A -> B) -> (B -> A) -> (A <-> B). Axiom iff_ref : forall A:prop, A <-> A. Axiom the_ex : forall P:set -> prop, (exists x, P x) -> P (the P). Axiom pred_ext : forall P Q:set -> prop, (forall x, P x <-> Q x) -> P = Q. Axiom prop_ext_2 : forall p q:prop, (p -> q) -> (q -> p) -> p = q. Axiom pred_ext_2 : forall P Q:set -> prop, P c= Q -> Q c= P -> P = Q. Axiom xm : forall P:prop, P \/ ~P. Definition nIn : set->set->prop := fun x X => ~In x X. (* Unicode /:e "2209" *) Infix /:e 502 := nIn. Notation SetEnum2 UPair. Notation SetEnum1 Sing. Axiom UPairE : forall x y z:set, x :e {y,z} -> x = y \/ x = z. Axiom UPairI1 : forall y z:set, y :e {y,z}. Axiom UPairI2 : forall y z:set, z :e {y,z}. Axiom SingI : forall x:set, x :e {x}. Axiom SingE : forall x y:set, y :e {x} -> y = x. Axiom Sing_UPair_def : forall x, {x} = {x,x}. Axiom Sing_inv : forall x Y, {x} = Y -> x :e Y /\ forall y :e Y, y = x. Axiom Empty_ex : exists X, forall x, x /:e X. (* Parameter Empty' "7491fed394c0760ecce5d4e1df80fe76188bef2528794da082e0223de99066ce" "2ef0dbc560f4aba05346926782e584726ed94e6cc5f65568b80a37ddbfa5d716" *) Parameter Empty' : set. Axiom EmptyE : forall x, x /:e Empty'. (* Parameter Power' "bb1c4bb2e7b5e9ffd2978980d2b27d615cbc8bb8a123decb3fd54fb80dc2fcb9" "9018ff5b96ad378f36dab276f58bdc7d8fc18222c596ca3177be08a1acee9d2e" *) (* Unicode Power' "1D4AB" *) Parameter Power' : set->set. (* Parameter omega "54f5b491560ccfc13fb2334a544117bd0f7903fe3f22751e4485e0b838a1016c" "80d24834aa9f66bdb9a5e1bbd38abd569c0980b113318e3a60b061de5affc484" *) Parameter omega : set. (* Parameter Repl' "fea72b9a680f666e24da732d2835c8d83e82d65c993a1597aca84bda2f745970" "3041a1cb0e073a46422f794fe16feb7d39d077e3958b5d236feecb2341d4ca6f" *) Parameter Repl' : set -> (set -> set) -> set. Notation Repl Repl'. (* Parameter Sep "8324d6b2a87d5e233d35100511422a76274b918c35d0c1ca109b0c52f6b24d83" "da98b582b06ed7e84a25bdac946c6310e931cc500e9c18c33b40a7d20304e6f9" *) Parameter Sep : set -> (set -> prop) -> set. Notation Sep Sep. (* Parameter ReplSep "7f5ba2b987e7d7cf10ad34e82699aa594573af19f242f0e85c661d42702f3dfd" "bf4f61e2fabe0a1fcc27644aebe41c2c9f551c7841eb70b7ea8aea9ec77c0617" *) Parameter ReplSep : set->(set->prop)->(set->set)->set. Notation ReplSep ReplSep. (* Parameter famunion "b37c45ca1b39ef7beb231562b95d8f2008d19d737d0aa5c61951d33806a71055" "333b249faa15a516bac392a709735971aac1959219180f6500350954b28acf90" *) Parameter famunion:set->(set->set)->set. (* Unicode \/_ "22C3" *) (* Subscript \/_ *) Binder \/_ , := famunion. Section EpsilonRec_i. Variable F:set -> (set -> set) -> set. (* Parameter In_rec_i "f97da687c51f5a332ff57562bd465232bc70c9165b0afe0a54e6440fc4962a9f" "fac413e747a57408ad38b3855d3cde8673f86206e95ccdadff2b5babaf0c219e" *) Parameter In_rec_i : set -> set. Hypothesis Fr:forall X:set, forall g h:set -> set, (forall x :e X, g x = h x) -> F X g = F X h. Axiom In_rec_i_eq : forall X:set, In_rec_i X = F X In_rec_i. End EpsilonRec_i. (* Parameter binunion "859e7011bdff89bb687e84e00cdf046122d077684a4e029a72b72931a8ccf2fd" "3828378f54d092a4eb3a7645cd8c22019202c50241d1dbee65a720f73be8d9ed" *) Parameter binunion : set -> set -> set. (* Unicode :\/: "222a" *) Infix :\/: 345 left := binunion. (* Parameter setminus "ab8fa98efe29083fe30a0fab65506354f55a312c53182074393bc5eb5aed1e5d" "cd8574867c700d5542bfe0bb1ed35fc4e5b530a086f5485ba1fb0b5ca87b38b2" *) Parameter setminus:set->set->set. (* Unicode :\: "2216" *) Infix :\: 350 := setminus. (* Parameter ordsucc "905e14778dc45ba874b5f3f5f516dc7dcb7b42823b510bde2e8463b6dfba641f" "19043aec9cd19235befab2698aecb56ec899722f50cbe2d51d3738ba20ab5fc3" *) Parameter ordsucc : set->set. Axiom ordsuccI1 : forall x:set, x c= ordsucc x. Axiom ordsuccI2 : forall x:set, x :e ordsucc x. Axiom ordsuccE : forall x y:set, y :e ordsucc x -> y :e x \/ y = x. Notation Nat Empty' ordsucc. (*** Injection of set into itself that will correspond to x |-> (1,x) after pairing is defined. ***) Definition Inj1 : set -> set := In_rec_i (fun X f => {0} :\/: {f x|x :e X}). (*** Injection of set into itself that will correspond to x |-> (0,x) after pairing is defined. ***) Definition Inj0 : set -> set := fun X => {Inj1 x|x :e X}. (*** Unj : Left inverse of Inj1 and Inj0 ***) Definition Unj : set -> set := In_rec_i (fun X f => {f x|x :e X :\: {0}}). (*** setsum ***) Definition setsum : set -> set -> set := fun X Y => {Inj0 x|x :e X} :\/: {Inj1 y|y :e Y}. (* Unicode :+: "002b" *) Infix :+: 450 left := setsum. Section pair_setsum. Let pair := setsum. Definition proj0 : set -> set := fun Z => {Unj z|z :e Z, exists x:set, Inj0 x = z}. Definition proj1 : set -> set := fun Z => {Unj z|z :e Z, exists y:set, Inj1 y = z}. (*** Sigma X Y = {(x,y) | x in X, y in Y x} ***) Definition Sigma : set -> (set -> set) -> set := fun X Y => \/_ x :e X, {pair x y|y :e Y x}. (* Unicode Sigma_ "2211" *) Binder+ Sigma_ , := Sigma. (* Unicode :*: "2a2f" *) Infix :*: 440 left := setprod. (*** lam X F = {(x,y) | x :e X, y :e F x} = \/_{x :e X} {(x,y) | y :e (F x)} = Sigma X F ***) Let lam : set -> (set -> set) -> set := Sigma. (*** ap f x = {proj1 z | z :e f, exists y, z = pair x y}} ***) Definition ap : set -> set -> set := fun f x => {proj1 z|z :e f, exists y:set, z = pair x y}. Definition Pi : set -> (set -> set) -> set := fun X Y => {f :e Power' (Sigma_ x :e X, Union (Y x)) | forall x :e X, ap f x :e Y x}. End pair_setsum. (* Unicode Sigma_ "2211" *) Binder+ Sigma_ , := Sigma. Notation SetImplicitOp ap. Notation SetLam Sigma. (* Unicode Pi_ "220f" *) Binder+ Pi_ , := Pi. Definition setexp : set->set->set := fun X Y:set => Pi_ y :e Y, X. (* Superscript :^: *) Infix :^: 430 left := setexp. Definition empty : set -> prop := fun X => forall x, x /:e X. (** specific for HOL4 **) Definition nonempty : set -> prop := fun X => ~empty X. Definition p : set -> prop := fun X => 0 :e X. Definition inj__o : prop -> set := fun P:prop => if P then 1 else 0.