src/HOL/Hyperreal/Transcendental.thy

 done
 
 lemma lemma_STAR_sin [simp]:
      "(if even n then 0  
        else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
-by (induct_tac "n", auto)
+by (induct "n", auto)
 
 lemma lemma_STAR_cos [simp]:
      "0 < n -->  
       (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct_tac "n", auto)
+by (induct "n", auto)
 
 lemma lemma_STAR_cos1 [simp]:
      "0 < n -->  
       (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct_tac "n", auto)
+by (induct "n", auto)
 
 lemma lemma_STAR_cos2 [simp]:
      "sumr 1 n (%n. if even n  
                     then (- 1) ^ (n div 2)/(real (fact n)) *  
                           0 ^ n  
                     else 0) = 0"
-apply (induct_tac "n")
+apply (induct "n")
 apply (case_tac [2] "n", auto)
 done
 
 lemma exp_converges: "(%n. inverse (real (fact n)) * x ^ n) sums exp(x)"
 apply (simp add: exp_def)

 apply (rule summable_cos [THEN summable_sums])
 done
 
 lemma lemma_realpow_diff [rule_format (no_asm)]:
      "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
-apply (induct_tac "n", auto)
+apply (induct "n", auto)
 apply (subgoal_tac "p = Suc n")
 apply (simp (no_asm_simp), auto)
 apply (drule sym)
 apply (simp add: Suc_diff_le mult_commute realpow_Suc [symmetric] 
        del: realpow_Suc)

 done
 
 lemma lemma_realpow_diff_sumr2:
      "x ^ (Suc n) - y ^ (Suc n) =  
       (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))"
-apply (induct_tac "n", simp)
+apply (induct "n", simp)
 apply (auto simp del: sumr_Suc)
 apply (subst sumr_Suc)
 apply (drule sym)
 apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: sumr_Suc)
 done

 text{*Show that we can shift the terms down one*}
 lemma lemma_diffs:
      "sumr 0 n (%n. (diffs c)(n) * (x ^ n)) =  
       sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) +  
       (real n * c(n) * x ^ (n - Suc 0))"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def)
 done
 
 lemma lemma_diffs2:
      "sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) =  

 
 lemma abs_exp_cancel [simp]: "\<bar>exp x\<bar> = exp x"
 by auto
 
 lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: real_of_nat_Suc right_distrib exp_add mult_commute)
 done
 
 lemma exp_diff: "exp(x - y) = exp(x)/(exp y)"
 apply (simp add: diff_minus divide_inverse)

 
 lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
 by (simp add: cos_add cos_double)
 
 lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: real_of_nat_Suc left_distrib)
 done
 
 lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: real_of_nat_Suc left_distrib)
 done
 
 lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
 apply (cut_tac n = n in sin_npi)