Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Quot/NPAIR.thy
author wenzelm
Sun, 31 Oct 1999 20:11:23 +0100
changeset 7990 0a604b2fc2b1
parent 5184 9b8547a9496a
child 8793 a735b1e74f3a
permissions -rw-r--r--
updated;

(*  Title:      HOL/Quot/NPAIR.thy
    ID:         $Id$
    Author:     Oscar Slotosch
    Copyright   1997 Technische Universitaet Muenchen

Example: define a PER on pairs of natural numbers (with embedding)

*)
NPAIR = PER + Datatype + (* representation for rational numbers *)

datatype NP = abs_NP "(nat * nat)"

consts	rep_NP :: "NP => nat * nat"

defs    rep_NP_def "rep_NP x == (case x of abs_NP y => y)"

(* NPAIR (continued) *)
defs	per_NP_def 
  "eqv ==(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"

(* for proves of this rule see [Slo97diss] *)
rules
	per_trans_NP	"[| eqv (x::NP) y;eqv y z |] ==> eqv x z"
end
isabelle