--- a/src/HOL/Complex/CSeries.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Complex/CSeries.thy Tue Oct 19 18:18:45 2004 +0200
@@ -30,30 +30,30 @@
*)
lemma sumc_Suc_zero [simp]: "sumc (Suc n) n f = 0"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma sumc_eq_bounds [simp]: "sumc m m f = 0"
-by (induct_tac "m", auto)
+by (induct "m", auto)
lemma sumc_Suc_eq [simp]: "sumc m (Suc m) f = f(m)"
by auto
lemma sumc_add_lbound_zero [simp]: "sumc (m+k) k f = 0"
-by (induct_tac "k", auto)
+by (induct "k", auto)
lemma sumc_add: "sumc m n f + sumc m n g = sumc m n (%n. f n + g n)"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: add_ac)
done
lemma sumc_mult: "r * sumc m n f = sumc m n (%n. r * f n)"
-apply (induct_tac "n", auto)
+apply (induct "n", auto)
apply (auto simp add: right_distrib)
done
lemma sumc_split_add [rule_format]:
"n < p --> sumc 0 n f + sumc n p f = sumc 0 p f"
-apply (induct_tac "p")
+apply (induct "p")
apply (auto dest!: leI dest: le_anti_sym)
done
@@ -64,16 +64,16 @@
done
lemma sumc_cmod: "cmod(sumc m n f) \<le> sumr m n (%i. cmod(f i))"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto intro: complex_mod_triangle_ineq [THEN order_trans])
done
lemma sumc_fun_eq [rule_format (no_asm)]:
"(\<forall>r. m \<le> r & r < n --> f r = g r) --> sumc m n f = sumc m n g"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma sumc_const [simp]: "sumc 0 n (%i. r) = complex_of_real (real n) * r"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: left_distrib real_of_nat_Suc)
done
@@ -86,29 +86,29 @@
by (simp add: diff_minus sumc_add_mult_const)
lemma sumc_less_bounds_zero [rule_format]: "n < m --> sumc m n f = 0"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma sumc_minus: "sumc m n (%i. - f i) = - sumc m n f"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma sumc_shift_bounds: "sumc (m+k) (n+k) f = sumc m n (%i. f(i + k))"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma sumc_minus_one_complexpow_zero [simp]:
"sumc 0 (2*n) (%i. (-1) ^ Suc i) = 0"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma sumc_interval_const [rule_format (no_asm)]:
"(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na
--> sumc m na f = (complex_of_real(real (na - m)) * r)"
-apply (induct_tac "na")
+apply (induct "na")
apply (auto simp add: Suc_diff_le real_of_nat_Suc left_distrib)
done
lemma sumc_interval_const2 [rule_format (no_asm)]:
"(\<forall>n. m \<le> n --> f n = r) & m \<le> na
--> sumc m na f = (complex_of_real(real (na - m)) * r)"
-apply (induct_tac "na")
+apply (induct "na")
apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc)
done
@@ -148,14 +148,14 @@
***)
lemma sumr_cmod_ge_zero [iff]: "0 \<le> sumr m n (%n. cmod (f n))"
-by (induct_tac "n", auto simp add: add_increasing)
+by (induct "n", auto simp add: add_increasing)
lemma rabs_sumc_cmod_cancel [simp]:
"abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))"
by (simp add: abs_if linorder_not_less)
lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0"
-apply (induct_tac "n")
+apply (induct "n")
apply (case_tac [2] "n", auto)
done
@@ -164,12 +164,12 @@
lemma sumc_subst [rule_format (no_asm)]:
"(\<forall>p. (m \<le> p & p < m + n --> (f p = g p))) --> sumc m n f = sumc m n g"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma sumc_group [simp]:
"sumc 0 n (%m. sumc (m * k) (m*k + k) f) = sumc 0 (n * k) f"
apply (subgoal_tac "k = 0 | 0 < k", auto)
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: sumc_split_add add_commute)
done
--- a/src/HOL/Divides.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Divides.thy Tue Oct 19 18:18:45 2004 +0200
@@ -88,7 +88,7 @@
by (simp add: mod_geq)
lemma mod_1 [simp]: "m mod Suc 0 = 0"
-apply (induct_tac "m")
+apply (induct "m")
apply (simp_all (no_asm_simp) add: mod_geq)
done
@@ -98,7 +98,7 @@
done
lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
-apply (subgoal_tac " (n + m) mod n = (n+m-n) mod n")
+apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
apply (simp add: add_commute)
apply (subst mod_geq [symmetric], simp_all)
done
@@ -107,7 +107,7 @@
by (simp add: add_commute mod_add_self2)
lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
-apply (induct_tac "k")
+apply (induct "k")
apply (simp_all add: add_left_commute [of _ n])
done
@@ -117,7 +117,7 @@
lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
apply (case_tac "n=0", simp)
apply (case_tac "k=0", simp)
-apply (induct_tac "m" rule: nat_less_induct)
+apply (induct "m" rule: nat_less_induct)
apply (subst mod_if, simp)
apply (simp add: mod_geq diff_less diff_mult_distrib)
done
@@ -127,7 +127,7 @@
lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
apply (case_tac "n=0", simp)
-apply (induct_tac "m", simp)
+apply (induct "m", simp)
apply (rename_tac "k")
apply (cut_tac m = "k*n" and n = n in mod_add_self2)
apply (simp add: add_commute)
@@ -158,7 +158,7 @@
(*Main Result about quotient and remainder.*)
lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
apply (case_tac "n=0", simp)
-apply (induct_tac "m" rule: nat_less_induct)
+apply (induct "m" rule: nat_less_induct)
apply (subst mod_if)
apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse diff_less)
done
@@ -219,7 +219,7 @@
by (cut_tac m = m and n = n in mod_div_equality2, arith)
lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
-apply (induct_tac "m" rule: nat_less_induct)
+apply (induct "m" rule: nat_less_induct)
apply (case_tac "na<n", simp)
txt{*case @{term "n \<le> na"}*}
apply (simp add: mod_geq diff_less)
@@ -389,7 +389,7 @@
subsection{*Further Facts about Quotient and Remainder*}
lemma div_1 [simp]: "m div Suc 0 = m"
-apply (induct_tac "m")
+apply (induct "m")
apply (simp_all (no_asm_simp) add: div_geq)
done
@@ -397,7 +397,7 @@
by (simp add: div_geq)
lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
-apply (subgoal_tac " (n + m) div n = Suc ((n+m-n) div n) ")
+apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
apply (simp add: add_commute)
apply (subst div_geq [symmetric], simp_all)
done
@@ -418,7 +418,7 @@
lemma div_le_mono [rule_format (no_asm)]:
"\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
apply (case_tac "k=0", simp)
-apply (induct_tac "n" rule: nat_less_induct, clarify)
+apply (induct "n" rule: nat_less_induct, clarify)
apply (case_tac "n<k")
(* 1 case n<k *)
apply simp
@@ -434,13 +434,13 @@
lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
apply (subgoal_tac "0<n")
prefer 2 apply simp
-apply (induct_tac "k" rule: nat_less_induct)
+apply (induct_tac k rule: nat_less_induct)
apply (rename_tac "k")
apply (case_tac "k<n", simp)
apply (subgoal_tac "~ (k<m) ")
prefer 2 apply simp
apply (simp add: div_geq)
-apply (subgoal_tac " (k-n) div n \<le> (k-m) div n")
+apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
prefer 2
apply (blast intro: div_le_mono diff_le_mono2)
apply (rule le_trans, simp)
@@ -457,14 +457,14 @@
(* Similar for "less than" *)
lemma div_less_dividend [rule_format, simp]:
"!!n::nat. 1<n ==> 0 < m --> m div n < m"
-apply (induct_tac "m" rule: nat_less_induct)
+apply (induct_tac m rule: nat_less_induct)
apply (rename_tac "m")
apply (case_tac "m<n", simp)
apply (subgoal_tac "0<n")
prefer 2 apply simp
apply (simp add: div_geq)
apply (case_tac "n<m")
- apply (subgoal_tac " (m-n) div n < (m-n) ")
+ apply (subgoal_tac "(m-n) div n < (m-n) ")
apply (rule impI less_trans_Suc)+
apply assumption
apply (simp_all add: diff_less)
@@ -473,7 +473,7 @@
text{*A fact for the mutilated chess board*}
lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
apply (case_tac "n=0", simp)
-apply (induct_tac "m" rule: nat_less_induct)
+apply (induct "m" rule: nat_less_induct)
apply (case_tac "Suc (na) <n")
(* case Suc(na) < n *)
apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
--- a/src/HOL/Hilbert_Choice.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Hilbert_Choice.thy Tue Oct 19 18:18:45 2004 +0200
@@ -392,7 +392,7 @@
lemma ex_has_greatest_nat_lemma:
"P k ==> \<forall>x. P x --> (\<exists>y. P y & ~ ((m y::nat) <= m x))
==> \<exists>y. P y & ~ (m y < m k + n)"
- apply (induct_tac n, force)
+ apply (induct n, force)
apply (force simp add: le_Suc_eq)
done
--- a/src/HOL/Hyperreal/EvenOdd.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Hyperreal/EvenOdd.thy Tue Oct 19 18:18:45 2004 +0200
@@ -13,7 +13,7 @@
subsection{*General Lemmas About Division*}
lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
-apply (induct_tac "m")
+apply (induct "m")
apply (simp_all add: mod_Suc)
done
--- a/src/HOL/Hyperreal/HyperNat.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Tue Oct 19 18:18:45 2004 +0200
@@ -601,7 +601,7 @@
lemma HNatInfinite_FreeUltrafilterNat_lemma:
"\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
==> {n. N < f n} \<in> FreeUltrafilterNat"
-apply (induct_tac "N")
+apply (induct_tac N)
apply (drule_tac x = 0 in spec)
apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem, drule FreeUltrafilterNat_Int, assumption, simp)
apply (drule_tac x = "Suc n" in spec, ultra)
--- a/src/HOL/Hyperreal/Integration.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Tue Oct 19 18:18:45 2004 +0200
@@ -96,7 +96,7 @@
lemma lemma_partition_lt_gen [rule_format]:
"partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) --> D(m) < D(m + Suc d)"
-apply (induct_tac "d", auto simp add: partition)
+apply (induct "d", auto simp add: partition)
apply (blast dest: Suc_le_lessD intro: less_le_trans order_less_trans)
done
@@ -133,11 +133,11 @@
lemma partition_lb: "partition(a,b) D ==> a \<le> D(r)"
apply (frule partition [THEN iffD1], safe)
-apply (induct_tac "r")
-apply (cut_tac [2] y = "Suc n" and x = "psize D" in linorder_le_less_linear, safe)
- apply (blast intro: order_trans partition_le)
-apply (drule_tac x = n in spec)
-apply (best intro: order_less_trans order_trans order_less_imp_le)
+apply (induct "r")
+apply (cut_tac [2] y = "Suc r" and x = "psize D" in linorder_le_less_linear)
+apply (auto intro: partition_le)
+apply (drule_tac x = r in spec)
+apply arith;
done
lemma partition_lb_lt: "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)"
@@ -332,7 +332,7 @@
lemma sumr_partition_eq_diff_bounds [simp]:
"sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0"
-by (induct_tac "m", auto)
+by (induct "m", auto)
lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
apply (auto simp add: order_le_less rsum_def Integral_def)
--- a/src/HOL/Hyperreal/Lim.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Tue Oct 19 18:18:45 2004 +0200
@@ -1114,7 +1114,7 @@
by (simp add: NSDERIV_DERIV_iff)
lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
-apply (induct_tac "n")
+apply (induct "n")
apply (drule_tac [2] DERIV_Id [THEN DERIV_mult])
apply (auto simp add: real_of_nat_Suc left_distrib)
apply (case_tac "0 < n")
@@ -1238,7 +1238,7 @@
All considerably tidied by lcp.*}
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)"
-apply (induct_tac "no")
+apply (induct "no")
apply (auto intro: order_trans)
done
@@ -1349,9 +1349,8 @@
"a \<le> b ==>
snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) =
(b-a) / (2 ^ n)"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: eq_divide_2_times_iff add_divide_distrib Let_def split_def)
-apply (auto simp add: add_ac Bolzano_bisect_le diff_minus)
done
lemmas Bolzano_nest_unique =
--- a/src/HOL/Hyperreal/MacLaurin.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Tue Oct 19 18:18:45 2004 +0200
@@ -10,10 +10,10 @@
begin
lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma sumr_offset2: "\<forall>f. sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma sumr_offset3: "sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f"
by (simp add: sumr_offset)
@@ -292,7 +292,7 @@
diff 0 0 =
(\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
diff n 0 * 0 ^ n / real (fact n)"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma Maclaurin_bi_le:
"[| diff 0 = f;
@@ -405,15 +405,15 @@
lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
"0 < n --> Suc (Suc (2 * n - 2)) = 2*n"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
"0 < n --> Suc (Suc (4*n - 2)) = 4*n"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma Suc_mult_two_diff_one [rule_format, simp]:
"0 < n --> Suc (2 * n - 1) = 2*n"
-by (induct_tac "n", auto)
+by (induct "n", auto)
text{*It is unclear why so many variant results are needed.*}
@@ -496,7 +496,7 @@
then (- 1) ^ (m div 2)/(real (fact m))
else 0) *
0 ^ m) = 1"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma Maclaurin_cos_expansion:
"\<exists>t. abs t \<le> abs x &
--- a/src/HOL/Hyperreal/NSA.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Tue Oct 19 18:18:45 2004 +0200
@@ -1961,7 +1961,7 @@
hence cannot belong to FreeUltrafilterNat
-------------------------------------------*)
lemma finite_nat_segment: "finite {n::nat. n < m}"
-apply (induct_tac "m")
+apply (induct "m")
apply (auto simp add: Suc_Un_eq)
done
--- a/src/HOL/Hyperreal/Poly.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Tue Oct 19 18:18:45 2004 +0200
@@ -108,7 +108,7 @@
lemma padd_Nil2: "p +++ [] = p"
-by (induct_tac "p", auto)
+by (induct "p", auto)
declare padd_Nil2 [simp]
lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)"
@@ -122,7 +122,7 @@
by simp
lemma poly_ident_mult: "1 %* t = t"
-by (induct_tac "t", auto)
+by (induct "t", auto)
declare poly_ident_mult [simp]
lemma poly_simple_add_Cons: "[a] +++ ((0)#t) = (a#t)"
@@ -139,23 +139,20 @@
done
lemma padd_assoc [rule_format]: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
-apply (induct_tac "a", simp, clarify)
+apply (induct "a", simp, clarify)
apply (case_tac b, simp_all)
done
lemma poly_cmult_distr [rule_format]:
"\<forall>q. a %* ( p +++ q) = (a %* p +++ a %* q)"
-apply (induct_tac "p", simp, clarify)
+apply (induct "p", simp, clarify)
apply (case_tac "q")
apply (simp_all add: right_distrib)
done
lemma pmult_by_x: "[0, 1] *** t = ((0)#t)"
-apply (induct_tac "t", simp)
-apply (simp add: poly_ident_mult padd_commut)
-apply (case_tac "list")
-apply (simp (no_asm_simp))
-apply (simp add: poly_ident_mult padd_commut)
+apply (induct "t", simp)
+apply (auto simp add: poly_ident_mult padd_commut)
done
declare pmult_by_x [simp]
@@ -170,7 +167,7 @@
done
lemma poly_cmult: "poly (c %* p) x = c * poly p x"
-apply (induct_tac "p")
+apply (induct "p")
apply (case_tac [2] "x=0")
apply (auto simp add: right_distrib mult_ac)
done
@@ -183,14 +180,14 @@
lemma poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x"
apply (subgoal_tac "\<forall>p2. poly (p1 *** p2) x = poly p1 x * poly p2 x")
apply (simp (no_asm_simp))
-apply (induct_tac "p1")
+apply (induct "p1")
apply (auto simp add: poly_cmult)
-apply (case_tac "list")
+apply (case_tac p1)
apply (auto simp add: poly_cmult poly_add left_distrib right_distrib mult_ac)
done
lemma poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: poly_cmult poly_mult)
done
@@ -204,11 +201,11 @@
by (simp add: poly_mult real_mult_assoc)
lemma poly_mult_Nil2: "poly (p *** []) x = 0"
-by (induct_tac "p", auto)
+by (induct "p", auto)
declare poly_mult_Nil2 [simp]
lemma poly_exp_add: "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d) x"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: poly_mult real_mult_assoc)
done
@@ -236,7 +233,7 @@
lemma lemma_DERIV_poly1: "\<forall>n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :>
x ^ n * poly (pderiv_aux (Suc n) p) x "
-apply (induct_tac "p")
+apply (induct "p")
apply (auto intro!: DERIV_add DERIV_cmult2
simp add: pderiv_def right_distrib real_mult_assoc [symmetric]
simp del: realpow_Suc)
@@ -253,7 +250,7 @@
by (rule lemma_DERIV_subst, rule DERIV_add, auto)
lemma poly_DERIV: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
-apply (induct_tac "p")
+apply (induct "p")
apply (auto simp add: pderiv_Cons)
apply (rule DERIV_add_const)
apply (rule lemma_DERIV_subst)
@@ -299,7 +296,7 @@
lemma lemma_poly_pderiv_aux_add: "\<forall>p2 n. poly (pderiv_aux n (p1 +++ p2)) x =
poly (pderiv_aux n p1 +++ pderiv_aux n p2) x"
-apply (induct_tac "p1", simp, clarify)
+apply (induct "p1", simp, clarify)
apply (case_tac "p2")
apply (auto simp add: right_distrib)
done
@@ -310,7 +307,7 @@
done
lemma lemma_poly_pderiv_aux_cmult: "\<forall>n. poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x"
-apply (induct_tac "p")
+apply (induct "p")
apply (auto simp add: poly_cmult mult_ac)
done
@@ -323,7 +320,7 @@
done
lemma lemma_poly_pderiv_aux_mult1: "\<forall>n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"
-apply (induct_tac "p")
+apply (induct "p")
apply (auto simp add: real_of_nat_Suc left_distrib)
done
@@ -331,7 +328,7 @@
by (simp add: lemma_poly_pderiv_aux_mult1)
lemma lemma_poly_pderiv_add: "\<forall>q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x"
-apply (induct_tac "p", simp, clarify)
+apply (induct "p", simp, clarify)
apply (case_tac "q")
apply (auto simp add: poly_pderiv_aux_add poly_add pderiv_def)
done
@@ -340,7 +337,7 @@
by (simp add: lemma_poly_pderiv_add)
lemma poly_pderiv_cmult: "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x"
-apply (induct_tac "p")
+apply (induct "p")
apply (auto simp add: poly_pderiv_aux_cmult poly_cmult pderiv_def)
done
@@ -350,13 +347,13 @@
lemma lemma_poly_mult_pderiv:
"poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x"
apply (simp add: pderiv_def)
-apply (induct_tac "t")
+apply (induct "t")
apply (auto simp add: poly_add lemma_poly_pderiv_aux_mult)
done
lemma poly_pderiv_mult: "\<forall>q. poly (pderiv (p *** q)) x =
poly (p *** (pderiv q) +++ q *** (pderiv p)) x"
-apply (induct_tac "p")
+apply (induct "p")
apply (auto simp add: poly_add poly_cmult poly_pderiv_cmult poly_pderiv_add poly_mult)
apply (rule lemma_poly_mult_pderiv [THEN ssubst])
apply (rule lemma_poly_mult_pderiv [THEN ssubst])
@@ -367,7 +364,7 @@
lemma poly_pderiv_exp: "poly (pderiv (p %^ (Suc n))) x =
poly ((real (Suc n)) %* (p %^ n) *** pderiv p) x"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: poly_add poly_pderiv_cmult poly_cmult poly_pderiv_mult
real_of_nat_zero poly_mult real_of_nat_Suc
right_distrib left_distrib mult_ac)
@@ -383,7 +380,7 @@
@{term "p(x)"} *}
lemma lemma_poly_linear_rem: "\<forall>h. \<exists>q r. h#t = [r] +++ [-a, 1] *** q"
-apply (induct_tac "t", safe)
+apply (induct "t", safe)
apply (rule_tac x = "[]" in exI)
apply (rule_tac x = h in exI, simp)
apply (drule_tac x = aa in spec, safe)
@@ -407,11 +404,11 @@
done
lemma lemma_poly_length_mult: "\<forall>h k a. length (k %* p +++ (h # (a %* p))) = Suc (length p)"
-by (induct_tac "p", auto)
+by (induct "p", auto)
declare lemma_poly_length_mult [simp]
lemma lemma_poly_length_mult2: "\<forall>h k. length (k %* p +++ (h # p)) = Suc (length p)"
-by (induct_tac "p", auto)
+by (induct "p", auto)
declare lemma_poly_length_mult2 [simp]
lemma poly_length_mult: "length([-a,1] *** q) = Suc (length q)"
@@ -422,13 +419,13 @@
subsection{*Polynomial length*}
lemma poly_cmult_length: "length (a %* p) = length p"
-by (induct_tac "p", auto)
+by (induct "p", auto)
declare poly_cmult_length [simp]
lemma poly_add_length [rule_format]:
"\<forall>p2. length (p1 +++ p2) =
(if (length p1 < length p2) then length p2 else length p1)"
-apply (induct_tac "p1", simp_all, arith)
+apply (induct "p1", simp_all, arith)
done
lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)"
@@ -447,14 +444,14 @@
text{*Normalisation Properties*}
lemma poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)"
-by (induct_tac "p", auto)
+by (induct "p", auto)
text{*A nontrivial polynomial of degree n has no more than n roots*}
lemma poly_roots_index_lemma [rule_format]:
"\<forall>p x. poly p x \<noteq> poly [] x & length p = n
--> (\<exists>i. \<forall>x. (poly p x = (0::real)) --> (\<exists>m. (m \<le> n & x = i m)))"
-apply (induct_tac "n", safe)
+apply (induct "n", safe)
apply (rule ccontr)
apply (subgoal_tac "\<exists>a. poly p a = 0", safe)
apply (drule poly_linear_divides [THEN iffD1], safe)
@@ -464,7 +461,7 @@
apply (erule exE)
apply (drule_tac x = "%m. if m = Suc n then a else i m" in spec, safe)
apply (drule poly_mult_eq_zero_disj [THEN iffD1], safe)
-apply (drule_tac x = "Suc (length q) " in spec)
+apply (drule_tac x = "Suc (length q)" in spec)
apply simp
apply (drule_tac x = xa in spec, safe)
apply (drule_tac x = m in spec, simp, blast)
@@ -478,25 +475,23 @@
lemma poly_roots_finite_lemma: "poly p x \<noteq> poly [] x ==>
\<exists>N i. \<forall>x. (poly p x = 0) --> (\<exists>n. (n::nat) < N & x = i n)"
apply (drule poly_roots_index_length, safe)
-apply (rule_tac x = "Suc (length p) " in exI)
+apply (rule_tac x = "Suc (length p)" in exI)
apply (rule_tac x = i in exI)
apply (simp add: less_Suc_eq_le)
done
(* annoying proof *)
lemma real_finite_lemma [rule_format (no_asm)]:
- "\<forall>P. (\<forall>x. P x --> (\<exists>n. (n::nat) < N & x = (j::nat=>real) n))
+ "\<forall>P. (\<forall>x. P x --> (\<exists>n. n < N & x = (j::nat=>real) n))
--> (\<exists>a. \<forall>x. P x --> x < a)"
-apply (induct_tac "N", simp, safe)
-apply (drule_tac x = "%z. P z & (z \<noteq> (j::nat=>real) n) " in spec)
-apply auto
-apply (drule_tac x = x in spec, safe)
-apply (rule_tac x = na in exI)
-apply (auto simp add: less_Suc_eq)
-apply (rule_tac x = "abs a + abs (j n) + 1" in exI)
+apply (induct "N", simp, safe)
+apply (drule_tac x = "%z. P z & (z \<noteq> j N)" in spec)
+apply (auto simp add: less_Suc_eq)
+apply (rename_tac N P a)
+apply (rule_tac x = "abs a + abs (j N) + 1" in exI)
apply safe
-apply (drule_tac x = x in spec, safe)
-apply (drule_tac x = "j na" in spec, arith+)
+apply (drule_tac x = x in spec, safe)
+apply (drule_tac x = "j n" in spec, arith+)
done
lemma poly_roots_finite: "(poly p \<noteq> poly []) =
@@ -515,7 +510,7 @@
==> poly (p *** q) \<noteq> poly []"
apply (auto simp add: poly_roots_finite)
apply (rule_tac x = "N + Na" in exI)
-apply (rule_tac x = "%n. if n < N then j n else ja (n - N) " in exI)
+apply (rule_tac x = "%n. if n < N then j n else ja (n - N)" in exI)
apply (auto simp add: poly_mult_eq_zero_disj, force)
done
@@ -579,7 +574,7 @@
lemma poly_zero: "(poly p = poly []) = list_all (%c. c = 0) p"
-apply (induct_tac "p", simp)
+apply (induct "p", simp)
apply (rule iffI)
apply (drule poly_zero_lemma, auto)
done
@@ -588,7 +583,7 @@
lemma pderiv_aux_iszero [rule_format, simp]:
"\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p"
-by (induct_tac "p", auto)
+by (induct "p", auto)
lemma pderiv_aux_iszero_num: "(number_of n :: nat) \<noteq> 0
==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
@@ -601,14 +596,14 @@
lemma pderiv_iszero [rule_format]:
"poly (pderiv p) = poly [] --> (\<exists>h. poly p = poly [h])"
apply (simp add: poly_zero)
-apply (induct_tac "p", force)
+apply (induct "p", force)
apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons)
apply (auto simp add: poly_zero [symmetric])
done
lemma pderiv_zero_obj: "poly p = poly [] --> (poly (pderiv p) = poly [])"
apply (simp add: poly_zero)
-apply (induct_tac "p", force)
+apply (induct "p", force)
apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons)
done
@@ -697,13 +692,13 @@
lemma poly_order_exists_lemma [rule_format]:
"\<forall>p. length p = d --> poly p \<noteq> poly []
--> (\<exists>n q. p = mulexp n [-a, 1] q & poly q a \<noteq> 0)"
-apply (induct_tac "d")
+apply (induct "d")
apply (simp add: fun_eq, safe)
apply (case_tac "poly p a = 0")
apply (drule_tac poly_linear_divides [THEN iffD1], safe)
apply (drule_tac x = q in spec)
apply (drule_tac poly_entire_neg [THEN iffD1], safe, force, blast)
-apply (rule_tac x = "Suc na" in exI)
+apply (rule_tac x = "Suc n" in exI)
apply (rule_tac x = qa in exI)
apply (simp del: pmult_Cons)
apply (rule_tac x = 0 in exI, force)
@@ -780,7 +775,7 @@
by (auto simp add: fun_eq divides_def poly_mult order_def)
lemma pexp_one: "p %^ (Suc 0) = p"
-apply (induct_tac "p")
+apply (induct "p")
apply (auto simp add: numeral_1_eq_1)
done
declare pexp_one [simp]
@@ -788,7 +783,7 @@
lemma lemma_order_root [rule_format]:
"\<forall>p a. 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
--> poly p a = 0"
-apply (induct_tac "n", blast)
+apply (induct "n", blast)
apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
done
@@ -851,7 +846,7 @@
poly (pderiv p) \<noteq> poly [] &
poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q
--> n = Suc (order a (pderiv p))"
-apply (induct_tac "n", safe)
+apply (induct "n", safe)
apply (rule order_unique_lemma, rule conjI, assumption)
apply (subgoal_tac "\<forall>r. r divides (pderiv p) = r divides (pderiv ([-a, 1] %^ Suc n *** q))")
apply (drule_tac [2] poly_pderiv_welldef)
@@ -862,7 +857,7 @@
apply (rule_tac x = "[-a, 1] *** (pderiv q) +++ real (Suc n) %* q" in exI)
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)
apply (simp add: poly_mult right_distrib left_distrib mult_ac del: pmult_Cons)
-apply (erule_tac V = "\<forall>r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q) " in thin_rl)
+apply (erule_tac V = "\<forall>r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q)" in thin_rl)
apply (unfold divides_def)
apply (simp (no_asm) add: poly_pderiv_mult poly_pderiv_exp_prime fun_eq poly_add poly_mult del: pmult_Cons pexp_Suc)
apply (rule swap, assumption)
@@ -872,7 +867,7 @@
apply (subgoal_tac "poly ([-a, 1] %^ n *** q) = poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* (qa +++ -- (pderiv q))))) ")
apply (drule poly_mult_left_cancel [THEN iffD1], simp)
apply (simp add: fun_eq poly_mult poly_add poly_cmult poly_minus del: pmult_Cons mult_cancel_left field_mult_cancel_left, safe)
-apply (rule_tac c1 = "real (Suc n) " in real_mult_left_cancel [THEN iffD1])
+apply (rule_tac c1 = "real (Suc n)" in real_mult_left_cancel [THEN iffD1])
apply (simp (no_asm))
apply (subgoal_tac "real (Suc n) * (poly ([- a, 1] %^ n) xa * poly q xa) =
(poly qa xa + - poly (pderiv q) xa) *
@@ -901,13 +896,13 @@
poly d = poly (r *** p +++ s *** pderiv p)
|] ==> order a q = (if order a p = 0 then 0 else 1)"
apply (subgoal_tac "order a p = order a q + order a d")
-apply (rule_tac [2] s = "order a (q *** d) " in trans)
+apply (rule_tac [2] s = "order a (q *** d)" in trans)
prefer 2 apply (blast intro: order_poly)
apply (rule_tac [2] order_mult)
prefer 2 apply force
apply (case_tac "order a p = 0", simp)
apply (subgoal_tac "order a (pderiv p) = order a e + order a d")
-apply (rule_tac [2] s = "order a (e *** d) " in trans)
+apply (rule_tac [2] s = "order a (e *** d)" in trans)
prefer 2 apply (blast intro: order_poly)
apply (rule_tac [2] order_mult)
prefer 2 apply force
@@ -997,7 +992,7 @@
text{*Normalization of a polynomial.*}
lemma poly_normalize: "poly (pnormalize p) = poly p"
-apply (induct_tac "p")
+apply (induct "p")
apply (auto simp add: fun_eq)
done
declare poly_normalize [simp]
@@ -1007,7 +1002,7 @@
lemma lemma_degree_zero [rule_format]:
"list_all (%c. c = 0) p --> pnormalize p = []"
-by (induct_tac "p", auto)
+by (induct "p", auto)
lemma degree_zero: "poly p = poly [] ==> degree p = 0"
apply (simp add: degree_def)
@@ -1028,8 +1023,8 @@
text{*bound for polynomial.*}
lemma poly_mono: "abs(x) \<le> k ==> abs(poly p x) \<le> poly (map abs p) k"
-apply (induct_tac "p", auto)
-apply (rule_tac j = "abs a + abs (x * poly list x) " in real_le_trans)
+apply (induct "p", auto)
+apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
apply (rule abs_triangle_ineq)
apply (auto intro!: mult_mono simp add: abs_mult, arith)
done
--- a/src/HOL/Hyperreal/SEQ.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Tue Oct 19 18:18:45 2004 +0200
@@ -462,7 +462,7 @@
lemma lemma_finite_NSBseq2:
"finite {n. f n \<le> (u::nat) & real(Suc n) < \<bar>X(f n)\<bar>}"
-apply (induct_tac "u")
+apply (induct "u")
apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
apply (rule_tac B = "{n. real (Suc n) < \<bar>X 0\<bar> }" in finite_subset)
apply (auto intro: finite_real_of_nat_less_real
@@ -995,7 +995,7 @@
lemma NSLIMSEQ_pow [rule_format]:
"(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
-apply (induct_tac "m")
+apply (induct "m")
apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
done
--- a/src/HOL/Hyperreal/Series.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy Tue Oct 19 18:18:45 2004 +0200
@@ -38,7 +38,7 @@
lemma sumr_split_add [rule_format]:
"n < p --> sumr 0 n f + sumr n p f = sumr 0 p (f::nat=>real)"
-apply (induct_tac "p", auto)
+apply (induct "p", auto)
apply (rename_tac k)
apply (subgoal_tac "n=k", auto)
done
@@ -70,34 +70,34 @@
by (simp add: Finite_Set.setsum_negf)
lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma sumr_minus_one_realpow_zero [simp]: "sumr 0 (2*n) (%i. (-1) ^ Suc i) = 0"
-by (induct_tac "n", auto)
+by (induct "n", auto)
-lemma sumr_interval_const [rule_format (no_asm)]:
- "(\<forall>n. m \<le> Suc n --> f n = r) --> m \<le> k --> sumr m k f = (real(k-m) * r)"
-apply (induct_tac "k", auto)
-apply (drule_tac x = n in spec)
+lemma sumr_interval_const:
+ "\<lbrakk>\<forall>n. m \<le> Suc n --> f n = r; m \<le> k\<rbrakk> \<Longrightarrow> sumr m k f = (real(k-m) * r)"
+apply (induct "k", auto)
+apply (drule_tac x = k in spec)
apply (auto dest!: le_imp_less_or_eq)
apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
done
-lemma sumr_interval_const2 [rule_format (no_asm)]:
- "(\<forall>n. m \<le> n --> f n = r) --> m \<le> k
- --> sumr m k f = (real (k - m) * r)"
-apply (induct_tac "k", auto)
-apply (drule_tac x = n in spec)
+lemma sumr_interval_const2:
+ "[|\<forall>n. m \<le> n --> f n = r; m \<le> k|]
+ ==> sumr m k f = (real (k - m) * r)"
+apply (induct "k", auto)
+apply (drule_tac x = k in spec)
apply (auto dest!: le_imp_less_or_eq)
apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
done
-lemma sumr_le [rule_format (no_asm)]:
- "(\<forall>n. m \<le> n --> 0 \<le> f n) --> m < k --> sumr 0 m f \<le> sumr 0 k f"
-apply (induct_tac "k")
+lemma sumr_le:
+ "[|\<forall>n. m \<le> n --> 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f"
+apply (induct "k")
apply (auto simp add: less_Suc_eq_le)
-apply (drule_tac [!] x = n in spec, safe)
+apply (drule_tac x = k in spec, safe)
apply (drule le_imp_less_or_eq, safe)
apply (arith)
apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto)
@@ -105,22 +105,22 @@
lemma sumr_le2 [rule_format (no_asm)]:
"(\<forall>r. m \<le> r & r < n --> f r \<le> g r) --> sumr m n f \<le> sumr m n g"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto intro: add_mono simp add: le_def)
done
-lemma sumr_ge_zero [rule_format]: "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
-apply (induct_tac "n", auto)
+lemma sumr_ge_zero: "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
+apply (induct "n", auto)
apply (drule_tac x = n in spec, arith)
done
lemma rabs_sumr_rabs_cancel [simp]:
"abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))"
-by (induct_tac "n", simp_all add: add_increasing)
+by (induct "n", simp_all add: add_increasing)
lemma sumr_zero [rule_format]:
"\<forall>n. N \<le> n --> f n = 0 ==> N \<le> m --> sumr m n f = 0"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma Suc_le_imp_diff_ge2:
"[|\<forall>n. N \<le> n --> f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
@@ -129,7 +129,7 @@
done
lemma sumr_one_lb_realpow_zero [simp]: "sumr (Suc 0) n (%n. f(n) * 0 ^ n) = 0"
-apply (induct_tac "n")
+apply (induct "n")
apply (case_tac [2] "n", auto)
done
@@ -138,26 +138,26 @@
lemma sumr_subst [rule_format (no_asm)]:
"(\<forall>p. m \<le> p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g"
-by (induct_tac "n", auto)
+by (induct "n", auto)
lemma sumr_bound [rule_format (no_asm)]:
"(\<forall>p. m \<le> p & p < m + n --> (f(p) \<le> K))
--> (sumr m (m + n) f \<le> (real n * K))"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc)
done
lemma sumr_bound2 [rule_format (no_asm)]:
"(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))
--> (sumr 0 n f \<le> (real n * K))"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute)
done
lemma sumr_group [simp]:
"sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f"
apply (subgoal_tac "k = 0 | 0 < k", auto)
-apply (induct_tac "n")
+apply (induct "n")
apply (simp_all add: sumr_split_add add_commute)
done
@@ -250,10 +250,8 @@
lemma sumr_pos_lt_pair_lemma:
"[|\<forall>d. - f (n + (d + d)) < f (Suc (n + (d + d)))|]
==> sumr 0 (n + Suc (Suc 0)) f \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f"
-apply (induct_tac "no", simp)
-apply (rule_tac y = "sumr 0 (Suc (Suc 0) * (Suc na) +n) f" in order_trans)
-apply assumption
-apply (drule_tac x = "Suc na" in spec)
+apply (induct "no", auto)
+apply (drule_tac x = "Suc no" in spec)
apply (simp add: add_ac)
done
@@ -311,7 +309,7 @@
text{*Sum of a geometric progression.*}
lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
-apply (induct_tac "n", auto)
+apply (induct "n", auto)
apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
apply (auto simp add: mult_assoc left_distrib times_divide_eq)
apply (simp add: right_distrib diff_minus mult_commute)
@@ -456,7 +454,7 @@
lemma DERIV_sumr [rule_format (no_asm)]:
"(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
--> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto intro: DERIV_add)
done
--- a/src/HOL/Hyperreal/Transcendental.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Tue Oct 19 18:18:45 2004 +0200
@@ -309,24 +309,24 @@
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
@@ -353,7 +353,7 @@
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)
@@ -377,7 +377,7 @@
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)
@@ -447,7 +447,7 @@
"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
@@ -893,7 +893,7 @@
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
@@ -1552,12 +1552,12 @@
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
--- a/src/HOL/Integ/IntDef.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy Tue Oct 19 18:18:45 2004 +0200
@@ -344,11 +344,11 @@
subsection{*Strict Monotonicity of Multiplication*}
text{*strict, in 1st argument; proof is by induction on k>0*}
-lemma zmult_zless_mono2_lemma [rule_format]:
- "i<j ==> 0<k --> int k * i < int k * j"
-apply (induct_tac "k", simp)
+lemma zmult_zless_mono2_lemma:
+ "i<j ==> 0<k ==> int k * i < int k * j"
+apply (induct "k", simp)
apply (simp add: int_Suc)
-apply (case_tac "n=0")
+apply (case_tac "k=0")
apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
apply (simp add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
done
--- a/src/HOL/Integ/IntDiv.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Integ/IntDiv.thy Tue Oct 19 18:18:45 2004 +0200
@@ -1172,7 +1172,7 @@
lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
-apply (induct_tac "y", auto)
+apply (induct "y", auto)
apply (rule zmod_zmult1_eq [THEN trans])
apply (simp (no_asm_simp))
apply (rule zmod_zmult_distrib [symmetric])
@@ -1186,12 +1186,12 @@
lemma zero_less_zpower_abs_iff [simp]:
"(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: zero_less_mult_iff)
done
lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: zero_le_mult_iff)
done
--- a/src/HOL/Integ/NatBin.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Integ/NatBin.thy Tue Oct 19 18:18:45 2004 +0200
@@ -299,7 +299,7 @@
by (simp add: power2_eq_square)
lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: power_Suc power_add)
done
@@ -520,7 +520,7 @@
subsection{*Literal arithmetic involving powers*}
lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
-apply (induct_tac "n")
+apply (induct "n")
apply (simp_all (no_asm_simp) add: nat_mult_distrib)
done
--- a/src/HOL/Integ/Parity.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Integ/Parity.thy Tue Oct 19 18:18:45 2004 +0200
@@ -31,7 +31,7 @@
subsection {* Casting a nat power to an integer *}
lemma zpow_int: "int (x^y) = (int x)^y"
- apply (induct_tac y)
+ apply (induct y)
apply (simp, simp add: zmult_int [THEN sym])
done
@@ -90,12 +90,12 @@
lemma even_pow_gt_zero [rule_format]:
"even (x::int) ==> 0 < n --> even (x^n)"
- apply (induct_tac n)
+ apply (induct n)
apply (auto simp add: even_product)
done
lemma odd_pow: "odd x ==> odd((x::int)^n)"
- apply (induct_tac n)
+ apply (induct n)
apply (simp add: even_def)
apply (simp add: even_product)
done
@@ -237,7 +237,7 @@
lemma neg_one_even_odd_power:
"(even x --> (-1::'a::{number_ring,recpower})^x = 1) &
(odd x --> (-1::'a)^x = -1)"
- apply (induct_tac x)
+ apply (induct x)
apply (simp, simp add: power_Suc)
done
--- a/src/HOL/List.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/List.thy Tue Oct 19 18:18:45 2004 +0200
@@ -838,7 +838,7 @@
done
lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
-apply (induct_tac xs, simp, simp)
+apply (induct xs, simp, simp)
apply safe
apply (rule_tac x = 0 in exI, simp)
apply (rule_tac x = "Suc i" in exI, simp)
@@ -1503,10 +1503,10 @@
by (induct xs) auto
lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
- by (induct_tac x, auto)
+ by (induct x, auto)
lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
- by (induct_tac x, auto)
+ by (induct x, auto)
lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
by (induct xs) auto
@@ -1528,7 +1528,7 @@
it is useful. *}
lemma distinct_conv_nth:
"distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j --> xs!i \<noteq> xs!j)"
-apply (induct_tac xs, simp, simp)
+apply (induct xs, simp, simp)
apply (rule iffI, clarsimp)
apply (case_tac i)
apply (case_tac j, simp)
@@ -1653,7 +1653,7 @@
subsection {* Lexicographic orderings on lists *}
lemma wf_lexn: "wf r ==> wf (lexn r n)"
-apply (induct_tac n, simp, simp)
+apply (induct n, simp, simp)
apply(rule wf_subset)
prefer 2 apply (rule Int_lower1)
apply(rule wf_prod_fun_image)
@@ -1678,7 +1678,7 @@
"lexn r n =
{(xs,ys). length xs = n \<and> length ys = n \<and>
(\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
-apply (induct_tac n, simp, blast)
+apply (induct n, simp, blast)
apply (simp add: image_Collect lex_prod_def, safe, blast)
apply (rule_tac x = "ab # xys" in exI, simp)
apply (case_tac xys, simp_all, blast)
--- a/src/HOL/Map.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Map.thy Tue Oct 19 18:18:45 2004 +0200
@@ -180,7 +180,7 @@
by (induct rule:list_induct2, simp_all)
lemma finite_range_map_of: "finite (range (map_of xys))"
-apply (induct_tac xys)
+apply (induct xys)
apply (simp_all (no_asm) add: image_constant)
apply (rule finite_subset)
prefer 2 apply assumption
@@ -188,27 +188,27 @@
done
lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
-by (induct_tac "xs", auto)
+by (induct "xs", auto)
lemma map_of_mapk_SomeI [rule_format (no_asm)]: "inj f ==> map_of t k = Some x -->
map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
-apply (induct_tac "t")
+apply (induct "t")
apply (auto simp add: inj_eq)
done
lemma weak_map_of_SomeI [rule_format (no_asm)]: "(k, x) : set l --> (? x. map_of l k = Some x)"
-by (induct_tac "l", auto)
+by (induct "l", auto)
lemma map_of_filter_in:
"[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z"
apply (rule mp)
prefer 2 apply assumption
apply (erule thin_rl)
-apply (induct_tac "xs", auto)
+apply (induct "xs", auto)
done
lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
-by (induct_tac "xs", auto)
+by (induct "xs", auto)
subsection {* @{term option_map} related *}
@@ -270,7 +270,7 @@
lemma map_of_append[simp]: "map_of (xs@ys) = map_of ys ++ map_of xs"
apply (unfold map_add_def)
-apply (induct_tac "xs")
+apply (induct "xs")
apply (simp (no_asm))
apply (rule ext)
apply (simp (no_asm_simp) split add: option.split)
@@ -279,7 +279,7 @@
declare fun_upd_apply [simp del]
lemma finite_range_map_of_map_add:
"finite (range f) ==> finite (range (f ++ map_of l))"
-apply (induct_tac "l", auto)
+apply (induct "l", auto)
apply (erule finite_range_updI)
done
declare fun_upd_apply [simp]
@@ -445,7 +445,7 @@
lemma finite_dom_map_of: "finite (dom (map_of l))"
apply (unfold dom_def)
-apply (induct_tac "l")
+apply (induct "l")
apply (auto simp add: insert_Collect [symmetric])
done
--- a/src/HOL/Nat.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Nat.thy Tue Oct 19 18:18:45 2004 +0200
@@ -149,7 +149,7 @@
theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
(!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
apply (rule_tac x = m in spec)
- apply (induct_tac n)
+ apply (induct n)
prefer 2
apply (rule allI)
apply (induct_tac x, rules+)
@@ -261,8 +261,8 @@
text {* "Less than" is a linear ordering *}
lemma less_linear: "m < n | m = n | n < (m::nat)"
- apply (induct_tac m)
- apply (induct_tac n)
+ apply (induct m)
+ apply (induct n)
apply (rule refl [THEN disjI1, THEN disjI2])
apply (rule zero_less_Suc [THEN disjI1])
apply (blast intro: Suc_mono less_SucI elim: lessE)
@@ -614,10 +614,10 @@
text {* Difference *}
lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
- by (induct_tac n) simp_all
+ by (induct n) simp_all
lemma diff_Suc_Suc [simp, code]: "Suc(m) - Suc(n) = m - n"
- by (induct_tac n) simp_all
+ by (induct n) simp_all
text {*
@@ -730,7 +730,7 @@
qed
lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
- apply (induct_tac m)
+ apply (induct m)
apply (induct_tac [2] n, simp_all)
done
@@ -743,7 +743,7 @@
text {* strict, in both arguments *}
lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
apply (rule add_less_mono1 [THEN less_trans], assumption+)
- apply (induct_tac j, simp_all)
+ apply (induct j, simp_all)
done
text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
@@ -999,8 +999,8 @@
done
lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
- apply (induct_tac m, simp)
- apply (induct_tac n, simp, fastsimp)
+ apply (induct m, simp)
+ apply (induct n, simp, fastsimp)
done
lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
--- 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
--- a/src/HOL/Real/RealPow.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/Real/RealPow.thy Tue Oct 19 18:18:45 2004 +0200
@@ -57,7 +57,7 @@
by (insert power_increasing [of 0 n "2::real"], simp)
lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: real_of_nat_Suc)
apply (subst mult_2)
apply (rule real_add_less_le_mono)
@@ -97,12 +97,12 @@
done
lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: real_of_nat_one real_of_nat_mult)
done
lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: real_of_nat_mult zero_less_mult_iff)
done
@@ -113,12 +113,12 @@
lemma zero_less_realpow_abs_iff [simp]:
"(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: zero_less_mult_iff)
done
lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n"
-apply (induct_tac "n")
+apply (induct "n")
apply (auto simp add: zero_le_mult_iff)
done
@@ -126,7 +126,7 @@
subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}
lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
-apply (induct_tac "n")
+apply (induct "n")
apply (simp_all add: nat_mult_distrib)
done
declare real_of_int_power [symmetric, simp]
@@ -235,7 +235,7 @@
by (case_tac "n", auto)
lemma real_num_zero_less_two_pow [simp]: "0 < (2::real) ^ (4*d)"
-apply (induct_tac "d")
+apply (induct "d")
apply (auto simp add: realpow_num_eq_if)
done
--- a/src/HOL/SetInterval.thy Mon Oct 18 13:40:45 2004 +0200
+++ b/src/HOL/SetInterval.thy Tue Oct 19 18:18:45 2004 +0200
@@ -335,7 +335,7 @@
subsubsection {* Cardinality *}
lemma card_lessThan [simp]: "card {..<u} = u"
- by (induct_tac u, simp_all add: lessThan_Suc)
+ by (induct u, simp_all add: lessThan_Suc)
lemma card_atMost [simp]: "card {..u} = Suc u"
by (simp add: lessThan_Suc_atMost [THEN sym])