author wenzelm Wed Oct 12 20:16:48 2011 +0200 (2011-10-12) changeset 45129 1fce03e3e8ad parent 45128 5af3a3203a76 child 45130 563caf031b50
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
 src/HOL/Decision_Procs/Approximation.thy file | annotate | diff | revisions src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy file | annotate | diff | revisions src/HOL/IMP/Compiler.thy file | annotate | diff | revisions src/HOL/Imperative_HOL/ex/Sublist.thy file | annotate | diff | revisions src/HOL/Library/Univ_Poly.thy file | annotate | diff | revisions src/HOL/Nominal/Examples/Pattern.thy file | annotate | diff | revisions src/HOL/Quotient_Examples/DList.thy file | annotate | diff | revisions src/HOL/Quotient_Examples/FSet.thy file | annotate | diff | revisions
```     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.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.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.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.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
```