src/HOL/Integ/IntDef.thy
author wenzelm
Fri, 05 Oct 2001 21:52:39 +0200
changeset 11701 3d51fbf81c17
parent 11451 8abfb4f7bd02
child 11713 883d559b0b8c
permissions -rw-r--r--
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
     1
(*  Title:      IntDef.thy
691c70898518 new files in Integ
paulson
parents:
diff changeset
     2
    ID:         $Id$
691c70898518 new files in Integ
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
691c70898518 new files in Integ
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
691c70898518 new files in Integ
paulson
parents:
diff changeset
     5
691c70898518 new files in Integ
paulson
parents:
diff changeset
     6
The integers as equivalence classes over nat*nat.
691c70898518 new files in Integ
paulson
parents:
diff changeset
     7
*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
     8
11451
8abfb4f7bd02 partial restructuring to reduce dependence on Axiom of Choice
paulson
parents: 10834
diff changeset
     9
IntDef = Equiv + NatArith + 
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    10
constdefs
691c70898518 new files in Integ
paulson
parents:
diff changeset
    11
  intrel      :: "((nat * nat) * (nat * nat)) set"
9392
c8e6529cc082 changed / to // for quotienting
paulson
parents: 8937
diff changeset
    12
  "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    13
691c70898518 new files in Integ
paulson
parents:
diff changeset
    14
typedef (Integ)
9392
c8e6529cc082 changed / to // for quotienting
paulson
parents: 8937
diff changeset
    15
  int = "UNIV//intrel"            (Equiv.quotient_def)
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    16
691c70898518 new files in Integ
paulson
parents:
diff changeset
    17
instance
8937
7328d7c8d201 defining 0::int to be (int 0)
paulson
parents: 7375
diff changeset
    18
  int :: {ord, zero, plus, times, minus}
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    19
691c70898518 new files in Integ
paulson
parents:
diff changeset
    20
defs
691c70898518 new files in Integ
paulson
parents:
diff changeset
    21
  zminus_def
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
    22
    "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel``{(y,x)})"
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    23
691c70898518 new files in Integ
paulson
parents:
diff changeset
    24
constdefs
691c70898518 new files in Integ
paulson
parents:
diff changeset
    25
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
    26
  int :: nat => int
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
    27
  "int m == Abs_Integ(intrel `` {(m,0)})"
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    28
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
    29
  neg   :: int => bool
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
    30
  "neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    31
691c70898518 new files in Integ
paulson
parents:
diff changeset
    32
  (*For simplifying equalities*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
    33
  iszero :: int => bool
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
    34
  "iszero z == z = int 0"
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    35
  
9392
c8e6529cc082 changed / to // for quotienting
paulson
parents: 8937
diff changeset
    36
defs (*of overloaded constants*)
c8e6529cc082 changed / to // for quotienting
paulson
parents: 8937
diff changeset
    37
  
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11451
diff changeset
    38
  Zero_int_def      "0 == int 0"
8937
7328d7c8d201 defining 0::int to be (int 0)
paulson
parents: 7375
diff changeset
    39
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    40
  zadd_def
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
    41
   "z + w == 
7375
2cb340e66d15 tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents: 7127
diff changeset
    42
       Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
    43
		 intrel``{(x1+x2, y1+y2)})"
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    44
7127
48e235179ffb added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents: 5594
diff changeset
    45
  zdiff_def "z - (w::int) == z + (-w)"
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    46
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
    47
  zless_def "z<w == neg(z - w)"
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    48
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
    49
  zle_def   "z <= (w::int) == ~(w < z)"
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    50
691c70898518 new files in Integ
paulson
parents:
diff changeset
    51
  zmult_def
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
    52
   "z * w == 
7375
2cb340e66d15 tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents: 7127
diff changeset
    53
       Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
    54
		 intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    55
691c70898518 new files in Integ
paulson
parents:
diff changeset
    56
end