isabelle: src/HOL/Hyperreal/hypreal_arith.ML@3314057c3b57 (annotated)

14309 f508492af9b4 moving HyperArith0.ML to other theories paulson parents: 14305 diff changeset	1	(* Title: HOL/Hyperreal/hypreal_arith.ML
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	2	ID: $Id$
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	3	Author: Tobias Nipkow, TU Muenchen
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	4	Copyright 1999 TU Muenchen
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	5
14352 a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14334 diff changeset	6	Simprocs for common factor cancellation & Rational coefficient handling
a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14334 diff changeset	7
a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14334 diff changeset	8	Instantiation of the generic linear arithmetic package for type hypreal.
10751 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
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	11	local
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	12
20254 58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	13	val simps = [thm "star_of_zero",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	14	thm "star_of_one",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	15	thm "star_of_number_of",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	16	thm "star_of_add",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	17	thm "star_of_minus",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	18	thm "star_of_diff",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	19	thm "star_of_mult"]
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	20
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	21	val real_inj_thms = [thm "star_of_le" RS iffD2,
17318 bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic; huffman parents: 15923 diff changeset	22	thm "star_of_less" RS iffD2,
20254 58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	23	thm "star_of_eq" RS iffD2]
14369 c50188fe6366 tidying up arithmetic for the hyperreals paulson parents: 14352 diff changeset	24
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	25	in
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	26
20254 58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	27	val hyprealT = Type ("StarDef.star", [HOLogic.realT]);
14387 e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses paulson parents: 14370 diff changeset	28
14352 a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14334 diff changeset	29	val fast_hypreal_arith_simproc =
20254 58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	30	Simplifier.simproc (the_context ())
14352 a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14334 diff changeset	31	"fast_hypreal_arith"
a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14334 diff changeset	32	["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14334 diff changeset	33	Fast_Arith.lin_arith_prover;
a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14334 diff changeset	34
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	35	val hypreal_arith_setup =
18708 4b3dadb4fe33 setup: theory -> theory; wenzelm parents: 17876 diff changeset	36	Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
14369 c50188fe6366 tidying up arithmetic for the hyperreals paulson parents: 14352 diff changeset	37	{add_mono_thms = add_mono_thms,
15184 d2c19aea17bc made mult_mono_thms generic. nipkow parents: 14387 diff changeset	38	mult_mono_thms = mult_mono_thms,
20254 58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	39	inj_thms = real_inj_thms @ inj_thms,
14352 a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14334 diff changeset	40	lessD = lessD, (Can't change LA_Data_Ref.lessD: the hypreals are dense!)
15923 01d5d0c1c078 fixed lin.arith nipkow parents: 15186 diff changeset	41	neqE = neqE,
20254 58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	42	simpset = simpset addsimps simps}) #>
18708 4b3dadb4fe33 setup: theory -> theory; wenzelm parents: 17876 diff changeset	43	arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
4b3dadb4fe33 setup: theory -> theory; wenzelm parents: 17876 diff changeset	44	(fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy));
10751 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	end;

author	huffman
	Wed, 16 May 2007 23:03:45 +0200
changeset 22983	3314057c3b57
parent 20254	58b71535ed00
child 24075	366d4d234814
permissions	-rw-r--r--