author paulson Tue, 15 Jan 2002 10:23:58 +0100 changeset 12762 a0c0a1e3a53a parent 12761 b0c39f9837af child 12763 6cecd9dfd53f
split can now be unfolded even with one argument
 src/ZF/ZF.thy file | annotate | diff | comparison | revisions
```--- a/src/ZF/ZF.thy	Tue Jan 15 00:13:20 2002 +0100
+++ b/src/ZF/ZF.thy	Tue Jan 15 10:23:58 2002 +0100
@@ -6,7 +6,7 @@
Zermelo-Fraenkel Set Theory
*)

-ZF = FOL + Let +
+ZF = FOL + Let +

global

@@ -198,7 +198,7 @@
foundation    "A=0 | (EX x:A. ALL y:x. y~:A)"

(*Schema axiom since predicate P is a higher-order variable*)
-  replacement   "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
+  replacement   "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"

defs
@@ -240,7 +240,7 @@
Pair_def      "<a,b>  == {{a,a}, {a,b}}"
fst_def       "fst(p) == THE a. EX b. p=<a,b>"
snd_def       "snd(p) == THE b. EX a. p=<a,b>"
-  split_def     "split(c,p) == c(fst(p), snd(p))"
+  split_def     "split(c) == %p. c(fst(p), snd(p))"
Sigma_def     "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"

(* Operations on relations *)
@@ -251,7 +251,7 @@
domain_def    "domain(r) == {x. w:r, EX y. w=<x,y>}"
range_def     "range(r) == domain(converse(r))"
field_def     "field(r) == domain(r) Un range(r)"
-  function_def  "function(r) == ALL x y. <x,y>:r -->
+  function_def  "function(r) == ALL x y. <x,y>:r -->
(ALL y'. <x,y'>:r --> y=y')"
image_def     "r `` A  == {y : range(r) . EX x:A. <x,y> : r}"
vimage_def    "r -`` A == converse(r)``A"
@@ -272,7 +272,7 @@

(* Pattern-matching and 'Dependent' type operators *)

-val print_translation =
+val print_translation =
[(*("split", split_tr'),*)
("Pi",    dependent_tr' ("@PROD", "op ->")),
("Sigma", dependent_tr' ("@SUM", "op *"))];```