converted some induct_tac to induct
authorpaulson
Tue Oct 19 18:18:45 2004 +0200 (2004-10-19)
changeset 15251bb6f072c8d10
parent 15250 217bececa2bd
child 15252 d4f1b11c336b
converted some induct_tac to induct
src/HOL/Complex/CSeries.thy
src/HOL/Divides.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hyperreal/EvenOdd.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/IntDiv.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/Parity.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/Nat.thy
src/HOL/Power.thy
src/HOL/Real/RealPow.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Complex/CSeries.thy	Mon Oct 18 13:40:45 2004 +0200
     1.2 +++ b/src/HOL/Complex/CSeries.thy	Tue Oct 19 18:18:45 2004 +0200
     1.3 @@ -30,30 +30,30 @@
     1.4  *)
     1.5  
     1.6  lemma sumc_Suc_zero [simp]: "sumc (Suc n) n f = 0"
     1.7 -by (induct_tac "n", auto)
     1.8 +by (induct "n", auto)
     1.9  
    1.10  lemma sumc_eq_bounds [simp]: "sumc m m f = 0"
    1.11 -by (induct_tac "m", auto)
    1.12 +by (induct "m", auto)
    1.13  
    1.14  lemma sumc_Suc_eq [simp]: "sumc m (Suc m) f = f(m)"
    1.15  by auto
    1.16  
    1.17  lemma sumc_add_lbound_zero [simp]: "sumc (m+k) k f = 0"
    1.18 -by (induct_tac "k", auto)
    1.19 +by (induct "k", auto)
    1.20  
    1.21  lemma sumc_add: "sumc m n f + sumc m n g = sumc m n (%n. f n + g n)"
    1.22 -apply (induct_tac "n")
    1.23 +apply (induct "n")
    1.24  apply (auto simp add: add_ac)
    1.25  done
    1.26  
    1.27  lemma sumc_mult: "r * sumc m n f = sumc m n (%n. r * f n)"
    1.28 -apply (induct_tac "n", auto)
    1.29 +apply (induct "n", auto)
    1.30  apply (auto simp add: right_distrib)
    1.31  done
    1.32  
    1.33  lemma sumc_split_add [rule_format]:
    1.34       "n < p --> sumc 0 n f + sumc n p f = sumc 0 p f"
    1.35 -apply (induct_tac "p") 
    1.36 +apply (induct "p") 
    1.37  apply (auto dest!: leI dest: le_anti_sym)
    1.38  done
    1.39  
    1.40 @@ -64,16 +64,16 @@
    1.41  done
    1.42  
    1.43  lemma sumc_cmod: "cmod(sumc m n f) \<le> sumr m n (%i. cmod(f i))"
    1.44 -apply (induct_tac "n")
    1.45 +apply (induct "n")
    1.46  apply (auto intro: complex_mod_triangle_ineq [THEN order_trans])
    1.47  done
    1.48  
    1.49  lemma sumc_fun_eq [rule_format (no_asm)]:
    1.50       "(\<forall>r. m \<le> r & r < n --> f r = g r) --> sumc m n f = sumc m n g"
    1.51 -by (induct_tac "n", auto)
    1.52 +by (induct "n", auto)
    1.53  
    1.54  lemma sumc_const [simp]: "sumc 0 n (%i. r) = complex_of_real (real n) * r"
    1.55 -apply (induct_tac "n")
    1.56 +apply (induct "n")
    1.57  apply (auto simp add: left_distrib real_of_nat_Suc)
    1.58  done
    1.59  
    1.60 @@ -86,29 +86,29 @@
    1.61  by (simp add: diff_minus sumc_add_mult_const)
    1.62  
    1.63  lemma sumc_less_bounds_zero [rule_format]: "n < m --> sumc m n f = 0"
    1.64 -by (induct_tac "n", auto)
    1.65 +by (induct "n", auto)
    1.66  
    1.67  lemma sumc_minus: "sumc m n (%i. - f i) = - sumc m n f"
    1.68 -by (induct_tac "n", auto)
    1.69 +by (induct "n", auto)
    1.70  
    1.71  lemma sumc_shift_bounds: "sumc (m+k) (n+k) f = sumc m n (%i. f(i + k))"
    1.72 -by (induct_tac "n", auto)
    1.73 +by (induct "n", auto)
    1.74  
    1.75  lemma sumc_minus_one_complexpow_zero [simp]:
    1.76       "sumc 0 (2*n) (%i. (-1) ^ Suc i) = 0"
    1.77 -by (induct_tac "n", auto)
    1.78 +by (induct "n", auto)
    1.79  
    1.80  lemma sumc_interval_const [rule_format (no_asm)]:
    1.81       "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
    1.82        --> sumc m na f = (complex_of_real(real (na - m)) * r)"
    1.83 -apply (induct_tac "na")
    1.84 +apply (induct "na")
    1.85  apply (auto simp add: Suc_diff_le real_of_nat_Suc left_distrib)
    1.86  done
    1.87  
    1.88  lemma sumc_interval_const2 [rule_format (no_asm)]:
    1.89       "(\<forall>n. m \<le> n --> f n = r) & m \<le> na  
    1.90        --> sumc m na f = (complex_of_real(real (na - m)) * r)"
    1.91 -apply (induct_tac "na")
    1.92 +apply (induct "na")
    1.93  apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc)
    1.94  done
    1.95  
    1.96 @@ -148,14 +148,14 @@
    1.97  ***)
    1.98  
    1.99  lemma sumr_cmod_ge_zero [iff]: "0 \<le> sumr m n (%n. cmod (f n))"
   1.100 -by (induct_tac "n", auto simp add: add_increasing) 
   1.101 +by (induct "n", auto simp add: add_increasing) 
   1.102  
   1.103  lemma rabs_sumc_cmod_cancel [simp]:
   1.104       "abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))"
   1.105  by (simp add: abs_if linorder_not_less)
   1.106  
   1.107  lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0"
   1.108 -apply (induct_tac "n")
   1.109 +apply (induct "n")
   1.110  apply (case_tac [2] "n", auto)
   1.111  done
   1.112  
   1.113 @@ -164,12 +164,12 @@
   1.114  
   1.115  lemma sumc_subst [rule_format (no_asm)]:
   1.116       "(\<forall>p. (m \<le> p & p < m + n --> (f p = g p))) --> sumc m n f = sumc m n g"
   1.117 -by (induct_tac "n", auto)
   1.118 +by (induct "n", auto)
   1.119  
   1.120  lemma sumc_group [simp]:
   1.121       "sumc 0 n (%m. sumc (m * k) (m*k + k) f) = sumc 0 (n * k) f"
   1.122  apply (subgoal_tac "k = 0 | 0 < k", auto)
   1.123 -apply (induct_tac "n")
   1.124 +apply (induct "n")
   1.125  apply (auto simp add: sumc_split_add add_commute)
   1.126  done
   1.127  
     2.1 --- a/src/HOL/Divides.thy	Mon Oct 18 13:40:45 2004 +0200
     2.2 +++ b/src/HOL/Divides.thy	Tue Oct 19 18:18:45 2004 +0200
     2.3 @@ -88,7 +88,7 @@
     2.4  by (simp add: mod_geq)
     2.5  
     2.6  lemma mod_1 [simp]: "m mod Suc 0 = 0"
     2.7 -apply (induct_tac "m")
     2.8 +apply (induct "m")
     2.9  apply (simp_all (no_asm_simp) add: mod_geq)
    2.10  done
    2.11  
    2.12 @@ -98,7 +98,7 @@
    2.13  done
    2.14  
    2.15  lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
    2.16 -apply (subgoal_tac " (n + m) mod n = (n+m-n) mod n") 
    2.17 +apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n") 
    2.18  apply (simp add: add_commute)
    2.19  apply (subst mod_geq [symmetric], simp_all)
    2.20  done
    2.21 @@ -107,7 +107,7 @@
    2.22  by (simp add: add_commute mod_add_self2)
    2.23  
    2.24  lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
    2.25 -apply (induct_tac "k")
    2.26 +apply (induct "k")
    2.27  apply (simp_all add: add_left_commute [of _ n])
    2.28  done
    2.29  
    2.30 @@ -117,7 +117,7 @@
    2.31  lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
    2.32  apply (case_tac "n=0", simp)
    2.33  apply (case_tac "k=0", simp)
    2.34 -apply (induct_tac "m" rule: nat_less_induct)
    2.35 +apply (induct "m" rule: nat_less_induct)
    2.36  apply (subst mod_if, simp)
    2.37  apply (simp add: mod_geq diff_less diff_mult_distrib)
    2.38  done
    2.39 @@ -127,7 +127,7 @@
    2.40  
    2.41  lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
    2.42  apply (case_tac "n=0", simp)
    2.43 -apply (induct_tac "m", simp)
    2.44 +apply (induct "m", simp)
    2.45  apply (rename_tac "k")
    2.46  apply (cut_tac m = "k*n" and n = n in mod_add_self2)
    2.47  apply (simp add: add_commute)
    2.48 @@ -158,7 +158,7 @@
    2.49  (*Main Result about quotient and remainder.*)
    2.50  lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
    2.51  apply (case_tac "n=0", simp)
    2.52 -apply (induct_tac "m" rule: nat_less_induct)
    2.53 +apply (induct "m" rule: nat_less_induct)
    2.54  apply (subst mod_if)
    2.55  apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse diff_less)
    2.56  done
    2.57 @@ -219,7 +219,7 @@
    2.58  by (cut_tac m = m and n = n in mod_div_equality2, arith)
    2.59  
    2.60  lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
    2.61 -apply (induct_tac "m" rule: nat_less_induct)
    2.62 +apply (induct "m" rule: nat_less_induct)
    2.63  apply (case_tac "na<n", simp) 
    2.64  txt{*case @{term "n \<le> na"}*}
    2.65  apply (simp add: mod_geq diff_less)
    2.66 @@ -389,7 +389,7 @@
    2.67  subsection{*Further Facts about Quotient and Remainder*}
    2.68  
    2.69  lemma div_1 [simp]: "m div Suc 0 = m"
    2.70 -apply (induct_tac "m")
    2.71 +apply (induct "m")
    2.72  apply (simp_all (no_asm_simp) add: div_geq)
    2.73  done
    2.74  
    2.75 @@ -397,7 +397,7 @@
    2.76  by (simp add: div_geq)
    2.77  
    2.78  lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
    2.79 -apply (subgoal_tac " (n + m) div n = Suc ((n+m-n) div n) ")
    2.80 +apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
    2.81  apply (simp add: add_commute)
    2.82  apply (subst div_geq [symmetric], simp_all)
    2.83  done
    2.84 @@ -418,7 +418,7 @@
    2.85  lemma div_le_mono [rule_format (no_asm)]:
    2.86       "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
    2.87  apply (case_tac "k=0", simp)
    2.88 -apply (induct_tac "n" rule: nat_less_induct, clarify)
    2.89 +apply (induct "n" rule: nat_less_induct, clarify)
    2.90  apply (case_tac "n<k")
    2.91  (* 1  case n<k *)
    2.92  apply simp
    2.93 @@ -434,13 +434,13 @@
    2.94  lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
    2.95  apply (subgoal_tac "0<n")
    2.96   prefer 2 apply simp 
    2.97 -apply (induct_tac "k" rule: nat_less_induct)
    2.98 +apply (induct_tac k rule: nat_less_induct)
    2.99  apply (rename_tac "k")
   2.100  apply (case_tac "k<n", simp)
   2.101  apply (subgoal_tac "~ (k<m) ")
   2.102   prefer 2 apply simp 
   2.103  apply (simp add: div_geq)
   2.104 -apply (subgoal_tac " (k-n) div n \<le> (k-m) div n")
   2.105 +apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
   2.106   prefer 2
   2.107   apply (blast intro: div_le_mono diff_le_mono2)
   2.108  apply (rule le_trans, simp)
   2.109 @@ -457,14 +457,14 @@
   2.110  (* Similar for "less than" *) 
   2.111  lemma div_less_dividend [rule_format, simp]:
   2.112       "!!n::nat. 1<n ==> 0 < m --> m div n < m"
   2.113 -apply (induct_tac "m" rule: nat_less_induct)
   2.114 +apply (induct_tac m rule: nat_less_induct)
   2.115  apply (rename_tac "m")
   2.116  apply (case_tac "m<n", simp)
   2.117  apply (subgoal_tac "0<n")
   2.118   prefer 2 apply simp 
   2.119  apply (simp add: div_geq)
   2.120  apply (case_tac "n<m")
   2.121 - apply (subgoal_tac " (m-n) div n < (m-n) ")
   2.122 + apply (subgoal_tac "(m-n) div n < (m-n) ")
   2.123    apply (rule impI less_trans_Suc)+
   2.124  apply assumption
   2.125    apply (simp_all add: diff_less)
   2.126 @@ -473,7 +473,7 @@
   2.127  text{*A fact for the mutilated chess board*}
   2.128  lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
   2.129  apply (case_tac "n=0", simp)
   2.130 -apply (induct_tac "m" rule: nat_less_induct)
   2.131 +apply (induct "m" rule: nat_less_induct)
   2.132  apply (case_tac "Suc (na) <n")
   2.133  (* case Suc(na) < n *)
   2.134  apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
     3.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Oct 18 13:40:45 2004 +0200
     3.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Oct 19 18:18:45 2004 +0200
     3.3 @@ -392,7 +392,7 @@
     3.4  lemma ex_has_greatest_nat_lemma:
     3.5    "P k ==> \<forall>x. P x --> (\<exists>y. P y & ~ ((m y::nat) <= m x))
     3.6      ==> \<exists>y. P y & ~ (m y < m k + n)"
     3.7 -  apply (induct_tac n, force)
     3.8 +  apply (induct n, force)
     3.9    apply (force simp add: le_Suc_eq)
    3.10    done
    3.11  
     4.1 --- a/src/HOL/Hyperreal/EvenOdd.thy	Mon Oct 18 13:40:45 2004 +0200
     4.2 +++ b/src/HOL/Hyperreal/EvenOdd.thy	Tue Oct 19 18:18:45 2004 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4  subsection{*General Lemmas About Division*}
     4.5  
     4.6  lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
     4.7 -apply (induct_tac "m")
     4.8 +apply (induct "m")
     4.9  apply (simp_all add: mod_Suc)
    4.10  done
    4.11  
     5.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Mon Oct 18 13:40:45 2004 +0200
     5.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Tue Oct 19 18:18:45 2004 +0200
     5.3 @@ -601,7 +601,7 @@
     5.4  lemma HNatInfinite_FreeUltrafilterNat_lemma:
     5.5       "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
     5.6        ==> {n. N < f n} \<in> FreeUltrafilterNat"
     5.7 -apply (induct_tac "N")
     5.8 +apply (induct_tac N)
     5.9  apply (drule_tac x = 0 in spec)
    5.10  apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem, drule FreeUltrafilterNat_Int, assumption, simp)
    5.11  apply (drule_tac x = "Suc n" in spec, ultra)
     6.1 --- a/src/HOL/Hyperreal/Integration.thy	Mon Oct 18 13:40:45 2004 +0200
     6.2 +++ b/src/HOL/Hyperreal/Integration.thy	Tue Oct 19 18:18:45 2004 +0200
     6.3 @@ -96,7 +96,7 @@
     6.4  
     6.5  lemma lemma_partition_lt_gen [rule_format]:
     6.6   "partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) --> D(m) < D(m + Suc d)"
     6.7 -apply (induct_tac "d", auto simp add: partition)
     6.8 +apply (induct "d", auto simp add: partition)
     6.9  apply (blast dest: Suc_le_lessD  intro: less_le_trans order_less_trans)
    6.10  done
    6.11  
    6.12 @@ -133,11 +133,11 @@
    6.13  
    6.14  lemma partition_lb: "partition(a,b) D ==> a \<le> D(r)"
    6.15  apply (frule partition [THEN iffD1], safe)
    6.16 -apply (induct_tac "r")
    6.17 -apply (cut_tac [2] y = "Suc n" and x = "psize D" in linorder_le_less_linear, safe)
    6.18 - apply (blast intro: order_trans partition_le)
    6.19 -apply (drule_tac x = n in spec)
    6.20 -apply (best intro: order_less_trans order_trans order_less_imp_le)
    6.21 +apply (induct "r")
    6.22 +apply (cut_tac [2] y = "Suc r" and x = "psize D" in linorder_le_less_linear)
    6.23 +apply (auto intro: partition_le)
    6.24 +apply (drule_tac x = r in spec)
    6.25 +apply arith; 
    6.26  done
    6.27  
    6.28  lemma partition_lb_lt: "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)"
    6.29 @@ -332,7 +332,7 @@
    6.30  
    6.31  lemma sumr_partition_eq_diff_bounds [simp]:
    6.32       "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0"
    6.33 -by (induct_tac "m", auto)
    6.34 +by (induct "m", auto)
    6.35  
    6.36  lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
    6.37  apply (auto simp add: order_le_less rsum_def Integral_def)
     7.1 --- a/src/HOL/Hyperreal/Lim.thy	Mon Oct 18 13:40:45 2004 +0200
     7.2 +++ b/src/HOL/Hyperreal/Lim.thy	Tue Oct 19 18:18:45 2004 +0200
     7.3 @@ -1114,7 +1114,7 @@
     7.4  by (simp add: NSDERIV_DERIV_iff)
     7.5  
     7.6  lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
     7.7 -apply (induct_tac "n")
     7.8 +apply (induct "n")
     7.9  apply (drule_tac [2] DERIV_Id [THEN DERIV_mult])
    7.10  apply (auto simp add: real_of_nat_Suc left_distrib)
    7.11  apply (case_tac "0 < n")
    7.12 @@ -1238,7 +1238,7 @@
    7.13       All considerably tidied by lcp.*}
    7.14  
    7.15  lemma lemma_f_mono_add [rule_format (no_asm)]: "(\<forall>n. (f::nat=>real) n \<le> f (Suc n)) --> f m \<le> f(m + no)"
    7.16 -apply (induct_tac "no")
    7.17 +apply (induct "no")
    7.18  apply (auto intro: order_trans)
    7.19  done
    7.20  
    7.21 @@ -1349,9 +1349,8 @@
    7.22       "a \<le> b ==>
    7.23        snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) =
    7.24        (b-a) / (2 ^ n)"
    7.25 -apply (induct_tac "n")
    7.26 +apply (induct "n")
    7.27  apply (auto simp add: eq_divide_2_times_iff add_divide_distrib Let_def split_def)
    7.28 -apply (auto simp add: add_ac Bolzano_bisect_le diff_minus)
    7.29  done
    7.30  
    7.31  lemmas Bolzano_nest_unique =
     8.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Mon Oct 18 13:40:45 2004 +0200
     8.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Oct 19 18:18:45 2004 +0200
     8.3 @@ -10,10 +10,10 @@
     8.4  begin
     8.5  
     8.6  lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
     8.7 -by (induct_tac "n", auto)
     8.8 +by (induct "n", auto)
     8.9  
    8.10  lemma sumr_offset2: "\<forall>f. sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
    8.11 -by (induct_tac "n", auto)
    8.12 +by (induct "n", auto)
    8.13  
    8.14  lemma sumr_offset3: "sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f"
    8.15  by (simp  add: sumr_offset)
    8.16 @@ -292,7 +292,7 @@
    8.17         diff 0 0 =
    8.18         (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
    8.19         diff n 0 * 0 ^ n / real (fact n)"
    8.20 -by (induct_tac "n", auto)
    8.21 +by (induct "n", auto)
    8.22  
    8.23  lemma Maclaurin_bi_le:
    8.24     "[| diff 0 = f;
    8.25 @@ -405,15 +405,15 @@
    8.26  
    8.27  lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
    8.28       "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"
    8.29 -by (induct_tac "n", auto)
    8.30 +by (induct "n", auto)
    8.31  
    8.32  lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
    8.33       "0 < n --> Suc (Suc (4*n - 2)) = 4*n"
    8.34 -by (induct_tac "n", auto)
    8.35 +by (induct "n", auto)
    8.36  
    8.37  lemma Suc_mult_two_diff_one [rule_format, simp]:
    8.38        "0 < n --> Suc (2 * n - 1) = 2*n"
    8.39 -by (induct_tac "n", auto)
    8.40 +by (induct "n", auto)
    8.41  
    8.42  
    8.43  text{*It is unclear why so many variant results are needed.*}
    8.44 @@ -496,7 +496,7 @@
    8.45                 then (- 1) ^ (m div 2)/(real  (fact m))
    8.46                 else 0) *
    8.47                0 ^ m) = 1"
    8.48 -by (induct_tac "n", auto)
    8.49 +by (induct "n", auto)
    8.50  
    8.51  lemma Maclaurin_cos_expansion:
    8.52       "\<exists>t. abs t \<le> abs x &
     9.1 --- a/src/HOL/Hyperreal/NSA.thy	Mon Oct 18 13:40:45 2004 +0200
     9.2 +++ b/src/HOL/Hyperreal/NSA.thy	Tue Oct 19 18:18:45 2004 +0200
     9.3 @@ -1961,7 +1961,7 @@
     9.4    hence cannot belong to FreeUltrafilterNat
     9.5   -------------------------------------------*)
     9.6  lemma finite_nat_segment: "finite {n::nat. n < m}"
     9.7 -apply (induct_tac "m")
     9.8 +apply (induct "m")
     9.9  apply (auto simp add: Suc_Un_eq)
    9.10  done
    9.11  
    10.1 --- a/src/HOL/Hyperreal/Poly.thy	Mon Oct 18 13:40:45 2004 +0200
    10.2 +++ b/src/HOL/Hyperreal/Poly.thy	Tue Oct 19 18:18:45 2004 +0200
    10.3 @@ -108,7 +108,7 @@
    10.4  
    10.5  
    10.6  lemma padd_Nil2: "p +++ [] = p"
    10.7 -by (induct_tac "p", auto)
    10.8 +by (induct "p", auto)
    10.9  declare padd_Nil2 [simp]
   10.10  
   10.11  lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)"
   10.12 @@ -122,7 +122,7 @@
   10.13  by simp
   10.14  
   10.15  lemma poly_ident_mult: "1 %* t = t"
   10.16 -by (induct_tac "t", auto)
   10.17 +by (induct "t", auto)
   10.18  declare poly_ident_mult [simp]
   10.19  
   10.20  lemma poly_simple_add_Cons: "[a] +++ ((0)#t) = (a#t)"
   10.21 @@ -139,23 +139,20 @@
   10.22  done
   10.23  
   10.24  lemma padd_assoc [rule_format]: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
   10.25 -apply (induct_tac "a", simp, clarify)
   10.26 +apply (induct "a", simp, clarify)
   10.27  apply (case_tac b, simp_all)
   10.28  done
   10.29  
   10.30  lemma poly_cmult_distr [rule_format]:
   10.31       "\<forall>q. a %* ( p +++ q) = (a %* p +++ a %* q)"
   10.32 -apply (induct_tac "p", simp, clarify)
   10.33 +apply (induct "p", simp, clarify) 
   10.34  apply (case_tac "q")
   10.35  apply (simp_all add: right_distrib)
   10.36  done
   10.37  
   10.38  lemma pmult_by_x: "[0, 1] *** t = ((0)#t)"
   10.39 -apply (induct_tac "t", simp)
   10.40 -apply (simp add: poly_ident_mult padd_commut)
   10.41 -apply (case_tac "list")
   10.42 -apply (simp (no_asm_simp))
   10.43 -apply (simp add: poly_ident_mult padd_commut)
   10.44 +apply (induct "t", simp)
   10.45 +apply (auto simp add: poly_ident_mult padd_commut)
   10.46  done
   10.47  declare pmult_by_x [simp]
   10.48  
   10.49 @@ -170,7 +167,7 @@
   10.50  done
   10.51  
   10.52  lemma poly_cmult: "poly (c %* p) x = c * poly p x"
   10.53 -apply (induct_tac "p")
   10.54 +apply (induct "p") 
   10.55  apply (case_tac [2] "x=0")
   10.56  apply (auto simp add: right_distrib mult_ac)
   10.57  done
   10.58 @@ -183,14 +180,14 @@
   10.59  lemma poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x"
   10.60  apply (subgoal_tac "\<forall>p2. poly (p1 *** p2) x = poly p1 x * poly p2 x")
   10.61  apply (simp (no_asm_simp))
   10.62 -apply (induct_tac "p1")
   10.63 +apply (induct "p1")
   10.64  apply (auto simp add: poly_cmult)
   10.65 -apply (case_tac "list")
   10.66 +apply (case_tac p1)
   10.67  apply (auto simp add: poly_cmult poly_add left_distrib right_distrib mult_ac)
   10.68  done
   10.69  
   10.70  lemma poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
   10.71 -apply (induct_tac "n")
   10.72 +apply (induct "n")
   10.73  apply (auto simp add: poly_cmult poly_mult)
   10.74  done
   10.75  
   10.76 @@ -204,11 +201,11 @@
   10.77  by (simp add: poly_mult real_mult_assoc)
   10.78  
   10.79  lemma poly_mult_Nil2: "poly (p *** []) x = 0"
   10.80 -by (induct_tac "p", auto)
   10.81 +by (induct "p", auto)
   10.82  declare poly_mult_Nil2 [simp]
   10.83  
   10.84  lemma poly_exp_add: "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d) x"
   10.85 -apply (induct_tac "n")
   10.86 +apply (induct "n")
   10.87  apply (auto simp add: poly_mult real_mult_assoc)
   10.88  done
   10.89  
   10.90 @@ -236,7 +233,7 @@
   10.91  
   10.92  lemma lemma_DERIV_poly1: "\<forall>n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :>
   10.93          x ^ n * poly (pderiv_aux (Suc n) p) x "
   10.94 -apply (induct_tac "p")
   10.95 +apply (induct "p")
   10.96  apply (auto intro!: DERIV_add DERIV_cmult2 
   10.97              simp add: pderiv_def right_distrib real_mult_assoc [symmetric] 
   10.98              simp del: realpow_Suc)
   10.99 @@ -253,7 +250,7 @@
  10.100  by (rule lemma_DERIV_subst, rule DERIV_add, auto)
  10.101  
  10.102  lemma poly_DERIV: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
  10.103 -apply (induct_tac "p")
  10.104 +apply (induct "p")
  10.105  apply (auto simp add: pderiv_Cons)
  10.106  apply (rule DERIV_add_const)
  10.107  apply (rule lemma_DERIV_subst)
  10.108 @@ -299,7 +296,7 @@
  10.109  
  10.110  lemma lemma_poly_pderiv_aux_add: "\<forall>p2 n. poly (pderiv_aux n (p1 +++ p2)) x =
  10.111                  poly (pderiv_aux n p1 +++ pderiv_aux n p2) x"
  10.112 -apply (induct_tac "p1", simp, clarify) 
  10.113 +apply (induct "p1", simp, clarify) 
  10.114  apply (case_tac "p2")
  10.115  apply (auto simp add: right_distrib)
  10.116  done
  10.117 @@ -310,7 +307,7 @@
  10.118  done
  10.119  
  10.120  lemma lemma_poly_pderiv_aux_cmult: "\<forall>n. poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x"
  10.121 -apply (induct_tac "p")
  10.122 +apply (induct "p")
  10.123  apply (auto simp add: poly_cmult mult_ac)
  10.124  done
  10.125  
  10.126 @@ -323,7 +320,7 @@
  10.127  done
  10.128  
  10.129  lemma lemma_poly_pderiv_aux_mult1: "\<forall>n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"
  10.130 -apply (induct_tac "p")
  10.131 +apply (induct "p")
  10.132  apply (auto simp add: real_of_nat_Suc left_distrib)
  10.133  done
  10.134  
  10.135 @@ -331,7 +328,7 @@
  10.136  by (simp add: lemma_poly_pderiv_aux_mult1)
  10.137  
  10.138  lemma lemma_poly_pderiv_add: "\<forall>q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x"
  10.139 -apply (induct_tac "p", simp, clarify) 
  10.140 +apply (induct "p", simp, clarify) 
  10.141  apply (case_tac "q")
  10.142  apply (auto simp add: poly_pderiv_aux_add poly_add pderiv_def)
  10.143  done
  10.144 @@ -340,7 +337,7 @@
  10.145  by (simp add: lemma_poly_pderiv_add)
  10.146  
  10.147  lemma poly_pderiv_cmult: "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x"
  10.148 -apply (induct_tac "p")
  10.149 +apply (induct "p")
  10.150  apply (auto simp add: poly_pderiv_aux_cmult poly_cmult pderiv_def)
  10.151  done
  10.152  
  10.153 @@ -350,13 +347,13 @@
  10.154  lemma lemma_poly_mult_pderiv:
  10.155     "poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x"
  10.156  apply (simp add: pderiv_def)
  10.157 -apply (induct_tac "t")
  10.158 +apply (induct "t")
  10.159  apply (auto simp add: poly_add lemma_poly_pderiv_aux_mult)
  10.160  done
  10.161  
  10.162  lemma poly_pderiv_mult: "\<forall>q. poly (pderiv (p *** q)) x =
  10.163        poly (p *** (pderiv q) +++ q *** (pderiv p)) x"
  10.164 -apply (induct_tac "p")
  10.165 +apply (induct "p")
  10.166  apply (auto simp add: poly_add poly_cmult poly_pderiv_cmult poly_pderiv_add poly_mult)
  10.167  apply (rule lemma_poly_mult_pderiv [THEN ssubst])
  10.168  apply (rule lemma_poly_mult_pderiv [THEN ssubst])
  10.169 @@ -367,7 +364,7 @@
  10.170  
  10.171  lemma poly_pderiv_exp: "poly (pderiv (p %^ (Suc n))) x =
  10.172           poly ((real (Suc n)) %* (p %^ n) *** pderiv p) x"
  10.173 -apply (induct_tac "n")
  10.174 +apply (induct "n")
  10.175  apply (auto simp add: poly_add poly_pderiv_cmult poly_cmult poly_pderiv_mult
  10.176                        real_of_nat_zero poly_mult real_of_nat_Suc 
  10.177                        right_distrib left_distrib mult_ac)
  10.178 @@ -383,7 +380,7 @@
  10.179   @{term "p(x)"} *}
  10.180  
  10.181  lemma lemma_poly_linear_rem: "\<forall>h. \<exists>q r. h#t = [r] +++ [-a, 1] *** q"
  10.182 -apply (induct_tac "t", safe)
  10.183 +apply (induct "t", safe)
  10.184  apply (rule_tac x = "[]" in exI)
  10.185  apply (rule_tac x = h in exI, simp)
  10.186  apply (drule_tac x = aa in spec, safe)
  10.187 @@ -407,11 +404,11 @@
  10.188  done
  10.189  
  10.190  lemma lemma_poly_length_mult: "\<forall>h k a. length (k %* p +++  (h # (a %* p))) = Suc (length p)"
  10.191 -by (induct_tac "p", auto)
  10.192 +by (induct "p", auto)
  10.193  declare lemma_poly_length_mult [simp]
  10.194  
  10.195  lemma lemma_poly_length_mult2: "\<forall>h k. length (k %* p +++  (h # p)) = Suc (length p)"
  10.196 -by (induct_tac "p", auto)
  10.197 +by (induct "p", auto)
  10.198  declare lemma_poly_length_mult2 [simp]
  10.199  
  10.200  lemma poly_length_mult: "length([-a,1] *** q) = Suc (length q)"
  10.201 @@ -422,13 +419,13 @@
  10.202  subsection{*Polynomial length*}
  10.203  
  10.204  lemma poly_cmult_length: "length (a %* p) = length p"
  10.205 -by (induct_tac "p", auto)
  10.206 +by (induct "p", auto)
  10.207  declare poly_cmult_length [simp]
  10.208  
  10.209  lemma poly_add_length [rule_format]:
  10.210       "\<forall>p2. length (p1 +++ p2) =
  10.211               (if (length p1 < length p2) then length p2 else length p1)"
  10.212 -apply (induct_tac "p1", simp_all, arith)
  10.213 +apply (induct "p1", simp_all, arith)
  10.214  done
  10.215  
  10.216  lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)"
  10.217 @@ -447,14 +444,14 @@
  10.218  text{*Normalisation Properties*}
  10.219  
  10.220  lemma poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)"
  10.221 -by (induct_tac "p", auto)
  10.222 +by (induct "p", auto)
  10.223  
  10.224  text{*A nontrivial polynomial of degree n has no more than n roots*}
  10.225  
  10.226  lemma poly_roots_index_lemma [rule_format]:
  10.227     "\<forall>p x. poly p x \<noteq> poly [] x & length p = n
  10.228      --> (\<exists>i. \<forall>x. (poly p x = (0::real)) --> (\<exists>m. (m \<le> n & x = i m)))"
  10.229 -apply (induct_tac "n", safe)
  10.230 +apply (induct "n", safe)
  10.231  apply (rule ccontr)
  10.232  apply (subgoal_tac "\<exists>a. poly p a = 0", safe)
  10.233  apply (drule poly_linear_divides [THEN iffD1], safe)
  10.234 @@ -464,7 +461,7 @@
  10.235  apply (erule exE)
  10.236  apply (drule_tac x = "%m. if m = Suc n then a else i m" in spec, safe)
  10.237  apply (drule poly_mult_eq_zero_disj [THEN iffD1], safe)
  10.238 -apply (drule_tac x = "Suc (length q) " in spec)
  10.239 +apply (drule_tac x = "Suc (length q)" in spec)
  10.240  apply simp
  10.241  apply (drule_tac x = xa in spec, safe)
  10.242  apply (drule_tac x = m in spec, simp, blast)
  10.243 @@ -478,25 +475,23 @@
  10.244  lemma poly_roots_finite_lemma: "poly p x \<noteq> poly [] x ==>
  10.245        \<exists>N i. \<forall>x. (poly p x = 0) --> (\<exists>n. (n::nat) < N & x = i n)"
  10.246  apply (drule poly_roots_index_length, safe)
  10.247 -apply (rule_tac x = "Suc (length p) " in exI)
  10.248 +apply (rule_tac x = "Suc (length p)" in exI)
  10.249  apply (rule_tac x = i in exI) 
  10.250  apply (simp add: less_Suc_eq_le)
  10.251  done
  10.252  
  10.253  (* annoying proof *)
  10.254  lemma real_finite_lemma [rule_format (no_asm)]:
  10.255 -     "\<forall>P. (\<forall>x. P x --> (\<exists>n. (n::nat) < N & x = (j::nat=>real) n))
  10.256 +     "\<forall>P. (\<forall>x. P x --> (\<exists>n. n < N & x = (j::nat=>real) n))
  10.257        --> (\<exists>a. \<forall>x. P x --> x < a)"
  10.258 -apply (induct_tac "N", simp, safe)
  10.259 -apply (drule_tac x = "%z. P z & (z \<noteq> (j::nat=>real) n) " in spec)
  10.260 -apply auto
  10.261 -apply (drule_tac x = x in spec, safe)
  10.262 -apply (rule_tac x = na in exI)
  10.263 -apply (auto simp add: less_Suc_eq) 
  10.264 -apply (rule_tac x = "abs a + abs (j n) + 1" in exI)
  10.265 +apply (induct "N", simp, safe)
  10.266 +apply (drule_tac x = "%z. P z & (z \<noteq> j N)" in spec)
  10.267 +apply (auto simp add: less_Suc_eq)
  10.268 +apply (rename_tac N P a) 
  10.269 +apply (rule_tac x = "abs a + abs (j N) + 1" in exI)
  10.270  apply safe
  10.271 -apply (drule_tac x = x in spec, safe)
  10.272 -apply (drule_tac x = "j na" in spec, arith+)
  10.273 +apply (drule_tac x = x in spec, safe) 
  10.274 +apply (drule_tac x = "j n" in spec, arith+)
  10.275  done
  10.276  
  10.277  lemma poly_roots_finite: "(poly p \<noteq> poly []) =
  10.278 @@ -515,7 +510,7 @@
  10.279        ==>  poly (p *** q) \<noteq> poly []"
  10.280  apply (auto simp add: poly_roots_finite)
  10.281  apply (rule_tac x = "N + Na" in exI)
  10.282 -apply (rule_tac x = "%n. if n < N then j n else ja (n - N) " in exI)
  10.283 +apply (rule_tac x = "%n. if n < N then j n else ja (n - N)" in exI)
  10.284  apply (auto simp add: poly_mult_eq_zero_disj, force) 
  10.285  done
  10.286  
  10.287 @@ -579,7 +574,7 @@
  10.288  
  10.289  
  10.290  lemma poly_zero: "(poly p = poly []) = list_all (%c. c = 0) p"
  10.291 -apply (induct_tac "p", simp)
  10.292 +apply (induct "p", simp)
  10.293  apply (rule iffI)
  10.294  apply (drule poly_zero_lemma, auto)
  10.295  done
  10.296 @@ -588,7 +583,7 @@
  10.297  
  10.298  lemma pderiv_aux_iszero [rule_format, simp]:
  10.299      "\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p"
  10.300 -by (induct_tac "p", auto)
  10.301 +by (induct "p", auto)
  10.302  
  10.303  lemma pderiv_aux_iszero_num: "(number_of n :: nat) \<noteq> 0
  10.304        ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
  10.305 @@ -601,14 +596,14 @@
  10.306  lemma pderiv_iszero [rule_format]:
  10.307       "poly (pderiv p) = poly [] --> (\<exists>h. poly p = poly [h])"
  10.308  apply (simp add: poly_zero)
  10.309 -apply (induct_tac "p", force)
  10.310 +apply (induct "p", force)
  10.311  apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons)
  10.312  apply (auto simp add: poly_zero [symmetric])
  10.313  done
  10.314  
  10.315  lemma pderiv_zero_obj: "poly p = poly [] --> (poly (pderiv p) = poly [])"
  10.316  apply (simp add: poly_zero)
  10.317 -apply (induct_tac "p", force)
  10.318 +apply (induct "p", force)
  10.319  apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons)
  10.320  done
  10.321  
  10.322 @@ -697,13 +692,13 @@
  10.323  lemma poly_order_exists_lemma [rule_format]:
  10.324       "\<forall>p. length p = d --> poly p \<noteq> poly [] 
  10.325               --> (\<exists>n q. p = mulexp n [-a, 1] q & poly q a \<noteq> 0)"
  10.326 -apply (induct_tac "d")
  10.327 +apply (induct "d")
  10.328  apply (simp add: fun_eq, safe)
  10.329  apply (case_tac "poly p a = 0")
  10.330  apply (drule_tac poly_linear_divides [THEN iffD1], safe)
  10.331  apply (drule_tac x = q in spec)
  10.332  apply (drule_tac poly_entire_neg [THEN iffD1], safe, force, blast) 
  10.333 -apply (rule_tac x = "Suc na" in exI)
  10.334 +apply (rule_tac x = "Suc n" in exI)
  10.335  apply (rule_tac x = qa in exI)
  10.336  apply (simp del: pmult_Cons)
  10.337  apply (rule_tac x = 0 in exI, force) 
  10.338 @@ -780,7 +775,7 @@
  10.339  by (auto simp add: fun_eq divides_def poly_mult order_def)
  10.340  
  10.341  lemma pexp_one: "p %^ (Suc 0) = p"
  10.342 -apply (induct_tac "p")
  10.343 +apply (induct "p")
  10.344  apply (auto simp add: numeral_1_eq_1)
  10.345  done
  10.346  declare pexp_one [simp]
  10.347 @@ -788,7 +783,7 @@
  10.348  lemma lemma_order_root [rule_format]:
  10.349       "\<forall>p a. 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
  10.350               --> poly p a = 0"
  10.351 -apply (induct_tac "n", blast)
  10.352 +apply (induct "n", blast)
  10.353  apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
  10.354  done
  10.355  
  10.356 @@ -851,7 +846,7 @@
  10.357         poly (pderiv p) \<noteq> poly [] &
  10.358         poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q
  10.359         --> n = Suc (order a (pderiv p))"
  10.360 -apply (induct_tac "n", safe)
  10.361 +apply (induct "n", safe)
  10.362  apply (rule order_unique_lemma, rule conjI, assumption)
  10.363  apply (subgoal_tac "\<forall>r. r divides (pderiv p) = r divides (pderiv ([-a, 1] %^ Suc n *** q))")
  10.364  apply (drule_tac [2] poly_pderiv_welldef)
  10.365 @@ -862,7 +857,7 @@
  10.366  apply (rule_tac x = "[-a, 1] *** (pderiv q) +++ real (Suc n) %* q" in exI)
  10.367  apply (simp add: poly_pderiv_mult poly_pderiv_exp_prime poly_add poly_mult poly_cmult right_distrib mult_ac del: pmult_Cons pexp_Suc)
  10.368  apply (simp add: poly_mult right_distrib left_distrib mult_ac del: pmult_Cons)
  10.369 -apply (erule_tac V = "\<forall>r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q) " in thin_rl)
  10.370 +apply (erule_tac V = "\<forall>r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q)" in thin_rl)
  10.371  apply (unfold divides_def)
  10.372  apply (simp (no_asm) add: poly_pderiv_mult poly_pderiv_exp_prime fun_eq poly_add poly_mult del: pmult_Cons pexp_Suc)
  10.373  apply (rule swap, assumption)
  10.374 @@ -872,7 +867,7 @@
  10.375  apply (subgoal_tac "poly ([-a, 1] %^ n *** q) = poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* (qa +++ -- (pderiv q))))) ")
  10.376  apply (drule poly_mult_left_cancel [THEN iffD1], simp)
  10.377  apply (simp add: fun_eq poly_mult poly_add poly_cmult poly_minus del: pmult_Cons mult_cancel_left field_mult_cancel_left, safe)
  10.378 -apply (rule_tac c1 = "real (Suc n) " in real_mult_left_cancel [THEN iffD1])
  10.379 +apply (rule_tac c1 = "real (Suc n)" in real_mult_left_cancel [THEN iffD1])
  10.380  apply (simp (no_asm))
  10.381  apply (subgoal_tac "real (Suc n) * (poly ([- a, 1] %^ n) xa * poly q xa) =
  10.382            (poly qa xa + - poly (pderiv q) xa) *
  10.383 @@ -901,13 +896,13 @@
  10.384           poly d = poly (r *** p +++ s *** pderiv p)
  10.385        |] ==> order a q = (if order a p = 0 then 0 else 1)"
  10.386  apply (subgoal_tac "order a p = order a q + order a d")
  10.387 -apply (rule_tac [2] s = "order a (q *** d) " in trans)
  10.388 +apply (rule_tac [2] s = "order a (q *** d)" in trans)
  10.389  prefer 2 apply (blast intro: order_poly)
  10.390  apply (rule_tac [2] order_mult)
  10.391   prefer 2 apply force
  10.392  apply (case_tac "order a p = 0", simp)
  10.393  apply (subgoal_tac "order a (pderiv p) = order a e + order a d")
  10.394 -apply (rule_tac [2] s = "order a (e *** d) " in trans)
  10.395 +apply (rule_tac [2] s = "order a (e *** d)" in trans)
  10.396  prefer 2 apply (blast intro: order_poly)
  10.397  apply (rule_tac [2] order_mult)
  10.398   prefer 2 apply force
  10.399 @@ -997,7 +992,7 @@
  10.400  text{*Normalization of a polynomial.*}
  10.401  
  10.402  lemma poly_normalize: "poly (pnormalize p) = poly p"
  10.403 -apply (induct_tac "p")
  10.404 +apply (induct "p")
  10.405  apply (auto simp add: fun_eq)
  10.406  done
  10.407  declare poly_normalize [simp]
  10.408 @@ -1007,7 +1002,7 @@
  10.409  
  10.410  lemma lemma_degree_zero [rule_format]:
  10.411       "list_all (%c. c = 0) p -->  pnormalize p = []"
  10.412 -by (induct_tac "p", auto)
  10.413 +by (induct "p", auto)
  10.414  
  10.415  lemma degree_zero: "poly p = poly [] ==> degree p = 0"
  10.416  apply (simp add: degree_def)
  10.417 @@ -1028,8 +1023,8 @@
  10.418  text{*bound for polynomial.*}
  10.419  
  10.420  lemma poly_mono: "abs(x) \<le> k ==> abs(poly p x) \<le> poly (map abs p) k"
  10.421 -apply (induct_tac "p", auto)
  10.422 -apply (rule_tac j = "abs a + abs (x * poly list x) " in real_le_trans)
  10.423 +apply (induct "p", auto)
  10.424 +apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
  10.425  apply (rule abs_triangle_ineq)
  10.426  apply (auto intro!: mult_mono simp add: abs_mult, arith)
  10.427  done
    11.1 --- a/src/HOL/Hyperreal/SEQ.thy	Mon Oct 18 13:40:45 2004 +0200
    11.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Tue Oct 19 18:18:45 2004 +0200
    11.3 @@ -462,7 +462,7 @@
    11.4  
    11.5  lemma lemma_finite_NSBseq2:
    11.6       "finite {n. f n \<le> (u::nat) &  real(Suc n) < \<bar>X(f n)\<bar>}"
    11.7 -apply (induct_tac "u")
    11.8 +apply (induct "u")
    11.9  apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
   11.10  apply (rule_tac B = "{n. real (Suc n) < \<bar>X 0\<bar> }" in finite_subset)
   11.11  apply (auto intro: finite_real_of_nat_less_real 
   11.12 @@ -995,7 +995,7 @@
   11.13  
   11.14  lemma NSLIMSEQ_pow [rule_format]:
   11.15       "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
   11.16 -apply (induct_tac "m")
   11.17 +apply (induct "m")
   11.18  apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
   11.19  done
   11.20  
    12.1 --- a/src/HOL/Hyperreal/Series.thy	Mon Oct 18 13:40:45 2004 +0200
    12.2 +++ b/src/HOL/Hyperreal/Series.thy	Tue Oct 19 18:18:45 2004 +0200
    12.3 @@ -38,7 +38,7 @@
    12.4  
    12.5  lemma sumr_split_add [rule_format]:
    12.6       "n < p --> sumr 0 n f + sumr n p f = sumr 0 p (f::nat=>real)"
    12.7 -apply (induct_tac "p", auto)
    12.8 +apply (induct "p", auto)
    12.9  apply (rename_tac k) 
   12.10  apply (subgoal_tac "n=k", auto) 
   12.11  done
   12.12 @@ -70,34 +70,34 @@
   12.13  by (simp add: Finite_Set.setsum_negf)
   12.14  
   12.15  lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
   12.16 -by (induct_tac "n", auto)
   12.17 +by (induct "n", auto)
   12.18  
   12.19  lemma sumr_minus_one_realpow_zero [simp]: "sumr 0 (2*n) (%i. (-1) ^ Suc i) = 0"
   12.20 -by (induct_tac "n", auto)
   12.21 +by (induct "n", auto)
   12.22  
   12.23 -lemma sumr_interval_const [rule_format (no_asm)]:
   12.24 -     "(\<forall>n. m \<le> Suc n --> f n = r) --> m \<le> k --> sumr m k f = (real(k-m) * r)"
   12.25 -apply (induct_tac "k", auto) 
   12.26 -apply (drule_tac x = n in spec)
   12.27 +lemma sumr_interval_const:
   12.28 +     "\<lbrakk>\<forall>n. m \<le> Suc n --> f n = r; m \<le> k\<rbrakk> \<Longrightarrow> sumr m k f = (real(k-m) * r)"
   12.29 +apply (induct "k", auto) 
   12.30 +apply (drule_tac x = k in spec)
   12.31  apply (auto dest!: le_imp_less_or_eq)
   12.32  apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
   12.33  done
   12.34  
   12.35 -lemma sumr_interval_const2 [rule_format (no_asm)]:
   12.36 -     "(\<forall>n. m \<le> n --> f n = r) --> m \<le> k  
   12.37 -      --> sumr m k f = (real (k - m) * r)"
   12.38 -apply (induct_tac "k", auto) 
   12.39 -apply (drule_tac x = n in spec)
   12.40 +lemma sumr_interval_const2:
   12.41 +     "[|\<forall>n. m \<le> n --> f n = r; m \<le> k|]
   12.42 +      ==> sumr m k f = (real (k - m) * r)"
   12.43 +apply (induct "k", auto) 
   12.44 +apply (drule_tac x = k in spec)
   12.45  apply (auto dest!: le_imp_less_or_eq)
   12.46  apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
   12.47  done
   12.48  
   12.49  
   12.50 -lemma sumr_le [rule_format (no_asm)]:
   12.51 -     "(\<forall>n. m \<le> n --> 0 \<le> f n) --> m < k --> sumr 0 m f \<le> sumr 0 k f"
   12.52 -apply (induct_tac "k")
   12.53 +lemma sumr_le:
   12.54 +     "[|\<forall>n. m \<le> n --> 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f"
   12.55 +apply (induct "k")
   12.56  apply (auto simp add: less_Suc_eq_le)
   12.57 -apply (drule_tac [!] x = n in spec, safe)
   12.58 +apply (drule_tac x = k in spec, safe)
   12.59  apply (drule le_imp_less_or_eq, safe)
   12.60  apply (arith) 
   12.61  apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto)
   12.62 @@ -105,22 +105,22 @@
   12.63  
   12.64  lemma sumr_le2 [rule_format (no_asm)]:
   12.65       "(\<forall>r. m \<le> r & r < n --> f r \<le> g r) --> sumr m n f \<le> sumr m n g"
   12.66 -apply (induct_tac "n")
   12.67 +apply (induct "n")
   12.68  apply (auto intro: add_mono simp add: le_def)
   12.69  done
   12.70  
   12.71 -lemma sumr_ge_zero [rule_format]: "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
   12.72 -apply (induct_tac "n", auto)
   12.73 +lemma sumr_ge_zero: "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
   12.74 +apply (induct "n", auto)
   12.75  apply (drule_tac x = n in spec, arith)
   12.76  done
   12.77  
   12.78  lemma rabs_sumr_rabs_cancel [simp]:
   12.79       "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))"
   12.80 -by (induct_tac "n", simp_all add: add_increasing)
   12.81 +by (induct "n", simp_all add: add_increasing)
   12.82  
   12.83  lemma sumr_zero [rule_format]:
   12.84       "\<forall>n. N \<le> n --> f n = 0 ==> N \<le> m --> sumr m n f = 0"
   12.85 -by (induct_tac "n", auto)
   12.86 +by (induct "n", auto)
   12.87  
   12.88  lemma Suc_le_imp_diff_ge2:
   12.89       "[|\<forall>n. N \<le> n --> f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
   12.90 @@ -129,7 +129,7 @@
   12.91  done
   12.92  
   12.93  lemma sumr_one_lb_realpow_zero [simp]: "sumr (Suc 0) n (%n. f(n) * 0 ^ n) = 0"
   12.94 -apply (induct_tac "n")
   12.95 +apply (induct "n")
   12.96  apply (case_tac [2] "n", auto)
   12.97  done
   12.98  
   12.99 @@ -138,26 +138,26 @@
  12.100  
  12.101  lemma sumr_subst [rule_format (no_asm)]:
  12.102       "(\<forall>p. m \<le> p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g"
  12.103 -by (induct_tac "n", auto)
  12.104 +by (induct "n", auto)
  12.105  
  12.106  lemma sumr_bound [rule_format (no_asm)]:
  12.107       "(\<forall>p. m \<le> p & p < m + n --> (f(p) \<le> K))  
  12.108        --> (sumr m (m + n) f \<le> (real n * K))"
  12.109 -apply (induct_tac "n")
  12.110 +apply (induct "n")
  12.111  apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc)
  12.112  done
  12.113  
  12.114  lemma sumr_bound2 [rule_format (no_asm)]:
  12.115       "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))  
  12.116        --> (sumr 0 n f \<le> (real n * K))"
  12.117 -apply (induct_tac "n")
  12.118 +apply (induct "n")
  12.119  apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute)
  12.120  done
  12.121  
  12.122  lemma sumr_group [simp]:
  12.123       "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f"
  12.124  apply (subgoal_tac "k = 0 | 0 < k", auto)
  12.125 -apply (induct_tac "n")
  12.126 +apply (induct "n")
  12.127  apply (simp_all add: sumr_split_add add_commute)
  12.128  done
  12.129  
  12.130 @@ -250,10 +250,8 @@
  12.131  lemma sumr_pos_lt_pair_lemma:
  12.132       "[|\<forall>d. - f (n + (d + d)) < f (Suc (n + (d + d)))|]
  12.133        ==> sumr 0 (n + Suc (Suc 0)) f \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f"
  12.134 -apply (induct_tac "no", simp)
  12.135 -apply (rule_tac y = "sumr 0 (Suc (Suc 0) * (Suc na) +n) f" in order_trans)
  12.136 -apply assumption
  12.137 -apply (drule_tac x = "Suc na" in spec)
  12.138 +apply (induct "no", auto)
  12.139 +apply (drule_tac x = "Suc no" in spec)
  12.140  apply (simp add: add_ac) 
  12.141  done
  12.142  
  12.143 @@ -311,7 +309,7 @@
  12.144  text{*Sum of a geometric progression.*}
  12.145  
  12.146  lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
  12.147 -apply (induct_tac "n", auto)
  12.148 +apply (induct "n", auto)
  12.149  apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
  12.150  apply (auto simp add: mult_assoc left_distrib  times_divide_eq)
  12.151  apply (simp add: right_distrib diff_minus mult_commute)
  12.152 @@ -456,7 +454,7 @@
  12.153  lemma DERIV_sumr [rule_format (no_asm)]:
  12.154       "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
  12.155        --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"
  12.156 -apply (induct_tac "n")
  12.157 +apply (induct "n")
  12.158  apply (auto intro: DERIV_add)
  12.159  done
  12.160  
    13.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Mon Oct 18 13:40:45 2004 +0200
    13.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Oct 19 18:18:45 2004 +0200
    13.3 @@ -309,24 +309,24 @@
    13.4  lemma lemma_STAR_sin [simp]:
    13.5       "(if even n then 0  
    13.6         else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
    13.7 -by (induct_tac "n", auto)
    13.8 +by (induct "n", auto)
    13.9  
   13.10  lemma lemma_STAR_cos [simp]:
   13.11       "0 < n -->  
   13.12        (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
   13.13 -by (induct_tac "n", auto)
   13.14 +by (induct "n", auto)
   13.15  
   13.16  lemma lemma_STAR_cos1 [simp]:
   13.17       "0 < n -->  
   13.18        (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
   13.19 -by (induct_tac "n", auto)
   13.20 +by (induct "n", auto)
   13.21  
   13.22  lemma lemma_STAR_cos2 [simp]:
   13.23       "sumr 1 n (%n. if even n  
   13.24                      then (- 1) ^ (n div 2)/(real (fact n)) *  
   13.25                            0 ^ n  
   13.26                      else 0) = 0"
   13.27 -apply (induct_tac "n")
   13.28 +apply (induct "n")
   13.29  apply (case_tac [2] "n", auto)
   13.30  done
   13.31  
   13.32 @@ -353,7 +353,7 @@
   13.33  
   13.34  lemma lemma_realpow_diff [rule_format (no_asm)]:
   13.35       "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
   13.36 -apply (induct_tac "n", auto)
   13.37 +apply (induct "n", auto)
   13.38  apply (subgoal_tac "p = Suc n")
   13.39  apply (simp (no_asm_simp), auto)
   13.40  apply (drule sym)
   13.41 @@ -377,7 +377,7 @@
   13.42  lemma lemma_realpow_diff_sumr2:
   13.43       "x ^ (Suc n) - y ^ (Suc n) =  
   13.44        (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))"
   13.45 -apply (induct_tac "n", simp)
   13.46 +apply (induct "n", simp)
   13.47  apply (auto simp del: sumr_Suc)
   13.48  apply (subst sumr_Suc)
   13.49  apply (drule sym)
   13.50 @@ -447,7 +447,7 @@
   13.51       "sumr 0 n (%n. (diffs c)(n) * (x ^ n)) =  
   13.52        sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) +  
   13.53        (real n * c(n) * x ^ (n - Suc 0))"
   13.54 -apply (induct_tac "n")
   13.55 +apply (induct "n")
   13.56  apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def)
   13.57  done
   13.58  
   13.59 @@ -893,7 +893,7 @@
   13.60  by auto
   13.61  
   13.62  lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
   13.63 -apply (induct_tac "n")
   13.64 +apply (induct "n")
   13.65  apply (auto simp add: real_of_nat_Suc right_distrib exp_add mult_commute)
   13.66  done
   13.67  
   13.68 @@ -1552,12 +1552,12 @@
   13.69  by (simp add: cos_add cos_double)
   13.70  
   13.71  lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
   13.72 -apply (induct_tac "n")
   13.73 +apply (induct "n")
   13.74  apply (auto simp add: real_of_nat_Suc left_distrib)
   13.75  done
   13.76  
   13.77  lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
   13.78 -apply (induct_tac "n")
   13.79 +apply (induct "n")
   13.80  apply (auto simp add: real_of_nat_Suc left_distrib)
   13.81  done
   13.82  
    14.1 --- a/src/HOL/Integ/IntDef.thy	Mon Oct 18 13:40:45 2004 +0200
    14.2 +++ b/src/HOL/Integ/IntDef.thy	Tue Oct 19 18:18:45 2004 +0200
    14.3 @@ -344,11 +344,11 @@
    14.4  subsection{*Strict Monotonicity of Multiplication*}
    14.5  
    14.6  text{*strict, in 1st argument; proof is by induction on k>0*}
    14.7 -lemma zmult_zless_mono2_lemma [rule_format]:
    14.8 -     "i<j ==> 0<k --> int k * i < int k * j"
    14.9 -apply (induct_tac "k", simp)
   14.10 +lemma zmult_zless_mono2_lemma:
   14.11 +     "i<j ==> 0<k ==> int k * i < int k * j"
   14.12 +apply (induct "k", simp)
   14.13  apply (simp add: int_Suc)
   14.14 -apply (case_tac "n=0")
   14.15 +apply (case_tac "k=0")
   14.16  apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
   14.17  apply (simp add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
   14.18  done
    15.1 --- a/src/HOL/Integ/IntDiv.thy	Mon Oct 18 13:40:45 2004 +0200
    15.2 +++ b/src/HOL/Integ/IntDiv.thy	Tue Oct 19 18:18:45 2004 +0200
    15.3 @@ -1172,7 +1172,7 @@
    15.4  
    15.5  
    15.6  lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
    15.7 -apply (induct_tac "y", auto)
    15.8 +apply (induct "y", auto)
    15.9  apply (rule zmod_zmult1_eq [THEN trans])
   15.10  apply (simp (no_asm_simp))
   15.11  apply (rule zmod_zmult_distrib [symmetric])
   15.12 @@ -1186,12 +1186,12 @@
   15.13  
   15.14  lemma zero_less_zpower_abs_iff [simp]:
   15.15       "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
   15.16 -apply (induct_tac "n")
   15.17 +apply (induct "n")
   15.18  apply (auto simp add: zero_less_mult_iff)
   15.19  done
   15.20  
   15.21  lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
   15.22 -apply (induct_tac "n")
   15.23 +apply (induct "n")
   15.24  apply (auto simp add: zero_le_mult_iff)
   15.25  done
   15.26  
    16.1 --- a/src/HOL/Integ/NatBin.thy	Mon Oct 18 13:40:45 2004 +0200
    16.2 +++ b/src/HOL/Integ/NatBin.thy	Tue Oct 19 18:18:45 2004 +0200
    16.3 @@ -299,7 +299,7 @@
    16.4    by (simp add: power2_eq_square)
    16.5  
    16.6  lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
    16.7 -apply (induct_tac "n")
    16.8 +apply (induct "n")
    16.9  apply (auto simp add: power_Suc power_add)
   16.10  done
   16.11  
   16.12 @@ -520,7 +520,7 @@
   16.13  subsection{*Literal arithmetic involving powers*}
   16.14  
   16.15  lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
   16.16 -apply (induct_tac "n")
   16.17 +apply (induct "n")
   16.18  apply (simp_all (no_asm_simp) add: nat_mult_distrib)
   16.19  done
   16.20  
    17.1 --- a/src/HOL/Integ/Parity.thy	Mon Oct 18 13:40:45 2004 +0200
    17.2 +++ b/src/HOL/Integ/Parity.thy	Tue Oct 19 18:18:45 2004 +0200
    17.3 @@ -31,7 +31,7 @@
    17.4  subsection {* Casting a nat power to an integer *}
    17.5  
    17.6  lemma zpow_int: "int (x^y) = (int x)^y"
    17.7 -  apply (induct_tac y)
    17.8 +  apply (induct y)
    17.9    apply (simp, simp add: zmult_int [THEN sym])
   17.10    done
   17.11  
   17.12 @@ -90,12 +90,12 @@
   17.13  
   17.14  lemma even_pow_gt_zero [rule_format]: 
   17.15      "even (x::int) ==> 0 < n --> even (x^n)"
   17.16 -  apply (induct_tac n)
   17.17 +  apply (induct n)
   17.18    apply (auto simp add: even_product)
   17.19    done
   17.20  
   17.21  lemma odd_pow: "odd x ==> odd((x::int)^n)"
   17.22 -  apply (induct_tac n)
   17.23 +  apply (induct n)
   17.24    apply (simp add: even_def)
   17.25    apply (simp add: even_product)
   17.26    done
   17.27 @@ -237,7 +237,7 @@
   17.28  lemma neg_one_even_odd_power:
   17.29       "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & 
   17.30        (odd x --> (-1::'a)^x = -1)"
   17.31 -  apply (induct_tac x)
   17.32 +  apply (induct x)
   17.33    apply (simp, simp add: power_Suc)
   17.34    done
   17.35  
    18.1 --- a/src/HOL/List.thy	Mon Oct 18 13:40:45 2004 +0200
    18.2 +++ b/src/HOL/List.thy	Tue Oct 19 18:18:45 2004 +0200
    18.3 @@ -838,7 +838,7 @@
    18.4  done
    18.5  
    18.6  lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
    18.7 -apply (induct_tac xs, simp, simp)
    18.8 +apply (induct xs, simp, simp)
    18.9  apply safe
   18.10  apply (rule_tac x = 0 in exI, simp)
   18.11   apply (rule_tac x = "Suc i" in exI, simp)
   18.12 @@ -1503,10 +1503,10 @@
   18.13  by (induct xs) auto
   18.14  
   18.15  lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
   18.16 -  by (induct_tac x, auto) 
   18.17 +  by (induct x, auto) 
   18.18  
   18.19  lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
   18.20 -  by (induct_tac x, auto)
   18.21 +  by (induct x, auto)
   18.22  
   18.23  lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
   18.24  by (induct xs) auto
   18.25 @@ -1528,7 +1528,7 @@
   18.26  it is useful. *}
   18.27  lemma distinct_conv_nth:
   18.28  "distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j --> xs!i \<noteq> xs!j)"
   18.29 -apply (induct_tac xs, simp, simp)
   18.30 +apply (induct xs, simp, simp)
   18.31  apply (rule iffI, clarsimp)
   18.32   apply (case_tac i)
   18.33  apply (case_tac j, simp)
   18.34 @@ -1653,7 +1653,7 @@
   18.35  subsection {* Lexicographic orderings on lists *}
   18.36  
   18.37  lemma wf_lexn: "wf r ==> wf (lexn r n)"
   18.38 -apply (induct_tac n, simp, simp)
   18.39 +apply (induct n, simp, simp)
   18.40  apply(rule wf_subset)
   18.41   prefer 2 apply (rule Int_lower1)
   18.42  apply(rule wf_prod_fun_image)
   18.43 @@ -1678,7 +1678,7 @@
   18.44  "lexn r n =
   18.45  {(xs,ys). length xs = n \<and> length ys = n \<and>
   18.46  (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
   18.47 -apply (induct_tac n, simp, blast)
   18.48 +apply (induct n, simp, blast)
   18.49  apply (simp add: image_Collect lex_prod_def, safe, blast)
   18.50   apply (rule_tac x = "ab # xys" in exI, simp)
   18.51  apply (case_tac xys, simp_all, blast)
    19.1 --- a/src/HOL/Map.thy	Mon Oct 18 13:40:45 2004 +0200
    19.2 +++ b/src/HOL/Map.thy	Tue Oct 19 18:18:45 2004 +0200
    19.3 @@ -180,7 +180,7 @@
    19.4  by (induct rule:list_induct2, simp_all)
    19.5  
    19.6  lemma finite_range_map_of: "finite (range (map_of xys))"
    19.7 -apply (induct_tac xys)
    19.8 +apply (induct xys)
    19.9  apply  (simp_all (no_asm) add: image_constant)
   19.10  apply (rule finite_subset)
   19.11  prefer 2 apply assumption
   19.12 @@ -188,27 +188,27 @@
   19.13  done
   19.14  
   19.15  lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
   19.16 -by (induct_tac "xs", auto)
   19.17 +by (induct "xs", auto)
   19.18  
   19.19  lemma map_of_mapk_SomeI [rule_format (no_asm)]: "inj f ==> map_of t k = Some x -->  
   19.20     map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
   19.21 -apply (induct_tac "t")
   19.22 +apply (induct "t")
   19.23  apply  (auto simp add: inj_eq)
   19.24  done
   19.25  
   19.26  lemma weak_map_of_SomeI [rule_format (no_asm)]: "(k, x) : set l --> (? x. map_of l k = Some x)"
   19.27 -by (induct_tac "l", auto)
   19.28 +by (induct "l", auto)
   19.29  
   19.30  lemma map_of_filter_in: 
   19.31  "[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z"
   19.32  apply (rule mp)
   19.33  prefer 2 apply assumption
   19.34  apply (erule thin_rl)
   19.35 -apply (induct_tac "xs", auto)
   19.36 +apply (induct "xs", auto)
   19.37  done
   19.38  
   19.39  lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
   19.40 -by (induct_tac "xs", auto)
   19.41 +by (induct "xs", auto)
   19.42  
   19.43  
   19.44  subsection {* @{term option_map} related *}
   19.45 @@ -270,7 +270,7 @@
   19.46  
   19.47  lemma map_of_append[simp]: "map_of (xs@ys) = map_of ys ++ map_of xs"
   19.48  apply (unfold map_add_def)
   19.49 -apply (induct_tac "xs")
   19.50 +apply (induct "xs")
   19.51  apply (simp (no_asm))
   19.52  apply (rule ext)
   19.53  apply (simp (no_asm_simp) split add: option.split)
   19.54 @@ -279,7 +279,7 @@
   19.55  declare fun_upd_apply [simp del]
   19.56  lemma finite_range_map_of_map_add:
   19.57   "finite (range f) ==> finite (range (f ++ map_of l))"
   19.58 -apply (induct_tac "l", auto)
   19.59 +apply (induct "l", auto)
   19.60  apply (erule finite_range_updI)
   19.61  done
   19.62  declare fun_upd_apply [simp]
   19.63 @@ -445,7 +445,7 @@
   19.64  
   19.65  lemma finite_dom_map_of: "finite (dom (map_of l))"
   19.66  apply (unfold dom_def)
   19.67 -apply (induct_tac "l")
   19.68 +apply (induct "l")
   19.69  apply (auto simp add: insert_Collect [symmetric])
   19.70  done
   19.71  
    20.1 --- a/src/HOL/Nat.thy	Mon Oct 18 13:40:45 2004 +0200
    20.2 +++ b/src/HOL/Nat.thy	Tue Oct 19 18:18:45 2004 +0200
    20.3 @@ -149,7 +149,7 @@
    20.4  theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    20.5      (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
    20.6    apply (rule_tac x = m in spec)
    20.7 -  apply (induct_tac n)
    20.8 +  apply (induct n)
    20.9    prefer 2
   20.10    apply (rule allI)
   20.11    apply (induct_tac x, rules+)
   20.12 @@ -261,8 +261,8 @@
   20.13  
   20.14  text {* "Less than" is a linear ordering *}
   20.15  lemma less_linear: "m < n | m = n | n < (m::nat)"
   20.16 -  apply (induct_tac m)
   20.17 -  apply (induct_tac n)
   20.18 +  apply (induct m)
   20.19 +  apply (induct n)
   20.20    apply (rule refl [THEN disjI1, THEN disjI2])
   20.21    apply (rule zero_less_Suc [THEN disjI1])
   20.22    apply (blast intro: Suc_mono less_SucI elim: lessE)
   20.23 @@ -614,10 +614,10 @@
   20.24  text {* Difference *}
   20.25  
   20.26  lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
   20.27 -  by (induct_tac n) simp_all
   20.28 +  by (induct n) simp_all
   20.29  
   20.30  lemma diff_Suc_Suc [simp, code]: "Suc(m) - Suc(n) = m - n"
   20.31 -  by (induct_tac n) simp_all
   20.32 +  by (induct n) simp_all
   20.33  
   20.34  
   20.35  text {*
   20.36 @@ -730,7 +730,7 @@
   20.37  qed
   20.38  
   20.39  lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   20.40 -  apply (induct_tac m)
   20.41 +  apply (induct m)
   20.42    apply (induct_tac [2] n, simp_all)
   20.43    done
   20.44  
   20.45 @@ -743,7 +743,7 @@
   20.46  text {* strict, in both arguments *}
   20.47  lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
   20.48    apply (rule add_less_mono1 [THEN less_trans], assumption+)
   20.49 -  apply (induct_tac j, simp_all)
   20.50 +  apply (induct j, simp_all)
   20.51    done
   20.52  
   20.53  text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
   20.54 @@ -999,8 +999,8 @@
   20.55    done
   20.56  
   20.57  lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
   20.58 -  apply (induct_tac m, simp)
   20.59 -  apply (induct_tac n, simp, fastsimp)
   20.60 +  apply (induct m, simp)
   20.61 +  apply (induct n, simp, fastsimp)
   20.62    done
   20.63  
   20.64  lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
    21.1 --- a/src/HOL/Power.thy	Mon Oct 18 13:40:45 2004 +0200
    21.2 +++ b/src/HOL/Power.thy	Tue Oct 19 18:18:45 2004 +0200
    21.3 @@ -22,10 +22,10 @@
    21.4  
    21.5  text{*It looks plausible as a simprule, but its effect can be strange.*}
    21.6  lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::recpower))"
    21.7 -by (induct_tac "n", auto)
    21.8 +by (induct "n", auto)
    21.9  
   21.10  lemma power_one [simp]: "1^n = (1::'a::recpower)"
   21.11 -apply (induct_tac "n")
   21.12 +apply (induct "n")
   21.13  apply (auto simp add: power_Suc)
   21.14  done
   21.15  
   21.16 @@ -33,23 +33,23 @@
   21.17  by (simp add: power_Suc)
   21.18  
   21.19  lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)"
   21.20 -apply (induct_tac "n")
   21.21 +apply (induct "n")
   21.22  apply (simp_all add: power_Suc mult_ac)
   21.23  done
   21.24  
   21.25  lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n"
   21.26 -apply (induct_tac "n")
   21.27 +apply (induct "n")
   21.28  apply (simp_all add: power_Suc power_add)
   21.29  done
   21.30  
   21.31  lemma power_mult_distrib: "((a::'a::recpower) * b) ^ n = (a^n) * (b^n)"
   21.32 -apply (induct_tac "n")
   21.33 +apply (induct "n")
   21.34  apply (auto simp add: power_Suc mult_ac)
   21.35  done
   21.36  
   21.37  lemma zero_less_power:
   21.38       "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"
   21.39 -apply (induct_tac "n")
   21.40 +apply (induct "n")
   21.41  apply (simp_all add: power_Suc zero_less_one mult_pos)
   21.42  done
   21.43  
   21.44 @@ -62,7 +62,7 @@
   21.45  
   21.46  lemma one_le_power:
   21.47       "1 \<le> (a::'a::{ordered_semidom,recpower}) ==> 1 \<le> a^n"
   21.48 -apply (induct_tac "n")
   21.49 +apply (induct "n")
   21.50  apply (simp_all add: power_Suc)
   21.51  apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
   21.52  apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
   21.53 @@ -124,7 +124,7 @@
   21.54  
   21.55  lemma power_mono:
   21.56       "[|a \<le> b; (0::'a::{recpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n"
   21.57 -apply (induct_tac "n")
   21.58 +apply (induct "n")
   21.59  apply (simp_all add: power_Suc)
   21.60  apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b])
   21.61  done
   21.62 @@ -132,20 +132,20 @@
   21.63  lemma power_strict_mono [rule_format]:
   21.64       "[|a < b; (0::'a::{recpower,ordered_semidom}) \<le> a|]
   21.65        ==> 0 < n --> a^n < b^n"
   21.66 -apply (induct_tac "n")
   21.67 +apply (induct "n")
   21.68  apply (auto simp add: mult_strict_mono zero_le_power power_Suc
   21.69                        order_le_less_trans [of 0 a b])
   21.70  done
   21.71  
   21.72  lemma power_eq_0_iff [simp]:
   21.73       "(a^n = 0) = (a = (0::'a::{ordered_idom,recpower}) & 0<n)"
   21.74 -apply (induct_tac "n")
   21.75 +apply (induct "n")
   21.76  apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
   21.77  done
   21.78  
   21.79  lemma field_power_eq_0_iff [simp]:
   21.80       "(a^n = 0) = (a = (0::'a::{field,recpower}) & 0<n)"
   21.81 -apply (induct_tac "n")
   21.82 +apply (induct "n")
   21.83  apply (auto simp add: power_Suc field_mult_eq_0_iff zero_neq_one[THEN not_sym])
   21.84  done
   21.85  
   21.86 @@ -154,14 +154,14 @@
   21.87  
   21.88  lemma nonzero_power_inverse:
   21.89    "a \<noteq> 0 ==> inverse ((a::'a::{field,recpower}) ^ n) = (inverse a) ^ n"
   21.90 -apply (induct_tac "n")
   21.91 +apply (induct "n")
   21.92  apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute)
   21.93  done
   21.94  
   21.95  text{*Perhaps these should be simprules.*}
   21.96  lemma power_inverse:
   21.97    "inverse ((a::'a::{field,division_by_zero,recpower}) ^ n) = (inverse a) ^ n"
   21.98 -apply (induct_tac "n")
   21.99 +apply (induct "n")
  21.100  apply (auto simp add: power_Suc inverse_mult_distrib)
  21.101  done
  21.102  
  21.103 @@ -177,7 +177,7 @@
  21.104  done
  21.105  
  21.106  lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,recpower}) ^ n"
  21.107 -apply (induct_tac "n")
  21.108 +apply (induct "n")
  21.109  apply (auto simp add: power_Suc abs_mult)
  21.110  done
  21.111  
  21.112 @@ -193,7 +193,7 @@
  21.113  
  21.114  lemma zero_le_power_abs [simp]:
  21.115       "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n"
  21.116 -apply (induct_tac "n")
  21.117 +apply (induct "n")
  21.118  apply (auto simp add: zero_le_one zero_le_power)
  21.119  done
  21.120  
  21.121 @@ -207,7 +207,7 @@
  21.122  lemma power_Suc_less:
  21.123       "[|(0::'a::{ordered_semidom,recpower}) < a; a < 1|]
  21.124        ==> a * a^n < a^n"
  21.125 -apply (induct_tac n)
  21.126 +apply (induct n)
  21.127  apply (auto simp add: power_Suc mult_strict_left_mono)
  21.128  done
  21.129  
  21.130 @@ -215,7 +215,7 @@
  21.131       "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,recpower})|]
  21.132        ==> a^N < a^n"
  21.133  apply (erule rev_mp)
  21.134 -apply (induct_tac "N")
  21.135 +apply (induct "N")
  21.136  apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
  21.137  apply (rename_tac m)
  21.138  apply (subgoal_tac "a * a^m < 1 * a^n", simp)
  21.139 @@ -228,7 +228,7 @@
  21.140       "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semidom,recpower})|]
  21.141        ==> a^N \<le> a^n"
  21.142  apply (erule rev_mp)
  21.143 -apply (induct_tac "N")
  21.144 +apply (induct "N")
  21.145  apply (auto simp add: power_Suc  le_Suc_eq)
  21.146  apply (rename_tac m)
  21.147  apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
  21.148 @@ -245,7 +245,7 @@
  21.149  lemma power_increasing:
  21.150       "[|n \<le> N; (1::'a::{ordered_semidom,recpower}) \<le> a|] ==> a^n \<le> a^N"
  21.151  apply (erule rev_mp)
  21.152 -apply (induct_tac "N")
  21.153 +apply (induct "N")
  21.154  apply (auto simp add: power_Suc le_Suc_eq)
  21.155  apply (rename_tac m)
  21.156  apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
  21.157 @@ -256,14 +256,14 @@
  21.158  text{*Lemma for @{text power_strict_increasing}*}
  21.159  lemma power_less_power_Suc:
  21.160       "(1::'a::{ordered_semidom,recpower}) < a ==> a^n < a * a^n"
  21.161 -apply (induct_tac n)
  21.162 +apply (induct n)
  21.163  apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
  21.164  done
  21.165  
  21.166  lemma power_strict_increasing:
  21.167       "[|n < N; (1::'a::{ordered_semidom,recpower}) < a|] ==> a^n < a^N"
  21.168  apply (erule rev_mp)
  21.169 -apply (induct_tac "N")
  21.170 +apply (induct "N")
  21.171  apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
  21.172  apply (rename_tac m)
  21.173  apply (subgoal_tac "1 * a^n < a * a^m", simp)
  21.174 @@ -332,10 +332,10 @@
  21.175  done
  21.176  
  21.177  lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
  21.178 -by (induct_tac "n", auto)
  21.179 +by (induct "n", auto)
  21.180  
  21.181  lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
  21.182 -apply (induct_tac "j")
  21.183 +apply (induct "j")
  21.184  apply (simp_all add: le_Suc_eq)
  21.185  apply (blast dest!: dvd_mult_right)
  21.186  done
  21.187 @@ -371,7 +371,7 @@
  21.188  by simp
  21.189  
  21.190  lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
  21.191 -apply (induct_tac "n", auto)
  21.192 +apply (induct "n", auto)
  21.193  apply (erule allE)
  21.194  apply (erule mp, arith)
  21.195  done
  21.196 @@ -379,15 +379,15 @@
  21.197  declare binomial_0 [simp del] binomial_Suc [simp del]
  21.198  
  21.199  lemma binomial_n_n [simp]: "(n choose n) = 1"
  21.200 -apply (induct_tac "n")
  21.201 +apply (induct "n")
  21.202  apply (simp_all add: binomial_eq_0)
  21.203  done
  21.204  
  21.205  lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
  21.206 -by (induct_tac "n", simp_all)
  21.207 +by (induct "n", simp_all)
  21.208  
  21.209  lemma binomial_1 [simp]: "(n choose Suc 0) = n"
  21.210 -by (induct_tac "n", simp_all)
  21.211 +by (induct "n", simp_all)
  21.212  
  21.213  lemma zero_less_binomial [rule_format]: "k \<le> n --> 0 < (n choose k)"
  21.214  by (rule_tac m = n and n = k in diff_induct, simp_all)
  21.215 @@ -404,7 +404,7 @@
  21.216  (*Might be more useful if re-oriented*)
  21.217  lemma Suc_times_binomial_eq [rule_format]:
  21.218       "\<forall>k. k \<le> n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
  21.219 -apply (induct_tac "n")
  21.220 +apply (induct "n")
  21.221  apply (simp add: binomial_0, clarify)
  21.222  apply (case_tac "k")
  21.223  apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
    22.1 --- a/src/HOL/Real/RealPow.thy	Mon Oct 18 13:40:45 2004 +0200
    22.2 +++ b/src/HOL/Real/RealPow.thy	Tue Oct 19 18:18:45 2004 +0200
    22.3 @@ -57,7 +57,7 @@
    22.4  by (insert power_increasing [of 0 n "2::real"], simp)
    22.5  
    22.6  lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
    22.7 -apply (induct_tac "n")
    22.8 +apply (induct "n")
    22.9  apply (auto simp add: real_of_nat_Suc)
   22.10  apply (subst mult_2)
   22.11  apply (rule real_add_less_le_mono)
   22.12 @@ -97,12 +97,12 @@
   22.13  done
   22.14  
   22.15  lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
   22.16 -apply (induct_tac "n")
   22.17 +apply (induct "n")
   22.18  apply (auto simp add: real_of_nat_one real_of_nat_mult)
   22.19  done
   22.20  
   22.21  lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
   22.22 -apply (induct_tac "n")
   22.23 +apply (induct "n")
   22.24  apply (auto simp add: real_of_nat_mult zero_less_mult_iff)
   22.25  done
   22.26  
   22.27 @@ -113,12 +113,12 @@
   22.28  
   22.29  lemma zero_less_realpow_abs_iff [simp]:
   22.30       "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)" 
   22.31 -apply (induct_tac "n")
   22.32 +apply (induct "n")
   22.33  apply (auto simp add: zero_less_mult_iff)
   22.34  done
   22.35  
   22.36  lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n"
   22.37 -apply (induct_tac "n")
   22.38 +apply (induct "n")
   22.39  apply (auto simp add: zero_le_mult_iff)
   22.40  done
   22.41  
   22.42 @@ -126,7 +126,7 @@
   22.43  subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}
   22.44  
   22.45  lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
   22.46 -apply (induct_tac "n")
   22.47 +apply (induct "n")
   22.48  apply (simp_all add: nat_mult_distrib)
   22.49  done
   22.50  declare real_of_int_power [symmetric, simp]
   22.51 @@ -235,7 +235,7 @@
   22.52  by (case_tac "n", auto)
   22.53  
   22.54  lemma real_num_zero_less_two_pow [simp]: "0 < (2::real) ^ (4*d)"
   22.55 -apply (induct_tac "d")
   22.56 +apply (induct "d")
   22.57  apply (auto simp add: realpow_num_eq_if)
   22.58  done
   22.59  
    23.1 --- a/src/HOL/SetInterval.thy	Mon Oct 18 13:40:45 2004 +0200
    23.2 +++ b/src/HOL/SetInterval.thy	Tue Oct 19 18:18:45 2004 +0200
    23.3 @@ -335,7 +335,7 @@
    23.4  subsubsection {* Cardinality *}
    23.5  
    23.6  lemma card_lessThan [simp]: "card {..<u} = u"
    23.7 -  by (induct_tac u, simp_all add: lessThan_Suc)
    23.8 +  by (induct u, simp_all add: lessThan_Suc)
    23.9  
   23.10  lemma card_atMost [simp]: "card {..u} = Suc u"
   23.11    by (simp add: lessThan_Suc_atMost [THEN sym])