isabelle: src/HOL/Real/RealDef.thy@c5fc121c2067 (annotated)

5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	1	(* Title : Real/RealDef.thy
7219 4e3f386c2e37 inserted Id: lines paulson parents: 7127 diff changeset	2	ID : $Id$
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	3	Author : Jacques D. Fleuriot
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	4	Copyright : 1998 University of Cambridge
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	5	Description : The reals
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	6	*)
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	7
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	8	RealDef = PReal +
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	9
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	10	constdefs
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	11	realrel :: "((preal * preal) * (preal * preal)) set"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	12	"realrel == {p. ? x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	13
9391 a6ab3a442da6 changed / to // for quotienting; general tidying paulson parents: 9365 diff changeset	14	typedef real = "UNIV//realrel" (Equiv.quotient_def)
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	15
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	16
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	17	instance
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 7219 diff changeset	18	real :: {ord, zero, plus, times, minus}
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	19
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	20	consts
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	21
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	22	"1r" :: real ("1r")
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	23
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	24	defs
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	25
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	26	real_zero_def
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 7219 diff changeset	27	"0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	28	preal_of_prat(prat_of_pnat 1p))})"
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	29	real_one_def
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	30	"1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) +
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	31	preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	32
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	33	real_minus_def
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	34	"- R == Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	35
7127 48e235179ffb added parentheses to cope with a possible reduction of the precedence of unary paulson parents: 7077 diff changeset	36	real_diff_def "x - y == x + (- y :: real)"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	37
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	38	constdefs
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	39
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	40	real_of_preal :: preal => real
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	41	"real_of_preal m ==
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	42	Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p),
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	43	preal_of_prat(prat_of_pnat 1p))})"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	44
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	45	rinv :: real => real
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 7219 diff changeset	46	"rinv(R) == (@S. R ~= 0 & S*R = 1r)"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	47
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	48	real_of_posnat :: nat => real
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	49	"real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	50
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	51	real_of_nat :: nat => real
7127 48e235179ffb added parentheses to cope with a possible reduction of the precedence of unary paulson parents: 7077 diff changeset	52	"real_of_nat n == real_of_posnat n + (-1r)"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	53
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	54	defs
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	55
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	56	real_add_def
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	57	"P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
9365 0cced1b20d68 use split syntax; wenzelm parents: 9043 diff changeset	58	(%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	59
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	60	real_mult_def
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	61	"P * Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
9365 0cced1b20d68 use split syntax; wenzelm parents: 9043 diff changeset	62	(%(x1,y1). (%(x2,y2). realrel^^{(x1x2+y1y2,x1y2+x2y1)}) p2) p1)"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	63
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	64	real_less_def
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	65	"P < Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 &
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	66	(x1,y1):Rep_real(P) &
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	67	(x2,y2):Rep_real(Q)"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	68	real_le_def
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	69	"P <= (Q::real) == ~(Q < P)"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	70
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	71	end

author	wenzelm
	Mon, 28 Aug 2000 14:09:33 +0200
changeset 9697	c5fc121c2067
parent 9391	a6ab3a442da6
child 10606	e3229a37d53f
permissions	-rw-r--r--