replaced "rules" by "defs"
authorlcp
Tue Nov 29 00:31:31 1994 +0100 (1994-11-29)
changeset 753ec86863e87c8
parent 752 b89462f9d5f1
child 754 521a6f3ff279
replaced "rules" by "defs"
src/ZF/Arith.thy
src/ZF/Bool.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Epsilon.thy
src/ZF/EquivClass.thy
src/ZF/Fixedpt.thy
src/ZF/IMP/Com.thy
src/ZF/IMP/Denotation.thy
src/ZF/List.thy
src/ZF/Nat.thy
src/ZF/OrderArith.thy
src/ZF/OrderType.thy
src/ZF/Ordinal.thy
src/ZF/Perm.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/Rel.thy
src/ZF/Sum.thy
src/ZF/Trancl.thy
src/ZF/Univ.thy
src/ZF/Zorn.thy
src/ZF/ex/BT.thy
src/ZF/ex/Bin.thy
src/ZF/ex/Comb.thy
src/ZF/ex/Integ.thy
src/ZF/ex/LList.thy
src/ZF/ex/Primrec.thy
src/ZF/ex/PropLog.thy
src/ZF/ex/Ramsey.thy
src/ZF/ex/TF.thy
src/ZF/ex/Term.thy
     1.1 --- a/src/ZF/Arith.thy	Mon Nov 28 19:48:30 1994 +0100
     1.2 +++ b/src/ZF/Arith.thy	Tue Nov 29 00:31:31 1994 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4      "#+" :: "[i,i]=>i"      		(infixl 65)
     1.5      "#-" :: "[i,i]=>i"      		(infixl 65)
     1.6  
     1.7 -rules
     1.8 +defs
     1.9      rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
    1.10  
    1.11      add_def  "m#+n == rec(m, n, %u v.succ(v))"
     2.1 --- a/src/ZF/Bool.thy	Mon Nov 28 19:48:30 1994 +0100
     2.2 +++ b/src/ZF/Bool.thy	Tue Nov 29 00:31:31 1994 +0100
     2.3 @@ -19,7 +19,7 @@
     2.4  translations
     2.5     "1"  == "succ(0)"
     2.6  
     2.7 -rules
     2.8 +defs
     2.9      bool_def	"bool == {0,1}"
    2.10      cond_def	"cond(b,c,d) == if(b=1,c,d)"
    2.11      not_def	"not(b) == cond(b,0,1)"
     3.1 --- a/src/ZF/Cardinal.thy	Mon Nov 28 19:48:30 1994 +0100
     3.2 +++ b/src/ZF/Cardinal.thy	Tue Nov 29 00:31:31 1994 +0100
     3.3 @@ -15,7 +15,7 @@
     3.4  
     3.5    swap       :: "[i,i,i]=>i"     (*not used; useful??*)
     3.6  
     3.7 -rules
     3.8 +defs
     3.9  
    3.10    (*least ordinal operator*)
    3.11    Least_def  "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
     4.1 --- a/src/ZF/CardinalArith.thy	Mon Nov 28 19:48:30 1994 +0100
     4.2 +++ b/src/ZF/CardinalArith.thy	Tue Nov 29 00:31:31 1994 +0100
     4.3 @@ -16,7 +16,7 @@
     4.4    jump_cardinal :: "i=>i"
     4.5    csucc       :: "i=>i"
     4.6  
     4.7 -rules
     4.8 +defs
     4.9  
    4.10    InfCard_def  "InfCard(i) == Card(i) & nat le i"
    4.11  
     5.1 --- a/src/ZF/Epsilon.thy	Mon Nov 28 19:48:30 1994 +0100
     5.2 +++ b/src/ZF/Epsilon.thy	Tue Nov 29 00:31:31 1994 +0100
     5.3 @@ -11,7 +11,7 @@
     5.4      eclose,rank ::      "i=>i"
     5.5      transrec    ::      "[i, [i,i]=>i] =>i"
     5.6  
     5.7 -rules
     5.8 +defs
     5.9    eclose_def	"eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
    5.10    transrec_def	"transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
    5.11    rank_def    	"rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
     6.1 --- a/src/ZF/EquivClass.thy	Mon Nov 28 19:48:30 1994 +0100
     6.2 +++ b/src/ZF/EquivClass.thy	Tue Nov 29 00:31:31 1994 +0100
     6.3 @@ -12,7 +12,7 @@
     6.4      congruent	::	"[i,i=>i]=>o"
     6.5      congruent2  ::      "[i,[i,i]=>i]=>o"
     6.6  
     6.7 -rules
     6.8 +defs
     6.9      quotient_def  "A/r == {r``{x} . x:A}"
    6.10      congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
    6.11  
     7.1 --- a/src/ZF/Fixedpt.thy	Mon Nov 28 19:48:30 1994 +0100
     7.2 +++ b/src/ZF/Fixedpt.thy	Tue Nov 29 00:31:31 1994 +0100
     7.3 @@ -11,7 +11,7 @@
     7.4    bnd_mono    :: "[i,i=>i]=>o"
     7.5    lfp, gfp    :: "[i,i=>i]=>i"
     7.6  
     7.7 -rules
     7.8 +defs
     7.9    (*monotone operator from Pow(D) to itself*)
    7.10    bnd_mono_def 
    7.11        "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))"
     8.1 --- a/src/ZF/IMP/Com.thy	Mon Nov 28 19:48:30 1994 +0100
     8.2 +++ b/src/ZF/IMP/Com.thy	Tue Nov 29 00:31:31 1994 +0100
     8.3 @@ -96,7 +96,7 @@
     8.4  translations
     8.5         "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
     8.6  
     8.7 -rules 
     8.8 +defs 
     8.9  	assign_def	"sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
    8.10  
    8.11  inductive
     9.1 --- a/src/ZF/IMP/Denotation.thy	Mon Nov 28 19:48:30 1994 +0100
     9.2 +++ b/src/ZF/IMP/Denotation.thy	Tue Nov 29 00:31:31 1994 +0100
     9.3 @@ -14,7 +14,7 @@
     9.4    C     :: "i => i"
     9.5    Gamma :: "[i,i,i] => i"
     9.6  
     9.7 -rules
     9.8 +rules	(*NOT definitional*)
     9.9    A_nat_def	"A(N(n)) == (%sigma. n)"
    9.10    A_loc_def	"A(X(x)) == (%sigma. sigma`x)" 
    9.11    A_op1_def	"A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
    10.1 --- a/src/ZF/List.thy	Mon Nov 28 19:48:30 1994 +0100
    10.2 +++ b/src/ZF/List.thy	Tue Nov 29 00:31:31 1994 +0100
    10.3 @@ -39,7 +39,7 @@
    10.4    "[]"          == "Nil"
    10.5  
    10.6  
    10.7 -rules
    10.8 +defs
    10.9  
   10.10    hd_def	"hd(l)	     == list_case(0, %x xs.x, l)"
   10.11    tl_def	"tl(l)       == list_case(Nil, %x xs.xs, l)"
    11.1 --- a/src/ZF/Nat.thy	Mon Nov 28 19:48:30 1994 +0100
    11.2 +++ b/src/ZF/Nat.thy	Tue Nov 29 00:31:31 1994 +0100
    11.3 @@ -12,7 +12,7 @@
    11.4      nat_case    ::      "[i, i=>i, i]=>i"
    11.5      nat_rec     ::      "[i, i, [i,i]=>i]=>i"
    11.6  
    11.7 -rules
    11.8 +defs
    11.9  
   11.10      nat_def     "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
   11.11  
    12.1 --- a/src/ZF/OrderArith.thy	Mon Nov 28 19:48:30 1994 +0100
    12.2 +++ b/src/ZF/OrderArith.thy	Tue Nov 29 00:31:31 1994 +0100
    12.3 @@ -11,7 +11,7 @@
    12.4    radd, rmult      :: "[i,i,i,i]=>i"
    12.5    rvimage          :: "[i,i,i]=>i"
    12.6  
    12.7 -rules
    12.8 +defs
    12.9    (*disjoint sum of two relations; underlies ordinal addition*)
   12.10    radd_def "radd(A,r,B,s) == \
   12.11  \                {z: (A+B) * (A+B).  \
    13.1 --- a/src/ZF/OrderType.thy	Mon Nov 28 19:48:30 1994 +0100
    13.2 +++ b/src/ZF/OrderType.thy	Tue Nov 29 00:31:31 1994 +0100
    13.3 @@ -13,7 +13,7 @@
    13.4    ordermap  :: "[i,i]=>i"
    13.5    ordertype :: "[i,i]=>i"
    13.6  
    13.7 -rules
    13.8 +defs
    13.9    ordermap_def
   13.10        "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
   13.11  
    14.1 --- a/src/ZF/Ordinal.thy	Mon Nov 28 19:48:30 1994 +0100
    14.2 +++ b/src/ZF/Ordinal.thy	Tue Nov 29 00:31:31 1994 +0100
    14.3 @@ -17,12 +17,11 @@
    14.4  translations
    14.5    "x le y"      == "x < succ(y)"
    14.6  
    14.7 -rules
    14.8 +defs
    14.9    Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
   14.10    Transset_def	"Transset(i) == ALL x:i. x<=i"
   14.11    Ord_def     	"Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
   14.12    lt_def        "i<j         == i:j & Ord(j)"
   14.13    Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
   14.14  
   14.15 -
   14.16  end
    15.1 --- a/src/ZF/Perm.thy	Mon Nov 28 19:48:30 1994 +0100
    15.2 +++ b/src/ZF/Perm.thy	Tue Nov 29 00:31:31 1994 +0100
    15.3 @@ -15,7 +15,7 @@
    15.4      id  	::      "i=>i"
    15.5      inj,surj,bij::      "[i,i]=>i"
    15.6  
    15.7 -rules
    15.8 +defs
    15.9  
   15.10      (*composition of relations and functions; NOT Suppes's relative product*)
   15.11      comp_def	"r O s == {xz : domain(s)*range(r) . \
    16.1 --- a/src/ZF/QPair.thy	Mon Nov 28 19:48:30 1994 +0100
    16.2 +++ b/src/ZF/QPair.thy	Tue Nov 29 00:31:31 1994 +0100
    16.3 @@ -29,7 +29,7 @@
    16.4    "QSUM x:A. B"  => "QSigma(A, %x. B)"
    16.5    "A <*> B"      => "QSigma(A, _K(B))"
    16.6  
    16.7 -rules
    16.8 +defs
    16.9    QPair_def       "<a;b> == a+b"
   16.10    qsplit_def      "qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)"
   16.11    qfsplit_def     "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)"
    17.1 --- a/src/ZF/QUniv.thy	Mon Nov 28 19:48:30 1994 +0100
    17.2 +++ b/src/ZF/QUniv.thy	Tue Nov 29 00:31:31 1994 +0100
    17.3 @@ -10,7 +10,7 @@
    17.4  consts
    17.5      quniv        :: "i=>i"
    17.6  
    17.7 -rules
    17.8 +defs
    17.9      quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
   17.10  
   17.11  end
    18.1 --- a/src/ZF/Rel.thy	Mon Nov 28 19:48:30 1994 +0100
    18.2 +++ b/src/ZF/Rel.thy	Tue Nov 29 00:31:31 1994 +0100
    18.3 @@ -12,7 +12,7 @@
    18.4      sym,asym,antisym,trans :: "i=>o"
    18.5      trans_on               :: "[i,i]=>o"	("trans[_]'(_')")
    18.6  
    18.7 -rules
    18.8 +defs
    18.9    refl_def     "refl(A,r) == (ALL x: A. <x,x> : r)"
   18.10  
   18.11    irrefl_def   "irrefl(A,r) == ALL x: A. <x,x> ~: r"
    19.1 --- a/src/ZF/Sum.thy	Mon Nov 28 19:48:30 1994 +0100
    19.2 +++ b/src/ZF/Sum.thy	Tue Nov 29 00:31:31 1994 +0100
    19.3 @@ -14,7 +14,7 @@
    19.4      case        :: "[i=>i, i=>i, i]=>i"
    19.5      Part        :: "[i,i=>i] => i"
    19.6  
    19.7 -rules
    19.8 +defs
    19.9      sum_def     "A+B == {0}*A Un {1}*B"
   19.10      Inl_def     "Inl(a) == <0,a>"
   19.11      Inr_def     "Inr(b) == <1,b>"
    20.1 --- a/src/ZF/Trancl.thy	Mon Nov 28 19:48:30 1994 +0100
    20.2 +++ b/src/ZF/Trancl.thy	Tue Nov 29 00:31:31 1994 +0100
    20.3 @@ -11,7 +11,7 @@
    20.4      rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
    20.5      trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
    20.6  
    20.7 -rules
    20.8 +defs
    20.9      rtrancl_def	"r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
   20.10      trancl_def  "r^+ == r O r^*"
   20.11  end
    21.1 --- a/src/ZF/Univ.thy	Mon Nov 28 19:48:30 1994 +0100
    21.2 +++ b/src/ZF/Univ.thy	Tue Nov 29 00:31:31 1994 +0100
    21.3 @@ -21,7 +21,7 @@
    21.4  translations
    21.5      "Vset(x)"   == 	"Vfrom(0,x)"
    21.6  
    21.7 -rules
    21.8 +defs
    21.9      Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
   21.10  
   21.11      Vrec_def
    22.1 --- a/src/ZF/Zorn.thy	Mon Nov 28 19:48:30 1994 +0100
    22.2 +++ b/src/ZF/Zorn.thy	Tue Nov 29 00:31:31 1994 +0100
    22.3 @@ -19,7 +19,7 @@
    22.4    chain, maxchain :: "i=>i"
    22.5    super           :: "[i,i]=>i"
    22.6  
    22.7 -rules
    22.8 +defs
    22.9    Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
   22.10    increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
   22.11  
    23.1 --- a/src/ZF/ex/BT.thy	Mon Nov 28 19:48:30 1994 +0100
    23.2 +++ b/src/ZF/ex/BT.thy	Tue Nov 29 00:31:31 1994 +0100
    23.3 @@ -18,7 +18,7 @@
    23.4  datatype
    23.5    "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
    23.6    
    23.7 -rules
    23.8 +defs
    23.9    bt_rec_def
   23.10      "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
   23.11  
    24.1 --- a/src/ZF/ex/Bin.thy	Mon Nov 28 19:48:30 1994 +0100
    24.2 +++ b/src/ZF/ex/Bin.thy	Tue Nov 29 00:31:31 1994 +0100
    24.3 @@ -23,7 +23,7 @@
    24.4          | "$$" ("w: bin", "b: bool")    (infixl 60)
    24.5    type_intrs "[bool_into_univ]"
    24.6    
    24.7 -rules
    24.8 +defs
    24.9  
   24.10    bin_rec_def
   24.11        "bin_rec(z,a,b,h) == \
    25.1 --- a/src/ZF/ex/Comb.thy	Mon Nov 28 19:48:30 1994 +0100
    25.2 +++ b/src/ZF/ex/Comb.thy	Tue Nov 29 00:31:31 1994 +0100
    25.3 @@ -71,7 +71,7 @@
    25.4    diamond   :: "i => o"
    25.5    I         :: "i"
    25.6  
    25.7 -rules
    25.8 +defs
    25.9  
   25.10    diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
   25.11  \                            (ALL y'. <x,y'>:r --> \
    26.1 --- a/src/ZF/ex/Integ.thy	Mon Nov 28 19:48:30 1994 +0100
    26.2 +++ b/src/ZF/ex/Integ.thy	Tue Nov 29 00:31:31 1994 +0100
    26.3 @@ -20,7 +20,7 @@
    26.4      "$-"        ::      "[i,i]=>i"      (infixl 65)
    26.5      "$<"	:: 	"[i,i]=>o"  	(infixl 50)
    26.6  
    26.7 -rules
    26.8 +defs
    26.9  
   26.10      intrel_def
   26.11       "intrel == {p:(nat*nat)*(nat*nat). 		\
    27.1 --- a/src/ZF/ex/LList.thy	Mon Nov 28 19:48:30 1994 +0100
    27.2 +++ b/src/ZF/ex/LList.thy	Tue Nov 29 00:31:31 1994 +0100
    27.3 @@ -43,9 +43,10 @@
    27.4    lconst   :: "i => i"
    27.5    flip     :: "i => i"
    27.6  
    27.7 -rules
    27.8 +defs
    27.9    lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
   27.10  
   27.11 +rules
   27.12    flip_LNil   "flip(LNil) = LNil"
   27.13  
   27.14    flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
    28.1 --- a/src/ZF/ex/Primrec.thy	Mon Nov 28 19:48:30 1994 +0100
    28.2 +++ b/src/ZF/ex/Primrec.thy	Tue Nov 29 00:31:31 1994 +0100
    28.3 @@ -28,7 +28,7 @@
    28.4  translations
    28.5    "ack(x,y)"  == "ACK(x) ` [y]"
    28.6  
    28.7 -rules
    28.8 +defs
    28.9  
   28.10    SC_def    "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
   28.11  
    29.1 --- a/src/ZF/ex/PropLog.thy	Mon Nov 28 19:48:30 1994 +0100
    29.2 +++ b/src/ZF/ex/PropLog.thy	Tue Nov 29 00:31:31 1994 +0100
    29.3 @@ -44,7 +44,7 @@
    29.4    "|="     :: "[i,i] => o"    			(infixl 50)
    29.5    hyps     :: "[i,i] => i"
    29.6  
    29.7 -rules
    29.8 +defs
    29.9  
   29.10    prop_rec_def
   29.11     "prop_rec(p,b,c,h) == \
    30.1 --- a/src/ZF/ex/Ramsey.thy	Mon Nov 28 19:48:30 1994 +0100
    30.2 +++ b/src/ZF/ex/Ramsey.thy	Tue Nov 29 00:31:31 1994 +0100
    30.3 @@ -24,7 +24,7 @@
    30.4    Atleast     		:: "[i,i]=>o"
    30.5    Clique,Indept,Ramsey	:: "[i,i,i]=>o"
    30.6  
    30.7 -rules
    30.8 +defs
    30.9  
   30.10    Symmetric_def
   30.11      "Symmetric(E) == (ALL x y. <x,y>:E --> <y,x>:E)"
    31.1 --- a/src/ZF/ex/TF.thy	Mon Nov 28 19:48:30 1994 +0100
    31.2 +++ b/src/ZF/ex/TF.thy	Tue Nov 29 00:31:31 1994 +0100
    31.3 @@ -22,7 +22,7 @@
    31.4  and
    31.5    "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
    31.6  
    31.7 -rules
    31.8 +defs
    31.9    TF_rec_def
   31.10      "TF_rec(z,b,c,d) == Vrec(z,  			\
   31.11  \      %z r. tree_forest_case(%x f. b(x, f, r`f), 	\
    32.1 --- a/src/ZF/ex/Term.thy	Mon Nov 28 19:48:30 1994 +0100
    32.2 +++ b/src/ZF/ex/Term.thy	Tue Nov 29 00:31:31 1994 +0100
    32.3 @@ -26,7 +26,7 @@
    32.4      type_intrs  "[list_univ RS subsetD]"
    32.5  *)
    32.6  
    32.7 -rules
    32.8 +defs
    32.9    term_rec_def
   32.10     "term_rec(t,d) == \
   32.11  \   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"