src/HOL/Power.thy

--- a/src/HOL/Power.thy	Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Power.thy	Tue Oct 19 18:18:45 2004 +0200
@@ -22,10 +22,10 @@
 
 text{*It looks plausible as a simprule, but its effect can be strange.*}
 lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::recpower))"
-by (induct_tac "n", auto)
+by (induct "n", auto)
 
 lemma power_one [simp]: "1^n = (1::'a::recpower)"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: power_Suc)
 done
 
@@ -33,23 +33,23 @@
 by (simp add: power_Suc)
 
 lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)"
-apply (induct_tac "n")
+apply (induct "n")
 apply (simp_all add: power_Suc mult_ac)
 done
 
 lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (simp_all add: power_Suc power_add)
 done
 
 lemma power_mult_distrib: "((a::'a::recpower) * b) ^ n = (a^n) * (b^n)"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: power_Suc mult_ac)
 done
 
 lemma zero_less_power:
      "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (simp_all add: power_Suc zero_less_one mult_pos)
 done
 
@@ -62,7 +62,7 @@
 
 lemma one_le_power:
      "1 \<le> (a::'a::{ordered_semidom,recpower}) ==> 1 \<le> a^n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (simp_all add: power_Suc)
 apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
 apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
@@ -124,7 +124,7 @@
 
 lemma power_mono:
      "[|a \<le> b; (0::'a::{recpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (simp_all add: power_Suc)
 apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b])
 done
@@ -132,20 +132,20 @@
 lemma power_strict_mono [rule_format]:
      "[|a < b; (0::'a::{recpower,ordered_semidom}) \<le> a|]
       ==> 0 < n --> a^n < b^n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: mult_strict_mono zero_le_power power_Suc
                       order_le_less_trans [of 0 a b])
 done
 
 lemma power_eq_0_iff [simp]:
      "(a^n = 0) = (a = (0::'a::{ordered_idom,recpower}) & 0<n)"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
 done
 
 lemma field_power_eq_0_iff [simp]:
      "(a^n = 0) = (a = (0::'a::{field,recpower}) & 0<n)"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: power_Suc field_mult_eq_0_iff zero_neq_one[THEN not_sym])
 done
 
@@ -154,14 +154,14 @@
 
 lemma nonzero_power_inverse:
   "a \<noteq> 0 ==> inverse ((a::'a::{field,recpower}) ^ n) = (inverse a) ^ n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute)
 done
 
 text{*Perhaps these should be simprules.*}
 lemma power_inverse:
   "inverse ((a::'a::{field,division_by_zero,recpower}) ^ n) = (inverse a) ^ n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: power_Suc inverse_mult_distrib)
 done
 
@@ -177,7 +177,7 @@
 done
 
 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,recpower}) ^ n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: power_Suc abs_mult)
 done
 
@@ -193,7 +193,7 @@
 
 lemma zero_le_power_abs [simp]:
      "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n"
-apply (induct_tac "n")
+apply (induct "n")
 apply (auto simp add: zero_le_one zero_le_power)
 done
 
@@ -207,7 +207,7 @@
 lemma power_Suc_less:
      "[|(0::'a::{ordered_semidom,recpower}) < a; a < 1|]
       ==> a * a^n < a^n"
-apply (induct_tac n)
+apply (induct n)
 apply (auto simp add: power_Suc mult_strict_left_mono)
 done
 
@@ -215,7 +215,7 @@
      "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,recpower})|]
       ==> a^N < a^n"
 apply (erule rev_mp)
-apply (induct_tac "N")
+apply (induct "N")
 apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
 apply (rename_tac m)
 apply (subgoal_tac "a * a^m < 1 * a^n", simp)
@@ -228,7 +228,7 @@
      "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semidom,recpower})|]
       ==> a^N \<le> a^n"
 apply (erule rev_mp)
-apply (induct_tac "N")
+apply (induct "N")
 apply (auto simp add: power_Suc  le_Suc_eq)
 apply (rename_tac m)
 apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
@@ -245,7 +245,7 @@
 lemma power_increasing:
      "[|n \<le> N; (1::'a::{ordered_semidom,recpower}) \<le> a|] ==> a^n \<le> a^N"
 apply (erule rev_mp)
-apply (induct_tac "N")
+apply (induct "N")
 apply (auto simp add: power_Suc le_Suc_eq)
 apply (rename_tac m)
 apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
@@ -256,14 +256,14 @@
 text{*Lemma for @{text power_strict_increasing}*}
 lemma power_less_power_Suc:
      "(1::'a::{ordered_semidom,recpower}) < a ==> a^n < a * a^n"
-apply (induct_tac n)
+apply (induct n)
 apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
 done
 
 lemma power_strict_increasing:
      "[|n < N; (1::'a::{ordered_semidom,recpower}) < a|] ==> a^n < a^N"
 apply (erule rev_mp)
-apply (induct_tac "N")
+apply (induct "N")
 apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
 apply (rename_tac m)
 apply (subgoal_tac "1 * a^n < a * a^m", simp)
@@ -332,10 +332,10 @@
 done
 
 lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
-by (induct_tac "n", auto)
+by (induct "n", auto)
 
 lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
-apply (induct_tac "j")
+apply (induct "j")
 apply (simp_all add: le_Suc_eq)
 apply (blast dest!: dvd_mult_right)
 done
@@ -371,7 +371,7 @@
 by simp
 
 lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
-apply (induct_tac "n", auto)
+apply (induct "n", auto)
 apply (erule allE)
 apply (erule mp, arith)
 done
@@ -379,15 +379,15 @@
 declare binomial_0 [simp del] binomial_Suc [simp del]
 
 lemma binomial_n_n [simp]: "(n choose n) = 1"
-apply (induct_tac "n")
+apply (induct "n")
 apply (simp_all add: binomial_eq_0)
 done
 
 lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
-by (induct_tac "n", simp_all)
+by (induct "n", simp_all)
 
 lemma binomial_1 [simp]: "(n choose Suc 0) = n"
-by (induct_tac "n", simp_all)
+by (induct "n", simp_all)
 
 lemma zero_less_binomial [rule_format]: "k \<le> n --> 0 < (n choose k)"
 by (rule_tac m = n and n = k in diff_induct, simp_all)
@@ -404,7 +404,7 @@
 (*Might be more useful if re-oriented*)
 lemma Suc_times_binomial_eq [rule_format]:
      "\<forall>k. k \<le> n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
-apply (induct_tac "n")
+apply (induct "n")
 apply (simp add: binomial_0, clarify)
 apply (case_tac "k")
 apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq