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

9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	1	(* Title: HOL/Real/real_arith.ML
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
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	4	Copyright 1999 TU Muenchen
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	5
10722 55c8367bab05 rational linear arithmetic nipkow parents: 10693 diff changeset	6	Augmentation of real linear arithmetic with rational coefficient handling
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	7	*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	8
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	9	local
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	10
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	11	(* reduce contradictory <= to False *)
10722 55c8367bab05 rational linear arithmetic nipkow parents: 10693 diff changeset	12	val simps = [True_implies_equals,inst "w" "number_of ?v" real_add_mult_distrib2,
55c8367bab05 rational linear arithmetic nipkow parents: 10693 diff changeset	13	real_divide_1,real_times_divide1_eq,real_times_divide2_eq];
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	14
10758 9d766f21cf41 minor tidying of simprocs paulson parents: 10722 diff changeset	15	val simprocs = [real_cancel_numeral_factors_divide];
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	16
10693 9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic nipkow parents: 10574 diff changeset	17	fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic nipkow parents: 10574 diff changeset	18
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic nipkow parents: 10574 diff changeset	19	val real_mult_mono_thms =
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic nipkow parents: 10574 diff changeset	20	[(rotate_prems 1 real_mult_less_mono2,
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic nipkow parents: 10574 diff changeset	21	cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))),
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic nipkow parents: 10574 diff changeset	22	(real_mult_le_mono2,
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic nipkow parents: 10574 diff changeset	23	cvar(real_mult_le_mono2, hd(tl(prems_of real_mult_le_mono2))))]
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic nipkow parents: 10574 diff changeset	24
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	25	in
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	26
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	27	val real_arith_setup =
10693 9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic nipkow parents: 10574 diff changeset	28	[Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
10722 55c8367bab05 rational linear arithmetic nipkow parents: 10693 diff changeset	29	{add_mono_thms = add_mono_thms,
10693 9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic nipkow parents: 10574 diff changeset	30	mult_mono_thms = mult_mono_thms @ real_mult_mono_thms,
10722 55c8367bab05 rational linear arithmetic nipkow parents: 10693 diff changeset	31	inj_thms = inj_thms,
55c8367bab05 rational linear arithmetic nipkow parents: 10693 diff changeset	32	lessD = lessD,
55c8367bab05 rational linear arithmetic nipkow parents: 10693 diff changeset	33	simpset = simpset addsimps simps addsimprocs simprocs})];
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	34
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	35	end;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	36
10722 55c8367bab05 rational linear arithmetic nipkow parents: 10693 diff changeset	37	(*
55c8367bab05 rational linear arithmetic nipkow parents: 10693 diff changeset	38	Procedure "assoc_fold" needed?
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: diff changeset	39	*)

author	kleing
	Fri, 09 Feb 2001 16:22:30 +0100
changeset 11086	e714862ecc0a
parent 10758	9d766f21cf41
child 14288	d149e3cbdb39
permissions	-rw-r--r--