isabelle: src/HOL/Real/real_arith.ML@2f45c1b1b05d (annotated)

14426 de890c247b38 fixed bugs in the setup of arithmetic procedures paulson parents: 14390 diff changeset	1	(* Title: HOL/Real/real_arith.ML
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	2	ID: $Id$
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	3	Author: Tobias Nipkow, TU Muenchen
14352 a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14336 diff changeset	4	Copyright 1999 TU Muenchen
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	5
14352 a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14336 diff changeset	6	Simprocs for common factor cancellation & Rational coefficient handling
a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14336 diff changeset	7
a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14336 diff changeset	8	Instantiation of the generic linear arithmetic package for type real.
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	9	*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	10
14289 deb8e1e62002 combining Real/{RealArith0,real_arith}.ML paulson parents: 14288 diff changeset	11	local
deb8e1e62002 combining Real/{RealArith0,real_arith}.ML paulson parents: 14288 diff changeset	12
23080 2f8d7aa1263b remove redundant simproc; remove legacy ML bindings huffman parents: 22970 diff changeset	13	val simps = [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings huffman parents: 22970 diff changeset	14	@{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings huffman parents: 22970 diff changeset	15	@{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings huffman parents: 22970 diff changeset	16	@{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings huffman parents: 22970 diff changeset	17	@{thm real_of_nat_number_of}, @{thm real_number_of}]
14355 67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real. nipkow parents: 14352 diff changeset	18
23080 2f8d7aa1263b remove redundant simproc; remove legacy ML bindings huffman parents: 22970 diff changeset	19	val nat_inj_thms = [@{thm real_of_nat_le_iff} RS iffD2,
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings huffman parents: 22970 diff changeset	20	@{thm real_of_nat_inject} RS iffD2]
20254 58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	21	(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	22	real_of_nat_less_iff RS iffD2 *)
14355 67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real. nipkow parents: 14352 diff changeset	23
23080 2f8d7aa1263b remove redundant simproc; remove legacy ML bindings huffman parents: 22970 diff changeset	24	val int_inj_thms = [@{thm real_of_int_le_iff} RS iffD2,
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings huffman parents: 22970 diff changeset	25	@{thm real_of_int_inject} RS iffD2]
20254 58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	26	(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs) webertj parents: 18708 diff changeset	27	real_of_int_less_iff RS iffD2 *)
14352 a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14336 diff changeset	28
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	29	in
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	30
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	31	val real_arith_setup =
24093 5d0ecd0c8f3c tuned LinArith setup; wenzelm parents: 23081 diff changeset	32	LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
14368 2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup paulson parents: 14365 diff changeset	33	{add_mono_thms = add_mono_thms,
15184 d2c19aea17bc made mult_mono_thms generic. nipkow parents: 15003 diff changeset	34	mult_mono_thms = mult_mono_thms,
14355 67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real. nipkow parents: 14352 diff changeset	35	inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
24093 5d0ecd0c8f3c tuned LinArith setup; wenzelm parents: 23081 diff changeset	36	lessD = lessD, (Can't change lessD: the reals are dense!)
15923 01d5d0c1c078 fixed lin.arith nipkow parents: 15661 diff changeset	37	neqE = neqE,
18708 4b3dadb4fe33 setup: theory -> theory; wenzelm parents: 17876 diff changeset	38	simpset = simpset addsimps simps}) #>
4b3dadb4fe33 setup: theory -> theory; wenzelm parents: 17876 diff changeset	39	arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #>
23080 2f8d7aa1263b remove redundant simproc; remove legacy ML bindings huffman parents: 22970 diff changeset	40	arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT)
14352 a8b1a44d8264 Modified real arithmetic simplification paulson parents: 14336 diff changeset	41
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	42	end;

author	wenzelm
	Sun, 08 Jun 2008 14:29:09 +0200
changeset 27090	2f45c1b1b05d
parent 24093	5d0ecd0c8f3c
child 27545	7165068bb61f
permissions	-rw-r--r--