src/HOL/Algebra/UnivPoly.thy
 changeset 32960 69916a850301 parent 32456 341c83339aeb child 33657 a4179bf442d1
```     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sat Oct 17 01:05:59 2009 +0200
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sat Oct 17 14:43:18 2009 +0200
1.3 @@ -349,19 +349,19 @@
1.4        fix nn assume Succ: "n = Suc nn"
1.5        have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = coeff P p (Suc nn)"
1.6        proof -
1.7 -	have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = (\<Oplus>i\<in>{..Suc nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" using R by simp
1.8 -	also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>) \<oplus> (\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))"
1.9 -	  using finsum_Suc [of "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "nn"] unfolding Pi_def using R by simp
1.10 -	also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>)"
1.11 -	proof -
1.12 -	  have "(\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>)) = (\<Oplus>i\<in>{..nn}. \<zero>)"
1.13 -	    using finsum_cong [of "{..nn}" "{..nn}" "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "(\<lambda>i::nat. \<zero>)"] using R
1.14 -	    unfolding Pi_def by simp
1.15 -	  also have "\<dots> = \<zero>" by simp
1.16 -	  finally show ?thesis using r_zero R by simp
1.17 -	qed
1.18 -	also have "\<dots> = coeff P p (Suc nn)" using R by simp
1.19 -	finally show ?thesis by simp
1.20 +        have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = (\<Oplus>i\<in>{..Suc nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" using R by simp
1.21 +        also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>) \<oplus> (\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))"
1.22 +          using finsum_Suc [of "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "nn"] unfolding Pi_def using R by simp
1.23 +        also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>)"
1.24 +        proof -
1.25 +          have "(\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>)) = (\<Oplus>i\<in>{..nn}. \<zero>)"
1.26 +            using finsum_cong [of "{..nn}" "{..nn}" "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "(\<lambda>i::nat. \<zero>)"] using R
1.27 +            unfolding Pi_def by simp
1.28 +          also have "\<dots> = \<zero>" by simp
1.29 +          finally show ?thesis using r_zero R by simp
1.30 +        qed
1.31 +        also have "\<dots> = coeff P p (Suc nn)" using R by simp
1.32 +        finally show ?thesis by simp
1.33        qed
1.34        then show ?thesis using Succ by simp
1.35      }
1.36 @@ -627,11 +627,11 @@
1.37      then show "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k)"
1.38      proof -
1.39        have lhs: "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
1.40 -	unfolding monom_one_Suc [of "Suc k"] unfolding hypo ..
1.41 +        unfolding monom_one_Suc [of "Suc k"] unfolding hypo ..
1.42        note cl = monom_closed [OF R.one_closed, of 1]
1.43        note clk = monom_closed [OF R.one_closed, of k]
1.44        have rhs: "monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
1.45 -	unfolding monom_one_Suc [of k] unfolding sym [OF m_assoc  [OF cl clk cl]] ..
1.46 +        unfolding monom_one_Suc [of k] unfolding sym [OF m_assoc  [OF cl clk cl]] ..
1.47        from lhs rhs show ?thesis by simp
1.48      qed
1.49    }
1.50 @@ -670,25 +670,25 @@
1.51      case True
1.52      {
1.53        show ?thesis
1.54 -	unfolding True [symmetric]
1.55 -	  coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of "n + m"]
1.56 -	  coeff_monom [OF a_in_R, of n] coeff_monom [OF b_in_R, of m]
1.57 -	using R.finsum_cong [of "{.. n + m}" "{.. n + m}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = n + m - i then b else \<zero>))"
1.58 -	  "(\<lambda>i. if n = i then a \<otimes> b else \<zero>)"]
1.59 -	  a_in_R b_in_R
1.60 -	unfolding simp_implies_def
1.61 -	using R.finsum_singleton [of n "{.. n + m}" "(\<lambda>i. a \<otimes> b)"]
1.62 -	unfolding Pi_def by auto
1.63 +        unfolding True [symmetric]
1.64 +          coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of "n + m"]
1.65 +          coeff_monom [OF a_in_R, of n] coeff_monom [OF b_in_R, of m]
1.66 +        using R.finsum_cong [of "{.. n + m}" "{.. n + m}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = n + m - i then b else \<zero>))"
1.67 +          "(\<lambda>i. if n = i then a \<otimes> b else \<zero>)"]
1.68 +          a_in_R b_in_R
1.69 +        unfolding simp_implies_def
1.70 +        using R.finsum_singleton [of n "{.. n + m}" "(\<lambda>i. a \<otimes> b)"]
1.71 +        unfolding Pi_def by auto
1.72      }
1.73    next
1.74      case False
1.75      {
1.76        show ?thesis
1.77 -	unfolding coeff_monom [OF R.m_closed [OF a_in_R b_in_R], of "n + m" k] apply (simp add: False)
1.78 -	unfolding coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of k]
1.79 -	unfolding coeff_monom [OF a_in_R, of n] unfolding coeff_monom [OF b_in_R, of m] using False
1.80 -	using R.finsum_cong [of "{..k}" "{..k}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = k - i then b else \<zero>))" "(\<lambda>i. \<zero>)"]
1.81 -	unfolding Pi_def simp_implies_def using a_in_R b_in_R by force
1.82 +        unfolding coeff_monom [OF R.m_closed [OF a_in_R b_in_R], of "n + m" k] apply (simp add: False)
1.83 +        unfolding coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of k]
1.84 +        unfolding coeff_monom [OF a_in_R, of n] unfolding coeff_monom [OF b_in_R, of m] using False
1.85 +        using R.finsum_cong [of "{..k}" "{..k}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = k - i then b else \<zero>))" "(\<lambda>i. \<zero>)"]
1.86 +        unfolding Pi_def simp_implies_def using a_in_R b_in_R by force
1.87      }
1.88    qed
1.89  qed (simp_all add: a_in_R b_in_R)
1.90 @@ -1517,7 +1517,7 @@
1.91        then have max_sl: "max (deg R p) (deg R q) < m" by simp
1.92        then have "deg R (p \<oplus>\<^bsub>P\<^esub> q) < m" using deg_add [OF p_in_P q_in_P] by arith
1.93        with deg_R_p deg_R_q show ?thesis using coeff_add [OF p_in_P q_in_P, of m]
1.94 -	using deg_aboveD [of "p \<oplus>\<^bsub>P\<^esub> q" m] using p_in_P q_in_P by simp
1.95 +        using deg_aboveD [of "p \<oplus>\<^bsub>P\<^esub> q" m] using p_in_P q_in_P by simp
1.96      qed
1.97    qed (simp add: p_in_P q_in_P)
1.98    moreover have deg_ne: "deg R (p \<oplus>\<^bsub>P\<^esub> q) \<noteq> deg R r"
1.99 @@ -1582,114 +1582,114 @@
1.100        (*JE: we now apply the induction hypothesis with some additional facts required*)
1.101        from f_in_P deg_g_le_deg_f show ?thesis
1.102        proof (induct n \<equiv> "deg R f" arbitrary: "f" rule: nat_less_induct)
1.103 -	fix n f
1.104 -	assume hypo: "\<forall>m<n. \<forall>x. x \<in> carrier P \<longrightarrow>
1.105 +        fix n f
1.106 +        assume hypo: "\<forall>m<n. \<forall>x. x \<in> carrier P \<longrightarrow>
1.107            deg R g \<le> deg R x \<longrightarrow>
1.108 -	  m = deg R x \<longrightarrow>
1.109 -	  (\<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.110 -	  and prem: "n = deg R f" and f_in_P [simp]: "f \<in> carrier P"
1.111 -	  and deg_g_le_deg_f: "deg R g \<le> deg R f"
1.112 -	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.113 -	  and ?q = "monom P (lcoeff f) (deg R f - deg R g)"
1.114 -	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.115 -	proof -
1.116 -	  (*JE: we first extablish the existence of a triple satisfying the previous equation.
1.117 -	    Then we will have to prove the second part of the predicate.*)
1.118 -	  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.120 -	    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.121 -	    using r_neg by auto
1.122 -	  show ?thesis
1.123 -	  proof (cases "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R g")
1.124 -	    (*JE: if the degree of the remainder satisfies the statement property we are done*)
1.125 -	    case True
1.126 -	    {
1.127 -	      show ?thesis
1.128 -	      proof (rule exI3 [of _ ?q "\<ominus>\<^bsub>P\<^esub> ?r" ?k], intro conjI)
1.129 -		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.130 -		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.131 -	      qed (simp_all)
1.132 -	    }
1.133 -	  next
1.134 -	    case False note n_deg_r_l_deg_g = False
1.135 -	    {
1.136 -	      (*JE: otherwise, we verify the conditions of the induction hypothesis.*)
1.137 -	      show ?thesis
1.138 -	      proof (cases "deg R f = 0")
1.139 -		(*JE: the solutions are different if the degree of f is zero or not*)
1.140 -		case True
1.141 -		{
1.142 -		  have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
1.143 -		  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.144 -		    unfolding deg_g apply simp
1.145 -		    unfolding sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
1.146 -		    using deg_zero_impl_monom [OF g_in_P deg_g] by simp
1.147 -		  then show ?thesis using f_in_P by blast
1.148 -		}
1.149 -	      next
1.150 -		case False note deg_f_nzero = False
1.151 -		{
1.152 -		  (*JE: now it only remains the case where the induction hypothesis can be used.*)
1.153 -		  (*JE: we first prove that the degree of the remainder is smaller than the one of f*)
1.154 -		  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n"
1.155 -		  proof -
1.156 -		    have "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp
1.157 -		    also have "\<dots> < deg R f"
1.158 -		    proof (rule deg_lcoeff_cancel)
1.159 -		      show "deg R (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
1.160 -			using deg_smult_ring [of "lcoeff g" f] using prem
1.161 -			using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
1.162 -		      show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
1.163 -			using monom_deg_mult [OF _ g_in_P, of f "lcoeff f"] and deg_g_le_deg_f
1.164 -			by simp
1.165 -		      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.166 -			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.167 -			unfolding coeff_monom [OF lcoeff_closed [OF f_in_P], of "(deg R f - deg R g)"]
1.168 -			using R.finsum_cong' [of "{..deg R f}" "{..deg R f}"
1.169 -			  "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then lcoeff f else \<zero>))"
1.170 -			  "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> lcoeff f else \<zero>)"]
1.171 -			using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> lcoeff f)"]
1.172 -			unfolding Pi_def using deg_g_le_deg_f by force
1.173 -		    qed (simp_all add: deg_f_nzero)
1.174 -		    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n" unfolding prem .
1.175 -		  qed
1.176 -		  moreover have "\<ominus>\<^bsub>P\<^esub> ?r \<in> carrier P" by simp
1.177 -		  moreover obtain m where deg_rem_eq_m: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = m" by auto
1.178 -		  moreover have "deg R g \<le> deg R (\<ominus>\<^bsub>P\<^esub> ?r)" using n_deg_r_l_deg_g by simp
1.179 -		    (*JE: now, by applying the induction hypothesis, we obtain new quotient, remainder and exponent.*)
1.180 -		  ultimately obtain q' r' k'
1.181 -		    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.182 -		    and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
1.183 -		    using hypo by blast
1.184 -		      (*JE: we now prove that the new quotient, remainder and exponent can be used to get
1.185 -		      the quotient, remainder and exponent of the long division theorem*)
1.186 -		  show ?thesis
1.187 -		  proof (rule exI3 [of _ "((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
1.188 -		    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.189 -		    proof -
1.190 -		      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.191 -			using smult_assoc1 exist by simp
1.192 -		      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.193 -			using UP_smult_r_distr by simp
1.194 -		      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.195 -			using rem_desc by simp
1.196 -		      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.197 -			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.198 -			using q'_in_carrier r'_in_carrier by simp
1.199 -		      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.200 -			using q'_in_carrier by (auto simp add: m_comm)
1.201 -		      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.202 -			using smult_assoc2 q'_in_carrier by auto
1.203 -		      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.204 -			using sym [OF l_distr] and q'_in_carrier by auto
1.205 -		      finally show ?thesis using m_comm q'_in_carrier by auto
1.206 -		    qed
1.207 -		  qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
1.208 -		}
1.209 -	      qed
1.210 -	    }
1.211 -	  qed
1.212 -	qed
1.213 +          m = deg R x \<longrightarrow>
1.214 +          (\<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.215 +          and prem: "n = deg R f" and f_in_P [simp]: "f \<in> carrier P"
1.216 +          and deg_g_le_deg_f: "deg R g \<le> deg R f"
1.217 +        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.218 +          and ?q = "monom P (lcoeff f) (deg R f - deg R g)"
1.219 +        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.220 +        proof -
1.221 +          (*JE: we first extablish the existence of a triple satisfying the previous equation.
1.222 +            Then we will have to prove the second part of the predicate.*)
1.223 +          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.225 +            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.226 +            using r_neg by auto
1.227 +          show ?thesis
1.228 +          proof (cases "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R g")
1.229 +            (*JE: if the degree of the remainder satisfies the statement property we are done*)
1.230 +            case True
1.231 +            {
1.232 +              show ?thesis
1.233 +              proof (rule exI3 [of _ ?q "\<ominus>\<^bsub>P\<^esub> ?r" ?k], intro conjI)
1.234 +                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.235 +                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.236 +              qed (simp_all)
1.237 +            }
1.238 +          next
1.239 +            case False note n_deg_r_l_deg_g = False
1.240 +            {
1.241 +              (*JE: otherwise, we verify the conditions of the induction hypothesis.*)
1.242 +              show ?thesis
1.243 +              proof (cases "deg R f = 0")
1.244 +                (*JE: the solutions are different if the degree of f is zero or not*)
1.245 +                case True
1.246 +                {
1.247 +                  have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
1.248 +                  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.249 +                    unfolding deg_g apply simp
1.250 +                    unfolding sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
1.251 +                    using deg_zero_impl_monom [OF g_in_P deg_g] by simp
1.252 +                  then show ?thesis using f_in_P by blast
1.253 +                }
1.254 +              next
1.255 +                case False note deg_f_nzero = False
1.256 +                {
1.257 +                  (*JE: now it only remains the case where the induction hypothesis can be used.*)
1.258 +                  (*JE: we first prove that the degree of the remainder is smaller than the one of f*)
1.259 +                  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n"
1.260 +                  proof -
1.261 +                    have "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp
1.262 +                    also have "\<dots> < deg R f"
1.263 +                    proof (rule deg_lcoeff_cancel)
1.264 +                      show "deg R (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
1.265 +                        using deg_smult_ring [of "lcoeff g" f] using prem
1.266 +                        using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
1.267 +                      show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
1.268 +                        using monom_deg_mult [OF _ g_in_P, of f "lcoeff f"] and deg_g_le_deg_f
1.269 +                        by simp
1.270 +                      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.271 +                        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.272 +                        unfolding coeff_monom [OF lcoeff_closed [OF f_in_P], of "(deg R f - deg R g)"]
1.273 +                        using R.finsum_cong' [of "{..deg R f}" "{..deg R f}"
1.274 +                          "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then lcoeff f else \<zero>))"
1.275 +                          "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> lcoeff f else \<zero>)"]
1.276 +                        using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> lcoeff f)"]
1.277 +                        unfolding Pi_def using deg_g_le_deg_f by force
1.278 +                    qed (simp_all add: deg_f_nzero)
1.279 +                    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n" unfolding prem .
1.280 +                  qed
1.281 +                  moreover have "\<ominus>\<^bsub>P\<^esub> ?r \<in> carrier P" by simp
1.282 +                  moreover obtain m where deg_rem_eq_m: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = m" by auto
1.283 +                  moreover have "deg R g \<le> deg R (\<ominus>\<^bsub>P\<^esub> ?r)" using n_deg_r_l_deg_g by simp
1.284 +                    (*JE: now, by applying the induction hypothesis, we obtain new quotient, remainder and exponent.*)
1.285 +                  ultimately obtain q' r' k'
1.286 +                    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.287 +                    and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
1.288 +                    using hypo by blast
1.289 +                      (*JE: we now prove that the new quotient, remainder and exponent can be used to get
1.290 +                      the quotient, remainder and exponent of the long division theorem*)
1.291 +                  show ?thesis
1.292 +                  proof (rule exI3 [of _ "((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
1.293 +                    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.294 +                    proof -
1.295 +                      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.296 +                        using smult_assoc1 exist by simp
1.297 +                      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.298 +                        using UP_smult_r_distr by simp
1.299 +                      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.300 +                        using rem_desc by simp
1.301 +                      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.302 +                        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.303 +                        using q'_in_carrier r'_in_carrier by simp
1.304 +                      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.305 +                        using q'_in_carrier by (auto simp add: m_comm)
1.306 +                      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.307 +                        using smult_assoc2 q'_in_carrier by auto
1.308 +                      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.309 +                        using sym [OF l_distr] and q'_in_carrier by auto
1.310 +                      finally show ?thesis using m_comm q'_in_carrier by auto
1.311 +                    qed
1.312 +                  qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
1.313 +                }
1.314 +              qed
1.315 +            }
1.316 +          qed
1.317 +        qed
1.318        qed
1.319      }
1.320    qed
```