--- a/src/HOL/Complex/CSeries.thy Mon Oct 09 02:19:51 2006 +0200
+++ b/src/HOL/Complex/CSeries.thy Mon Oct 09 02:19:51 2006 +0200
@@ -30,52 +30,42 @@
*)
lemma sumc_Suc_zero [simp]: "sumc (Suc n) n f = 0"
-by (induct "n", auto)
+by (induct n) auto
lemma sumc_eq_bounds [simp]: "sumc m m f = 0"
-by (induct "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 "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 "n")
-apply (auto simp add: add_ac)
-done
+by (induct n) (auto simp add: add_ac)
lemma sumc_mult: "r * sumc m n f = sumc m n (%n. r * f n)"
-apply (induct "n", auto)
-apply (auto simp add: right_distrib)
-done
+by (induct n) (auto simp add: right_distrib)
lemma sumc_split_add [rule_format]:
"n < p --> sumc 0 n f + sumc n p f = sumc 0 p f"
-apply (induct "p")
-apply (auto dest!: leI dest: le_anti_sym)
-done
+by (induct p) (auto dest!: leI dest: le_anti_sym)
lemma sumc_split_add_minus:
"n < p ==> sumc 0 p f + - sumc 0 n f = sumc n p f"
-apply (drule_tac f1 = f in sumc_split_add [symmetric])
+apply (drule_tac f = f in sumc_split_add [symmetric])
apply (simp add: add_ac)
done
lemma sumc_cmod: "cmod(sumc m n f) \<le> (\<Sum>i=m..<n. cmod(f i))"
-apply (induct "n")
-apply (auto intro: complex_mod_triangle_ineq [THEN order_trans])
-done
+by (induct n) (auto intro: complex_mod_triangle_ineq [THEN order_trans])
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 "n", auto)
lemma sumc_const [simp]: "sumc 0 n (%i. r) = complex_of_real (real n) * r"
-apply (induct "n")
-apply (auto simp add: left_distrib real_of_nat_Suc)
-done
+by (induct n) (auto simp add: left_distrib real_of_nat_Suc)
lemma sumc_add_mult_const:
"sumc 0 n f + -(complex_of_real(real n) * r) = sumc 0 n (%i. f i + -r)"
@@ -86,31 +76,27 @@
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 "n", auto)
+by (induct n) auto
lemma sumc_minus: "sumc m n (%i. - f i) = - sumc m n f"
-by (induct "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 "n", auto)
+by (induct n) auto
lemma sumc_minus_one_complexpow_zero [simp]:
"sumc 0 (2*n) (%i. (-1) ^ Suc i) = 0"
-by (induct "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 "na")
-apply (auto simp add: Suc_diff_le real_of_nat_Suc left_distrib)
-done
+by (induct na) (auto simp add: Suc_diff_le real_of_nat_Suc left_distrib)
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 "na")
-apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc)
-done
+by (induct na) (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc)
(***
Goal "(\<forall>n. m \<le> n --> 0 \<le> cmod(f n)) & m < k --> cmod(sumc 0 m f) \<le> cmod(sumc 0 k f)"
@@ -148,14 +134,14 @@
***)
lemma sumr_cmod_ge_zero [iff]: "0 \<le> (\<Sum>n=m..<n::nat. cmod (f n))"
-by (induct "n", auto simp add: add_increasing)
+by (induct n) (auto simp add: add_increasing)
lemma rabs_sumc_cmod_cancel [simp]:
"abs (\<Sum>n=m..<n::nat. cmod (f n)) = (\<Sum>n=m..<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 "n")
+apply (induct n)
apply (case_tac [2] "n", auto)
done
@@ -164,7 +150,7 @@
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 "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"
@@ -174,4 +160,3 @@
done
end
-