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.41                      qed (simp_all add: deg_f_nzero)
    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