isabelle: src/HOL/Real/RealDef.thy@e3229a37d53f (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
10606 e3229a37d53f converted rinv to inverse; bauerg parents: 9391 diff changeset	18	real :: {ord, zero, plus, times, minus, inverse}
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
10606 e3229a37d53f converted rinv to inverse; bauerg parents: 9391 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
10606 e3229a37d53f converted rinv to inverse; bauerg parents: 9391 diff changeset	30	"1r == 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	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
10606 e3229a37d53f converted rinv to inverse; bauerg parents: 9391 diff changeset	34	"- R == Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
e3229a37d53f converted rinv to inverse; bauerg parents: 9391 diff changeset	35
e3229a37d53f converted rinv to inverse; bauerg parents: 9391 diff changeset	36	real_diff_def
e3229a37d53f converted rinv to inverse; bauerg parents: 9391 diff changeset	37	"R - (S::real) == R + - S"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	38
10606 e3229a37d53f converted rinv to inverse; bauerg parents: 9391 diff changeset	39	real_inverse_def
e3229a37d53f converted rinv to inverse; bauerg parents: 9391 diff changeset	40	"inverse (R::real) == (@S. R ~= 0 & S*R = 1r)"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	41
10606 e3229a37d53f converted rinv to inverse; bauerg parents: 9391 diff changeset	42	real_divide_def
e3229a37d53f converted rinv to inverse; bauerg parents: 9391 diff changeset	43	"R / (S::real) == R * inverse S"
e3229a37d53f converted rinv to inverse; bauerg parents: 9391 diff changeset	44
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	45	constdefs
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	46
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	47	real_of_preal :: preal => real
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	48	"real_of_preal m ==
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	49	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	50	preal_of_prat(prat_of_pnat 1p))})"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	51
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	52	real_of_posnat :: nat => real
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	53	"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	54
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	55	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	56	"real_of_nat n == real_of_posnat n + (-1r)"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	57
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	58	defs
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_add_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^^{(x1+x2, y1+y2)}) 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_mult_def
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	65	"P * Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
9365 0cced1b20d68 use split syntax; wenzelm parents: 9043 diff changeset	66	(%(x1,y1). (%(x2,y2). realrel^^{(x1x2+y1y2,x1y2+x2y1)}) p2) p1)"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	67
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	68	real_less_def
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	69	"P < Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 &
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	70	(x1,y1):Rep_real(P) &
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	71	(x2,y2):Rep_real(Q)"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	72	real_le_def
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	73	"P <= (Q::real) == ~(Q < P)"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	74
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	75	end

author	bauerg
	Wed, 06 Dec 2000 12:34:12 +0100
changeset 10606	e3229a37d53f
parent 9391	a6ab3a442da6
child 10648	a8c647cfa31f
permissions	-rw-r--r--