isabelle: src/HOL/Real/RealPow.ML@98ddd0138cbf (annotated)

7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	1	(* Title : RealPow.ML
7219 4e3f386c2e37 inserted Id: lines paulson parents: 7077 diff changeset	2	ID : $Id$
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	3	Author : Jacques D. Fleuriot
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	4	Copyright : 1998 University of Cambridge
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	5	Description : Natural Powers of reals theory
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	6	*)
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	7
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	8	Goal "(#0::real) ^ (Suc n) = #0";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	9	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	10	qed "realpow_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	11	Addsimps [realpow_zero];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	12
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	13	Goal "r ~= (#0::real) --> r ^ n ~= #0";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	14	by (induct_tac "n" 1);
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	15	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	16	qed_spec_mp "realpow_not_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	17
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	18	Goal "r ^ n = (#0::real) ==> r = #0";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	19	by (rtac ccontr 1);
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	20	by (auto_tac (claset() addDs [realpow_not_zero], simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	21	qed "realpow_zero_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	22
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	23	Goal "r ~= #0 --> rinv(r ^ n) = (rinv r) ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	24	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	25	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	26	by (forw_inst_tac [("n","n")] realpow_not_zero 1);
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	27	by (auto_tac (claset() addDs [rename_numerals real_rinv_distrib],
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	28	simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	29	qed_spec_mp "realpow_rinv";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	30
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	31	Goal "abs (r::real) ^ n = abs (r ^ n)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	32	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	33	by (auto_tac (claset(),simpset() addsimps
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	34	[abs_mult,abs_one]));
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	35	qed "realpow_abs";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	36
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	37	Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	38	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	39	by (auto_tac (claset(),simpset() addsimps real_mult_ac));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	40	qed "realpow_add";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	41
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	42	Goal "(r::real) ^ 1 = r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	43	by (Simp_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	44	qed "realpow_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	45	Addsimps [realpow_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	46
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	47	Goal "(r::real) ^ 2 = r * r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	48	by (Simp_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	49	qed "realpow_two";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	50
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	51	Goal "(#0::real) < r --> #0 <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	52	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	53	by (auto_tac (claset() addDs [real_less_imp_le]
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	54	addIs [rename_numerals real_le_mult_order],
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	55	simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	56	qed_spec_mp "realpow_ge_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	57
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	58	Goal "(#0::real) < r --> #0 < r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	59	by (induct_tac "n" 1);
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	60	by (auto_tac (claset() addIs [rename_numerals real_mult_order],
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	61	simpset() addsimps [real_zero_less_one]));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	62	qed_spec_mp "realpow_gt_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	63
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	64	Goal "(#0::real) <= r --> #0 <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	65	by (induct_tac "n" 1);
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	66	by (auto_tac (claset() addIs [rename_numerals real_le_mult_order],
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	67	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	68	qed_spec_mp "realpow_ge_zero2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	69
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	70	Goal "(#0::real) < x & x <= y --> x ^ n <= y ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	71	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	72	by (auto_tac (claset() addSIs [real_mult_le_mono],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	73	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	74	by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	75	qed_spec_mp "realpow_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	76
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	77	Goal "(#0::real) <= x & x <= y --> x ^ n <= y ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	78	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	79	by (auto_tac (claset() addSIs [real_mult_le_mono4],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	80	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	81	by (asm_simp_tac (simpset() addsimps [realpow_ge_zero2]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	82	qed_spec_mp "realpow_le2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	83
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	84	Goal "(#0::real) < x & x < y & 0 < n --> x ^ n < y ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	85	by (induct_tac "n" 1);
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	86	by (auto_tac (claset() addIs [rename_numerals real_mult_less_mono, gr0I]
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	87	addDs [realpow_gt_zero],
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	88	simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	89	qed_spec_mp "realpow_less";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	90
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	91	Goal "#1 ^ n = (#1::real)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	92	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	93	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	94	qed "realpow_eq_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	95	Addsimps [realpow_eq_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	96
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	97	Goal "abs(-(#1 ^ n)) = (#1::real)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	98	by (simp_tac (simpset() addsimps
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	99	[abs_minus_cancel,abs_one]) 1);
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	100	qed "abs_minus_realpow_one";
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	101	Addsimps [abs_minus_realpow_one];
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	102
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	103	Goal "abs((-#1) ^ n) = (#1::real)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	104	by (induct_tac "n" 1);
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	105	by (auto_tac (claset(),simpset() addsimps [abs_mult,
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	106	abs_minus_cancel,abs_one]));
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	107	qed "abs_realpow_minus_one";
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	108	Addsimps [abs_realpow_minus_one];
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	109
10043 a0364652e115 Updated Files with new theorems fleuriot parents: 9428 diff changeset	110	Goal "abs((#-1) ^ n) = (#1::real)";
a0364652e115 Updated Files with new theorems fleuriot parents: 9428 diff changeset	111	by (rtac (simplify (simpset()) abs_realpow_minus_one) 1);
a0364652e115 Updated Files with new theorems fleuriot parents: 9428 diff changeset	112	qed "abs_realpow_minus_one2";
a0364652e115 Updated Files with new theorems fleuriot parents: 9428 diff changeset	113	Addsimps [abs_realpow_minus_one2];
a0364652e115 Updated Files with new theorems fleuriot parents: 9428 diff changeset	114
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	115	Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	116	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	117	by (auto_tac (claset(),simpset() addsimps real_mult_ac));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	118	qed "realpow_mult";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	119
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	120	Goal "(#0::real) <= r ^ 2";
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	121	by (simp_tac (simpset() addsimps [rename_numerals real_le_square]) 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	122	qed "realpow_two_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	123	Addsimps [realpow_two_le];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	124
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	125	Goal "abs((x::real) ^ 2) = x ^ 2";
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	126	by (simp_tac (simpset() addsimps [abs_eqI1,
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	127	rename_numerals real_le_square]) 1);
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	128	qed "abs_realpow_two";
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	129	Addsimps [abs_realpow_two];
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	130
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	131	Goal "abs(x::real) ^ 2 = x ^ 2";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	132	by (simp_tac (simpset() addsimps
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	133	[realpow_abs,abs_eqI1] delsimps [thm "realpow_Suc"]) 1);
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	134	qed "realpow_two_abs";
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	135	Addsimps [realpow_two_abs];
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	136
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	137	Goal "(#1::real) < r ==> #1 < r ^ 2";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	138	by Auto_tac;
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	139	by (cut_facts_tac [rename_numerals real_zero_less_one] 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	140	by (forw_inst_tac [("R1.0","#0")] real_less_trans 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	141	by (assume_tac 1);
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	142	by (dres_inst_tac [("z","r"),("x","#1")]
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	143	(rename_numerals real_mult_less_mono1) 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	144	by (auto_tac (claset() addIs [real_less_trans],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	145	qed "realpow_two_gt_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	146
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	147	Goal "(#1::real) < r --> #1 <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	148	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	149	by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	150	simpset()));
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	151	by (dtac (rename_numerals (real_zero_less_one RS real_mult_less_mono)) 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	152	by (dtac sym 4);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	153	by (auto_tac (claset() addSIs [real_less_imp_le],
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	154	simpset() addsimps [real_zero_less_one]));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	155	qed_spec_mp "realpow_ge_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	156
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	157	Goal "(#1::real) < r ==> #1 < r ^ (Suc n)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	158	by (forw_inst_tac [("n","n")] realpow_ge_one 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	159	by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	160	by (dtac sym 2);
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	161	by (ftac (rename_numerals (real_zero_less_one RS real_less_trans)) 1);
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	162	by (dres_inst_tac [("y","r ^ n")]
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	163	(rename_numerals real_mult_less_mono2) 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	164	by (assume_tac 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	165	by (auto_tac (claset() addDs [real_less_trans],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	166	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	167	qed "realpow_Suc_gt_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	168
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	169	Goal "(#1::real) <= r ==> #1 <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	170	by (dtac real_le_imp_less_or_eq 1);
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	171	by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	172	qed "realpow_ge_one2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	173
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	174	Goal "(#0::real) < r ==> #0 < r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	175	by (forw_inst_tac [("n","n")] realpow_ge_zero 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	176	by (forw_inst_tac [("n1","n")]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	177	((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	178	by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	179	addIs [rename_numerals real_mult_order],
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	180	simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	181	qed "realpow_Suc_gt_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	182
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	183	Goal "(#0::real) <= r ==> #0 <= r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	184	by (etac (real_le_imp_less_or_eq RS disjE) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	185	by (etac (realpow_ge_zero) 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	186	by (dtac sym 1);
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	187	by (Asm_simp_tac 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	188	qed "realpow_Suc_ge_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	189
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	190	Goal "(#1::real) <= #2 ^ n";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	191	by (res_inst_tac [("j","#1 ^ n")] real_le_trans 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	192	by (rtac realpow_le 2);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	193	by (auto_tac (claset() addIs [real_less_imp_le],simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	194	qed "two_realpow_ge_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	195
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	196	Goal "real_of_nat n < #2 ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	197	by (induct_tac "n" 1);
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	198	by Auto_tac;
99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	199	by (stac real_mult_2 1);
99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	200	by (rtac real_add_less_le_mono 1);
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	201	by (auto_tac (claset(),
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	202	simpset() addsimps [two_realpow_ge_one]));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	203	qed "two_realpow_gt";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	204	Addsimps [two_realpow_gt,two_realpow_ge_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	205
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	206	Goal "(-#1) ^ (2*n) = (#1::real)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	207	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	208	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	209	qed "realpow_minus_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	210	Addsimps [realpow_minus_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	211
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	212	Goal "(-#1) ^ (n + n) = (#1::real)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	213	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	214	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	215	qed "realpow_minus_one2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	216	Addsimps [realpow_minus_one2];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	217
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	218	Goal "(-#1) ^ Suc (n + n) = -(#1::real)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	219	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	220	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	221	qed "realpow_minus_one_odd";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	222	Addsimps [realpow_minus_one_odd];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	223
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	224	Goal "(-#1) ^ Suc (Suc (n + n)) = (#1::real)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	225	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	226	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	227	qed "realpow_minus_one_even";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	228	Addsimps [realpow_minus_one_even];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	229
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	230	Goal "(#0::real) < r & r < (#1::real) --> r ^ Suc n < r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	231	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	232	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	233	qed_spec_mp "realpow_Suc_less";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	234
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	235	Goal "#0 <= r & r < (#1::real) --> r ^ Suc n <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	236	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	237	by (auto_tac (claset() addIs [real_less_imp_le] addSDs
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	238	[real_le_imp_less_or_eq],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	239	qed_spec_mp "realpow_Suc_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	240
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	241	Goal "(#0::real) <= #0 ^ n";
8442 96023903c2df case_tac now subsumes both boolean and datatype cases; wenzelm parents: 8423 diff changeset	242	by (case_tac "n" 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	243	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	244	qed "realpow_zero_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	245	Addsimps [realpow_zero_le];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	246
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	247	Goal "#0 < r & r < (#1::real) --> r ^ Suc n <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	248	by (blast_tac (claset() addSIs [real_less_imp_le,
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	249	realpow_Suc_less]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	250	qed_spec_mp "realpow_Suc_le2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	251
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	252	Goal "[\| #0 <= r; r < (#1::real) \|] ==> r ^ Suc n <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	253	by (etac (real_le_imp_less_or_eq RS disjE) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	254	by (rtac realpow_Suc_le2 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	255	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	256	qed "realpow_Suc_le3";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	257
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	258	Goal "#0 <= r & r < (#1::real) & n < N --> r ^ N <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	259	by (induct_tac "N" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	260	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	261	by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	262	by (ALLGOALS(dtac (rename_numerals real_mult_le_mono3)));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	263	by (REPEAT(assume_tac 1));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	264	by (REPEAT(assume_tac 3));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	265	by (auto_tac (claset(),simpset() addsimps
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	266	[less_Suc_eq]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	267	qed_spec_mp "realpow_less_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	268
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	269	Goal "[\| #0 <= r; r < (#1::real); n <= N \|] ==> r ^ N <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	270	by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	271	by (auto_tac (claset() addIs [realpow_less_le],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	272	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	273	qed "realpow_le_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	274
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	275	Goal "[\| #0 < r; r < (#1::real) \|] ==> r ^ Suc n <= r";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	276	by (dres_inst_tac [("n","1"),("N","Suc n")]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	277	(real_less_imp_le RS realpow_le_le) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	278	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	279	qed "realpow_Suc_le_self";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	280
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	281	Goal "[\| #0 < r; r < (#1::real) \|] ==> r ^ Suc n < #1";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	282	by (blast_tac (claset() addIs [realpow_Suc_le_self,
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	283	real_le_less_trans]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	284	qed "realpow_Suc_less_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	285
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	286	Goal "(#1::real) <= r --> r ^ n <= r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	287	by (induct_tac "n" 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	288	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	289	qed_spec_mp "realpow_le_Suc";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	290
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	291	Goal "(#1::real) < r --> r ^ n < r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	292	by (induct_tac "n" 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	293	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	294	qed_spec_mp "realpow_less_Suc";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	295
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	296	Goal "(#1::real) < r --> r ^ n <= r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	297	by (blast_tac (claset() addSIs [real_less_imp_le,
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	298	realpow_less_Suc]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	299	qed_spec_mp "realpow_le_Suc2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	300
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	301	Goal "(#1::real) < r & n < N --> r ^ n <= r ^ N";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	302	by (induct_tac "N" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	303	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	304	by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	305	by (ALLGOALS(dtac (rename_numerals real_mult_self_le)));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	306	by (assume_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	307	by (assume_tac 2);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	308	by (auto_tac (claset() addIs [real_le_trans],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	309	simpset() addsimps [less_Suc_eq]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	310	qed_spec_mp "realpow_gt_ge";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	311
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	312	Goal "(#1::real) <= r & n < N --> r ^ n <= r ^ N";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	313	by (induct_tac "N" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	314	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	315	by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	316	by (ALLGOALS(dtac (rename_numerals real_mult_self_le2)));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	317	by (assume_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	318	by (assume_tac 2);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	319	by (auto_tac (claset() addIs [real_le_trans],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	320	simpset() addsimps [less_Suc_eq]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	321	qed_spec_mp "realpow_gt_ge2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	322
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	323	Goal "[\| (#1::real) < r; n <= N \|] ==> r ^ n <= r ^ N";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	324	by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	325	by (auto_tac (claset() addIs [realpow_gt_ge],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	326	qed "realpow_ge_ge";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	327
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	328	Goal "[\| (#1::real) <= r; n <= N \|] ==> r ^ n <= r ^ N";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	329	by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	330	by (auto_tac (claset() addIs [realpow_gt_ge2],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	331	qed "realpow_ge_ge2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	332
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	333	Goal "(#1::real) < r ==> r <= r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	334	by (dres_inst_tac [("n","1"),("N","Suc n")]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	335	realpow_ge_ge 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	336	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	337	qed_spec_mp "realpow_Suc_ge_self";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	338
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	339	Goal "(#1::real) <= r ==> r <= r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	340	by (dres_inst_tac [("n","1"),("N","Suc n")]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	341	realpow_ge_ge2 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	342	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	343	qed_spec_mp "realpow_Suc_ge_self2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	344
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	345	Goal "[\| (#1::real) < r; 0 < n \|] ==> r <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	346	by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	347	by (auto_tac (claset() addSIs
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	348	[realpow_Suc_ge_self],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	349	qed "realpow_ge_self";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	350
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	351	Goal "[\| (#1::real) <= r; 0 < n \|] ==> r <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	352	by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	353	by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	354	qed "realpow_ge_self2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	355
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	356	Goal "0 < n --> (x::real) ^ (n - 1) * x = x ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	357	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	358	by (auto_tac (claset(),simpset()
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	359	addsimps [real_mult_commute]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	360	qed_spec_mp "realpow_minus_mult";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	361	Addsimps [realpow_minus_mult];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	362
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	363	Goal "r ~= #0 ==> r * rinv(r) ^ 2 = rinv r";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	364	by (asm_simp_tac (simpset() addsimps [realpow_two,
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	365	real_mult_assoc RS sym]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	366	qed "realpow_two_mult_rinv";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	367	Addsimps [realpow_two_mult_rinv];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	368
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	369	(* 05/00 *)
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	370	Goal "(-x) ^ 2 = (x::real) ^ 2";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	371	by (Simp_tac 1);
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	372	qed "realpow_two_minus";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	373	Addsimps [realpow_two_minus];
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	374
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	375	Goal "(x::real) ^ 2 + - (y ^ 2) = (x + -y) * (x + y)";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	376	by (simp_tac (simpset() addsimps [real_add_mult_distrib2,
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	377	real_add_mult_distrib, real_minus_mult_eq2 RS sym]
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	378	@ real_mult_ac) 1);
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	379	qed "realpow_two_add_minus";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	380
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	381	Goalw [real_diff_def]
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	382	"(x::real) ^ 2 - y ^ 2 = (x - y) * (x + y)";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	383	by (simp_tac (simpset() addsimps [realpow_two_add_minus]
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	384	delsimps [thm "realpow_Suc"]) 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	385	qed "realpow_two_diff";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	386
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	387	Goalw [real_diff_def]
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	388	"((x::real) ^ 2 = y ^ 2) = (x = y \| x = -y)";
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	389	by (auto_tac (claset(),simpset() delsimps [thm "realpow_Suc"]));
c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	390	by (dtac (rename_numerals (real_eq_minus_iff RS iffD1 RS sym)) 1);
c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	391	by (auto_tac (claset() addDs [rename_numerals real_add_minus_eq_minus],
c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	392	simpset() addsimps [realpow_two_add_minus] delsimps [thm "realpow_Suc"]));
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	393	qed "realpow_two_disj";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	394
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	395	(* used in Transc *)
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	396	Goal "[\|x ~= #0; m <= n \|] ==> x ^ (n - m) = x ^ n * rinv(x ^ m)";
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	397	by (auto_tac (claset(),
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	398	simpset() addsimps [le_eq_less_or_eq,
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	399	less_iff_Suc_add,realpow_add,
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	400	realpow_not_zero] @ real_mult_ac));
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	401	qed "realpow_diff";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	402
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	403	Goal "real_of_nat (m) ^ n = real_of_nat (m ^ n)";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	404	by (induct_tac "n" 1);
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	405	by (auto_tac (claset(),
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	406	simpset() addsimps [real_of_nat_one, real_of_nat_mult]));
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	407	qed "realpow_real_of_nat";
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	408
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	409	Goal "#0 < real_of_nat (2 ^ n)";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	410	by (induct_tac "n" 1);
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	411	by (auto_tac (claset(),
99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	412	simpset() addsimps [real_of_nat_mult, real_zero_less_mult_iff]));
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	413	qed "realpow_real_of_nat_two_pos";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	414	Addsimps [realpow_real_of_nat_two_pos];
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	415
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	416
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	417	(* REALORD.ML, AFTER real_rinv_less_iff *)
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	418	Goal "[\| 0 < r; 0 < x\|] ==> (rinv x <= rinv r) = (r <= x)";
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	419	by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	420	real_rinv_less_iff]) 1);
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	421	qed "real_rinv_le_iff";
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	422
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	423	Goal "(#0::real) <= x --> #0 <= y --> x ^ Suc n <= y ^ Suc n --> x <= y";
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	424	by (induct_tac "n" 1);
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	425	by Auto_tac;
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	426	by (rtac real_leI 1);
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	427	by (auto_tac (claset(),
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	428	simpset() addsimps [inst "x" "#0" order_le_less,
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	429	real_mult_le_0_iff]));
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	430	by (subgoal_tac "rinv x * (x * (x * x ^ n)) <= rinv y * (y * (y * y ^ n))" 1);
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	431	by (rtac real_mult_le_mono 2);
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	432	by (asm_full_simp_tac (simpset() addsimps [realpow_ge_zero, real_0_le_mult_iff]) 4);
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	433	by (asm_full_simp_tac (simpset() addsimps [real_rinv_le_iff]) 3);
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	434	by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	435	by (rtac real_rinv_gt_zero 1);
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	436	by Auto_tac;
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	437	qed_spec_mp "realpow_increasing";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	438
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	439	Goal "[\| (#0::real) <= x; #0 <= y; x ^ Suc n = y ^ Suc n \|] ==> x = y";
99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	440	by (blast_tac (claset() addIs [realpow_increasing, order_antisym,
99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	441	order_eq_refl, sym]) 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	442	qed_spec_mp "realpow_Suc_cancel_eq";

author	wenzelm
	Mon, 02 Oct 2000 14:59:04 +0200
changeset 10128	98ddd0138cbf
parent 10043	a0364652e115
child 10606	e3229a37d53f
permissions	-rw-r--r--