src/HOL/Real/PNat.thy
author kleing
Tue, 13 May 2003 08:59:21 +0200
changeset 14024 213dcc39358f
parent 12018 ec054019c910
permissions -rw-r--r--
HOL-Real -> HOL-Complex
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     1
(*  Title       : PNat.thy
7219
4e3f386c2e37 inserted Id: lines
paulson
parents: 7077
diff changeset
     2
    ID          : $Id$
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     3
    Author      : Jacques D. Fleuriot
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     4
    Copyright   : 1998  University of Cambridge
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     5
    Description : The positive naturals
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     6
*) 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     7
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     8
8856
435187ffc64e fixed theory deps;
wenzelm
parents: 7562
diff changeset
     9
PNat = Main +
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    10
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    11
typedef
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11464
diff changeset
    12
  pnat = "lfp(%X. {Suc 0} Un Suc`X)"   (lfp_def)
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    13
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    14
instance
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
    15
   pnat :: {ord, one, plus, times}
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    16
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    17
consts
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    18
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    19
  pSuc       :: pnat => pnat
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    20
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    21
constdefs
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    22
  
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 5078
diff changeset
    23
  pnat_of_nat  :: nat => pnat           
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 5078
diff changeset
    24
  "pnat_of_nat n     == Abs_pnat(n + 1)"
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    25
 
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    26
defs
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    27
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 5078
diff changeset
    28
  pnat_one_def      
12018
ec054019c910 Numerals and simprocs for types real and hypreal. The abstract
paulson
parents: 11701
diff changeset
    29
       "1 == Abs_pnat(Suc 0)"
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 5078
diff changeset
    30
  pnat_Suc_def      
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 5078
diff changeset
    31
       "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    32
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    33
  pnat_add_def
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    34
       "x + y == Abs_pnat(Rep_pnat(x) +  Rep_pnat(y))"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    35
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    36
  pnat_mult_def
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    37
       "x * y == Abs_pnat(Rep_pnat(x) * Rep_pnat(y))"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    38
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 5078
diff changeset
    39
  pnat_less_def
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    40
       "x < (y::pnat) == Rep_pnat(x) < Rep_pnat(y)"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    41
7077
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names;
paulson
parents: 5078
diff changeset
    42
  pnat_le_def
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    43
       "x <= (y::pnat) ==  ~(y < x)"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    44
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    45
end