isabelle: src/HOL/Real/RealPow.ML@3c19160b6432 (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	*)
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	8
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	9	Goal "0r ^ (Suc n) = 0r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	10	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	11	qed "realpow_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	12	Addsimps [realpow_zero];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	13
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	14	Goal "r ~= 0r --> r ^ n ~= 0r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	15	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	16	by (auto_tac (claset() addIs [real_mult_not_zeroE],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	17	simpset() addsimps [real_zero_not_eq_one RS not_sym]));
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
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	20	Goal "r ^ n = 0r ==> r = 0r";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	21	by (blast_tac (claset() addIs [ccontr]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	22	addDs [realpow_not_zero]) 1);
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
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	25	Goal "r ~= 0r --> rinv(r ^ n) = (rinv r) ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	26	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	27	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	28	by (forw_inst_tac [("n","n")] realpow_not_zero 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	29	by (auto_tac (claset() addDs [real_rinv_distrib],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	30	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	31	qed_spec_mp "realpow_rinv";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	32
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	33	Goal "rabs r ^ n = rabs (r ^ n)";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	34	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	35	by (auto_tac (claset(),simpset() addsimps
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	36	[rabs_mult,rabs_one]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	37	qed "realpow_rabs";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	38
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	39	Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	40	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	41	by (auto_tac (claset(),simpset() addsimps real_mult_ac));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	42	qed "realpow_add";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	43
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	44	Goal "(r::real) ^ 1 = r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	45	by (Simp_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	46	qed "realpow_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	47	Addsimps [realpow_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	48
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	49	Goal "(r::real) ^ 2 = r * r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	50	by (Simp_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	51	qed "realpow_two";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	52
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	53	Goal "0r < r --> 0r <= r ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	54	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	55	by (auto_tac (claset() addDs [real_less_imp_le]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	56	addIs [real_le_mult_order],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	57	qed_spec_mp "realpow_ge_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	58
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	59	Goal "0r < r --> 0r < r ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	60	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	61	by (auto_tac (claset() addIs [real_mult_order],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	62	simpset() addsimps [real_zero_less_one]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	63	qed_spec_mp "realpow_gt_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	64
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	65	Goal "0r <= r --> 0r <= r ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	66	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	67	by (auto_tac (claset() addIs [real_le_mult_order],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	68	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	69	qed_spec_mp "realpow_ge_zero2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	70
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	71	Goal "0r < x & x <= y --> x ^ n <= y ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	72	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	73	by (auto_tac (claset() addSIs [real_mult_le_mono],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	74	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	75	by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	76	qed_spec_mp "realpow_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	77
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	78	Goal "0r <= x & x <= y --> x ^ n <= y ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	79	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	80	by (auto_tac (claset() addSIs [real_mult_le_mono4],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	81	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	82	by (asm_simp_tac (simpset() addsimps [realpow_ge_zero2]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	83	qed_spec_mp "realpow_le2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	84
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	85	Goal "0r < x & x < y & 0 < n --> x ^ n < y ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	86	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	87	by (auto_tac (claset() addIs [real_mult_less_mono,
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	88	gr0I] addDs [realpow_gt_zero],simpset()));
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
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	91	Goal "1r ^ n = 1r";
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
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	97	(** New versions using #0 and #1 instead of 0r and 1r
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	98	REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	99
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	100	Addsimps (map (rename_numerals thy) [realpow_zero, realpow_eq_one]);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	101
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	102
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	103	Goal "rabs(-(1r ^ n)) = 1r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	104	by (simp_tac (simpset() addsimps
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	105	[rabs_minus_cancel,rabs_one]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	106	qed "rabs_minus_realpow_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	107	Addsimps [rabs_minus_realpow_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	108
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	109	Goal "rabs((-1r) ^ n) = 1r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	110	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	111	by (auto_tac (claset(),simpset() addsimps [rabs_mult,
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	112	rabs_minus_cancel,rabs_one]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	113	qed "rabs_realpow_minus_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	114	Addsimps [rabs_realpow_minus_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	115
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	116	Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	117	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	118	by (auto_tac (claset(),simpset() addsimps real_mult_ac));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	119	qed "realpow_mult";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	120
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	121	Goal "0r <= r ^ 2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	122	by (simp_tac (simpset() addsimps [realpow_two]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	123	qed "realpow_two_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	124	Addsimps [realpow_two_le];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	125
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	126	Goal "rabs(x ^ 2) = x ^ 2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	127	by (simp_tac (simpset() addsimps [rabs_eqI1]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	128	qed "rabs_realpow_two";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	129	Addsimps [rabs_realpow_two];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	130
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	131	Goal "rabs(x) ^ 2 = x ^ 2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	132	by (simp_tac (simpset() addsimps
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	133	[realpow_rabs,rabs_eqI1] delsimps [realpow_Suc]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	134	qed "realpow_two_rabs";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	135	Addsimps [realpow_two_rabs];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	136
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	137	Goal "1r < r ==> 1r < r ^ 2";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	138	by (auto_tac (claset(),simpset() addsimps [realpow_two]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	139	by (cut_facts_tac [real_zero_less_one] 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	140	by (forw_inst_tac [("R1.0","0r")] real_less_trans 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	141	by (assume_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	142	by (dres_inst_tac [("z","r"),("x","1r")] real_mult_less_mono1 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	143	by (auto_tac (claset() addIs [real_less_trans],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	144	qed "realpow_two_gt_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	145
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	146	Goal "1r < r --> 1r <= r ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	147	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	148	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	149	simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	150	by (dtac (real_zero_less_one RS real_mult_less_mono) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	151	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	152	simpset() addsimps [real_zero_less_one]));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	153	qed_spec_mp "realpow_ge_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	154
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	155	Goal "1r < r ==> 1r < r ^ (Suc n)";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	156	by (forw_inst_tac [("n","n")] realpow_ge_one 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	157	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	158	by (dtac sym 2);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	159	by (forward_tac [real_zero_less_one RS real_less_trans] 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	160	by (dres_inst_tac [("y","r ^ n")] real_mult_less_mono2 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	161	by (auto_tac (claset() addDs [real_less_trans],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	162	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	163	qed "realpow_Suc_gt_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	164
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	165	Goal "1r <= r ==> 1r <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	166	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	167	by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	168	qed "realpow_ge_one2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	169
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	170	Goal "0r < r ==> 0r < r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	171	by (forw_inst_tac [("n","n")] realpow_ge_zero 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	172	by (forw_inst_tac [("n1","n")]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	173	((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	174	by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	175	addIs [real_mult_order],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	176	qed "realpow_Suc_gt_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	177
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	178	Goal "0r <= r ==> 0r <= r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	179	by (etac (real_le_imp_less_or_eq RS disjE) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	180	by (etac (realpow_ge_zero) 1);
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	181	by (Asm_simp_tac 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	182	qed "realpow_Suc_ge_zero";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	183
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	184	Goal "(#1::real) <= #2 ^ n";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	185	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	186	by (rtac realpow_le 2);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	187	by (auto_tac (claset() addIs [real_less_imp_le],
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	188	simpset() addsimps [zero_eq_numeral_0]));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	189	qed "two_realpow_ge_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	190
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	191	Goal "real_of_nat n < #2 ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	192	by (induct_tac "n" 1);
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	193	by (auto_tac (claset(),
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	194	simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1,
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	195	real_mult_2,
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	196	real_of_nat_Suc, real_of_nat_zero,
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	197	real_add_less_le_mono, two_realpow_ge_one]));
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	198	qed "two_realpow_gt";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	199	Addsimps [two_realpow_gt,two_realpow_ge_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	200
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	201	Goal "(-1r) ^ (2*n) = 1r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	202	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	203	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	204	qed "realpow_minus_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	205	Addsimps [realpow_minus_one];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	206
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	207	Goal "(-1r) ^ (n + n) = 1r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	208	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	209	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	210	qed "realpow_minus_one2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	211	Addsimps [realpow_minus_one2];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	212
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	213	Goal "(-1r) ^ Suc (n + n) = -1r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	214	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	215	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	216	qed "realpow_minus_one_odd";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	217	Addsimps [realpow_minus_one_odd];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	218
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	219	Goal "(-1r) ^ Suc (Suc (n + n)) = 1r";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	220	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	221	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	222	qed "realpow_minus_one_even";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	223	Addsimps [realpow_minus_one_even];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	224
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	225	Goal "0r < r & r < 1r --> r ^ Suc n < r ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	226	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	227	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	228	qed_spec_mp "realpow_Suc_less";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	229
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	230	Goal "0r <= r & r < 1r --> r ^ Suc n <= r ^ n";
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 (claset() addIs [real_less_imp_le] addSDs
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	233	[real_le_imp_less_or_eq],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	234	qed_spec_mp "realpow_Suc_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	235
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	236	Goal "0r <= 0r ^ n";
8423 3c19160b6432 exhaust_tac -> cases_tac nipkow parents: 7588 diff changeset	237	by (cases_tac "n" 1);
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	238	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	239	qed "realpow_zero_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	240	Addsimps [realpow_zero_le];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	241
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	242	Goal "0r < r & r < 1r --> r ^ Suc n <= r ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	243	by (blast_tac (claset() addSIs [real_less_imp_le,
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	244	realpow_Suc_less]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	245	qed_spec_mp "realpow_Suc_le2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	246
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	247	Goal "[\| 0r <= r; r < 1r \|] ==> r ^ Suc n <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	248	by (etac (real_le_imp_less_or_eq RS disjE) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	249	by (rtac realpow_Suc_le2 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	250	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	251	qed "realpow_Suc_le3";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	252
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	253	Goal "0r <= r & r < 1r & n < N --> r ^ N <= r ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	254	by (induct_tac "N" 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	by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	257	by (ALLGOALS(dtac real_mult_le_mono3));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	258	by (REPEAT(assume_tac 1));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	259	by (REPEAT(assume_tac 3));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	260	by (auto_tac (claset(),simpset() addsimps
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	261	[less_Suc_eq]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	262	qed_spec_mp "realpow_less_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	263
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	264	Goal "[\| 0r <= r; r < 1r; n <= N \|] ==> r ^ N <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	265	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	266	by (auto_tac (claset() addIs [realpow_less_le],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	267	simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	268	qed "realpow_le_le";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	269
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	270	Goal "[\| 0r < r; r < 1r \|] ==> r ^ Suc n <= r";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	271	by (dres_inst_tac [("n","1"),("N","Suc n")]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	272	(real_less_imp_le RS realpow_le_le) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	273	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	274	qed "realpow_Suc_le_self";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	275
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	276	Goal "[\| 0r < r; r < 1r \|] ==> r ^ Suc n < 1r";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	277	by (blast_tac (claset() addIs [realpow_Suc_le_self,
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	278	real_le_less_trans]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	279	qed "realpow_Suc_less_one";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	280
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	281	Goal "1r <= r --> r ^ n <= r ^ Suc n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	282	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	283	by (auto_tac (claset() addSIs [real_mult_le_le_mono1],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	284	by (rtac ccontr 1 THEN dtac not_real_leE 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	285	by (dtac real_le_less_trans 1 THEN assume_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	286	by (etac (real_zero_less_one RS real_less_asym) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	287	qed_spec_mp "realpow_le_Suc";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	288
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	289	Goal "1r < r --> r ^ n < r ^ Suc n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	290	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	291	by (auto_tac (claset() addSIs [real_mult_less_mono2],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	292	by (rtac ccontr 1 THEN dtac real_leI 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	293	by (dtac real_less_le_trans 1 THEN assume_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	294	by (etac (real_zero_less_one RS real_less_asym) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	295	qed_spec_mp "realpow_less_Suc";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	296
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	297	Goal "1r < r --> r ^ n <= r ^ Suc n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	298	by (blast_tac (claset() addSIs [real_less_imp_le,
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	299	realpow_less_Suc]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	300	qed_spec_mp "realpow_le_Suc2";
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 "1r < r & n < N --> r ^ n <= r ^ 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);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	305	by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	306	by (ALLGOALS(dtac real_mult_self_le));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	307	by (assume_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	308	by (assume_tac 2);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	309	by (auto_tac (claset() addIs [real_le_trans],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	310	simpset() addsimps [less_Suc_eq]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	311	qed_spec_mp "realpow_gt_ge";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	312
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	313	Goal "1r <= r & n < N --> r ^ n <= r ^ N";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	314	by (induct_tac "N" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	315	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	316	by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	317	by (ALLGOALS(dtac real_mult_self_le2));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	318	by (assume_tac 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	319	by (assume_tac 2);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	320	by (auto_tac (claset() addIs [real_le_trans],
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	321	simpset() addsimps [less_Suc_eq]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	322	qed_spec_mp "realpow_gt_ge2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	323
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	324	Goal "[\| 1r < r; n <= N \|] ==> r ^ n <= r ^ N";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	325	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	326	by (auto_tac (claset() addIs [realpow_gt_ge],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	327	qed "realpow_ge_ge";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	328
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	329	Goal "[\| 1r <= r; n <= N \|] ==> r ^ n <= r ^ N";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	330	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	331	by (auto_tac (claset() addIs [realpow_gt_ge2],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	332	qed "realpow_ge_ge2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	333
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	334	Goal "1r < r ==> r <= r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	335	by (dres_inst_tac [("n","1"),("N","Suc n")]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	336	realpow_ge_ge 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	337	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	338	qed_spec_mp "realpow_Suc_ge_self";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	339
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	340	Goal "1r <= r ==> r <= r ^ Suc n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	341	by (dres_inst_tac [("n","1"),("N","Suc n")]
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	342	realpow_ge_ge2 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	343	by (Auto_tac);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	344	qed_spec_mp "realpow_Suc_ge_self2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	345
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	346	Goal "[\| 1r < r; 0 < n \|] ==> r <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	347	by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	348	by (auto_tac (claset() addSIs
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	349	[realpow_Suc_ge_self],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	350	qed "realpow_ge_self";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	351
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	352	Goal "[\| 1r <= r; 0 < n \|] ==> r <= r ^ n";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	353	by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	354	by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset()));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	355	qed "realpow_ge_self2";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	356
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	357	Goal "0 < n --> (x::real) ^ (n - 1) * x = x ^ n";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	358	by (induct_tac "n" 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	359	by (auto_tac (claset(),simpset()
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	360	addsimps [real_mult_commute]));
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	361	qed_spec_mp "realpow_minus_mult";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	362	Addsimps [realpow_minus_mult];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	363
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: 7219 diff changeset	364	Goal "r ~= 0r ==> r * rinv(r) ^ 2 = rinv r";
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	365	by (asm_simp_tac (simpset() addsimps [realpow_two,
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	366	real_mult_assoc RS sym]) 1);
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	367	qed "realpow_two_mult_rinv";
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	368	Addsimps [realpow_two_mult_rinv];
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: diff changeset	369
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	370
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	371	(** New versions using #0 and #1 instead of 0r and 1r
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	372	REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	373
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	374	Addsimps (map (rename_numerals thy)
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	375	[realpow_two_le, realpow_zero_le,
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	376	rabs_minus_realpow_one, rabs_realpow_minus_one,
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7292 diff changeset	377	realpow_minus_one, realpow_minus_one2, realpow_minus_one_odd]);

author	nipkow
	Mon, 13 Mar 2000 12:51:10 +0100
changeset 8423	3c19160b6432
parent 7588	26384af93359
child 8442	96023903c2df
permissions	-rw-r--r--