# HG changeset patch
# User wenzelm
# Date 1318443408 -7200
# Node ID 1fce03e3e8ad1cff74015579405229cda77dbd68
# Parent  5af3a3203a76c2879f81972b6ac8cddd69c0d0ad
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;

diff -r 5af3a3203a76 -r 1fce03e3e8ad src/HOL/Decision_Procs/Approximation.thy
--- 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"
diff -r 5af3a3203a76 -r 1fce03e3e8ad src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- 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"
diff -r 5af3a3203a76 -r 1fce03e3e8ad src/HOL/IMP/Compiler.thy
--- 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
diff -r 5af3a3203a76 -r 1fce03e3e8ad src/HOL/Imperative_HOL/ex/Sublist.thy
--- 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
diff -r 5af3a3203a76 -r 1fce03e3e8ad src/HOL/Library/Univ_Poly.thy
--- 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
 
diff -r 5af3a3203a76 -r 1fce03e3e8ad src/HOL/Nominal/Examples/Pattern.thy
--- 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
diff -r 5af3a3203a76 -r 1fce03e3e8ad src/HOL/Quotient_Examples/DList.thy
--- 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:
diff -r 5af3a3203a76 -r 1fce03e3e8ad src/HOL/Quotient_Examples/FSet.thy
--- 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