isabelle: src/HOL/Quot/NPAIR.thy@b55686a7b22c (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	*)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	9	NPAIR = Arith + Prod + PER + (* representation for rational numbers *)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	10
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	11	types np = "(nat * nat)" (* is needed for datatype *)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	12
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	13	datatype NP = abs_NP np
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	14
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	15	consts rep_NP :: "NP => nat * nat"
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	16
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	17	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	18
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	19	(* NPAIR (continued) *)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	20	defs per_NP_def
3842 b55686a7b22c fixed dots; wenzelm parents: 2906 diff changeset	21	"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	22
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	23	(* for proves of this rule see [Slo97diss] *)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	24	rules
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	25	per_trans_NP "[\| eqv (x::NP) y;eqv y z \|] ==> eqv x z"
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	26	end

author	wenzelm
	Fri, 10 Oct 1997 19:02:28 +0200
changeset 3842	b55686a7b22c
parent 2906	171dedbc9bdb
child 4531	20a7fddb706a
permissions	-rw-r--r--