src/HOL/Nat.thy
changeset 1625 40501958d0f6
parent 1540 eacaa07e9078
child 1660 8cb42cd97579
equal deleted inserted replaced
1624:e2a6102b9369 1625:40501958d0f6
    42 
    42 
    43 (* abstract constants and syntax *)
    43 (* abstract constants and syntax *)
    44 
    44 
    45 consts
    45 consts
    46   "0"       :: nat                ("0")
    46   "0"       :: nat                ("0")
       
    47   "1"       :: nat                ("1")
       
    48   "2"       :: nat                ("2")
    47   Suc       :: nat => nat
    49   Suc       :: nat => nat
    48   nat_case  :: ['a, nat => 'a, nat] => 'a
    50   nat_case  :: ['a, nat => 'a, nat] => 'a
    49   pred_nat  :: "(nat * nat) set"
    51   pred_nat  :: "(nat * nat) set"
    50   nat_rec   :: [nat, 'a, [nat, 'a] => 'a] => 'a
    52   nat_rec   :: [nat, 'a, [nat, 'a] => 'a] => 'a
    51 
    53 
    52   Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    54   Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    53 
    55 
    54 translations
    56 translations
       
    57    "1"  == "Suc(0)"
       
    58    "2"  == "Suc(1)"
    55   "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
    59   "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
    56 
    60 
    57 defs
    61 defs
    58   Zero_def      "0 == Abs_Nat(Zero_Rep)"
    62   Zero_def      "0 == Abs_Nat(Zero_Rep)"
    59   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    63   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"