isabelle: src/HOL/Real/ex/BinEx.ML@a901bafe4578 (annotated)

7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	1	(* Title: HOL/Real/ex/BinEx.ML
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	2	ID: $Id$
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	4	Copyright 1999 University of Cambridge
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	5
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	6	Examples of performing binary arithmetic by simplification
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	7	This time we use the reals, though the representation is just of integers.
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	8	*)
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	9
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	10	(* Addition *)
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	11
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	12	Goal "(#1359::real) + #-2468 = #-1109";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	13	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	14	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	15
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	16	Goal "(#93746::real) + #-46375 = #47371";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	17	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	18	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	19
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	20	(* Negation *)
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	21
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	22	Goal "- (#65745::real) = #-65745";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	23	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	24	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	25
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	26	Goal "- (#-54321::real) = #54321";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	27	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	28	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	29
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	30
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	31	(* Multiplication *)
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	32
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	33	Goal "(#-84::real) * #51 = #-4284";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	34	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	35	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	36
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	37	Goal "(#255::real) * #255 = #65025";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	38	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	39	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	40
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	41	Goal "(#1359::real) * #-2468 = #-3354012";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	42	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	43	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	44
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	45	(* Inequalities *)
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	46
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	47	Goal "(#89::real) * #10 ~= #889";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	48	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	49	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	50
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	51	Goal "(#13::real) < #18 - #4";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	52	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	53	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	54
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	55	Goal "(#-345::real) < #-242 + #-100";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	56	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	57	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	58
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	59	Goal "(#13557456::real) < #18678654";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	60	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	61	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	62
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	63	Goal "(#999999::real) <= (#1000001 + #1)-#2";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	64	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	65	qed "";
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	66
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	67	Goal "(#1234567::real) <= #1234567";
4137c951b36b new directory HOL/Real/ex of real examples paulson parents: diff changeset	68	by (Simp_tac 1);
7577 644f9b4ae764 proper theory setup for Real/ex/BinEx; wenzelm parents: 7392 diff changeset	69	qed "";
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	70
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	71	( Tests )
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	72	Goal "(x + y = x) = (y = (#0::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	73	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	74
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	75	Goal "(x + y = y) = (x = (#0::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	76	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	77
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	78	Goal "(x + y = (#0::real)) = (x = -y)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	79	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	80
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	81	Goal "(x + y = (#0::real)) = (y = -x)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	82	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	83
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	84	Goal "((x + y) < (x + z)) = (y < (z::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	85	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	86
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	87	Goal "((x + z) < (y + z)) = (x < (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	88	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	89
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	90	Goal "(~ x < y) = (y <= (x::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	91	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	92
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	93	Goal "~(x < y & y < (x::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	94	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	95
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	96	Goal "(x::real) < y ==> ~ y < x";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	97	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	98
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	99	Goal "((x::real) ~= y) = (x < y \| y < x)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	100	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	101
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	102	Goal "(~ x <= y) = (y < (x::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	103	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	104
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	105	Goal "x <= y \| y <= (x::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	106	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	107
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	108	Goal "x <= y \| y < (x::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	109	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	110
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	111	Goal "x < y \| y <= (x::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	112	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	113
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	114	Goal "x <= (x::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	115	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	116
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	117	Goal "((x::real) <= y) = (x < y \| x = y)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	118	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	119
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	120	Goal "((x::real) <= y & y <= x) = (x = y)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	121	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	122
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	123	Goal "~(x < y & y <= (x::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	124	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	125
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	126	Goal "~(x <= y & y < (x::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	127	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	128
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	129	Goal "(-x < (#0::real)) = (#0 < x)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	130	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	131
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	132	Goal "((#0::real) < -x) = (x < #0)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	133	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	134
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	135	Goal "(-x <= (#0::real)) = (#0 <= x)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	136	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	137
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	138	Goal "((#0::real) <= -x) = (x <= #0)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	139	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	140
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	141	Goal "(x::real) = y \| x < y \| y < x";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	142	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	143
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	144	Goal "(x::real) = #0 \| #0 < x \| #0 < -x";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	145	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	146
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	147	Goal "(#0::real) <= x \| #0 <= -x";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	148	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	149
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	150	Goal "((x::real) + y <= x + z) = (y <= z)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	151	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	152
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	153	Goal "((x::real) + z <= y + z) = (x <= y)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	154	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	155
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	156	Goal "(w::real) < x & y < z ==> w + y < x + z";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	157	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	158
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	159	Goal "(w::real) <= x & y <= z ==> w + y <= x + z";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	160	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	161
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	162	Goal "(#0::real) <= x & #0 <= y ==> #0 <= x + y";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	163	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	164
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	165	Goal "(#0::real) < x & #0 < y ==> #0 < x + y";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	166	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	167
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	168	Goal "(-x < y) = (#0 < x + (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	169	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	170
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	171	Goal "(x < -y) = (x + y < (#0::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	172	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	173
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	174	Goal "(y < x + -z) = (y + z < (x::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	175	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	176
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	177	Goal "(x + -y < z) = (x < z + (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	178	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	179
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	180	Goal "x <= y ==> x < y + (#1::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	181	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	182
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	183	Goal "(x - y) + y = (x::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	184	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	185
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	186	Goal "y + (x - y) = (x::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	187	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	188
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	189	Goal "x - x = (#0::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	190	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	191
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	192	Goal "(x - y = #0) = (x = (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	193	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	194
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	195	Goal "((#0::real) <= x + x) = (#0 <= x)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	196	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	197
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	198	Goal "(-x <= x) = ((#0::real) <= x)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	199	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	200
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	201	Goal "(x <= -x) = (x <= (#0::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	202	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	203
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	204	Goal "(-x = (#0::real)) = (x = #0)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	205	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	206
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	207	Goal "-(x - y) = y - (x::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	208	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	209
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	210	Goal "((#0::real) < x - y) = (y < x)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	211	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	212
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	213	Goal "((#0::real) <= x - y) = (y <= x)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	214	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	215
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	216	Goal "(x + y) - x = (y::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	217	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	218
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	219	Goal "(-x = y) = (x = (-y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	220	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	221
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	222	Goal "x < (y::real) ==> ~(x = y)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	223	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	224
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	225	Goal "(x <= x + y) = ((#0::real) <= y)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	226	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	227
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	228	Goal "(y <= x + y) = ((#0::real) <= x)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	229	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	230
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	231	Goal "(x < x + y) = ((#0::real) < y)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	232	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	233
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	234	Goal "(y < x + y) = ((#0::real) < x)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	235	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	236
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	237	Goal "(x - y) - x = (-y::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	238	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	239
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	240	Goal "(x + y < z) = (x < z - (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	241	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	242
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	243	Goal "(x - y < z) = (x < z + (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	244	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	245
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	246	Goal "(x < y - z) = (x + z < (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	247	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	248
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	249	Goal "(x <= y - z) = (x + z <= (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	250	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	251
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	252	Goal "(x - y <= z) = (x <= z + (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	253	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	254
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	255	Goal "(-x < -y) = (y < (x::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	256	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	257
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	258	Goal "(-x <= -y) = (y <= (x::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	259	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	260
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	261	Goal "(a + b) - (c + d) = (a - c) + (b - (d::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	262	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	263
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	264	Goal "(#0::real) - x = -x";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	265	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	266
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	267	Goal "x - (#0::real) = x";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	268	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	269
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	270	Goal "w <= x & y < z ==> w + y < x + (z::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	271	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	272
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	273	Goal "w < x & y <= z ==> w + y < x + (z::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	274	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	275
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	276	Goal "(#0::real) <= x & #0 < y ==> #0 < x + (y::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	277	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	278
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	279	Goal "(#0::real) < x & #0 <= y ==> #0 < x + y";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	280	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	281
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	282	Goal "-x - y = -(x + (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	283	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	284
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	285	Goal "x - (-y) = x + (y::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	286	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	287
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	288	Goal "-x - -y = y - (x::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	289	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	290
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	291	Goal "(a - b) + (b - c) = a - (c::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	292	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	293
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	294	Goal "(x = y - z) = (x + z = (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	295	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	296
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	297	Goal "(x - y = z) = (x = z + (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	298	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	299
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	300	Goal "x - (x - y) = (y::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	301	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	302
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	303	Goal "x - (x + y) = -(y::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	304	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	305
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	306	Goal "x = y ==> x <= (y::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	307	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	308
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	309	Goal "(#0::real) < x ==> ~(x = #0)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	310	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	311
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	312	Goal "(x + y) * (x - y) = (x * x) - (y * y)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	313
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	314	Goal "(-x = -y) = (x = (y::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	315	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	316
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	317	Goal "(-x < -y) = (y < (x::real))";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	318	by(arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	319
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	320	Goal "!!a::real. [\| a <= b; c <= d; x+y<z \|] ==> a+c <= b+d";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	321	by (fast_arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	322
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	323	Goal "!!a::real. [\| a < b; c < d \|] ==> a-d <= b+(-c)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	324	by (fast_arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	325
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	326	Goal "!!a::real. [\| a <= b; b+b <= c \|] ==> a+a <= c";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	327	by (fast_arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	328
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	329	Goal "!!a::real. [\| a+b <= i+j; a<=b; i<=j \|] \
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	330	\ ==> a+a <= j+j";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	331	by (fast_arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	332
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	333	Goal "!!a::real. [\| a+b < i+j; a<b; i<j \|] \
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	334	\ ==> a+a < j+j";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	335	by (fast_arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	336
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	337	Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	338	by (arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	339
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	340	Goal "!!a::real. [\| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l \|] \
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	341	\ ==> a <= l";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	342	by (fast_arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	343
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	344	Goal "!!a::real. [\| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l \|] \
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	345	\ ==> a+a+a+a <= l+l+l+l";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	346	by (fast_arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	347
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	348	(* Too slow. Needs "combine_coefficients" simproc
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	349	Goal "!!a::real. [\| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l \|] \
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	350	\ ==> a+a+a+a+a <= l+l+l+l+i";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	351	by (fast_arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	352
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	353	Goal "!!a::real. [\| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l \|] \
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	354	\ ==> a+a+a+a+a+a <= l+l+l+l+i+l";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	355	by (fast_arith_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	356	*)
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7577 diff changeset	357

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 7588	26384af93359
child 9082	8a15c3577770
permissions	-rw-r--r--