src/HOL/Nat.thy
changeset 1531 e5eb247ad13c
parent 1475 7f5a4cd08209
child 1540 eacaa07e9078
     1.1 --- a/src/HOL/Nat.thy	Mon Mar 04 12:28:48 1996 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Mar 04 14:37:33 1996 +0100
     1.3 @@ -43,11 +43,13 @@
     1.4  (* abstract constants and syntax *)
     1.5  
     1.6  consts
     1.7 -  "0"           :: nat                ("0")
     1.8 -  Suc           :: nat => nat
     1.9 -  nat_case      :: ['a, nat => 'a, nat] => 'a
    1.10 -  pred_nat      :: "(nat * nat) set"
    1.11 -  nat_rec       :: [nat, 'a, [nat, 'a] => 'a] => 'a
    1.12 +  "0"       :: nat                ("0")
    1.13 +  Suc       :: nat => nat
    1.14 +  nat_case  :: ['a, nat => 'a, nat] => 'a
    1.15 +  pred_nat  :: "(nat * nat) set"
    1.16 +  nat_rec   :: [nat, 'a, [nat, 'a] => 'a] => 'a
    1.17 +
    1.18 +  Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    1.19  
    1.20  translations
    1.21    "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
    1.22 @@ -61,9 +63,13 @@
    1.23                                          & (!x. n=Suc(x) --> z=f(x))"
    1.24    pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
    1.25  
    1.26 -  less_def "m<n == (m,n):trancl(pred_nat)"
    1.27 +  less_def      "m<n == (m,n):trancl(pred_nat)"
    1.28 +
    1.29 +  le_def        "m<=(n::nat) == ~(n<m)"
    1.30  
    1.31 -  le_def   "m<=(n::nat) == ~(n<m)"
    1.32 +  nat_rec_def   "nat_rec n c d ==
    1.33 +		 wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
    1.34 +  (*least number operator*)
    1.35 +  Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
    1.36  
    1.37 -nat_rec_def"nat_rec n c d == wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
    1.38  end