isabelle: src/HOL/Hyperreal/NSA.thy@ba7aa8c426ad (annotated)

10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	1	(* Title : NSA.thy
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	2	Author : Jacques D. Fleuriot
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	3	Copyright : 1998 University of Cambridge
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	4	Description : Infinite numbers, Infinitesimals,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	5	infinitely close relation etc.
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	6	*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	7
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	8	NSA = HRealAbs + RComplete +
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	9
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	10	constdefs
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	11
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	12	Infinitesimal :: "hypreal set"
10919 144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10751 diff changeset	13	"Infinitesimal == {x. ALL r: Reals. 0 < r --> abs x < r}"
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	14
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	15	HFinite :: "hypreal set"
10919 144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10751 diff changeset	16	"HFinite == {x. EX r: Reals. abs x < r}"
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	17
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	18	HInfinite :: "hypreal set"
10919 144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10751 diff changeset	19	"HInfinite == {x. ALL r: Reals. r < abs x}"
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	20
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	21	(* standard part map *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	22	st :: hypreal => hypreal
10919 144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10751 diff changeset	23	"st == (%x. @r. x : HFinite & r:Reals & r @= x)"
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	24
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	25	monad :: hypreal => hypreal set
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	26	"monad x == {y. x @= y}"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	27
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	28	galaxy :: hypreal => hypreal set
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	29	"galaxy x == {y. (x + -y) : HFinite}"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	30
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	31	(* infinitely close *)
10919 144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10751 diff changeset	32	approx :: "[hypreal, hypreal] => bool" (infixl "@=" 50)
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	33	"x @= y == (x + -y) : Infinitesimal"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	34
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	35
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	36	defs
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	37
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	38	(standard real numbers as a subset of the hyperreals)
10919 144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10751 diff changeset	39	SReal_def "Reals == {x. EX r. x = hypreal_of_real r}"
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	40
12114 a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead; wenzelm parents: 10919 diff changeset	41	syntax (xsymbols)
10919 144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10751 diff changeset	42	approx :: "[hypreal, hypreal] => bool" (infixl "\\<approx>" 50)
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	43
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	44	end
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	45
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	46
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	47
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	48

author	paulson
	Tue, 06 May 2003 10:40:43 +0200
changeset 13963	ba7aa8c426ad
parent 12114	a8e860c86252
child 14370	b0064703967b
permissions	-rw-r--r--