author haftmann Tue, 24 Dec 2013 11:24:14 +0100 changeset 54856 356b4c0a2061 parent 54855 d700d054d022 child 54857 5c05f7c5f8ae
more general induction rule; tuned proofs
```--- a/src/HOL/Library/Polynomial.thy	Mon Dec 23 20:45:33 2013 +0100
+++ b/src/HOL/Library/Polynomial.thy	Tue Dec 24 11:24:14 2013 +0100
@@ -327,7 +327,7 @@

lemma pCons_induct [case_names 0 pCons, induct type: poly]:
assumes zero: "P 0"
-  assumes pCons: "\<And>a p. P p \<Longrightarrow> P (pCons a p)"
+  assumes pCons: "\<And>a p. a \<noteq> 0 \<or> p \<noteq> 0 \<Longrightarrow> P p \<Longrightarrow> P (pCons a p)"
shows "P p"
proof (induct p rule: measure_induct_rule [where f=degree])
case (less p)
@@ -345,8 +345,14 @@
then show "P q"
by (rule less.hyps)
qed
-  then have "P (pCons a q)"
-    by (rule pCons)
+  have "P (pCons a q)"
+  proof (cases "a \<noteq> 0 \<or> q \<noteq> 0")
+    case True
+    with `P q` show ?thesis by (auto intro: pCons)
+  next
+    case False
+    with zero show ?thesis by simp
+  qed
then show ?case
using `p = pCons a q` by simp
qed
@@ -412,7 +418,7 @@

lemma Poly_coeffs [simp, code abstype]:
"Poly (coeffs p) = p"
-  by (induct p) (simp_all add: cCons_def)
+  by (induct p) auto

lemma coeffs_Poly [simp]:
"coeffs (Poly as) = strip_while (HOL.eq 0) as"
@@ -778,7 +784,7 @@
lemma [code]:
fixes p q :: "'a::ab_group_add poly"
shows "p - q = p + - q"
-  by simp