isabelle: src/HOL/Real/RealPow.ML@2c6605049646 (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
10690 cd80241125b0 tidying and adding new proofs paulson parents: 10677 diff changeset	8	bind_thm ("realpow_Suc", thm "realpow_Suc");
cd80241125b0 tidying and adding new proofs paulson parents: 10677 diff changeset	9
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	10	Goal "(#0::real) ^ (Suc n) = #0";
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	11	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	12	qed "realpow_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	13	Addsimps [realpow_zero];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	14
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	15	Goal "r ~= (#0::real) --> r ^ n ~= #0";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	16	by (induct_tac "n" 1);
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	17	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	18	qed_spec_mp "realpow_not_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	19
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	20	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	21	by (rtac ccontr 1);
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	22	by (auto_tac (claset() addDs [realpow_not_zero], simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	23	qed "realpow_zero_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	24
10648 a8c647cfa31f first stage in tidying up Real and Hyperreal. paulson parents: 10606 diff changeset	25	Goal "inverse ((r::real) ^ n) = (inverse r) ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	26	by (induct_tac "n" 1);
10648 a8c647cfa31f first stage in tidying up Real and Hyperreal. paulson parents: 10606 diff changeset	27	by (auto_tac (claset(), simpset() addsimps [real_inverse_distrib]));
a8c647cfa31f first stage in tidying up Real and Hyperreal. paulson parents: 10606 diff changeset	28	qed "realpow_inverse";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	29
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	30	Goal "abs (r::real) ^ n = abs (r ^ n)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	31	by (induct_tac "n" 1);
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	32	by (auto_tac (claset(), simpset() addsimps [abs_mult]));
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	33	qed "realpow_abs";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	34
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	35	Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	36	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	37	by (auto_tac (claset(),simpset() addsimps real_mult_ac));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	38	qed "realpow_add";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	39
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	40	Goal "(r::real) ^ 1 = r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	41	by (Simp_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	42	qed "realpow_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	43	Addsimps [realpow_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	44
10712 351ba950d4d9 further tidying paulson parents: 10699 diff changeset	45	Goal "(r::real)^2 = r * r";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	46	by (Simp_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	47	qed "realpow_two";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	48
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	49	Goal "(#0::real) < r --> #0 <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	50	by (induct_tac "n" 1);
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	51	by (auto_tac (claset() addDs [order_less_imp_le]
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	52	addIs [rename_numerals real_le_mult_order],
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	53	simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	54	qed_spec_mp "realpow_ge_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	55
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	56	Goal "(#0::real) < r --> #0 < r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	57	by (induct_tac "n" 1);
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	58	by (auto_tac (claset() addIs [rename_numerals real_mult_order],
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	59	simpset() addsimps [real_zero_less_one]));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	60	qed_spec_mp "realpow_gt_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	61
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	62	Goal "(#0::real) <= r --> #0 <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	63	by (induct_tac "n" 1);
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	64	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	65	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	66	qed_spec_mp "realpow_ge_zero2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	67
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	68	Goal "(#0::real) < x & x <= y --> x ^ n <= y ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	69	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	70	by (auto_tac (claset() addSIs [real_mult_le_mono],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	71	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	72	by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	73	qed_spec_mp "realpow_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	74
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	75	Goal "(#0::real) <= x & x <= y --> x ^ n <= y ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	76	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	77	by (auto_tac (claset() addSIs [real_mult_le_mono4],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	78	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	79	by (asm_simp_tac (simpset() addsimps [realpow_ge_zero2]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	80	qed_spec_mp "realpow_le2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	81
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	82	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	83	by (induct_tac "n" 1);
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	84	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	85	addDs [realpow_gt_zero],
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	86	simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	87	qed_spec_mp "realpow_less";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	88
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	89	Goal "#1 ^ n = (#1::real)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	90	by (induct_tac "n" 1);
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	91	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	92	qed "realpow_eq_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	93	Addsimps [realpow_eq_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	94
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	95	Goal "abs((#-1) ^ n) = (#1::real)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	96	by (induct_tac "n" 1);
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	97	by (auto_tac (claset(), simpset() addsimps [abs_mult]));
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	98	qed "abs_realpow_minus_one";
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	99	Addsimps [abs_realpow_minus_one];
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	100
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	101	Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	102	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	103	by (auto_tac (claset(),simpset() addsimps real_mult_ac));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	104	qed "realpow_mult";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	105
10712 351ba950d4d9 further tidying paulson parents: 10699 diff changeset	106	Goal "(#0::real) <= r^2";
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	107	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	108	qed "realpow_two_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	109	Addsimps [realpow_two_le];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	110
10712 351ba950d4d9 further tidying paulson parents: 10699 diff changeset	111	Goal "abs((x::real)^2) = x^2";
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	112	by (simp_tac (simpset() addsimps [abs_eqI1,
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	113	rename_numerals real_le_square]) 1);
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	114	qed "abs_realpow_two";
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	115	Addsimps [abs_realpow_two];
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	116
10712 351ba950d4d9 further tidying paulson parents: 10699 diff changeset	117	Goal "abs(x::real) ^ 2 = x^2";
10690 cd80241125b0 tidying and adding new proofs paulson parents: 10677 diff changeset	118	by (simp_tac (simpset() addsimps [realpow_abs,abs_eqI1]
cd80241125b0 tidying and adding new proofs paulson parents: 10677 diff changeset	119	delsimps [realpow_Suc]) 1);
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	120	qed "realpow_two_abs";
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 8442 diff changeset	121	Addsimps [realpow_two_abs];
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	122
10712 351ba950d4d9 further tidying paulson parents: 10699 diff changeset	123	Goal "(#1::real) < r ==> #1 < r^2";
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	124	by Auto_tac;
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	125	by (cut_facts_tac [rename_numerals real_zero_less_one] 1);
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	126	by (forw_inst_tac [("x","#0")] order_less_trans 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	127	by (assume_tac 1);
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	128	by (dres_inst_tac [("z","r"),("x","#1")]
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	129	(rename_numerals real_mult_less_mono1) 1);
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	130	by (auto_tac (claset() addIs [order_less_trans], simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	131	qed "realpow_two_gt_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	132
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	133	Goal "(#1::real) < r --> #1 <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	134	by (induct_tac "n" 1);
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	135	by Auto_tac;
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	136	by (subgoal_tac "#1#1 <= r r^n" 1);
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	137	by (rtac real_mult_le_mono 2);
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	138	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	139	qed_spec_mp "realpow_ge_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	140
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	141	Goal "(#1::real) <= r ==> #1 <= r ^ n";
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	142	by (dtac order_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	143	by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	144	qed "realpow_ge_one2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	145
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	146	Goal "(#1::real) <= #2 ^ n";
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	147	by (res_inst_tac [("y","#1 ^ n")] order_trans 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	148	by (rtac realpow_le 2);
10778 2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10752 diff changeset	149	by (auto_tac (claset() addIs [order_less_imp_le], simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	150	qed "two_realpow_ge_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	151
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	152	Goal "real_of_nat n < #2 ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	153	by (induct_tac "n" 1);
10778 2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10752 diff changeset	154	by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	155	by (stac real_mult_2 1);
99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	156	by (rtac real_add_less_le_mono 1);
10778 2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10752 diff changeset	157	by (auto_tac (claset(), simpset() addsimps [two_realpow_ge_one]));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	158	qed "two_realpow_gt";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	159	Addsimps [two_realpow_gt,two_realpow_ge_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	160
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	161	Goal "(#-1) ^ (#2*n) = (#1::real)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	162	by (induct_tac "n" 1);
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	163	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	164	qed "realpow_minus_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	165	Addsimps [realpow_minus_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	166
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	167	Goal "(#-1) ^ Suc (#2*n) = -(#1::real)";
36625483213f further round of tidying paulson parents: 10648 diff changeset	168	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	169	qed "realpow_minus_one_odd";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	170	Addsimps [realpow_minus_one_odd];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	171
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	172	Goal "(#-1) ^ Suc (Suc (#2*n)) = (#1::real)";
36625483213f further round of tidying paulson parents: 10648 diff changeset	173	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	174	qed "realpow_minus_one_even";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	175	Addsimps [realpow_minus_one_even];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	176
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	177	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	178	by (induct_tac "n" 1);
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	179	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	180	qed_spec_mp "realpow_Suc_less";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	181
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	182	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	183	by (induct_tac "n" 1);
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	184	by (auto_tac (claset() addIs [order_less_imp_le]
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	185	addSDs [order_le_imp_less_or_eq],
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	186	simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	187	qed_spec_mp "realpow_Suc_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	188
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	189	Goal "(#0::real) <= #0 ^ n";
8442 96023903c2df case_tac now subsumes both boolean and datatype cases; wenzelm parents: 8423 diff changeset	190	by (case_tac "n" 1);
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	191	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	192	qed "realpow_zero_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	193	Addsimps [realpow_zero_le];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	194
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	195	Goal "#0 < r & r < (#1::real) --> r ^ Suc n <= r ^ n";
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	196	by (blast_tac (claset() addSIs [order_less_imp_le,
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	197	realpow_Suc_less]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	198	qed_spec_mp "realpow_Suc_le2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	199
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	200	Goal "[\| #0 <= r; r < (#1::real) \|] ==> r ^ Suc n <= r ^ n";
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	201	by (etac (order_le_imp_less_or_eq RS disjE) 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	202	by (rtac realpow_Suc_le2 1);
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	203	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	204	qed "realpow_Suc_le3";
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 "#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	207	by (induct_tac "N" 1);
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	208	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	209	by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	210	by (ALLGOALS(dtac (rename_numerals real_mult_le_mono3)));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	211	by (REPEAT(assume_tac 1));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	212	by (REPEAT(assume_tac 3));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	213	by (auto_tac (claset(),simpset() addsimps
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	214	[less_Suc_eq]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	215	qed_spec_mp "realpow_less_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	216
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	217	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	218	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	219	by (auto_tac (claset() addIs [realpow_less_le],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	220	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	221	qed "realpow_le_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	222
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	223	Goal "[\| #0 < r; r < (#1::real) \|] ==> r ^ Suc n <= r";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	224	by (dres_inst_tac [("n","1"),("N","Suc n")]
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	225	(order_less_imp_le RS realpow_le_le) 1);
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	226	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	227	qed "realpow_Suc_le_self";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	228
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	229	Goal "[\| #0 < r; r < (#1::real) \|] ==> r ^ Suc n < #1";
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	230	by (blast_tac (claset() addIs [realpow_Suc_le_self, order_le_less_trans]) 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	231	qed "realpow_Suc_less_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	232
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	233	Goal "(#1::real) <= r --> r ^ n <= r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	234	by (induct_tac "n" 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	235	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	236	qed_spec_mp "realpow_le_Suc";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	237
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	238	Goal "(#1::real) < r --> r ^ n < r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	239	by (induct_tac "n" 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	240	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	241	qed_spec_mp "realpow_less_Suc";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	242
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	243	Goal "(#1::real) < r --> r ^ n <= r ^ Suc n";
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	244	by (blast_tac (claset() addSIs [order_less_imp_le, realpow_less_Suc]) 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	245	qed_spec_mp "realpow_le_Suc2";
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 "(#1::real) < r & n < N --> r ^ n <= r ^ N";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	248	by (induct_tac "N" 1);
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	249	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	250	by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	251	by (ALLGOALS(dtac (rename_numerals real_mult_self_le)));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	252	by (assume_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	253	by (assume_tac 2);
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	254	by (auto_tac (claset() addIs [order_trans],
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	255	simpset() addsimps [less_Suc_eq]));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	256	qed_spec_mp "realpow_gt_ge";
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 "(#1::real) <= r & 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);
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	260	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	261	by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
9428 c8eb573114de rename_numerals: use implicit theory context; wenzelm parents: 9070 diff changeset	262	by (ALLGOALS(dtac (rename_numerals real_mult_self_le2)));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	263	by (assume_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	264	by (assume_tac 2);
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	265	by (auto_tac (claset() addIs [order_trans],
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	266	simpset() addsimps [less_Suc_eq]));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	267	qed_spec_mp "realpow_gt_ge2";
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 "[\| (#1::real) < r; 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);
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	271	by (auto_tac (claset() addIs [realpow_gt_ge], simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	272	qed "realpow_ge_ge";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	273
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	274	Goal "[\| (#1::real) <= r; n <= N \|] ==> r ^ n <= r ^ N";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	275	by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	276	by (auto_tac (claset() addIs [realpow_gt_ge2], simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	277	qed "realpow_ge_ge2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	278
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	279	Goal "(#1::real) < r ==> r <= r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	280	by (dres_inst_tac [("n","1"),("N","Suc n")]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	281	realpow_ge_ge 1);
10677 36625483213f further round of tidying paulson parents: 10648 diff changeset	282	by Auto_tac;
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	283	qed_spec_mp "realpow_Suc_ge_self";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	284
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	285	Goal "(#1::real) <= r ==> r <= r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	286	by (dres_inst_tac [("n","1"),("N","Suc n")]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	287	realpow_ge_ge2 1);
10677 36625483213f further round of tidying paulson parents: 10648 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_Suc_ge_self2";
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; 0 < n \|] ==> r <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	292	by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	293	by (auto_tac (claset() addSIs
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	294	[realpow_Suc_ge_self],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	295	qed "realpow_ge_self";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	296
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	297	Goal "[\| (#1::real) <= r; 0 < n \|] ==> r <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	298	by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	299	by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	300	qed "realpow_ge_self2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	301
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	302	Goal "0 < n --> (x::real) ^ (n - 1) * x = x ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	303	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	304	by (auto_tac (claset(),simpset()
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	305	addsimps [real_mult_commute]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	306	qed_spec_mp "realpow_minus_mult";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	307	Addsimps [realpow_minus_mult];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	308
10606 e3229a37d53f converted rinv to inverse; bauerg parents: 10043 diff changeset	309	Goal "r ~= #0 ==> r * inverse r ^ 2 = inverse (r::real)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	310	by (asm_simp_tac (simpset() addsimps [realpow_two,
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	311	real_mult_assoc RS sym]) 1);
10606 e3229a37d53f converted rinv to inverse; bauerg parents: 10043 diff changeset	312	qed "realpow_two_mult_inverse";
e3229a37d53f converted rinv to inverse; bauerg parents: 10043 diff changeset	313	Addsimps [realpow_two_mult_inverse];
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	314
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	315	(* 05/00 *)
10712 351ba950d4d9 further tidying paulson parents: 10699 diff changeset	316	Goal "(-x)^2 = (x::real) ^ 2";
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	317	by (Simp_tac 1);
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	318	qed "realpow_two_minus";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	319	Addsimps [realpow_two_minus];
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	320
10712 351ba950d4d9 further tidying paulson parents: 10699 diff changeset	321	Goalw [real_diff_def] "(x::real)^2 - y^2 = (x - y) * (x + y)";
351ba950d4d9 further tidying paulson parents: 10699 diff changeset	322	by (simp_tac (simpset() addsimps
351ba950d4d9 further tidying paulson parents: 10699 diff changeset	323	[real_add_mult_distrib2, real_add_mult_distrib,
351ba950d4d9 further tidying paulson parents: 10699 diff changeset	324	real_minus_mult_eq2 RS sym] @ real_mult_ac) 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	325	qed "realpow_two_diff";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	326
10712 351ba950d4d9 further tidying paulson parents: 10699 diff changeset	327	Goalw [real_diff_def] "((x::real)^2 = y^2) = (x = y \| x = -y)";
351ba950d4d9 further tidying paulson parents: 10699 diff changeset	328	by (cut_inst_tac [("x","x"),("y","y")] realpow_two_diff 1);
351ba950d4d9 further tidying paulson parents: 10699 diff changeset	329	by (auto_tac (claset(), simpset() delsimps [realpow_Suc]));
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	330	qed "realpow_two_disj";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	331
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	332	(* used in Transc *)
10606 e3229a37d53f converted rinv to inverse; bauerg parents: 10043 diff changeset	333	Goal "[\|(x::real) ~= #0; m <= n \|] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)";
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	334	by (auto_tac (claset(),
10712 351ba950d4d9 further tidying paulson parents: 10699 diff changeset	335	simpset() addsimps [le_eq_less_or_eq, less_iff_Suc_add, realpow_add,
351ba950d4d9 further tidying paulson parents: 10699 diff changeset	336	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	337	qed "realpow_diff";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	338
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	339	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	340	by (induct_tac "n" 1);
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	341	by (auto_tac (claset(),
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	342	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	343	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	344
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	345	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	346	by (induct_tac "n" 1);
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	347	by (auto_tac (claset(),
99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	348	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	349	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	350	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	351
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	352
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	353	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	354	by (induct_tac "n" 1);
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	355	by Auto_tac;
10752 c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	356	by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	357	by (swap_res_tac [real_mult_less_mono'] 1);
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	358	by Auto_tac;
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	359	by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff]));
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	360	by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	361	by (dres_inst_tac [("n","n")] realpow_gt_zero 1);
c4f1bf2acf4c tidying, and separation of HOL-Hyperreal from HOL-Real paulson parents: 10715 diff changeset	362	by Auto_tac;
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	363	qed_spec_mp "realpow_increasing";
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	364
9070 99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	365	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	366	by (blast_tac (claset() addIs [realpow_increasing, order_antisym,
99d93349914b full_rename_numerals -> rename_numerals; tidied paulson parents: 9043 diff changeset	367	order_eq_refl, sym]) 1);
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	368	qed_spec_mp "realpow_Suc_cancel_eq";

author	paulson
	Thu, 04 Jan 2001 10:23:01 +0100
changeset 10778	2c6605049646
parent 10752	c4f1bf2acf4c
child 10784	27e4d90b35b5
permissions	-rw-r--r--