src/HOL/Algebra/UnivPoly.thy
changeset 38131 df8fc03995a4
parent 36096 abc6a2ea4b88
child 44655 fe0365331566
     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.46 -            using minus_add
    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.68 +            by (simp add: minus_add r_neg sym [
    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