src/HOL/Quot/NPAIR.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 5184 9b8547a9496a
child 8793 a735b1e74f3a
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Quot/NPAIR.thy
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     Copyright   1997 Technische Universitaet Muenchen
     5 
     6 Example: define a PER on pairs of natural numbers (with embedding)
     7 
     8 *)
     9 NPAIR = PER + Datatype + (* representation for rational numbers *)
    10 
    11 datatype NP = abs_NP "(nat * nat)"
    12 
    13 consts	rep_NP :: "NP => nat * nat"
    14 
    15 defs    rep_NP_def "rep_NP x == (case x of abs_NP y => y)"
    16 
    17 (* NPAIR (continued) *)
    18 defs	per_NP_def 
    19   "eqv ==(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"
    20 
    21 (* for proves of this rule see [Slo97diss] *)
    22 rules
    23 	per_trans_NP	"[| eqv (x::NP) y;eqv y z |] ==> eqv x z"
    24 end