isabelle: src/HOL/Real/RealDef.thy@a901bafe4578 (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
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	14	typedef real = "{x::(preal*preal).True}/realrel" (Equiv.quotient_def)
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
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	18	real :: {ord, plus, times, minus}
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	"0r" :: real ("0r")
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	23	"1r" :: real ("1r")
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	24
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	25	defs
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	26
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	27	real_zero_def
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	28	"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	29	preal_of_prat(prat_of_pnat 1p))})"
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	30	real_one_def
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	31	"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	32	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	33
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	34	real_minus_def
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	35	"- R == Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	36
7127 48e235179ffb added parentheses to cope with a possible reduction of the precedence of unary paulson parents: 7077 diff changeset	37	real_diff_def "x - y == x + (- y :: real)"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	38
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	39	constdefs
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	40
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	41	real_of_preal :: preal => real
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	42	"real_of_preal m ==
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	43	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	44	preal_of_prat(prat_of_pnat 1p))})"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	45
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	46	rinv :: real => real
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	47	"rinv(R) == (@S. R ~= 0r & S*R = 1r)"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	48
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	49	real_of_posnat :: nat => real
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	50	"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	51
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5787 diff changeset	52	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	53	"real_of_nat n == real_of_posnat n + (-1r)"
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	54
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	55	defs
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	56
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	57	real_add_def
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	58	"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	59	split(%x1 y1. split(%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	60
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	61	real_mult_def
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	62	"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	63	split(%x1 y1. split(%x2 y2. realrel^^{(x1x2+y1y2,x1y2+x2y1)}) p2) p1)"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	64
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	65	real_less_def
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	66	"P < Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 &
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	67	(x1,y1):Rep_real(P) &
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	68	(x2,y2):Rep_real(Q)"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	69	real_le_def
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	70	"P <= (Q::real) == ~(Q < P)"
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	71
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: diff changeset	72	end

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 7219	4e3f386c2e37
child 9043	ca761fe227d8
permissions	-rw-r--r--