# HG changeset patch # User paulson # Date 1098202725 -7200 # Node ID bb6f072c8d10fe3376b6efc86cfc607a43a004bd # Parent 217bececa2bd12141362a3b80d7445c7bbbe43ab converted some induct_tac to induct diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Complex/CSeries.thy --- 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) \ 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)]: "(\r. m \ 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)]: "(\n. m \ Suc n --> f n = r) & m \ 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)]: "(\n. m \ n --> f n = r) & m \ 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 \ 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)]: "(\p. (m \ 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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Divides.thy --- 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 m mod n < (n::nat)" -apply (induct_tac "m" rule: nat_less_induct) +apply (induct "m" rule: nat_less_induct) apply (case_tac "na 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 (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)]: "\m::nat. m \ n --> (m div k) \ (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 "nn |] ==> (k div n) \ (k div m)" apply (subgoal_tac "0 (k-m) div n") +apply (subgoal_tac "(k-n) div n \ (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 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 \x. P x --> (\y. P y & ~ ((m y::nat) <= m x)) ==> \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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Hyperreal/EvenOdd.thy --- 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 Suc (k * m) mod k = 1" -apply (induct_tac "m") +apply (induct "m") apply (simp_all add: mod_Suc) done diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Hyperreal/HyperNat.thy --- 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: "\N::nat. {n. f n \ N} \ FreeUltrafilterNat ==> {n. N < f n} \ 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) diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Hyperreal/Integration.thy --- 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 \ n & n \ (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 \ 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 \ b ==> Integral(a,b) (%x. 1) (b - a)" apply (auto simp add: order_le_less rsum_def Integral_def) diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Hyperreal/Lim.thy --- 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)]: "(\n. (f::nat=>real) n \ f (Suc n)) --> f m \ f(m + no)" -apply (induct_tac "no") +apply (induct "no") apply (auto intro: order_trans) done @@ -1349,9 +1349,8 @@ "a \ 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 = diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Hyperreal/MacLaurin.thy --- 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: "\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 = (\m = 0.. 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: "\t. abs t \ abs x & diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Hyperreal/NSA.thy --- 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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Hyperreal/Poly.thy --- 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]: "\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]: "\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 "\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: "\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: "\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: "\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: "\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: "\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: "\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: "\h. \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: "\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: "\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]: "\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]: "\p x. poly p x \ poly [] x & length p = n --> (\i. \x. (poly p x = (0::real)) --> (\m. (m \ n & x = i m)))" -apply (induct_tac "n", safe) +apply (induct "n", safe) apply (rule ccontr) apply (subgoal_tac "\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 \ poly [] x ==> \N i. \x. (poly p x = 0) --> (\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)]: - "\P. (\x. P x --> (\n. (n::nat) < N & x = (j::nat=>real) n)) + "\P. (\x. P x --> (\n. n < N & x = (j::nat=>real) n)) --> (\a. \x. P x --> x < a)" -apply (induct_tac "N", simp, safe) -apply (drule_tac x = "%z. P z & (z \ (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 \ 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 \ poly []) = @@ -515,7 +510,7 @@ ==> poly (p *** q) \ 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]: "\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) \ 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 [] --> (\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]: "\p. length p = d --> poly p \ poly [] --> (\n q. p = mulexp n [-a, 1] q & poly q a \ 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]: "\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) \ 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 "\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 = "\r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q) " in thin_rl) +apply (erule_tac V = "\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) \ k ==> abs(poly p x) \ 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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Hyperreal/SEQ.thy --- 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 \ (u::nat) & real(Suc n) < \X(f n)\}" -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) < \X 0\ }" 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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Hyperreal/Series.thy --- 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)]: - "(\n. m \ Suc n --> f n = r) --> m \ 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: + "\\n. m \ Suc n --> f n = r; m \ 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_interval_const2 [rule_format (no_asm)]: - "(\n. m \ n --> f n = r) --> m \ 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: + "[|\n. m \ n --> f n = r; m \ 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)]: - "(\n. m \ n --> 0 \ f n) --> m < k --> sumr 0 m f \ sumr 0 k f" -apply (induct_tac "k") +lemma sumr_le: + "[|\n. m \ n --> 0 \ f n; m < k|] ==> sumr 0 m f \ 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)]: "(\r. m \ r & r < n --> f r \ g r) --> sumr m n f \ 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]: "(\n. m \ n --> 0 \ f n) --> 0 \ sumr m n f" -apply (induct_tac "n", auto) +lemma sumr_ge_zero: "(\n. m \ n --> 0 \ f n) --> 0 \ 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]: "\n. N \ n --> f n = 0 ==> N \ m --> sumr m n f = 0" -by (induct_tac "n", auto) +by (induct "n", auto) lemma Suc_le_imp_diff_ge2: "[|\n. N \ n --> f (Suc n) = 0; Suc N \ 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)]: "(\p. m \ 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)]: "(\p. m \ p & p < m + n --> (f(p) \ K)) --> (sumr m (m + n) f \ (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)]: "(\p. 0 \ p & p < n --> (f(p) \ K)) --> (sumr 0 n f \ (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: "[|\d. - f (n + (d + d)) < f (Suc (n + (d + d)))|] ==> sumr 0 (n + Suc (Suc 0)) f \ 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)]: "(\r. m \ 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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Hyperreal/Transcendental.thy --- 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 \ 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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Integ/IntDef.thy --- 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 0 int k * i < int k * j" -apply (induct_tac "k", simp) +lemma zmult_zless_mono2_lemma: + "i 0 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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Integ/IntDiv.thy --- 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 \ (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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Integ/NatBin.thy --- 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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Integ/Parity.thy --- 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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/List.thy --- 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 = (\i j. i < size xs \ j < size xs \ i \ j --> xs!i \ 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 \ length ys = n \ (\xys x y xs' ys'. xs= xys @ x#xs' \ ys= xys @ y # ys' \ (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) diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Map.thy --- 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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Nat.thy --- 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)" diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Power.thy --- a/src/HOL/Power.thy Mon Oct 18 13:40:45 2004 +0200 +++ b/src/HOL/Power.thy Tue Oct 19 18:18:45 2004 +0200 @@ -22,10 +22,10 @@ text{*It looks plausible as a simprule, but its effect can be strange.*} lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::recpower))" -by (induct_tac "n", auto) +by (induct "n", auto) lemma power_one [simp]: "1^n = (1::'a::recpower)" -apply (induct_tac "n") +apply (induct "n") apply (auto simp add: power_Suc) done @@ -33,23 +33,23 @@ by (simp add: power_Suc) lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)" -apply (induct_tac "n") +apply (induct "n") apply (simp_all add: power_Suc mult_ac) done lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n" -apply (induct_tac "n") +apply (induct "n") apply (simp_all add: power_Suc power_add) done lemma power_mult_distrib: "((a::'a::recpower) * b) ^ n = (a^n) * (b^n)" -apply (induct_tac "n") +apply (induct "n") apply (auto simp add: power_Suc mult_ac) done lemma zero_less_power: "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n" -apply (induct_tac "n") +apply (induct "n") apply (simp_all add: power_Suc zero_less_one mult_pos) done @@ -62,7 +62,7 @@ lemma one_le_power: "1 \ (a::'a::{ordered_semidom,recpower}) ==> 1 \ 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 \ b; (0::'a::{recpower,ordered_semidom}) \ a|] ==> a^n \ 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}) \ 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 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}) \ (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 \ 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 le_Suc_eq) apply (rename_tac m) apply (subgoal_tac "a * a^m \ 1 * a^n", simp) @@ -245,7 +245,7 @@ lemma power_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_Suc le_Suc_eq) apply (rename_tac m) apply (subgoal_tac "1 * a^n \ 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 \ (0::nat) | n=0)" -by (induct_tac "n", auto) +by (induct "n", auto) lemma power_le_dvd [rule_format]: "k^j dvd n --> i\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]: "\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 \ 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]: "\k. k \ 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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/Real/RealPow.thy --- 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 \ (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) \ (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 diff -r 217bececa2bd -r bb6f072c8d10 src/HOL/SetInterval.thy --- 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 {..