author haftmann Tue Dec 24 11:24:14 2013 +0100 (2013-12-24) changeset 54856 356b4c0a2061 parent 54855 d700d054d022 child 54857 5c05f7c5f8ae
more general induction rule;
tuned proofs
```     1.1 --- a/src/HOL/Library/Polynomial.thy	Mon Dec 23 20:45:33 2013 +0100
1.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Dec 24 11:24:14 2013 +0100
1.3 @@ -327,7 +327,7 @@
1.4
1.5  lemma pCons_induct [case_names 0 pCons, induct type: poly]:
1.6    assumes zero: "P 0"
1.7 -  assumes pCons: "\<And>a p. P p \<Longrightarrow> P (pCons a p)"
1.8 +  assumes pCons: "\<And>a p. a \<noteq> 0 \<or> p \<noteq> 0 \<Longrightarrow> P p \<Longrightarrow> P (pCons a p)"
1.9    shows "P p"
1.10  proof (induct p rule: measure_induct_rule [where f=degree])
1.11    case (less p)
1.12 @@ -345,8 +345,14 @@
1.13      then show "P q"
1.14        by (rule less.hyps)
1.15    qed
1.16 -  then have "P (pCons a q)"
1.17 -    by (rule pCons)
1.18 +  have "P (pCons a q)"
1.19 +  proof (cases "a \<noteq> 0 \<or> q \<noteq> 0")
1.20 +    case True
1.21 +    with `P q` show ?thesis by (auto intro: pCons)
1.22 +  next
1.23 +    case False
1.24 +    with zero show ?thesis by simp
1.25 +  qed
1.26    then show ?case
1.27      using `p = pCons a q` by simp
1.28  qed
1.29 @@ -412,7 +418,7 @@
1.30
1.31  lemma Poly_coeffs [simp, code abstype]:
1.32    "Poly (coeffs p) = p"
1.33 -  by (induct p) (simp_all add: cCons_def)
1.34 +  by (induct p) auto
1.35
1.36  lemma coeffs_Poly [simp]:
1.37    "coeffs (Poly as) = strip_while (HOL.eq 0) as"
1.38 @@ -778,7 +784,7 @@
1.39  lemma [code]:
1.40    fixes p q :: "'a::ab_group_add poly"
1.41    shows "p - q = p + - q"
1.42 -  by simp