src/ZF/ex/Integ.thy
author lcp
Thu May 04 02:02:54 1995 +0200 (1995-05-04)
changeset 1110 756aa2e81f6e
parent 753 ec86863e87c8
child 1155 928a16e02f9f
permissions -rw-r--r--
Changed some definitions and proofs to use pattern-matching.
     1 (*  Title: 	ZF/ex/integ.thy
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 The integers as equivalence classes over nat*nat.
     7 *)
     8 
     9 Integ = EquivClass + Arith +
    10 consts
    11     intrel,integ::      "i"
    12     znat	::	"i=>i"		("$# _" [80] 80)
    13     zminus	::	"i=>i"		("$~ _" [80] 80)
    14     znegative	::	"i=>o"
    15     zmagnitude	::	"i=>i"
    16     "$*"        ::      "[i,i]=>i"      (infixl 70)
    17     "$'/"       ::      "[i,i]=>i"      (infixl 70) 
    18     "$'/'/"     ::      "[i,i]=>i"      (infixl 70)
    19     "$+"	::      "[i,i]=>i"      (infixl 65)
    20     "$-"        ::      "[i,i]=>i"      (infixl 65)
    21     "$<"	:: 	"[i,i]=>o"  	(infixl 50)
    22 
    23 defs
    24 
    25     intrel_def
    26      "intrel == {p:(nat*nat)*(nat*nat). 		\
    27 \        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    28 
    29     integ_def   "integ == (nat*nat)/intrel"
    30     
    31     znat_def	"$# m == intrel `` {<m,0>}"
    32     
    33     zminus_def	"$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
    34     
    35     znegative_def
    36 	"znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
    37     
    38     zmagnitude_def
    39 	"zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
    40     
    41     (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
    42       Perhaps a "curried" or even polymorphic congruent predicate would be
    43       better.*)
    44     zadd_def
    45      "Z1 $+ Z2 == \
    46 \       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 \
    47 \                           in intrel``{<x1#+x2, y1#+y2>}"
    48     
    49     zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
    50     zless_def	"Z1 $< Z2 == znegative(Z1 $- Z2)"
    51     
    52     (*This illustrates the primitive form of definitions (no patterns)*)
    53     zmult_def
    54      "Z1 $* Z2 == \
    55 \       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        \
    56 \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    57     
    58  end