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.119 -	    using minus_add
   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.224 +            using minus_add
   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