isabelle: src/HOL/Quot/NPAIR.thy@6e0f23304061 (annotated)

2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	1	(* Title: HOL/Quot/NPAIR.thy
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	2	ID: $Id$
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	3	Author: Oscar Slotosch
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	4	Copyright 1997 Technische Universitaet Muenchen
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	5
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	6	Example: define a PER on pairs of natural numbers (with embedding)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	7
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	8	*)
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 4531 diff changeset	9	NPAIR = PER + Datatype + (* representation for rational numbers *)
2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	10
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 4531 diff changeset	11	datatype NP = abs_NP "(nat * nat)"
2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	12
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	13	consts rep_NP :: "NP => nat * nat"
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	14
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	15	defs rep_NP_def "rep_NP x == (case x of abs_NP y => y)"
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	16
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	17	(* NPAIR (continued) *)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	18	defs per_NP_def
3842 b55686a7b22c fixed dots; wenzelm parents: 2906 diff changeset	19	"eqv ==(%x y. fst(rep_NP x)snd(rep_NP y)=fst(rep_NP y)snd(rep_NP x))"
2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	20
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	21	(* for proves of this rule see [Slo97diss] *)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	22	rules
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	23	per_trans_NP "[\| eqv (x::NP) y;eqv y z \|] ==> eqv x z"
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 4531 diff changeset	24	end

author	wenzelm
	Thu, 16 Mar 2000 00:35:27 +0100
changeset 8490	6e0f23304061
parent 5184	9b8547a9496a
child 8793	a735b1e74f3a
permissions	-rw-r--r--