--- 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