isabelle: src/HOL/Integ/IntArith.ML@50ec59aff389 (annotated)

9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 9269 diff changeset	1	(* Title: HOL/Integ/IntArith.ML
7707 1f4b67fdfdae simprocs now in IntArith; wenzelm parents: diff changeset	2	ID: $Id$
1f4b67fdfdae simprocs now in IntArith; wenzelm parents: diff changeset	3	Authors: Larry Paulson and Tobias Nipkow
1f4b67fdfdae simprocs now in IntArith; wenzelm parents: diff changeset	4	*)
1f4b67fdfdae simprocs now in IntArith; wenzelm parents: diff changeset	5
9269 b62d5265b959 added zabs to arith_tac nipkow parents: 9214 diff changeset	6	Goal "abs(abs(x::int)) = abs(x)";
b62d5265b959 added zabs to arith_tac nipkow parents: 9214 diff changeset	7	by(arith_tac 1);
9214 9454f30eacc7 Defined abs on int. nipkow parents: 9079 diff changeset	8	qed "abs_abs";
9454f30eacc7 Defined abs on int. nipkow parents: 9079 diff changeset	9	Addsimps [abs_abs];
9454f30eacc7 Defined abs on int. nipkow parents: 9079 diff changeset	10
9269 b62d5265b959 added zabs to arith_tac nipkow parents: 9214 diff changeset	11	Goal "abs(-(x::int)) = abs(x)";
b62d5265b959 added zabs to arith_tac nipkow parents: 9214 diff changeset	12	by(arith_tac 1);
9214 9454f30eacc7 Defined abs on int. nipkow parents: 9079 diff changeset	13	qed "abs_minus";
9454f30eacc7 Defined abs on int. nipkow parents: 9079 diff changeset	14	Addsimps [abs_minus];
9454f30eacc7 Defined abs on int. nipkow parents: 9079 diff changeset	15
9269 b62d5265b959 added zabs to arith_tac nipkow parents: 9214 diff changeset	16	Goal "abs(x+y) <= abs(x) + abs(y::int)";
b62d5265b959 added zabs to arith_tac nipkow parents: 9214 diff changeset	17	by(arith_tac 1);
b62d5265b959 added zabs to arith_tac nipkow parents: 9214 diff changeset	18	qed "triangle_ineq";
b62d5265b959 added zabs to arith_tac nipkow parents: 9214 diff changeset	19
9214 9454f30eacc7 Defined abs on int. nipkow parents: 9079 diff changeset	20
9063 0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	21	(* Some convenient biconditionals for products of signs *)
7707 1f4b67fdfdae simprocs now in IntArith; wenzelm parents: diff changeset	22
9063 0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	23	Goal "[\| (#0::int) < i; #0 < j \|] ==> #0 < i*j";
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	24	by (dtac zmult_zless_mono1 1);
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	25	by Auto_tac;
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	26	qed "zmult_pos";
7707 1f4b67fdfdae simprocs now in IntArith; wenzelm parents: diff changeset	27
9063 0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	28	Goal "[\| i < (#0::int); j < #0 \|] ==> #0 < i*j";
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	29	by (dtac zmult_zless_mono1_neg 1);
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	30	by Auto_tac;
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	31	qed "zmult_neg";
7707 1f4b67fdfdae simprocs now in IntArith; wenzelm parents: diff changeset	32
9063 0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	33	Goal "[\| (#0::int) < i; j < #0 \|] ==> i*j < #0";
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	34	by (dtac zmult_zless_mono1_neg 1);
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	35	by Auto_tac;
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	36	qed "zmult_pos_neg";
7707 1f4b67fdfdae simprocs now in IntArith; wenzelm parents: diff changeset	37
9063 0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	38	Goal "((#0::int) < x*y) = (#0 < x & #0 < y \| x < #0 & y < #0)";
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	39	by (auto_tac (claset(),
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	40	simpset() addsimps [order_le_less, linorder_not_less,
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	41	zmult_pos, zmult_neg]));
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	42	by (ALLGOALS (rtac ccontr));
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	43	by (auto_tac (claset(),
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	44	simpset() addsimps [order_le_less, linorder_not_less]));
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	45	by (ALLGOALS (etac rev_mp));
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	46	by (ALLGOALS (dtac zmult_pos_neg THEN' assume_tac));
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	47	by (auto_tac (claset() addDs [order_less_not_sym],
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	48	simpset() addsimps [zmult_commute]));
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	49	qed "int_0_less_mult_iff";
7707 1f4b67fdfdae simprocs now in IntArith; wenzelm parents: diff changeset	50
9063 0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	51	Goal "((#0::int) <= x*y) = (#0 <= x & #0 <= y \| x <= #0 & y <= #0)";
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	52	by (auto_tac (claset(),
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	53	simpset() addsimps [order_le_less, linorder_not_less,
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	54	int_0_less_mult_iff]));
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	55	qed "int_0_le_mult_iff";
7707 1f4b67fdfdae simprocs now in IntArith; wenzelm parents: diff changeset	56
9063 0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	57	Goal "(x*y < (#0::int)) = (#0 < x & y < #0 \| x < #0 & #0 < y)";
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	58	by (auto_tac (claset(),
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	59	simpset() addsimps [int_0_le_mult_iff,
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	60	linorder_not_le RS sym]));
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	61	by (auto_tac (claset() addDs [order_less_not_sym],
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	62	simpset() addsimps [linorder_not_le]));
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	63	qed "zmult_less_0_iff";
7707 1f4b67fdfdae simprocs now in IntArith; wenzelm parents: diff changeset	64
9063 0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	65	Goal "(x*y <= (#0::int)) = (#0 <= x & y <= #0 \| x <= #0 & #0 <= y)";
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	66	by (auto_tac (claset() addDs [order_less_not_sym],
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	67	simpset() addsimps [int_0_less_mult_iff,
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	68	linorder_not_less RS sym]));
0d7628966069 new lemmas for signs of products paulson parents: 9000 diff changeset	69	qed "zmult_le_0_iff";

author	wenzelm
	Wed, 02 Aug 2000 19:40:14 +0200
changeset 9502	50ec59aff389
parent 9436	62bb04ab4b01
child 9509	0f3ee1f89ca8
permissions	-rw-r--r--