--- a/src/ZF/List.thy Fri Jun 14 12:37:21 1996 +0200
+++ b/src/ZF/List.thy Mon Jun 17 16:50:08 1996 +0200
@@ -13,15 +13,6 @@
List = Datatype +
consts
- "@" :: [i,i]=>i (infixr 60)
- list_rec :: [i, i, [i,i,i]=>i] => i
- map :: [i=>i, i] => i
- length,rev :: i=>i
- flat :: i=>i
- list_add :: i=>i
- hd,tl :: i=>i
- drop :: [i,i]=>i
-
(* List Enumeration *)
"[]" :: i ("[]")
"@List" :: is => i ("[(_)]")
@@ -39,19 +30,40 @@
"[]" == "Nil"
-defs
+constdefs
+ hd :: i=>i
+ "hd(l) == list_case(0, %x xs.x, l)"
+
+ tl :: i=>i
+ "tl(l) == list_case(Nil, %x xs.xs, l)"
+
+ drop :: [i,i]=>i
+ "drop(i,l) == rec(i, l, %j r. tl(r))"
- hd_def "hd(l) == list_case(0, %x xs.x, l)"
- tl_def "tl(l) == list_case(Nil, %x xs.xs, l)"
- drop_def "drop(i,l) == rec(i, l, %j r. tl(r))"
+ list_rec :: [i, i, [i,i,i]=>i] => i
+ "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
+
+ map :: [i=>i, i] => i
+ "map(f,l) == list_rec(l, Nil, %x xs r. Cons(f(x), r))"
+
+ length :: i=>i
+ "length(l) == list_rec(l, 0, %x xs r. succ(r))"
- list_rec_def
- "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
+
+consts (*Cannot use constdefs because @ is not an identifier*)
+ "@" :: [i,i]=>i (infixr 60)
+defs
+ app_def "xs@ys == list_rec(xs, ys, %x xs r. Cons(x,r))"
+
- map_def "map(f,l) == list_rec(l, Nil, %x xs r. Cons(f(x), r))"
- length_def "length(l) == list_rec(l, 0, %x xs r. succ(r))"
- app_def "xs@ys == list_rec(xs, ys, %x xs r. Cons(x,r))"
- rev_def "rev(l) == list_rec(l, Nil, %x xs r. r @ [x])"
- flat_def "flat(ls) == list_rec(ls, Nil, %l ls r. l @ r)"
- list_add_def "list_add(l) == list_rec(l, 0, %x xs r. x#+r)"
+constdefs
+ rev :: i=>i
+ "rev(l) == list_rec(l, Nil, %x xs r. r @ [x])"
+
+ flat :: i=>i
+ "flat(ls) == list_rec(ls, Nil, %l ls r. l @ r)"
+
+ list_add :: i=>i
+ "list_add(l) == list_rec(l, 0, %x xs r. x#+r)"
+
end
--- a/src/ZF/Perm.thy Fri Jun 14 12:37:21 1996 +0200
+++ b/src/ZF/Perm.thy Mon Jun 17 16:50:08 1996 +0200
@@ -11,26 +11,28 @@
Perm = ZF + "mono" +
consts
- O :: [i,i]=>i (infixr 60)
- id :: i=>i
- inj,surj,bij:: [i,i]=>i
+ O :: [i,i]=>i (infixr 60)
defs
+ (*composition of relations and functions; NOT Suppes's relative product*)
+ comp_def "r O s == {xz : domain(s)*range(r) .
+ EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
- (*composition of relations and functions; NOT Suppes's relative product*)
- comp_def "r O s == {xz : domain(s)*range(r) .
- EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
-
- (*the identity function for A*)
- id_def "id(A) == (lam x:A. x)"
+constdefs
+ (*the identity function for A*)
+ id :: i=>i
+ "id(A) == (lam x:A. x)"
- (*one-to-one functions from A to B*)
- inj_def "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
+ (*one-to-one functions from A to B*)
+ inj :: [i,i]=>i
+ "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
- (*onto functions from A to B*)
- surj_def "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
+ (*onto functions from A to B*)
+ surj :: [i,i]=>i
+ "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
- (*one-to-one and onto functions*)
- bij_def "bij(A,B) == inj(A,B) Int surj(A,B)"
+ (*one-to-one and onto functions*)
+ bij :: [i,i]=>i
+ "bij(A,B) == inj(A,B) Int surj(A,B)"
end
--- a/src/ZF/ex/Mutil.thy Fri Jun 14 12:37:21 1996 +0200
+++ b/src/ZF/ex/Mutil.thy Mon Jun 17 16:50:08 1996 +0200
@@ -12,7 +12,6 @@
consts
domino :: i
tiling :: i=>i
- evnodd :: [i,i]=>i
inductive
domains "domino" <= "Pow(nat*nat)"
@@ -30,7 +29,8 @@
type_intrs "[empty_subsetI, Union_upper, Un_least, PowI]"
type_elims "[make_elim PowD]"
-defs
- evnodd_def "evnodd(A,b) == {z:A. EX i j. z=<i,j> & (i#+j) mod 2 = b}"
+constdefs
+ evnodd :: [i,i]=>i
+ "evnodd(A,b) == {z:A. EX i j. z=<i,j> & (i#+j) mod 2 = b}"
end