(*  Title       : RealPow.ML
    ID          : $Id: RealPow.ML,v 1.4 1999/09/23 16:39:09 paulson Exp $
    Author      : Jacques D. Fleuriot  
    Copyright   : 1998  University of Cambridge
    Description : Natural Powers of reals theory

*)

Goal "0r ^ (Suc n) = 0r";
by (Auto_tac);
qed "realpow_zero";
Addsimps [realpow_zero];

Goal "r ~= 0r --> r ^ n ~= 0r";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [real_mult_not_zeroE],
    simpset() addsimps [real_zero_not_eq_one RS not_sym]));
qed_spec_mp "realpow_not_zero";

Goal "r ^ n = 0r ==> r = 0r";
by (blast_tac (claset() addIs [ccontr] 
    addDs [realpow_not_zero]) 1);
qed "realpow_zero_zero";

Goal "r ~= 0r --> rinv(r ^ n) = (rinv r) ^ n";
by (induct_tac "n" 1);
by (Auto_tac);
by (forw_inst_tac [("n","n")] realpow_not_zero 1);
by (auto_tac (claset() addDs [real_rinv_distrib],
    simpset()));
qed_spec_mp "realpow_rinv";

Goal "rabs r ^ n = rabs (r ^ n)";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps 
    [rabs_mult,rabs_one]));
qed "realpow_rabs";

Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps real_mult_ac));
qed "realpow_add";

Goal "(r::real) ^ 1 = r";
by (Simp_tac 1);
qed "realpow_one";
Addsimps [realpow_one];

Goal "(r::real) ^ 2 = r * r";
by (Simp_tac 1);
qed "realpow_two";

Goal "0r < r --> 0r <= r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addDs [real_less_imp_le] 
    addIs [real_le_mult_order],simpset()));
qed_spec_mp "realpow_ge_zero";

Goal "0r < r --> 0r < r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [real_mult_order],
    simpset() addsimps [real_zero_less_one]));
qed_spec_mp "realpow_gt_zero";

Goal "0r <= r --> 0r <= r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [real_le_mult_order],
              simpset()));
qed_spec_mp "realpow_ge_zero2";

Goal "0r < x & x <= y --> x ^ n <= y ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addSIs [real_mult_le_mono],
    simpset()));
by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1);
qed_spec_mp "realpow_le";

Goal "0r <= x & x <= y --> x ^ n <= y ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addSIs [real_mult_le_mono4],
    simpset()));
by (asm_simp_tac (simpset() addsimps [realpow_ge_zero2]) 1);
qed_spec_mp "realpow_le2";

Goal "0r < x & x < y & 0 < n --> x ^ n < y ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [real_mult_less_mono,
    gr0I] addDs [realpow_gt_zero],simpset()));
qed_spec_mp "realpow_less";

Goal  "1r ^ n = 1r";
by (induct_tac "n" 1);
by (Auto_tac);
qed "realpow_eq_one";
Addsimps [realpow_eq_one];

(** New versions using #0 and #1 instead of 0r and 1r
    REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)

Addsimps (map (rename_numerals thy) [realpow_zero, realpow_eq_one]);


Goal "rabs(-(1r ^ n)) = 1r";
by (simp_tac (simpset() addsimps 
    [rabs_minus_cancel,rabs_one]) 1);
qed "rabs_minus_realpow_one";
Addsimps [rabs_minus_realpow_one];

Goal "rabs((-1r) ^ n) = 1r";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [rabs_mult,
         rabs_minus_cancel,rabs_one]));
qed "rabs_realpow_minus_one";
Addsimps [rabs_realpow_minus_one];

Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps real_mult_ac));
qed "realpow_mult";

Goal "0r <= r ^ 2";
by (simp_tac (simpset() addsimps [realpow_two]) 1);
qed "realpow_two_le";
Addsimps [realpow_two_le];

Goal "rabs(x ^ 2) = x ^ 2";
by (simp_tac (simpset() addsimps [rabs_eqI1]) 1);
qed "rabs_realpow_two";
Addsimps [rabs_realpow_two];

Goal "rabs(x) ^ 2 = x ^ 2";
by (simp_tac (simpset() addsimps 
    [realpow_rabs,rabs_eqI1] delsimps [realpow_Suc]) 1);
qed "realpow_two_rabs";
Addsimps [realpow_two_rabs];

Goal "1r < r ==> 1r < r ^ 2";
by (auto_tac (claset(),simpset() addsimps [realpow_two]));
by (cut_facts_tac [real_zero_less_one] 1);
by (forw_inst_tac [("R1.0","0r")] real_less_trans 1);
by (assume_tac 1);
by (dres_inst_tac [("z","r"),("x","1r")] real_mult_less_mono1 1);
by (auto_tac (claset() addIs [real_less_trans],simpset()));
qed "realpow_two_gt_one";

Goal "1r < r --> 1r <= r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
	      simpset()));
by (dtac (real_zero_less_one RS real_mult_less_mono) 1);
by (auto_tac (claset() addSIs [real_less_imp_le],
	      simpset() addsimps [real_zero_less_one]));
qed_spec_mp "realpow_ge_one";

Goal "1r < r ==> 1r < r ^ (Suc n)";
by (forw_inst_tac [("n","n")] realpow_ge_one 1);
by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
by (dtac sym 2);
by (forward_tac [real_zero_less_one RS real_less_trans] 1);
by (dres_inst_tac [("y","r ^ n")] real_mult_less_mono2 1);
by (auto_tac (claset() addDs [real_less_trans],
     simpset()));
qed "realpow_Suc_gt_one";

Goal "1r <= r ==> 1r <= r ^ n";
by (dtac real_le_imp_less_or_eq 1); 
by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
qed "realpow_ge_one2";

Goal "0r < r ==> 0r < r ^ Suc n";
by (forw_inst_tac [("n","n")] realpow_ge_zero 1);
by (forw_inst_tac [("n1","n")]
    ((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1);
by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
     addIs [real_mult_order],simpset()));
qed "realpow_Suc_gt_zero";

Goal "0r <= r ==> 0r <= r ^ Suc n";
by (etac (real_le_imp_less_or_eq RS disjE) 1);
by (etac (realpow_ge_zero) 1);
by (Asm_simp_tac 1);
qed "realpow_Suc_ge_zero";

Goal "(#1::real) <= #2 ^ n";
by (res_inst_tac [("j","#1 ^ n")] real_le_trans 1);
by (rtac realpow_le 2);
by (auto_tac (claset() addIs [real_less_imp_le],
	      simpset() addsimps [zero_eq_numeral_0]));
qed "two_realpow_ge_one";

Goal "real_of_nat n < #2 ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(),
	      simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1,
				  real_mult_2,
				  real_of_nat_Suc, real_of_nat_zero,
				  real_add_less_le_mono, two_realpow_ge_one]));
qed "two_realpow_gt";
Addsimps [two_realpow_gt,two_realpow_ge_one];

Goal "(-1r) ^ (2*n) = 1r";
by (induct_tac "n" 1);
by (Auto_tac);
qed "realpow_minus_one";
Addsimps [realpow_minus_one];

Goal "(-1r) ^ (n + n) = 1r";
by (induct_tac "n" 1);
by (Auto_tac);
qed "realpow_minus_one2";
Addsimps [realpow_minus_one2];

Goal "(-1r) ^ Suc (n + n) = -1r";
by (induct_tac "n" 1);
by (Auto_tac);
qed "realpow_minus_one_odd";
Addsimps [realpow_minus_one_odd];

Goal "(-1r) ^ Suc (Suc (n + n)) = 1r";
by (induct_tac "n" 1);
by (Auto_tac);
qed "realpow_minus_one_even";
Addsimps [realpow_minus_one_even];

Goal "0r < r & r < 1r --> r ^ Suc n < r ^ n";
by (induct_tac "n" 1);
by (Auto_tac);
qed_spec_mp "realpow_Suc_less";

Goal "0r <= r & r < 1r --> r ^ Suc n <= r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addIs [real_less_imp_le] addSDs
     [real_le_imp_less_or_eq],simpset()));
qed_spec_mp "realpow_Suc_le";

Goal "0r <= 0r ^ n";
by (exhaust_tac "n" 1);
by (Auto_tac);
qed "realpow_zero_le";
Addsimps [realpow_zero_le];

Goal "0r < r & r < 1r --> r ^ Suc n <= r ^ n";
by (blast_tac (claset() addSIs [real_less_imp_le,
    realpow_Suc_less]) 1);
qed_spec_mp "realpow_Suc_le2";

Goal "[| 0r <= r; r < 1r |] ==> r ^ Suc n <= r ^ n";
by (etac (real_le_imp_less_or_eq RS disjE) 1);
by (rtac realpow_Suc_le2 1);
by (Auto_tac);
qed "realpow_Suc_le3";

Goal "0r <= r & r < 1r & n < N --> r ^ N <= r ^ n";
by (induct_tac "N" 1);
by (Auto_tac);
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
by (ALLGOALS(dtac real_mult_le_mono3));
by (REPEAT(assume_tac 1));
by (REPEAT(assume_tac 3));
by (auto_tac (claset(),simpset() addsimps 
    [less_Suc_eq]));
qed_spec_mp "realpow_less_le";

Goal "[| 0r <= r; r < 1r; n <= N |] ==> r ^ N <= r ^ n";
by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
by (auto_tac (claset() addIs [realpow_less_le],
    simpset()));
qed "realpow_le_le";

Goal "[| 0r < r; r < 1r |] ==> r ^ Suc n <= r";
by (dres_inst_tac [("n","1"),("N","Suc n")] 
    (real_less_imp_le RS realpow_le_le) 1);
by (Auto_tac);
qed "realpow_Suc_le_self";

Goal "[| 0r < r; r < 1r |] ==> r ^ Suc n < 1r";
by (blast_tac (claset() addIs [realpow_Suc_le_self,
               real_le_less_trans]) 1);
qed "realpow_Suc_less_one";

Goal "1r <= r --> r ^ n <= r ^ Suc n";
by (induct_tac "n" 1);
by (auto_tac (claset() addSIs [real_mult_le_le_mono1],simpset()));
by (rtac ccontr 1 THEN dtac not_real_leE 1);
by (dtac real_le_less_trans 1 THEN assume_tac 1);
by (etac (real_zero_less_one RS real_less_asym) 1);
qed_spec_mp "realpow_le_Suc";

Goal "1r < r --> r ^ n < r ^ Suc n";
by (induct_tac "n" 1);
by (auto_tac (claset() addSIs [real_mult_less_mono2],simpset()));
by (rtac ccontr 1 THEN dtac real_leI 1);
by (dtac real_less_le_trans 1 THEN assume_tac 1);
by (etac (real_zero_less_one RS real_less_asym) 1);
qed_spec_mp "realpow_less_Suc";

Goal "1r < r --> r ^ n <= r ^ Suc n";
by (blast_tac (claset() addSIs [real_less_imp_le,
    realpow_less_Suc]) 1);
qed_spec_mp "realpow_le_Suc2";

Goal "1r < r & n < N --> r ^ n <= r ^ N";
by (induct_tac "N" 1);
by (Auto_tac);
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
by (ALLGOALS(dtac real_mult_self_le));
by (assume_tac 1);
by (assume_tac 2);
by (auto_tac (claset() addIs [real_le_trans],
    simpset() addsimps [less_Suc_eq]));
qed_spec_mp "realpow_gt_ge";

Goal "1r <= r & n < N --> r ^ n <= r ^ N";
by (induct_tac "N" 1);
by (Auto_tac);
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
by (ALLGOALS(dtac real_mult_self_le2));
by (assume_tac 1);
by (assume_tac 2);
by (auto_tac (claset() addIs [real_le_trans],
    simpset() addsimps [less_Suc_eq]));
qed_spec_mp "realpow_gt_ge2";

Goal "[| 1r < r; n <= N |] ==> r ^ n <= r ^ N";
by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
by (auto_tac (claset() addIs [realpow_gt_ge],simpset()));
qed "realpow_ge_ge";

Goal "[| 1r <= r; n <= N |] ==> r ^ n <= r ^ N";
by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
by (auto_tac (claset() addIs [realpow_gt_ge2],simpset()));
qed "realpow_ge_ge2";

Goal "1r < r ==> r <= r ^ Suc n";
by (dres_inst_tac [("n","1"),("N","Suc n")] 
    realpow_ge_ge 1);
by (Auto_tac);
qed_spec_mp "realpow_Suc_ge_self";

Goal "1r <= r ==> r <= r ^ Suc n";
by (dres_inst_tac [("n","1"),("N","Suc n")] 
    realpow_ge_ge2 1);
by (Auto_tac);
qed_spec_mp "realpow_Suc_ge_self2";

Goal "[| 1r < r; 0 < n |] ==> r <= r ^ n";
by (dtac (less_not_refl2 RS  not0_implies_Suc) 1);
by (auto_tac (claset() addSIs 
    [realpow_Suc_ge_self],simpset()));
qed "realpow_ge_self";

Goal "[| 1r <= r; 0 < n |] ==> r <= r ^ n";
by (dtac (less_not_refl2 RS  not0_implies_Suc) 1);
by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset()));
qed "realpow_ge_self2";

Goal "0 < n --> (x::real) ^ (n - 1) * x = x ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() 
    addsimps [real_mult_commute]));
qed_spec_mp "realpow_minus_mult";
Addsimps [realpow_minus_mult];

Goal "r ~= 0r ==> r * rinv(r) ^ 2 = rinv r";
by (asm_simp_tac (simpset() addsimps [realpow_two,
                  real_mult_assoc RS sym]) 1);
qed "realpow_two_mult_rinv";
Addsimps [realpow_two_mult_rinv];


goal RealPow.thy "(-x) ^ 2 = (x::real) ^ 2";
by (Simp_tac 1);
qed "realpow_two_minus";
Addsimps [realpow_two_minus];

goal RealPow.thy "(x::real) ^ 2 + - (y ^ 2) = (x + -y) * (x + y)";
by (simp_tac (simpset() addsimps [real_add_mult_distrib2,
    real_add_mult_distrib, real_minus_mult_eq2 RS sym] 
    @ real_mult_ac) 1);
qed "realpow_two_add_minus";

goalw RealPow.thy [real_diff_def] 
      "(x::real) ^ 2 - y ^ 2 = (x - y) * (x + y)";
by (simp_tac (simpset() addsimps [realpow_two_add_minus]
               delsimps [realpow_Suc]) 1);
qed "realpow_two_diff";

goalw RealPow.thy [real_diff_def] 
      "((x::real) ^ 2 = y ^ 2) = (x = y | x = -y)";
by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
by (dtac ((real_eq_minus_iff RS iffD1) RS sym) 1);
by (auto_tac (claset() addSDs [real_mult_zero_disj]
    addDs [real_add_minus_eq_minus],
    simpset() addsimps [realpow_two_add_minus]
    delsimps [realpow_Suc]));
qed "realpow_two_disj";


goal RealPow.thy "!!x. [|x ~= 0r; m <= n |] ==> \
\      x ^ (n - m) = x ^ n * rinv(x ^ m)";
by (auto_tac (claset(),simpset() addsimps [le_eq_less_or_eq,
    less_iff_Suc_add,realpow_add,
    realpow_not_zero] @ real_mult_ac));
qed "realpow_diff";

goal RealPow.thy "real_of_nat (m) ^ n = real_of_nat (m ^ n)";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [real_of_nat_one,
    real_of_nat_mult]));
qed "realpow_real_of_nat";

goal RealPow.thy "0r < real_of_nat (2 ^ n)";
by (induct_tac "n" 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [real_of_nat_one,
    real_of_nat_add RS sym,real_zero_less_one,real_add_order])));
qed "realpow_real_of_nat_two_pos";
Addsimps [realpow_real_of_nat_two_pos];

Goal "0r <= x & 0r <= y &  x ^ Suc n <= y ^ Suc n --> x <= y";
by (induct_tac "n" 1);
by (Auto_tac);
by (dtac not_real_leE 1);
by (auto_tac (claset() addDs [real_less_asym],
    simpset() addsimps [real_le_less]));
by (forw_inst_tac [("r","y")] real_rinv_less_swap 1);
by (rtac real_linear_less2 2);
by (rtac real_linear_less2 5);
by (dtac ((real_not_refl2 RS not_sym) RS real_mult_not_zero) 9);
by (Auto_tac);
by (forw_inst_tac [("t","0r")] (real_not_refl2 RS not_sym) 1);
by (forward_tac [real_rinv_gt_zero] 1);
by (forw_inst_tac [("t","0r")] (real_not_refl2 RS not_sym) 3);
by (dtac real_rinv_gt_zero 3);
by (dtac real_mult_less_zero 3);
by (forw_inst_tac [("x","(y * y ^ n)"),("r1.0","y")] 
    real_mult_less_mono 2);
by (dres_inst_tac [("x","x * (x * x ^ n)"),("r1.0","rinv x")] 
    real_mult_less_mono 1);
by (Auto_tac);
by (auto_tac (claset() addIs [real_mult_order,realpow_gt_zero],
    simpset() addsimps [real_mult_assoc 
    RS sym,real_not_refl2 RS not_sym]));
qed_spec_mp "realpow_increasing";
  
Goal "0r <= x & 0r <= y &  x ^ Suc n = y ^ Suc n --> x = y";
by (induct_tac "n" 1);
by (Auto_tac);
by (res_inst_tac [("R1.0","x"),("R2.0","y")] 
    real_linear_less2 1);
by (auto_tac (claset() addDs [real_less_asym],
    simpset() addsimps [real_le_less]));
by (dres_inst_tac [("n","Suc(Suc n)")]
    (conjI RSN(2,conjI RS realpow_less)) 1);
by (dres_inst_tac [("n","Suc(Suc n)"),("x","y")]
    (conjI RSN(2,conjI RS realpow_less)) 5);
by (EVERY[dtac sym 4, dtac not_sym 4, rtac sym 4]);
by (auto_tac (claset() addDs [real_not_refl2 RS not_sym,
     real_mult_not_zero] addIs [ccontr],simpset()));
qed_spec_mp "realpow_Suc_cancel_eq";

(** New versions using #0 and #1 instead of 0r and 1r
    REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)

Addsimps (map (rename_numerals thy) 
	  [realpow_two_le, realpow_zero_le,
	   rabs_minus_realpow_one, rabs_realpow_minus_one,
	   realpow_minus_one, realpow_minus_one2, realpow_minus_one_odd]);