Nat.thy
changeset 0 7949f97df77a
child 51 934a58983311
equal deleted inserted replaced
-1:000000000000 0:7949f97df77a
       
     1 (*  Title: 	HOL/nat
       
     2     ID:         $Id$
       
     3     Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
       
     4     Copyright   1991  University of Cambridge
       
     5 
       
     6 Definition of types ind and nat.
       
     7 
       
     8 Type nat is defined as a set Nat over type ind.
       
     9 *)
       
    10 
       
    11 Nat = WF +
       
    12 types ind,nat 0
       
    13 arities ind,nat :: term
       
    14         nat :: ord
       
    15 
       
    16 consts
       
    17   Zero_Rep	:: "ind"
       
    18   Suc_Rep	:: "ind => ind"
       
    19   Nat		:: "ind set"
       
    20   Rep_Nat	:: "nat => ind"
       
    21   Abs_Nat	:: "ind => nat"
       
    22   Suc		:: "nat => nat"
       
    23   nat_case	:: "[nat, 'a, nat=>'a] =>'a"
       
    24   pred_nat	:: "(nat*nat) set"
       
    25   nat_rec	:: "[nat, 'a, [nat, 'a]=>'a] => 'a"
       
    26   "0"		:: "nat"		("0")
       
    27 
       
    28 rules
       
    29  (*the axiom of infinity in 2 parts*)
       
    30   inj_Suc_Rep  		"inj(Suc_Rep)"
       
    31   Suc_Rep_not_Zero_Rep	"~(Suc_Rep(x) = Zero_Rep)"
       
    32   Nat_def		"Nat == lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"
       
    33     (*faking a type definition...*)
       
    34   Rep_Nat 		"Rep_Nat(n): Nat"
       
    35   Rep_Nat_inverse 	"Abs_Nat(Rep_Nat(n)) = n"
       
    36   Abs_Nat_inverse 	"i: Nat ==> Rep_Nat(Abs_Nat(i)) = i"
       
    37     (*defining the abstract constants*)
       
    38   Zero_def  		"0 == Abs_Nat(Zero_Rep)"
       
    39   Suc_def  		"Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
       
    40      (*nat operations and recursion*)
       
    41   nat_case_def	"nat_case == (%n a f. @z.  (n=0 --> z=a)  \
       
    42 \                                          & (!x. n=Suc(x) --> z=f(x)))"
       
    43   pred_nat_def 	"pred_nat == {p. ? n. p = <n, Suc(n)>}"
       
    44 
       
    45   less_def "m<n == <m,n>:trancl(pred_nat)"
       
    46 
       
    47   le_def   "m<=n::nat == ~(n<m)"
       
    48 
       
    49   nat_rec_def	"nat_rec(n,c,d) == wfrec(pred_nat, n,   \
       
    50 \                        %l g. nat_case(l, c, %m. d(m,g(m))))"
       
    51 end