# HG changeset patch
# User haftmann
# Date 1379175852 -7200
# Node ID 9b5735de1f1a907d45a256afbc2a032d9a87c30a
# Parent  b6fb9151de66805d69c6c35d80ba9953fc4aa7da
tuned proof

diff -r b6fb9151de66 -r 9b5735de1f1a src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Sat Sep 14 14:01:48 2013 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Sat Sep 14 18:24:12 2013 +0200
@@ -71,6 +71,15 @@
 definition (in semiring_0) divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "divides" 70)
   where "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
 
+lemma (in semiring_0) dividesI:
+  "poly p2 = poly (p1 *** q) \<Longrightarrow> p1 divides p2"
+  by (auto simp add: divides_def)
+
+lemma (in semiring_0) dividesE:
+  assumes "p1 divides p2"
+  obtains q where "poly p2 = poly (p1 *** q)"
+  using assms by (auto simp add: divides_def)
+
     --{*order of a polynomial*}
 definition (in ring_1) order :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
   "order a p = (SOME n. ([-a, 1] %^ n) divides p \<and> ~ (([-a, 1] %^ (Suc n)) divides p))"
@@ -620,27 +629,39 @@
 
 lemma (in idom_char_0) poly_order_exists:
   assumes "length p = d" and "poly p \<noteq> poly []"
-  shows "\<exists>n. ([-a, 1] %^ n) divides p \<and> ~(([-a, 1] %^ (Suc n)) divides p)"
-  using assms
-  apply -
-  apply (drule poly_order_exists_lemma [where a=a], assumption, clarify)
-  apply (rule_tac x = n in exI, safe)
-  apply (unfold divides_def)
-  apply (rule_tac x = q in exI)
-  apply (induct_tac n, simp)
-  apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult distrib_left mult_ac)
-  apply safe
-  apply (subgoal_tac "poly (mulexp n [uminus a, one] q) \<noteq>
-    poly (pmult (pexp [uminus a, one] (Suc n)) qa)")
-  apply simp
-  apply (induct_tac n)
-  apply (simp del: pmult_Cons pexp_Suc)
-  apply (erule_tac Q = "poly q a = zero" in contrapos_np)
-  apply (simp add: poly_add poly_cmult)
-  apply (rule pexp_Suc [THEN ssubst])
-  apply (rule ccontr)
-  apply (simp add: poly_mult_left_cancel poly_mult_assoc del: pmult_Cons pexp_Suc)
-  done
+  shows "\<exists>n. [- a, 1] %^ n divides p \<and> \<not> [- a, 1] %^ Suc n divides p"
+proof -
+  from assms have "\<exists>n q. p = mulexp n [- a, 1] q \<and> poly q a \<noteq> 0"
+    by (rule poly_order_exists_lemma)
+  then obtain n q where p: "p = mulexp n [- a, 1] q" and "poly q a \<noteq> 0" by blast
+  have "[- a, 1] %^ n divides mulexp n [- a, 1] q"
+  proof (rule dividesI)
+    show "poly (mulexp n [- a, 1] q) = poly ([- a, 1] %^ n *** q)"
+      by (induct n) (simp_all add: poly_add poly_cmult poly_mult distrib_left mult_ac)
+  qed
+  moreover have "\<not> [- a, 1] %^ Suc n divides mulexp n [- a, 1] q"
+  proof
+    assume "[- a, 1] %^ Suc n divides mulexp n [- a, 1] q"
+    then obtain m where "poly (mulexp n [- a, 1] q) = poly ([- a, 1] %^ Suc n *** m)"
+      by (rule dividesE)
+    moreover have "poly (mulexp n [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc n *** m)"
+    proof (induct n)
+      case 0 show ?case
+      proof (rule ccontr)
+        assume "\<not> poly (mulexp 0 [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc 0 *** m)"
+        then have "poly q a = 0"
+          by (simp add: poly_add poly_cmult)
+        with `poly q a \<noteq> 0` show False by simp
+      qed
+    next
+      case (Suc n) show ?case
+        by (rule pexp_Suc [THEN ssubst], rule ccontr)
+          (simp add: poly_mult_left_cancel poly_mult_assoc Suc del: pmult_Cons pexp_Suc)
+    qed
+    ultimately show False by simp
+  qed
+  ultimately show ?thesis by (auto simp add: p)
+qed
 
 lemma (in semiring_1) poly_one_divides[simp]: "[1] divides p"
   by (auto simp add: divides_def)