# HG changeset patch
# User ballarin
# Date 1280780659 -7200
# Node ID df8fc03995a40b9456ce5812a4d0aa2150df9f3e
# Parent  faa18bf13b9b4274654430d02f2f38b1b83ea575
Revised proof of long division contributed by Jesus Aransay.

diff -r faa18bf13b9b -r df8fc03995a4 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Sun Aug 01 18:57:49 2010 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Mon Aug 02 22:24:19 2010 +0200
@@ -1557,128 +1557,93 @@
   assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
   and g_not_zero: "g \<noteq> \<zero>\<^bsub>P\<^esub>"
   shows "\<exists> q r (k::nat). (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> (lcoeff g)(^)\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g)"
-proof -
+  using f_in_P
+proof (induct "deg R f" arbitrary: "f" rule: nat_less_induct)
+  case (1 f)
+  note f_in_P [simp] = "1.prems"
   let ?pred = "(\<lambda> q r (k::nat).
-    (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> (lcoeff g)(^)\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g))"
-    and ?lg = "lcoeff g"
-  show ?thesis
-    (*JE: we distinguish some particular cases where the solution is almost direct.*)
+    (q \<in> carrier P) \<and> (r \<in> carrier P) 
+    \<and> (lcoeff g)(^)\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g))"
+  let ?lg = "lcoeff g" and ?lf = "lcoeff f"
+  show ?case
   proof (cases "deg R f < deg R g")
-    case True     
-      (*JE: if the degree of f is smaller than the one of g the solution is straightforward.*)
-      (* CB: avoid exI3 *)
-      have "?pred \<zero>\<^bsub>P\<^esub> f 0" using True by force
-      then show ?thesis by fast
+    case True
+    have "?pred \<zero>\<^bsub>P\<^esub> f 0" using True by force
+    then show ?thesis by blast
   next
     case False then have deg_g_le_deg_f: "deg R g \<le> deg R f" by simp
     {
-      (*JE: we now apply the induction hypothesis with some additional facts required*)
-      from f_in_P deg_g_le_deg_f show ?thesis
-      proof (induct "deg R f" arbitrary: "f" rule: less_induct)
-        case less
-        note f_in_P [simp] = `f \<in> carrier P`
-          and deg_g_le_deg_f = `deg R g \<le> deg R f`
-        let ?k = "1::nat" and ?r = "(g \<otimes>\<^bsub>P\<^esub> (monom P (lcoeff f) (deg R f - deg R g))) \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)"
-          and ?q = "monom P (lcoeff f) (deg R f - deg R g)"
-        show "\<exists> q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and> lcoeff g (^) k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r & (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g)"
-        proof -
-          (*JE: we first extablish the existence of a triple satisfying the previous equation. 
-            Then we will have to prove the second part of the predicate.*)
-          have exist: "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r"
-            using minus_add
-            using sym [OF a_assoc [of "g \<otimes>\<^bsub>P\<^esub> ?q" "\<ominus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "lcoeff g \<odot>\<^bsub>P\<^esub> f"]]
-            using r_neg by auto
+      let ?k = "1::nat"
+      let ?f1 = "(g \<otimes>\<^bsub>P\<^esub> (monom P (?lf) (deg R f - deg R g))) \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)"
+      let ?q = "monom P (?lf) (deg R f - deg R g)"
+      have f1_in_carrier: "?f1 \<in> carrier P" and q_in_carrier: "?q \<in> carrier P" by simp_all
+      show ?thesis
+      proof (cases "deg R f = 0")
+        case True
+        {
+          have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
+          have "?pred f \<zero>\<^bsub>P\<^esub> 1"
+            using deg_zero_impl_monom [OF g_in_P deg_g]
+            using sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
+            using deg_g by simp
+          then show ?thesis by blast
+        }
+      next
+        case False note deg_f_nzero = False
+        {
+          have exist: "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1"
+            by (simp add: minus_add r_neg sym [
+              OF a_assoc [of "g \<otimes>\<^bsub>P\<^esub> ?q" "\<ominus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "lcoeff g \<odot>\<^bsub>P\<^esub> f"]])
+          have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?f1) < deg R f"
+          proof (unfold deg_uminus [OF f1_in_carrier])
+            show "deg R ?f1 < deg R f"
+            proof (rule deg_lcoeff_cancel)
+              show "deg R (\<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
+                using deg_smult_ring [of ?lg f]
+                using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
+              show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
+                by (simp add: monom_deg_mult [OF f_in_P g_in_P deg_g_le_deg_f, of ?lf])
+              show "coeff P (g \<otimes>\<^bsub>P\<^esub> ?q) (deg R f) = \<ominus> coeff P (\<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)) (deg R f)"
+                unfolding coeff_mult [OF g_in_P monom_closed 
+                  [OF lcoeff_closed [OF f_in_P], 
+                    of "deg R f - deg R g"], of "deg R f"]
+                unfolding coeff_monom [OF lcoeff_closed 
+                  [OF f_in_P], of "(deg R f - deg R g)"]
+                using R.finsum_cong' [of "{..deg R f}" "{..deg R f}" 
+                  "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then ?lf else \<zero>))" 
+                  "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> ?lf else \<zero>)"]
+                using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> ?lf)"]
+                unfolding Pi_def using deg_g_le_deg_f by force
+            qed (simp_all add: deg_f_nzero)
+          qed
+          then obtain q' r' k'
+            where rem_desc: "?lg (^) (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?f1) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
+            and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
+            and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
+            using "1.hyps" using f1_in_carrier by blast
           show ?thesis
-          proof (cases "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R g")
-            (*JE: if the degree of the remainder satisfies the statement property we are done*)
-            case True
-            {
-              show ?thesis
-              proof (rule exI3 [of _ ?q "\<ominus>\<^bsub>P\<^esub> ?r" ?k], intro conjI)
-                show "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r" using exist by simp
-                show "\<ominus>\<^bsub>P\<^esub> ?r = \<zero>\<^bsub>P\<^esub> \<or> deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R g" using True by simp
-              qed (simp_all)
-            }
-          next
-            case False note n_deg_r_l_deg_g = False
-            {
-              (*JE: otherwise, we verify the conditions of the induction hypothesis.*)
-              show ?thesis
-              proof (cases "deg R f = 0")
-                (*JE: the solutions are different if the degree of f is zero or not*)
-                case True
-                {
-                  have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
-                  have "lcoeff g (^) (1::nat) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> f \<oplus>\<^bsub>P\<^esub> \<zero>\<^bsub>P\<^esub>"
-                    unfolding deg_g apply simp
-                    unfolding sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
-                    using deg_zero_impl_monom [OF g_in_P deg_g] by simp
-                  then show ?thesis using f_in_P by blast
-                }
-              next
-                case False note deg_f_nzero = False
-                {
-                  (*JE: now it only remains the case where the induction hypothesis can be used.*)
-                  (*JE: we first prove that the degree of the remainder is smaller than the one of f*)
-                  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f"
-                  proof -
-                    have "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp
-                    also have "\<dots> < deg R f"
-                    proof (rule deg_lcoeff_cancel)
-                      show "deg R (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
-                        using deg_smult_ring [of "lcoeff g" f]
-                        using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
-                      show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
-                        using monom_deg_mult [OF _ g_in_P, of f "lcoeff f"] and deg_g_le_deg_f
-                        by simp
-                      show "coeff P (g \<otimes>\<^bsub>P\<^esub> ?q) (deg R f) = \<ominus> coeff P (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) (deg R f)"
-                        unfolding coeff_mult [OF g_in_P monom_closed [OF lcoeff_closed [OF f_in_P], of "deg R f - deg R g"], of "deg R f"]
-                        unfolding coeff_monom [OF lcoeff_closed [OF f_in_P], of "(deg R f - deg R g)"]
-                        using R.finsum_cong' [of "{..deg R f}" "{..deg R f}" 
-                          "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then lcoeff f else \<zero>))" 
-                          "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> lcoeff f else \<zero>)"]
-                        using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> lcoeff f)"]
-                        unfolding Pi_def using deg_g_le_deg_f by force
-                    qed (simp_all add: deg_f_nzero)
-                    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f" .
-                  qed
-                  moreover have "\<ominus>\<^bsub>P\<^esub> ?r \<in> carrier P" by simp
-                  moreover obtain m where deg_rem_eq_m: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = m" by auto
-                  moreover have "deg R g \<le> deg R (\<ominus>\<^bsub>P\<^esub> ?r)" using n_deg_r_l_deg_g by simp
-                    (*JE: now, by applying the induction hypothesis, we obtain new quotient, remainder and exponent.*)
-                  ultimately obtain q' r' k'
-                    where rem_desc: "lcoeff g (^) (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?r) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
-                    and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
-                    using less by blast
-                      (*JE: we now prove that the new quotient, remainder and exponent can be used to get 
-                      the quotient, remainder and exponent of the long division theorem*)
-                  show ?thesis
-                  proof (rule exI3 [of _ "((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
-                    show "(lcoeff g (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<oplus>\<^bsub>P\<^esub> r'"
-                    proof -
-                      have "(lcoeff g (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r)" 
-                        using smult_assoc1 exist by simp
-                      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ( \<ominus>\<^bsub>P\<^esub> ?r))"
-                        using UP_smult_r_distr by simp
-                      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r')"
-                        using rem_desc by simp
-                      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
-                        using sym [OF a_assoc [of "lcoeff g (^) k' \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "g \<otimes>\<^bsub>P\<^esub> q'" "r'"]]
-                        using q'_in_carrier r'_in_carrier by simp
-                      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (?q \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
-                        using q'_in_carrier by (auto simp add: m_comm)
-                      also have "\<dots> = (((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q) \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'" 
-                        using smult_assoc2 q'_in_carrier by auto
-                      also have "\<dots> = ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
-                        using sym [OF l_distr] and q'_in_carrier by auto
-                      finally show ?thesis using m_comm q'_in_carrier by auto
-                    qed
-                  qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
-                }
-              qed
-            }
-          qed
-        qed
+          proof (rule exI3 [of _ "((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
+            show "(?lg (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<oplus>\<^bsub>P\<^esub> r'"
+            proof -
+              have "(?lg (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1)"
+                using smult_assoc1 [OF _ _ f_in_P] using exist by simp
+              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ( \<ominus>\<^bsub>P\<^esub> ?f1))"
+                using UP_smult_r_distr by simp
+              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r')"
+                unfolding rem_desc ..
+              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
+                using sym [OF a_assoc [of "?lg (^) k' \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "g \<otimes>\<^bsub>P\<^esub> q'" "r'"]]
+                using r'_in_carrier q'_in_carrier by simp
+              also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (?q \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
+                using q'_in_carrier by (auto simp add: m_comm)
+              also have "\<dots> = (((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q) \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'" 
+                using smult_assoc2 q'_in_carrier "1.prems" by auto
+              also have "\<dots> = ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
+                using sym [OF l_distr] and q'_in_carrier by auto
+              finally show ?thesis using m_comm q'_in_carrier by auto
+            qed
+          qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
+        }
       qed
     }
   qed