# HG changeset patch
# User haftmann
# Date 1387880654 -3600
# Node ID 356b4c0a2061de1f4fba51679dea15a036714575
# Parent  d700d054d02215d4c3aded010a334852032e856b
more general induction rule;
tuned proofs

diff -r d700d054d022 -r 356b4c0a2061 src/HOL/Library/Polynomial.thy
--- 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
+  by (fact ab_add_uminus_conv_diff)
 
 lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
   apply (induct p arbitrary: q, simp)