tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
authorwenzelm
Wed Oct 12 20:16:48 2011 +0200 (2011-10-12 ago)
changeset 451291fce03e3e8ad
parent 45128 5af3a3203a76
child 45130 563caf031b50
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/IMP/Compiler.thy
src/HOL/Imperative_HOL/ex/Sublist.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Nominal/Examples/Pattern.thy
src/HOL/Quotient_Examples/DList.thy
src/HOL/Quotient_Examples/FSet.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Oct 12 16:21:07 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Oct 12 20:16:48 2011 +0200
     1.3 @@ -31,12 +31,14 @@
     1.4  lemma horner_schema: fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
     1.5    assumes f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
     1.6    shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / (f (j' + j))) * x ^ j)"
     1.7 -proof (induct n arbitrary: i k j')
     1.8 +proof (induct n arbitrary: j')
     1.9 +  case 0
    1.10 +  then show ?case by auto
    1.11 +next
    1.12    case (Suc n)
    1.13 -
    1.14    show ?case unfolding horner.simps Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc]
    1.15      using horner_schema'[of "\<lambda> j. 1 / (f (j' + j))"] by auto
    1.16 -qed auto
    1.17 +qed
    1.18  
    1.19  lemma horner_bounds':
    1.20    fixes lb :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" and ub :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float"
    1.21 @@ -802,7 +804,7 @@
    1.22    let "?f n" = "fact (2 * n)"
    1.23  
    1.24    { fix n
    1.25 -    have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
    1.26 +    have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto
    1.27      have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 1 * (((\<lambda>i. i + 2) ^^ n) 1 + 1)"
    1.28        unfolding F by auto } note f_eq = this
    1.29  
    1.30 @@ -914,7 +916,7 @@
    1.31    let "?f n" = "fact (2 * n + 1)"
    1.32  
    1.33    { fix n
    1.34 -    have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
    1.35 +    have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto
    1.36      have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 2 * (((\<lambda>i. i + 2) ^^ n) 2 + 1)"
    1.37        unfolding F by auto } note f_eq = this
    1.38  
    1.39 @@ -2383,7 +2385,7 @@
    1.40    and "Some (l, u) = approx prec arith vs" (is "_ = ?g arith")
    1.41    shows "l \<le> interpret_floatarith arith xs \<and> interpret_floatarith arith xs \<le> u" (is "?P l u arith")
    1.42    using `Some (l, u) = approx prec arith vs`
    1.43 -proof (induct arith arbitrary: l u x)
    1.44 +proof (induct arith arbitrary: l u)
    1.45    case (Add a b)
    1.46    from lift_bin'[OF Add.prems[unfolded approx.simps]] Add.hyps
    1.47    obtain l1 u1 l2 u2 where "l = l1 + l2" and "u = u1 + u2"
     2.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Oct 12 16:21:07 2011 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Oct 12 20:16:48 2011 +0200
     2.3 @@ -693,7 +693,7 @@
     2.4    by (simp add: funpow_shift1)
     2.5  
     2.6  lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
     2.7 -by (induct p  arbitrary: n0 rule: poly_cmul.induct, auto simp add: field_simps)
     2.8 +  by (induct p rule: poly_cmul.induct) (auto simp add: field_simps)
     2.9  
    2.10  lemma behead:
    2.11    assumes np: "isnpolyh p n"
     3.1 --- a/src/HOL/IMP/Compiler.thy	Wed Oct 12 16:21:07 2011 +0200
     3.2 +++ b/src/HOL/IMP/Compiler.thy	Wed Oct 12 20:16:48 2011 +0200
     3.3 @@ -222,7 +222,7 @@
     3.4    "0 \<le> n \<Longrightarrow>
     3.5    bcomp b c n \<turnstile>
     3.6   (0,s,stk)  \<rightarrow>*  (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
     3.7 -proof(induction b arbitrary: c n m)
     3.8 +proof(induction b arbitrary: c n)
     3.9    case Not
    3.10    from Not(1)[where c="~c"] Not(2) show ?case by fastforce
    3.11  next
     4.1 --- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Wed Oct 12 16:21:07 2011 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Wed Oct 12 20:16:48 2011 +0200
     4.3 @@ -408,7 +408,7 @@
     4.4  by (induct xs arbitrary: i j, auto)
     4.5  
     4.6  lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
     4.7 -apply (induct xs arbitrary: a i j)
     4.8 +apply (induct xs arbitrary: i j)
     4.9  apply simp
    4.10  apply (case_tac j)
    4.11  apply simp
    4.12 @@ -418,7 +418,7 @@
    4.13  done
    4.14  
    4.15  lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
    4.16 -apply (induct xs arbitrary: a i j)
    4.17 +apply (induct xs arbitrary: i j)
    4.18  apply simp
    4.19  apply simp
    4.20  done
     5.1 --- a/src/HOL/Library/Univ_Poly.thy	Wed Oct 12 16:21:07 2011 +0200
     5.2 +++ b/src/HOL/Library/Univ_Poly.thy	Wed Oct 12 20:16:48 2011 +0200
     5.3 @@ -118,13 +118,13 @@
     5.4  qed
     5.5  
     5.6  lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
     5.7 -apply (induct a arbitrary: b c)
     5.8 +apply (induct a)
     5.9  apply (simp, clarify)
    5.10  apply (case_tac b, simp_all add: add_ac)
    5.11  done
    5.12  
    5.13  lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)"
    5.14 -apply (induct p arbitrary: q,simp)
    5.15 +apply (induct p arbitrary: q, simp)
    5.16  apply (case_tac q, simp_all add: right_distrib)
    5.17  done
    5.18  
     6.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Wed Oct 12 16:21:07 2011 +0200
     6.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Wed Oct 12 20:16:48 2011 +0200
     6.3 @@ -653,7 +653,7 @@
     6.4    shows "\<exists>pi::name prm. p = pi \<bullet> q \<and> t = pi \<bullet> u \<and>
     6.5      set pi \<subseteq> (supp p \<union> supp q) \<times> (supp p \<union> supp q)"
     6.6    using assms
     6.7 -proof (induct p arbitrary: q t u \<Delta>)
     6.8 +proof (induct p arbitrary: q t u)
     6.9    case (PVar x T)
    6.10    note PVar' = this
    6.11    show ?case
     7.1 --- a/src/HOL/Quotient_Examples/DList.thy	Wed Oct 12 16:21:07 2011 +0200
     7.2 +++ b/src/HOL/Quotient_Examples/DList.thy	Wed Oct 12 20:16:48 2011 +0200
     7.3 @@ -45,7 +45,7 @@
     7.4    assumes "remdups xa = remdups ya"
     7.5      shows "remdups (map f xa) = remdups (map f ya)"
     7.6    using assms
     7.7 -  by (induct xa ya arbitrary: fx fy rule: list_induct2')
     7.8 +  by (induct xa ya rule: list_induct2')
     7.9       (metis (full_types) remdups_nil_noteq_cons(2) remdups_map_remdups)+
    7.10  
    7.11  lemma remdups_eq_member_eq:
     8.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Wed Oct 12 16:21:07 2011 +0200
     8.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Wed Oct 12 20:16:48 2011 +0200
     8.3 @@ -1009,7 +1009,7 @@
     8.4  lemma fset_raw_strong_cases:
     8.5    obtains "xs = []"
     8.6      | ys x where "\<not> List.member ys x" and "xs \<approx> x # ys"
     8.7 -proof (induct xs arbitrary: x ys)
     8.8 +proof (induct xs)
     8.9    case Nil
    8.10    then show thesis by simp
    8.11  next