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 slotosch
Fri, 04 Apr 1997 16:03:11 +0200
changeset 2906 171dedbc9bdb
child 3842 b55686a7b22c
permissions -rw-r--r--
Example for higher order quotients: Fractionals

(*  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 = Arith + Prod + PER +  (* representation for rational numbers *)

types np = "(nat * nat)" (* is needed for datatype *)

datatype NP = abs_NP np

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