src/HOL/Nat.thy
changeset 1151 c820b3cc3df0
parent 972 e61b058d58d2
child 1370 7361ac9b024d
equal deleted inserted replaced
1150:66512c9e6bd6 1151:c820b3cc3df0
    55 defs
    55 defs
    56   Zero_def      "0 == Abs_Nat(Zero_Rep)"
    56   Zero_def      "0 == Abs_Nat(Zero_Rep)"
    57   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    57   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    58 
    58 
    59   (*nat operations and recursion*)
    59   (*nat operations and recursion*)
    60   nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  \
    60   nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
    61 \                                        & (!x. n=Suc(x) --> z=f(x))"
    61                                         & (!x. n=Suc(x) --> z=f(x))"
    62   pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
    62   pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
    63 
    63 
    64   less_def "m<n == (m,n):trancl(pred_nat)"
    64   less_def "m<n == (m,n):trancl(pred_nat)"
    65 
    65 
    66   le_def   "m<=(n::nat) == ~(n<m)"
    66   le_def   "m<=(n::nat) == ~(n<m)"
    67 
    67 
    68   nat_rec_def   "nat_rec n c d == wfrec pred_nat n  \
    68   nat_rec_def   "nat_rec n c d == wfrec pred_nat n  
    69 \                        (nat_case (%g.c) (%m g.(d m (g m))))"
    69                         (nat_case (%g.c) (%m g.(d m (g m))))"
    70 end
    70 end