src/HOL/Arith.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8970 3ac901561f33
child 9436 62bb04ab4b01
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title:      HOL/Arith.thy
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents: 3308
diff changeset
     6
Arithmetic operators + - and * (for div, mod and dvd, see Divides)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
Arith = Nat +
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
instance
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents: 3308
diff changeset
    12
  nat :: {plus, minus, times, power}
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
4360
40e5c97e988d pred n -> n-1
nipkow
parents: 3366
diff changeset
    14
(* size of a datatype value; overloaded *)
40e5c97e988d pred n -> n-1
nipkow
parents: 3366
diff changeset
    15
consts size :: 'a => nat
1796
c42db9ab8728 Tidied spacing
paulson
parents: 1475
diff changeset
    16
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 4711
diff changeset
    17
primrec
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents: 3308
diff changeset
    18
  add_0    "0 + n = n"
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents: 3308
diff changeset
    19
  add_Suc  "Suc m + n = Suc(m + n)"
2681
93ed51a91622 definitions of +,-,* replaced by primrec definitions
pusch
parents: 2099
diff changeset
    20
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 4711
diff changeset
    21
primrec
3235
351565b7321b The diff laws must be named: we do "Delsimps [diff_Suc];"
paulson
parents: 2887
diff changeset
    22
  diff_0   "m - 0 = m"
4360
40e5c97e988d pred n -> n-1
nipkow
parents: 3366
diff changeset
    23
  diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
40e5c97e988d pred n -> n-1
nipkow
parents: 3366
diff changeset
    24
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 4711
diff changeset
    25
primrec
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents: 3308
diff changeset
    26
  mult_0   "0 * n = 0"
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents: 3308
diff changeset
    27
  mult_Suc "Suc m * n = n + (m * n)"
2681
93ed51a91622 definitions of +,-,* replaced by primrec definitions
pusch
parents: 2099
diff changeset
    28
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    29
end