author ballarin Mon Aug 02 22:24:19 2010 +0200 (2010-08-02) changeset 38131 df8fc03995a4 parent 38130 faa18bf13b9b child 38132 d9955b3b06fe
Revised proof of long division contributed by Jesus Aransay.
```     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sun Aug 01 18:57:49 2010 +0200
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Mon Aug 02 22:24:19 2010 +0200
1.3 @@ -1557,128 +1557,93 @@
1.4    assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
1.5    and g_not_zero: "g \<noteq> \<zero>\<^bsub>P\<^esub>"
1.6    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)"
1.7 -proof -
1.8 +  using f_in_P
1.9 +proof (induct "deg R f" arbitrary: "f" rule: nat_less_induct)
1.10 +  case (1 f)
1.11 +  note f_in_P [simp] = "1.prems"
1.12    let ?pred = "(\<lambda> q r (k::nat).
1.13 -    (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))"
1.14 -    and ?lg = "lcoeff g"
1.15 -  show ?thesis
1.16 -    (*JE: we distinguish some particular cases where the solution is almost direct.*)
1.17 +    (q \<in> carrier P) \<and> (r \<in> carrier P)
1.18 +    \<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))"
1.19 +  let ?lg = "lcoeff g" and ?lf = "lcoeff f"
1.20 +  show ?case
1.21    proof (cases "deg R f < deg R g")
1.22 -    case True
1.23 -      (*JE: if the degree of f is smaller than the one of g the solution is straightforward.*)
1.24 -      (* CB: avoid exI3 *)
1.25 -      have "?pred \<zero>\<^bsub>P\<^esub> f 0" using True by force
1.26 -      then show ?thesis by fast
1.27 +    case True
1.28 +    have "?pred \<zero>\<^bsub>P\<^esub> f 0" using True by force
1.29 +    then show ?thesis by blast
1.30    next
1.31      case False then have deg_g_le_deg_f: "deg R g \<le> deg R f" by simp
1.32      {
1.33 -      (*JE: we now apply the induction hypothesis with some additional facts required*)
1.34 -      from f_in_P deg_g_le_deg_f show ?thesis
1.35 -      proof (induct "deg R f" arbitrary: "f" rule: less_induct)
1.36 -        case less
1.37 -        note f_in_P [simp] = `f \<in> carrier P`
1.38 -          and deg_g_le_deg_f = `deg R g \<le> deg R f`
1.39 -        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.40 -          and ?q = "monom P (lcoeff f) (deg R f - deg R g)"
1.41 -        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.42 -        proof -
1.43 -          (*JE: we first extablish the existence of a triple satisfying the previous equation.
1.44 -            Then we will have to prove the second part of the predicate.*)
1.45 -          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"
1.47 -            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"]]
1.48 -            using r_neg by auto
1.49 +      let ?k = "1::nat"
1.50 +      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)"
1.51 +      let ?q = "monom P (?lf) (deg R f - deg R g)"
1.52 +      have f1_in_carrier: "?f1 \<in> carrier P" and q_in_carrier: "?q \<in> carrier P" by simp_all
1.53 +      show ?thesis
1.54 +      proof (cases "deg R f = 0")
1.55 +        case True
1.56 +        {
1.57 +          have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
1.58 +          have "?pred f \<zero>\<^bsub>P\<^esub> 1"
1.59 +            using deg_zero_impl_monom [OF g_in_P deg_g]
1.60 +            using sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
1.61 +            using deg_g by simp
1.62 +          then show ?thesis by blast
1.63 +        }
1.64 +      next
1.65 +        case False note deg_f_nzero = False
1.66 +        {
1.67 +          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"
1.69 +              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"]])
1.70 +          have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?f1) < deg R f"
1.71 +          proof (unfold deg_uminus [OF f1_in_carrier])
1.72 +            show "deg R ?f1 < deg R f"
1.73 +            proof (rule deg_lcoeff_cancel)
1.74 +              show "deg R (\<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
1.75 +                using deg_smult_ring [of ?lg f]
1.76 +                using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
1.77 +              show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
1.78 +                by (simp add: monom_deg_mult [OF f_in_P g_in_P deg_g_le_deg_f, of ?lf])
1.79 +              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)"
1.80 +                unfolding coeff_mult [OF g_in_P monom_closed
1.81 +                  [OF lcoeff_closed [OF f_in_P],
1.82 +                    of "deg R f - deg R g"], of "deg R f"]
1.83 +                unfolding coeff_monom [OF lcoeff_closed
1.84 +                  [OF f_in_P], of "(deg R f - deg R g)"]
1.85 +                using R.finsum_cong' [of "{..deg R f}" "{..deg R f}"
1.86 +                  "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then ?lf else \<zero>))"
1.87 +                  "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> ?lf else \<zero>)"]
1.88 +                using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> ?lf)"]
1.89 +                unfolding Pi_def using deg_g_le_deg_f by force
1.90 +            qed (simp_all add: deg_f_nzero)
1.91 +          qed
1.92 +          then obtain q' r' k'
1.93 +            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'"
1.94 +            and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
1.95 +            and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
1.96 +            using "1.hyps" using f1_in_carrier by blast
1.97            show ?thesis
1.98 -          proof (cases "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R g")
1.99 -            (*JE: if the degree of the remainder satisfies the statement property we are done*)
1.100 -            case True
1.101 -            {
1.102 -              show ?thesis
1.103 -              proof (rule exI3 [of _ ?q "\<ominus>\<^bsub>P\<^esub> ?r" ?k], intro conjI)
1.104 -                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
1.105 -                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
1.106 -              qed (simp_all)
1.107 -            }
1.108 -          next
1.109 -            case False note n_deg_r_l_deg_g = False
1.110 -            {
1.111 -              (*JE: otherwise, we verify the conditions of the induction hypothesis.*)
1.112 -              show ?thesis
1.113 -              proof (cases "deg R f = 0")
1.114 -                (*JE: the solutions are different if the degree of f is zero or not*)
1.115 -                case True
1.116 -                {
1.117 -                  have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
1.118 -                  have "lcoeff g (^) (1::nat) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> f \<oplus>\<^bsub>P\<^esub> \<zero>\<^bsub>P\<^esub>"
1.119 -                    unfolding deg_g apply simp
1.120 -                    unfolding sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
1.121 -                    using deg_zero_impl_monom [OF g_in_P deg_g] by simp
1.122 -                  then show ?thesis using f_in_P by blast
1.123 -                }
1.124 -              next
1.125 -                case False note deg_f_nzero = False
1.126 -                {
1.127 -                  (*JE: now it only remains the case where the induction hypothesis can be used.*)
1.128 -                  (*JE: we first prove that the degree of the remainder is smaller than the one of f*)
1.129 -                  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f"
1.130 -                  proof -
1.131 -                    have "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp
1.132 -                    also have "\<dots> < deg R f"
1.133 -                    proof (rule deg_lcoeff_cancel)
1.134 -                      show "deg R (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
1.135 -                        using deg_smult_ring [of "lcoeff g" f]
1.136 -                        using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
1.137 -                      show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
1.138 -                        using monom_deg_mult [OF _ g_in_P, of f "lcoeff f"] and deg_g_le_deg_f
1.139 -                        by simp
1.140 -                      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)"
1.141 -                        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"]
1.142 -                        unfolding coeff_monom [OF lcoeff_closed [OF f_in_P], of "(deg R f - deg R g)"]
1.143 -                        using R.finsum_cong' [of "{..deg R f}" "{..deg R f}"
1.144 -                          "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then lcoeff f else \<zero>))"
1.145 -                          "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> lcoeff f else \<zero>)"]
1.146 -                        using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> lcoeff f)"]
1.147 -                        unfolding Pi_def using deg_g_le_deg_f by force
1.148 -                    qed (simp_all add: deg_f_nzero)
1.149 -                    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f" .
1.150 -                  qed
1.151 -                  moreover have "\<ominus>\<^bsub>P\<^esub> ?r \<in> carrier P" by simp
1.152 -                  moreover obtain m where deg_rem_eq_m: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = m" by auto
1.153 -                  moreover have "deg R g \<le> deg R (\<ominus>\<^bsub>P\<^esub> ?r)" using n_deg_r_l_deg_g by simp
1.154 -                    (*JE: now, by applying the induction hypothesis, we obtain new quotient, remainder and exponent.*)
1.155 -                  ultimately obtain q' r' k'
1.156 -                    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.157 -                    and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
1.158 -                    using less by blast
1.159 -                      (*JE: we now prove that the new quotient, remainder and exponent can be used to get
1.160 -                      the quotient, remainder and exponent of the long division theorem*)
1.161 -                  show ?thesis
1.162 -                  proof (rule exI3 [of _ "((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
1.163 -                    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'"
1.164 -                    proof -
1.165 -                      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)"
1.166 -                        using smult_assoc1 exist by simp
1.167 -                      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))"
1.168 -                        using UP_smult_r_distr by simp
1.169 -                      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')"
1.170 -                        using rem_desc by simp
1.171 -                      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'"
1.172 -                        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'"]]
1.173 -                        using q'_in_carrier r'_in_carrier by simp
1.174 -                      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'"
1.175 -                        using q'_in_carrier by (auto simp add: m_comm)
1.176 -                      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'"
1.177 -                        using smult_assoc2 q'_in_carrier by auto
1.178 -                      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'"
1.179 -                        using sym [OF l_distr] and q'_in_carrier by auto
1.180 -                      finally show ?thesis using m_comm q'_in_carrier by auto
1.181 -                    qed
1.182 -                  qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
1.183 -                }
1.184 -              qed
1.185 -            }
1.186 -          qed
1.187 -        qed
1.188 +          proof (rule exI3 [of _ "((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
1.189 +            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'"
1.190 +            proof -
1.191 +              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)"
1.192 +                using smult_assoc1 [OF _ _ f_in_P] using exist by simp
1.193 +              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))"
1.194 +                using UP_smult_r_distr by simp
1.195 +              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')"
1.196 +                unfolding rem_desc ..
1.197 +              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'"
1.198 +                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'"]]
1.199 +                using r'_in_carrier q'_in_carrier by simp
1.200 +              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'"
1.201 +                using q'_in_carrier by (auto simp add: m_comm)
1.202 +              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'"
1.203 +                using smult_assoc2 q'_in_carrier "1.prems" by auto
1.204 +              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'"
1.205 +                using sym [OF l_distr] and q'_in_carrier by auto
1.206 +              finally show ?thesis using m_comm q'_in_carrier by auto
1.207 +            qed
1.208 +          qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
1.209 +        }
1.210        qed
1.211      }
1.212    qed
```