src/ZF/ZF.thy
 author lcp Thu May 04 02:00:38 1995 +0200 (1995-05-04 ago) changeset 1106 62bdb9e5722b parent 690 b2bd1d5a3d16 child 1116 7fca5aabcbb0 permissions -rw-r--r--
Added pattern-matching code from CHOL/Prod.thy. Changed
definitions so that split is now defined in terms of fst, snd. Now split is
polymorphic. Deleted fsplit, as split(...)::o gives a similar effect -- NOT
identical though, as fsplit(P,z) implied that z was a pair, while split(P,z)
means only P(fst(z),snd(z)).
 wenzelm@615 ` 1` ```(* Title: ZF/ZF.thy ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 3` ``` Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1993 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```Zermelo-Fraenkel Set Theory ``` clasohm@0 ` 7` ```*) ``` clasohm@0 ` 8` lcp@1106 ` 9` ```ZF = FOL + Let + ``` clasohm@0 ` 10` clasohm@0 ` 11` ```types ``` wenzelm@615 ` 12` ``` i ``` clasohm@0 ` 13` clasohm@0 ` 14` ```arities ``` clasohm@0 ` 15` ``` i :: term ``` clasohm@0 ` 16` clasohm@0 ` 17` ```consts ``` clasohm@0 ` 18` lcp@675 ` 19` ``` "0" :: "i" ("0") (*the empty set*) ``` lcp@675 ` 20` ``` Pow :: "i => i" (*power sets*) ``` lcp@675 ` 21` ``` Inf :: "i" (*infinite set*) ``` clasohm@0 ` 22` clasohm@0 ` 23` ``` (* Bounded Quantifiers *) ``` clasohm@0 ` 24` lcp@675 ` 25` ``` Ball, Bex :: "[i, i => o] => o" ``` clasohm@0 ` 26` clasohm@0 ` 27` ``` (* General Union and Intersection *) ``` clasohm@0 ` 28` lcp@675 ` 29` ``` Union,Inter :: "i => i" ``` clasohm@0 ` 30` clasohm@0 ` 31` ``` (* Variations on Replacement *) ``` clasohm@0 ` 32` lcp@675 ` 33` ``` PrimReplace :: "[i, [i, i] => o] => i" ``` lcp@675 ` 34` ``` Replace :: "[i, [i, i] => o] => i" ``` lcp@675 ` 35` ``` RepFun :: "[i, i => i] => i" ``` lcp@675 ` 36` ``` Collect :: "[i, i => o] => i" ``` clasohm@0 ` 37` clasohm@0 ` 38` ``` (* Descriptions *) ``` clasohm@0 ` 39` lcp@675 ` 40` ``` The :: "(i => o) => i" (binder "THE " 10) ``` lcp@675 ` 41` ``` if :: "[o, i, i] => i" ``` clasohm@0 ` 42` clasohm@0 ` 43` ``` (* Finite Sets *) ``` clasohm@0 ` 44` lcp@675 ` 45` ``` Upair, cons :: "[i, i] => i" ``` lcp@675 ` 46` ``` succ :: "i => i" ``` clasohm@0 ` 47` wenzelm@615 ` 48` ``` (* Ordered Pairing *) ``` clasohm@0 ` 49` lcp@675 ` 50` ``` Pair :: "[i, i] => i" ``` lcp@675 ` 51` ``` fst, snd :: "i => i" ``` lcp@1106 ` 52` ``` split :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*) ``` clasohm@0 ` 53` clasohm@0 ` 54` ``` (* Sigma and Pi Operators *) ``` clasohm@0 ` 55` lcp@675 ` 56` ``` Sigma, Pi :: "[i, i => i] => i" ``` clasohm@0 ` 57` clasohm@0 ` 58` ``` (* Relations and Functions *) ``` clasohm@0 ` 59` lcp@675 ` 60` ``` domain :: "i => i" ``` lcp@675 ` 61` ``` range :: "i => i" ``` lcp@675 ` 62` ``` field :: "i => i" ``` lcp@675 ` 63` ``` converse :: "i => i" ``` lcp@690 ` 64` ``` function :: "i => o" (*is a relation a function?*) ``` lcp@675 ` 65` ``` Lambda :: "[i, i => i] => i" ``` lcp@675 ` 66` ``` restrict :: "[i, i] => i" ``` clasohm@0 ` 67` clasohm@0 ` 68` ``` (* Infixes in order of decreasing precedence *) ``` clasohm@0 ` 69` lcp@675 ` 70` ``` "``" :: "[i, i] => i" (infixl 90) (*image*) ``` lcp@675 ` 71` ``` "-``" :: "[i, i] => i" (infixl 90) (*inverse image*) ``` lcp@675 ` 72` ``` "`" :: "[i, i] => i" (infixl 90) (*function application*) ``` lcp@675 ` 73` ```(*"*" :: "[i, i] => i" (infixr 80) (*Cartesian product*)*) ``` lcp@675 ` 74` ``` "Int" :: "[i, i] => i" (infixl 70) (*binary intersection*) ``` lcp@675 ` 75` ``` "Un" :: "[i, i] => i" (infixl 65) (*binary union*) ``` lcp@675 ` 76` ``` "-" :: "[i, i] => i" (infixl 65) (*set difference*) ``` lcp@675 ` 77` ```(*"->" :: "[i, i] => i" (infixr 60) (*function space*)*) ``` lcp@675 ` 78` ``` "<=" :: "[i, i] => o" (infixl 50) (*subset relation*) ``` lcp@675 ` 79` ``` ":" :: "[i, i] => o" (infixl 50) (*membership relation*) ``` lcp@675 ` 80` ```(*"~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*)*) ``` clasohm@0 ` 81` clasohm@0 ` 82` wenzelm@615 ` 83` ```types ``` wenzelm@615 ` 84` ``` is ``` lcp@1106 ` 85` ``` pttrns ``` wenzelm@615 ` 86` wenzelm@615 ` 87` ```syntax ``` lcp@1106 ` 88` ``` "" :: "i => is" ("_") ``` lcp@1106 ` 89` ``` "@Enum" :: "[i, is] => is" ("_,/ _") ``` lcp@1106 ` 90` ``` "~:" :: "[i, i] => o" (infixl 50) ``` lcp@1106 ` 91` ``` "@Finset" :: "is => i" ("{(_)}") ``` lcp@1106 ` 92` ``` "@Tuple" :: "[i, is] => i" ("<(_,/ _)>") ``` lcp@1106 ` 93` ``` "@Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})") ``` lcp@1106 ` 94` ``` "@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})") ``` lcp@1106 ` 95` ``` "@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51]) ``` lcp@1106 ` 96` ``` "@INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10) ``` lcp@1106 ` 97` ``` "@UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10) ``` lcp@1106 ` 98` ``` "@PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10) ``` lcp@1106 ` 99` ``` "@SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10) ``` lcp@1106 ` 100` ``` "->" :: "[i, i] => i" (infixr 60) ``` lcp@1106 ` 101` ``` "*" :: "[i, i] => i" (infixr 80) ``` lcp@1106 ` 102` ``` "@lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10) ``` lcp@1106 ` 103` ``` "@Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10) ``` lcp@1106 ` 104` ``` "@Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10) ``` lcp@1106 ` 105` lcp@1106 ` 106` ``` (** Patterns -- extends pre-defined type "pttrn" used in abstractions **) ``` lcp@1106 ` 107` lcp@1106 ` 108` ``` "@pttrn" :: "pttrns => pttrn" ("<_>") ``` lcp@1106 ` 109` ``` "" :: " pttrn => pttrns" ("_") ``` lcp@1106 ` 110` ``` "@pttrns" :: "[pttrn,pttrns] => pttrns" ("_,/_") ``` wenzelm@615 ` 111` clasohm@0 ` 112` ```translations ``` wenzelm@615 ` 113` ``` "x ~: y" == "~ (x : y)" ``` clasohm@0 ` 114` ``` "{x, xs}" == "cons(x, {xs})" ``` clasohm@0 ` 115` ``` "{x}" == "cons(x, 0)" ``` clasohm@0 ` 116` ``` "{x:A. P}" == "Collect(A, %x. P)" ``` clasohm@0 ` 117` ``` "{y. x:A, Q}" == "Replace(A, %x y. Q)" ``` wenzelm@615 ` 118` ``` "{b. x:A}" == "RepFun(A, %x. b)" ``` clasohm@0 ` 119` ``` "INT x:A. B" == "Inter({B. x:A})" ``` clasohm@0 ` 120` ``` "UN x:A. B" == "Union({B. x:A})" ``` clasohm@0 ` 121` ``` "PROD x:A. B" => "Pi(A, %x. B)" ``` clasohm@0 ` 122` ``` "SUM x:A. B" => "Sigma(A, %x. B)" ``` wenzelm@49 ` 123` ``` "A -> B" => "Pi(A, _K(B))" ``` wenzelm@49 ` 124` ``` "A * B" => "Sigma(A, _K(B))" ``` clasohm@0 ` 125` ``` "lam x:A. f" == "Lambda(A, %x. f)" ``` clasohm@0 ` 126` ``` "ALL x:A. P" == "Ball(A, %x. P)" ``` clasohm@0 ` 127` ``` "EX x:A. P" == "Bex(A, %x. P)" ``` lcp@37 ` 128` lcp@1106 ` 129` ``` "" == ">" ``` lcp@1106 ` 130` ``` "" == "Pair(x, y)" ``` lcp@1106 ` 131` ``` "%.b" => "split(%x .b)" ``` lcp@1106 ` 132` ``` "%.b" => "split(%x y.b)" ``` lcp@1106 ` 133` ```(* The <= direction fails if split has more than one argument because ``` lcp@1106 ` 134` ``` ast-matching fails. Otherwise it would work fine *) ``` clasohm@0 ` 135` lcp@690 ` 136` ```defs ``` clasohm@0 ` 137` wenzelm@615 ` 138` ``` (* Bounded Quantifiers *) ``` wenzelm@615 ` 139` ``` Ball_def "Ball(A, P) == ALL x. x:A --> P(x)" ``` wenzelm@615 ` 140` ``` Bex_def "Bex(A, P) == EX x. x:A & P(x)" ``` lcp@690 ` 141` wenzelm@615 ` 142` ``` subset_def "A <= B == ALL x:A. x:B" ``` lcp@690 ` 143` ``` succ_def "succ(i) == cons(i, i)" ``` lcp@690 ` 144` lcp@690 ` 145` ```rules ``` clasohm@0 ` 146` wenzelm@615 ` 147` ``` (* ZF axioms -- see Suppes p.238 ``` wenzelm@615 ` 148` ``` Axioms for Union, Pow and Replace state existence only, ``` wenzelm@615 ` 149` ``` uniqueness is derivable using extensionality. *) ``` clasohm@0 ` 150` wenzelm@615 ` 151` ``` extension "A = B <-> A <= B & B <= A" ``` wenzelm@615 ` 152` ``` Union_iff "A : Union(C) <-> (EX B:C. A:B)" ``` wenzelm@615 ` 153` ``` Pow_iff "A : Pow(B) <-> A <= B" ``` clasohm@0 ` 154` wenzelm@615 ` 155` ``` (*We may name this set, though it is not uniquely defined.*) ``` wenzelm@615 ` 156` ``` infinity "0:Inf & (ALL y:Inf. succ(y): Inf)" ``` clasohm@0 ` 157` wenzelm@615 ` 158` ``` (*This formulation facilitates case analysis on A.*) ``` wenzelm@615 ` 159` ``` foundation "A=0 | (EX x:A. ALL y:x. y~:A)" ``` clasohm@0 ` 160` wenzelm@615 ` 161` ``` (*Schema axiom since predicate P is a higher-order variable*) ``` wenzelm@615 ` 162` ``` replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> \ ``` wenzelm@615 ` 163` ``` \ b : PrimReplace(A,P) <-> (EX x:A. P(x,b))" ``` wenzelm@615 ` 164` lcp@690 ` 165` ```defs ``` lcp@690 ` 166` wenzelm@615 ` 167` ``` (* Derived form of replacement, restricting P to its functional part. ``` wenzelm@615 ` 168` ``` The resulting set (for functional P) is the same as with ``` wenzelm@615 ` 169` ``` PrimReplace, but the rules are simpler. *) ``` clasohm@0 ` 170` wenzelm@615 ` 171` ``` Replace_def "Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))" ``` wenzelm@615 ` 172` wenzelm@615 ` 173` ``` (* Functional form of replacement -- analgous to ML's map functional *) ``` clasohm@0 ` 174` wenzelm@615 ` 175` ``` RepFun_def "RepFun(A,f) == {y . x:A, y=f(x)}" ``` clasohm@0 ` 176` wenzelm@615 ` 177` ``` (* Separation and Pairing can be derived from the Replacement ``` wenzelm@615 ` 178` ``` and Powerset Axioms using the following definitions. *) ``` clasohm@0 ` 179` wenzelm@615 ` 180` ``` Collect_def "Collect(A,P) == {y . x:A, x=y & P(x)}" ``` clasohm@0 ` 181` wenzelm@615 ` 182` ``` (*Unordered pairs (Upair) express binary union/intersection and cons; ``` wenzelm@615 ` 183` ``` set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*) ``` clasohm@0 ` 184` wenzelm@615 ` 185` ``` Upair_def "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}" ``` wenzelm@615 ` 186` ``` cons_def "cons(a,A) == Upair(a,a) Un A" ``` wenzelm@615 ` 187` wenzelm@615 ` 188` ``` (* Difference, general intersection, binary union and small intersection *) ``` clasohm@0 ` 189` wenzelm@615 ` 190` ``` Diff_def "A - B == { x:A . ~(x:B) }" ``` wenzelm@615 ` 191` ``` Inter_def "Inter(A) == { x:Union(A) . ALL y:A. x:y}" ``` wenzelm@615 ` 192` ``` Un_def "A Un B == Union(Upair(A,B))" ``` wenzelm@615 ` 193` ``` Int_def "A Int B == Inter(Upair(A,B))" ``` clasohm@0 ` 194` wenzelm@615 ` 195` ``` (* Definite descriptions -- via Replace over the set "1" *) ``` clasohm@0 ` 196` wenzelm@615 ` 197` ``` the_def "The(P) == Union({y . x:{0}, P(y)})" ``` wenzelm@615 ` 198` ``` if_def "if(P,a,b) == THE z. P & z=a | ~P & z=b" ``` clasohm@0 ` 199` wenzelm@615 ` 200` ``` (* Ordered pairs and disjoint union of a family of sets *) ``` clasohm@0 ` 201` wenzelm@615 ` 202` ``` (* this "symmetric" definition works better than {{a}, {a,b}} *) ``` wenzelm@615 ` 203` ``` Pair_def " == {{a,a}, {a,b}}" ``` lcp@1106 ` 204` ``` fst_def "fst(p) == THE a. EX b. p=" ``` lcp@1106 ` 205` ``` snd_def "snd(p) == THE b. EX a. p=" ``` lcp@1106 ` 206` ``` split_def "split(c,p) == c(fst(p), snd(p))" ``` wenzelm@615 ` 207` ``` Sigma_def "Sigma(A,B) == UN x:A. UN y:B(x). {}" ``` clasohm@0 ` 208` wenzelm@615 ` 209` ``` (* Operations on relations *) ``` clasohm@0 ` 210` wenzelm@615 ` 211` ``` (*converse of relation r, inverse of function*) ``` wenzelm@615 ` 212` ``` converse_def "converse(r) == {z. w:r, EX x y. w= & z=}" ``` clasohm@0 ` 213` wenzelm@615 ` 214` ``` domain_def "domain(r) == {x. w:r, EX y. w=}" ``` wenzelm@615 ` 215` ``` range_def "range(r) == domain(converse(r))" ``` wenzelm@615 ` 216` ``` field_def "field(r) == domain(r) Un range(r)" ``` lcp@690 ` 217` ``` function_def "function(r) == ALL x y. :r --> \ ``` lcp@690 ` 218` ```\ (ALL y'. :r --> y=y')" ``` wenzelm@615 ` 219` ``` image_def "r `` A == {y : range(r) . EX x:A. : r}" ``` wenzelm@615 ` 220` ``` vimage_def "r -`` A == converse(r)``A" ``` clasohm@0 ` 221` wenzelm@615 ` 222` ``` (* Abstraction, application and Cartesian product of a family of sets *) ``` clasohm@0 ` 223` wenzelm@615 ` 224` ``` lam_def "Lambda(A,b) == { . x:A}" ``` wenzelm@615 ` 225` ``` apply_def "f`a == THE y. : f" ``` lcp@690 ` 226` ``` Pi_def "Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}" ``` clasohm@0 ` 227` clasohm@0 ` 228` ``` (* Restrict the function f to the domain A *) ``` wenzelm@615 ` 229` ``` restrict_def "restrict(f,A) == lam x:A.f`x" ``` clasohm@0 ` 230` clasohm@0 ` 231` ```end ``` clasohm@0 ` 232` clasohm@0 ` 233` clasohm@0 ` 234` ```ML ``` clasohm@0 ` 235` lcp@1106 ` 236` ```(* Pattern-matching and 'Dependent' type operators *) ``` lcp@1106 ` 237` lcp@1106 ` 238` ```local open Syntax ``` lcp@1106 ` 239` lcp@1106 ` 240` ```fun pttrn s = const"@pttrn" \$ s; ``` lcp@1106 ` 241` ```fun pttrns s t = const"@pttrns" \$ s \$ t; ``` clasohm@0 ` 242` lcp@1106 ` 243` ```fun split2(Abs(x,T,t)) = ``` lcp@1106 ` 244` ``` let val (pats,u) = split1 t ``` lcp@1106 ` 245` ``` in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end ``` lcp@1106 ` 246` ``` | split2(Const("split",_) \$ r) = ``` lcp@1106 ` 247` ``` let val (pats,s) = split2(r) ``` lcp@1106 ` 248` ``` val (pats2,t) = split1(s) ``` lcp@1106 ` 249` ``` in (pttrns (pttrn pats) pats2, t) end ``` lcp@1106 ` 250` ```and split1(Abs(x,T,t)) = (Free(x,T), subst_bounds([free x],t)) ``` lcp@1106 ` 251` ``` | split1(Const("split",_)\$t) = split2(t); ``` lcp@1106 ` 252` lcp@1106 ` 253` ```fun split_tr'(t::args) = ``` lcp@1106 ` 254` ``` let val (pats,ft) = split2(t) ``` lcp@1106 ` 255` ``` in list_comb(const"_lambda" \$ pttrn pats \$ ft, args) end; ``` lcp@1106 ` 256` lcp@1106 ` 257` ```in ``` lcp@1106 ` 258` lcp@1106 ` 259` ```val print_translation = ``` lcp@1106 ` 260` ``` [("split", split_tr'), ``` lcp@1106 ` 261` ``` ("Pi", dependent_tr' ("@PROD", "op ->")), ``` wenzelm@632 ` 262` ``` ("Sigma", dependent_tr' ("@SUM", "op *"))]; ``` lcp@1106 ` 263` lcp@1106 ` 264` ```end; ```