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

5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	1	(* Title : Real/RealDef.thy
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	2	Author : Jacques D. Fleuriot
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	3	Copyright : 1998 University of Cambridge
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	4	Description : The reals
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	5	*)
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	6
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	7	RealDef = PReal +
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	8
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	9	constdefs
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	10	realrel :: "((preal * preal) * (preal * preal)) set"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	11	"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	12
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	13	typedef real = "{x::(preal*preal).True}/realrel" (Equiv.quotient_def)
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	14
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	15
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	16	instance
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	17	real :: {ord, plus, times, minus}
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	18
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	19	consts
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	20
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	21	"0r" :: real ("0r")
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
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	27	"0r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
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
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	46	"rinv(R) == (@S. R ~= 0r & S*R = 1r)"
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).
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	58	split(%x1 y1. split(%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)"
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).
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	62	split(%x1 y1. split(%x2 y2. realrel^^{(x1x2+y1y2,x1y2+x2y1)}) p2) p1)"
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	paulson
	Tue, 03 Aug 1999 13:15:54 +0200
changeset 7165	8c937127fd8c
parent 7127	48e235179ffb
child 7219	4e3f386c2e37
permissions	-rw-r--r--