--- a/src/HOL/Decision_Procs/Approximation.thy Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Oct 12 20:16:48 2011 +0200
@@ -31,12 +31,14 @@
lemma horner_schema: fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
assumes f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / (f (j' + j))) * x ^ j)"
-proof (induct n arbitrary: i k j')
+proof (induct n arbitrary: j')
+ case 0
+ then show ?case by auto
+next
case (Suc n)
-
show ?case unfolding horner.simps Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc]
using horner_schema'[of "\<lambda> j. 1 / (f (j' + j))"] by auto
-qed auto
+qed
lemma horner_bounds':
fixes lb :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" and ub :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float"
@@ -802,7 +804,7 @@
let "?f n" = "fact (2 * n)"
{ fix n
- have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
+ have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto
have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 1 * (((\<lambda>i. i + 2) ^^ n) 1 + 1)"
unfolding F by auto } note f_eq = this
@@ -914,7 +916,7 @@
let "?f n" = "fact (2 * n + 1)"
{ fix n
- have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
+ have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto
have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 2 * (((\<lambda>i. i + 2) ^^ n) 2 + 1)"
unfolding F by auto } note f_eq = this
@@ -2383,7 +2385,7 @@
and "Some (l, u) = approx prec arith vs" (is "_ = ?g arith")
shows "l \<le> interpret_floatarith arith xs \<and> interpret_floatarith arith xs \<le> u" (is "?P l u arith")
using `Some (l, u) = approx prec arith vs`
-proof (induct arith arbitrary: l u x)
+proof (induct arith arbitrary: l u)
case (Add a b)
from lift_bin'[OF Add.prems[unfolded approx.simps]] Add.hyps
obtain l1 u1 l2 u2 where "l = l1 + l2" and "u = u1 + u2"
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Wed Oct 12 20:16:48 2011 +0200
@@ -693,7 +693,7 @@
by (simp add: funpow_shift1)
lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
-by (induct p arbitrary: n0 rule: poly_cmul.induct, auto simp add: field_simps)
+ by (induct p rule: poly_cmul.induct) (auto simp add: field_simps)
lemma behead:
assumes np: "isnpolyh p n"
--- a/src/HOL/IMP/Compiler.thy Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy Wed Oct 12 20:16:48 2011 +0200
@@ -222,7 +222,7 @@
"0 \<le> n \<Longrightarrow>
bcomp b c n \<turnstile>
(0,s,stk) \<rightarrow>* (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
-proof(induction b arbitrary: c n m)
+proof(induction b arbitrary: c n)
case Not
from Not(1)[where c="~c"] Not(2) show ?case by fastforce
next
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Wed Oct 12 20:16:48 2011 +0200
@@ -408,7 +408,7 @@
by (induct xs arbitrary: i j, auto)
lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
-apply (induct xs arbitrary: a i j)
+apply (induct xs arbitrary: i j)
apply simp
apply (case_tac j)
apply simp
@@ -418,7 +418,7 @@
done
lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
-apply (induct xs arbitrary: a i j)
+apply (induct xs arbitrary: i j)
apply simp
apply simp
done
--- a/src/HOL/Library/Univ_Poly.thy Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Wed Oct 12 20:16:48 2011 +0200
@@ -118,13 +118,13 @@
qed
lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
-apply (induct a arbitrary: b c)
+apply (induct a)
apply (simp, clarify)
apply (case_tac b, simp_all add: add_ac)
done
lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)"
-apply (induct p arbitrary: q,simp)
+apply (induct p arbitrary: q, simp)
apply (case_tac q, simp_all add: right_distrib)
done
--- a/src/HOL/Nominal/Examples/Pattern.thy Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy Wed Oct 12 20:16:48 2011 +0200
@@ -653,7 +653,7 @@
shows "\<exists>pi::name prm. p = pi \<bullet> q \<and> t = pi \<bullet> u \<and>
set pi \<subseteq> (supp p \<union> supp q) \<times> (supp p \<union> supp q)"
using assms
-proof (induct p arbitrary: q t u \<Delta>)
+proof (induct p arbitrary: q t u)
case (PVar x T)
note PVar' = this
show ?case
--- a/src/HOL/Quotient_Examples/DList.thy Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/Quotient_Examples/DList.thy Wed Oct 12 20:16:48 2011 +0200
@@ -45,7 +45,7 @@
assumes "remdups xa = remdups ya"
shows "remdups (map f xa) = remdups (map f ya)"
using assms
- by (induct xa ya arbitrary: fx fy rule: list_induct2')
+ by (induct xa ya rule: list_induct2')
(metis (full_types) remdups_nil_noteq_cons(2) remdups_map_remdups)+
lemma remdups_eq_member_eq:
--- a/src/HOL/Quotient_Examples/FSet.thy Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Wed Oct 12 20:16:48 2011 +0200
@@ -1009,7 +1009,7 @@
lemma fset_raw_strong_cases:
obtains "xs = []"
| ys x where "\<not> List.member ys x" and "xs \<approx> x # ys"
-proof (induct xs arbitrary: x ys)
+proof (induct xs)
case Nil
then show thesis by simp
next