src/HOL/Nat.thy
 changeset 1151 c820b3cc3df0 parent 972 e61b058d58d2 child 1370 7361ac9b024d
equal 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`