--- a/src/ZF/Arith.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Arith.thy Tue Nov 29 00:31:31 1994 +0100
@@ -15,7 +15,7 @@
"#+" :: "[i,i]=>i" (infixl 65)
"#-" :: "[i,i]=>i" (infixl 65)
-rules
+defs
rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
add_def "m#+n == rec(m, n, %u v.succ(v))"
--- a/src/ZF/Bool.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Bool.thy Tue Nov 29 00:31:31 1994 +0100
@@ -19,7 +19,7 @@
translations
"1" == "succ(0)"
-rules
+defs
bool_def "bool == {0,1}"
cond_def "cond(b,c,d) == if(b=1,c,d)"
not_def "not(b) == cond(b,0,1)"
--- a/src/ZF/Cardinal.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Cardinal.thy Tue Nov 29 00:31:31 1994 +0100
@@ -15,7 +15,7 @@
swap :: "[i,i,i]=>i" (*not used; useful??*)
-rules
+defs
(*least ordinal operator*)
Least_def "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
--- a/src/ZF/CardinalArith.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/CardinalArith.thy Tue Nov 29 00:31:31 1994 +0100
@@ -16,7 +16,7 @@
jump_cardinal :: "i=>i"
csucc :: "i=>i"
-rules
+defs
InfCard_def "InfCard(i) == Card(i) & nat le i"
--- a/src/ZF/Epsilon.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Epsilon.thy Tue Nov 29 00:31:31 1994 +0100
@@ -11,7 +11,7 @@
eclose,rank :: "i=>i"
transrec :: "[i, [i,i]=>i] =>i"
-rules
+defs
eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
--- a/src/ZF/EquivClass.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/EquivClass.thy Tue Nov 29 00:31:31 1994 +0100
@@ -12,7 +12,7 @@
congruent :: "[i,i=>i]=>o"
congruent2 :: "[i,[i,i]=>i]=>o"
-rules
+defs
quotient_def "A/r == {r``{x} . x:A}"
congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
--- a/src/ZF/Fixedpt.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Fixedpt.thy Tue Nov 29 00:31:31 1994 +0100
@@ -11,7 +11,7 @@
bnd_mono :: "[i,i=>i]=>o"
lfp, gfp :: "[i,i=>i]=>i"
-rules
+defs
(*monotone operator from Pow(D) to itself*)
bnd_mono_def
"bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))"
--- a/src/ZF/IMP/Com.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/IMP/Com.thy Tue Nov 29 00:31:31 1994 +0100
@@ -96,7 +96,7 @@
translations
"<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
-rules
+defs
assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
inductive
--- a/src/ZF/IMP/Denotation.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/IMP/Denotation.thy Tue Nov 29 00:31:31 1994 +0100
@@ -14,7 +14,7 @@
C :: "i => i"
Gamma :: "[i,i,i] => i"
-rules
+rules (*NOT definitional*)
A_nat_def "A(N(n)) == (%sigma. n)"
A_loc_def "A(X(x)) == (%sigma. sigma`x)"
A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
--- a/src/ZF/List.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/List.thy Tue Nov 29 00:31:31 1994 +0100
@@ -39,7 +39,7 @@
"[]" == "Nil"
-rules
+defs
hd_def "hd(l) == list_case(0, %x xs.x, l)"
tl_def "tl(l) == list_case(Nil, %x xs.xs, l)"
--- a/src/ZF/Nat.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Nat.thy Tue Nov 29 00:31:31 1994 +0100
@@ -12,7 +12,7 @@
nat_case :: "[i, i=>i, i]=>i"
nat_rec :: "[i, i, [i,i]=>i]=>i"
-rules
+defs
nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
--- a/src/ZF/OrderArith.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/OrderArith.thy Tue Nov 29 00:31:31 1994 +0100
@@ -11,7 +11,7 @@
radd, rmult :: "[i,i,i,i]=>i"
rvimage :: "[i,i,i]=>i"
-rules
+defs
(*disjoint sum of two relations; underlies ordinal addition*)
radd_def "radd(A,r,B,s) == \
\ {z: (A+B) * (A+B). \
--- a/src/ZF/OrderType.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/OrderType.thy Tue Nov 29 00:31:31 1994 +0100
@@ -13,7 +13,7 @@
ordermap :: "[i,i]=>i"
ordertype :: "[i,i]=>i"
-rules
+defs
ordermap_def
"ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
--- a/src/ZF/Ordinal.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Ordinal.thy Tue Nov 29 00:31:31 1994 +0100
@@ -17,12 +17,11 @@
translations
"x le y" == "x < succ(y)"
-rules
+defs
Memrel_def "Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }"
Transset_def "Transset(i) == ALL x:i. x<=i"
Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))"
lt_def "i<j == i:j & Ord(j)"
Limit_def "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
-
end
--- a/src/ZF/Perm.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Perm.thy Tue Nov 29 00:31:31 1994 +0100
@@ -15,7 +15,7 @@
id :: "i=>i"
inj,surj,bij:: "[i,i]=>i"
-rules
+defs
(*composition of relations and functions; NOT Suppes's relative product*)
comp_def "r O s == {xz : domain(s)*range(r) . \
--- a/src/ZF/QPair.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/QPair.thy Tue Nov 29 00:31:31 1994 +0100
@@ -29,7 +29,7 @@
"QSUM x:A. B" => "QSigma(A, %x. B)"
"A <*> B" => "QSigma(A, _K(B))"
-rules
+defs
QPair_def "<a;b> == a+b"
qsplit_def "qsplit(c,p) == THE y. EX a b. p=<a;b> & y=c(a,b)"
qfsplit_def "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)"
--- a/src/ZF/QUniv.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/QUniv.thy Tue Nov 29 00:31:31 1994 +0100
@@ -10,7 +10,7 @@
consts
quniv :: "i=>i"
-rules
+defs
quniv_def "quniv(A) == Pow(univ(eclose(A)))"
end
--- a/src/ZF/Rel.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Rel.thy Tue Nov 29 00:31:31 1994 +0100
@@ -12,7 +12,7 @@
sym,asym,antisym,trans :: "i=>o"
trans_on :: "[i,i]=>o" ("trans[_]'(_')")
-rules
+defs
refl_def "refl(A,r) == (ALL x: A. <x,x> : r)"
irrefl_def "irrefl(A,r) == ALL x: A. <x,x> ~: r"
--- a/src/ZF/Sum.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Sum.thy Tue Nov 29 00:31:31 1994 +0100
@@ -14,7 +14,7 @@
case :: "[i=>i, i=>i, i]=>i"
Part :: "[i,i=>i] => i"
-rules
+defs
sum_def "A+B == {0}*A Un {1}*B"
Inl_def "Inl(a) == <0,a>"
Inr_def "Inr(b) == <1,b>"
--- a/src/ZF/Trancl.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Trancl.thy Tue Nov 29 00:31:31 1994 +0100
@@ -11,7 +11,7 @@
rtrancl :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*)
trancl :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*)
-rules
+defs
rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
trancl_def "r^+ == r O r^*"
end
--- a/src/ZF/Univ.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Univ.thy Tue Nov 29 00:31:31 1994 +0100
@@ -21,7 +21,7 @@
translations
"Vset(x)" == "Vfrom(0,x)"
-rules
+defs
Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
Vrec_def
--- a/src/ZF/Zorn.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Zorn.thy Tue Nov 29 00:31:31 1994 +0100
@@ -19,7 +19,7 @@
chain, maxchain :: "i=>i"
super :: "[i,i]=>i"
-rules
+defs
Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
--- a/src/ZF/ex/BT.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/BT.thy Tue Nov 29 00:31:31 1994 +0100
@@ -18,7 +18,7 @@
datatype
"bt(A)" = Lf | Br ("a: A", "t1: bt(A)", "t2: bt(A)")
-rules
+defs
bt_rec_def
"bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
--- a/src/ZF/ex/Bin.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Bin.thy Tue Nov 29 00:31:31 1994 +0100
@@ -23,7 +23,7 @@
| "$$" ("w: bin", "b: bool") (infixl 60)
type_intrs "[bool_into_univ]"
-rules
+defs
bin_rec_def
"bin_rec(z,a,b,h) == \
--- a/src/ZF/ex/Comb.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Comb.thy Tue Nov 29 00:31:31 1994 +0100
@@ -71,7 +71,7 @@
diamond :: "i => o"
I :: "i"
-rules
+defs
diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
\ (ALL y'. <x,y'>:r --> \
--- a/src/ZF/ex/Integ.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Integ.thy Tue Nov 29 00:31:31 1994 +0100
@@ -20,7 +20,7 @@
"$-" :: "[i,i]=>i" (infixl 65)
"$<" :: "[i,i]=>o" (infixl 50)
-rules
+defs
intrel_def
"intrel == {p:(nat*nat)*(nat*nat). \
--- a/src/ZF/ex/LList.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/LList.thy Tue Nov 29 00:31:31 1994 +0100
@@ -43,9 +43,10 @@
lconst :: "i => i"
flip :: "i => i"
-rules
+defs
lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
+rules
flip_LNil "flip(LNil) = LNil"
flip_LCons "[| x:bool; l: llist(bool) |] ==> \
--- a/src/ZF/ex/Primrec.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Primrec.thy Tue Nov 29 00:31:31 1994 +0100
@@ -28,7 +28,7 @@
translations
"ack(x,y)" == "ACK(x) ` [y]"
-rules
+defs
SC_def "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
--- a/src/ZF/ex/PropLog.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/PropLog.thy Tue Nov 29 00:31:31 1994 +0100
@@ -44,7 +44,7 @@
"|=" :: "[i,i] => o" (infixl 50)
hyps :: "[i,i] => i"
-rules
+defs
prop_rec_def
"prop_rec(p,b,c,h) == \
--- a/src/ZF/ex/Ramsey.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Ramsey.thy Tue Nov 29 00:31:31 1994 +0100
@@ -24,7 +24,7 @@
Atleast :: "[i,i]=>o"
Clique,Indept,Ramsey :: "[i,i,i]=>o"
-rules
+defs
Symmetric_def
"Symmetric(E) == (ALL x y. <x,y>:E --> <y,x>:E)"
--- a/src/ZF/ex/TF.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/TF.thy Tue Nov 29 00:31:31 1994 +0100
@@ -22,7 +22,7 @@
and
"forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)")
-rules
+defs
TF_rec_def
"TF_rec(z,b,c,d) == Vrec(z, \
\ %z r. tree_forest_case(%x f. b(x, f, r`f), \
--- a/src/ZF/ex/Term.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Term.thy Tue Nov 29 00:31:31 1994 +0100
@@ -26,7 +26,7 @@
type_intrs "[list_univ RS subsetD]"
*)
-rules
+defs
term_rec_def
"term_rec(t,d) == \
\ Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"