src/HOL/Nat.thy
changeset 972 e61b058d58d2
parent 923 ff1574a81019
child 1151 c820b3cc3df0
equal deleted inserted replaced
971:f4815812665b 972:e61b058d58d2
    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))))"