src/HOL/Algebra/UnivPoly.thy
 changeset 34915 7894c7dab132 parent 33657 a4179bf442d1 child 35848 5443079512ea child 36092 8f1e60d9f7cc
```     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sun Jan 10 18:41:07 2010 +0100
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sun Jan 10 18:43:45 2010 +0100
1.3 @@ -1581,14 +1581,10 @@
1.4      {
1.5        (*JE: we now apply the induction hypothesis with some additional facts required*)
1.6        from f_in_P deg_g_le_deg_f show ?thesis
1.7 -      proof (induct n \<equiv> "deg R f" arbitrary: "f" rule: nat_less_induct)
1.8 -        fix n f
1.9 -        assume hypo: "\<forall>m<n. \<forall>x. x \<in> carrier P \<longrightarrow>
1.10 -          deg R g \<le> deg R x \<longrightarrow>
1.11 -          m = deg R x \<longrightarrow>
1.12 -          (\<exists>q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and> lcoeff g (^) k \<odot>\<^bsub>P\<^esub> x = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r & (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g))"
1.13 -          and prem: "n = deg R f" and f_in_P [simp]: "f \<in> carrier P"
1.14 -          and deg_g_le_deg_f: "deg R g \<le> deg R f"
1.15 +      proof (induct "deg R f" arbitrary: "f" rule: less_induct)
1.16 +        case less
1.17 +        note f_in_P [simp] = `f \<in> carrier P`
1.18 +          and deg_g_le_deg_f = `deg R g \<le> deg R f`
1.19          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)"
1.20            and ?q = "monom P (lcoeff f) (deg R f - deg R g)"
1.21          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)"
1.22 @@ -1631,13 +1627,13 @@
1.23                  {
1.24                    (*JE: now it only remains the case where the induction hypothesis can be used.*)
1.25                    (*JE: we first prove that the degree of the remainder is smaller than the one of f*)
1.26 -                  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n"
1.27 +                  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f"
1.28                    proof -
1.29                      have "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp
1.30                      also have "\<dots> < deg R f"
1.31                      proof (rule deg_lcoeff_cancel)
1.32                        show "deg R (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
1.33 -                        using deg_smult_ring [of "lcoeff g" f] using prem
1.34 +                        using deg_smult_ring [of "lcoeff g" f]
1.35                          using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
1.36                        show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
1.37                          using monom_deg_mult [OF _ g_in_P, of f "lcoeff f"] and deg_g_le_deg_f
1.38 @@ -1651,7 +1647,7 @@
1.39                          using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> lcoeff f)"]
1.40                          unfolding Pi_def using deg_g_le_deg_f by force
1.42 -                    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n" unfolding prem .
1.43 +                    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f" .
1.44                    qed
1.45                    moreover have "\<ominus>\<^bsub>P\<^esub> ?r \<in> carrier P" by simp
1.46                    moreover obtain m where deg_rem_eq_m: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = m" by auto
1.47 @@ -1660,7 +1656,7 @@
1.48                    ultimately obtain q' r' k'
1.49                      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)"
1.50                      and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
1.51 -                    using hypo by blast
1.52 +                    using less by blast
1.53                        (*JE: we now prove that the new quotient, remainder and exponent can be used to get
1.54                        the quotient, remainder and exponent of the long division theorem*)
1.55                    show ?thesis
```