[STATEMENT]
lemma (in PolynRg) deg_mult_pols:"\<lbrakk>Idomain S;
      p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero> \<rbrakk> \<Longrightarrow>
      p \<cdot>\<^sub>r q \<noteq> \<zero> \<and>
     deg_n R S X (p \<cdot>\<^sub>r q) = deg_n R S X p + deg_n R S X q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> p \<cdot>\<^sub>r q \<noteq> \<zero> \<and> deg_n R S X (p \<cdot>\<^sub>r q) = deg_n R S X p + deg_n R S X q
[PROOF STEP]
apply (frule Idomain.idom_is_ring[of "S"],
       frule_tac x = p and y = q in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; p \<cdot>\<^sub>r q \<in> carrier R\<rbrakk> \<Longrightarrow> p \<cdot>\<^sub>r q \<noteq> \<zero> \<and> deg_n R S X (p \<cdot>\<^sub>r q) = deg_n R S X p + deg_n R S X q
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption,
        frule s_cf_expr[of q], assumption, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; p \<cdot>\<^sub>r q \<in> carrier R; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> p \<cdot>\<^sub>r q \<noteq> \<zero> \<and> deg_n R S X (p \<cdot>\<^sub>r q) = deg_n R S X p + deg_n R S X q
[PROOF STEP]
apply (frule_tac c = "s_cf R S X p" and d = "s_cf R S X q" in
        polyn_expr_tOp_c, assumption, erule exE, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; p \<cdot>\<^sub>r q \<in> carrier R; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; q = polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q); snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X p) + fst (s_cf R S X q); snd e (fst e) = snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)); polyn_expr R X (fst e) e = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q)\<rbrakk> \<Longrightarrow> p \<cdot>\<^sub>r q \<noteq> \<zero> \<and> deg_n R S X (p \<cdot>\<^sub>r q) = deg_n R S X p + deg_n R S X q
[PROOF STEP]
apply (drule sym, drule sym, simp,
        thin_tac "polyn_expr R X (fst (s_cf R S X q)) (s_cf R S X q) = q",
        thin_tac "polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; p \<cdot>\<^sub>r q \<in> carrier R; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X p) + fst (s_cf R S X q); snd e (fst (s_cf R S X p) + fst (s_cf R S X q)) = snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)); polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e = p \<cdot>\<^sub>r q\<rbrakk> \<Longrightarrow> p \<cdot>\<^sub>r q \<noteq> \<zero> \<and> deg_n R S X (p \<cdot>\<^sub>r q) = deg_n R S X p + deg_n R S X q
[PROOF STEP]
apply (rotate_tac -1, drule sym,
        frule ring_tOp_closed[of p q], assumption+,
        frule pol_coeff_mem[of "s_cf R S X p" "fst (s_cf R S X p)"], simp,
        frule pol_coeff_mem[of "s_cf R S X q" "fst (s_cf R S X q)"], simp,
        frule_tac x = "snd (s_cf R S X p) (fst (s_cf R S X p))" and
        y = "snd (s_cf R S X q) (fst (s_cf R S X q))" in
        Idomain.idom_tOp_nonzeros[of "S"], assumption+,
        frule_tac c = e in  coeff_nonzero_polyn_nonzero[ of _
        "deg_n R S X p + deg_n R S X q"], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>e. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e \<in> carrier R; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X p) + fst (s_cf R S X q); snd e (fst (s_cf R S X p) + fst (s_cf R S X q)) = snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)); p \<cdot>\<^sub>r q = polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e; snd (s_cf R S X p) (fst (s_cf R S X p)) \<in> carrier S; snd (s_cf R S X q) (fst (s_cf R S X q)) \<in> carrier S; snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> deg_n R S X p + deg_n R S X q \<le> fst (s_cf R S X p) + fst (s_cf R S X q)
 2. \<And>e. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; p \<cdot>\<^sub>r q \<in> carrier R; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X p) + fst (s_cf R S X q); snd e (fst (s_cf R S X p) + fst (s_cf R S X q)) = snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)); p \<cdot>\<^sub>r q = polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e; p \<cdot>\<^sub>r q \<in> carrier R; snd (s_cf R S X p) (fst (s_cf R S X p)) \<in> carrier S; snd (s_cf R S X q) (fst (s_cf R S X q)) \<in> carrier S; snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; (polyn_expr R X (deg_n R S X p + deg_n R S X q) e \<noteq> \<zero>) = (\<exists>j\<le>deg_n R S X p + deg_n R S X q. snd e j \<noteq> \<zero>\<^bsub>S\<^esub>)\<rbrakk> \<Longrightarrow> p \<cdot>\<^sub>r q \<noteq> \<zero> \<and> deg_n R S X (p \<cdot>\<^sub>r q) = deg_n R S X p + deg_n R S X q
[PROOF STEP]
apply (simp add:s_cf_deg, simp add:s_cf_deg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e \<in> carrier R; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X p) + fst (s_cf R S X q); snd e (fst (s_cf R S X p) + fst (s_cf R S X q)) = snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)); p \<cdot>\<^sub>r q = polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e; snd (s_cf R S X p) (fst (s_cf R S X p)) \<in> carrier S; snd (s_cf R S X q) (fst (s_cf R S X q)) \<in> carrier S; snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; (polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e \<noteq> \<zero>) = (\<exists>j\<le>fst (s_cf R S X p) + fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>)\<rbrakk> \<Longrightarrow> (\<exists>j\<le>fst (s_cf R S X p) + fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>) \<and> deg_n R S X (polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e) = fst (s_cf R S X p) + fst (s_cf R S X q)
[PROOF STEP]
apply (cut_tac n = "fst (s_cf R S X p) + fst (s_cf R S X q)" in le_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e \<in> carrier R; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X p) + fst (s_cf R S X q); snd e (fst (s_cf R S X p) + fst (s_cf R S X q)) = snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)); p \<cdot>\<^sub>r q = polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e; snd (s_cf R S X p) (fst (s_cf R S X p)) \<in> carrier S; snd (s_cf R S X q) (fst (s_cf R S X q)) \<in> carrier S; snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; (polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e \<noteq> \<zero>) = (\<exists>j\<le>fst (s_cf R S X p) + fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>); fst (s_cf R S X p) + fst (s_cf R S X q) \<le> fst (s_cf R S X p) + fst (s_cf R S X q)\<rbrakk> \<Longrightarrow> (\<exists>j\<le>fst (s_cf R S X p) + fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>) \<and> deg_n R S X (polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e) = fst (s_cf R S X p) + fst (s_cf R S X q)
[PROOF STEP]
apply (subgoal_tac "\<exists>j\<le>fst (s_cf R S X p) +
                       fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>e. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e \<in> carrier R; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X p) + fst (s_cf R S X q); snd e (fst (s_cf R S X p) + fst (s_cf R S X q)) = snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)); p \<cdot>\<^sub>r q = polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e; snd (s_cf R S X p) (fst (s_cf R S X p)) \<in> carrier S; snd (s_cf R S X q) (fst (s_cf R S X q)) \<in> carrier S; snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e \<noteq> \<zero>; \<exists>j\<le>fst (s_cf R S X p) + fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e) = fst (s_cf R S X p) + fst (s_cf R S X q)
 2. \<And>e. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e \<in> carrier R; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X p) + fst (s_cf R S X q); snd e (fst (s_cf R S X p) + fst (s_cf R S X q)) = snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)); p \<cdot>\<^sub>r q = polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e; snd (s_cf R S X p) (fst (s_cf R S X p)) \<in> carrier S; snd (s_cf R S X q) (fst (s_cf R S X q)) \<in> carrier S; snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; (polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e \<noteq> \<zero>) = (\<exists>j\<le>fst (s_cf R S X p) + fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>); fst (s_cf R S X p) + fst (s_cf R S X q) \<le> fst (s_cf R S X p) + fst (s_cf R S X q)\<rbrakk> \<Longrightarrow> \<exists>j\<le>fst (s_cf R S X p) + fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (cut_tac c = e in pol_deg_n[of "p \<cdot>\<^sub>r q" _
                "fst (s_cf R S X p) + fst (s_cf R S X q)"], simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e \<in> carrier R; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X p) + fst (s_cf R S X q); snd e (fst (s_cf R S X p) + fst (s_cf R S X q)) = snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)); p \<cdot>\<^sub>r q = polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e; snd (s_cf R S X p) (fst (s_cf R S X p)) \<in> carrier S; snd (s_cf R S X q) (fst (s_cf R S X q)) \<in> carrier S; snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; (polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e \<noteq> \<zero>) = (\<exists>j\<le>fst (s_cf R S X p) + fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>j\<le>fst (s_cf R S X p) + fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (thin_tac "(polyn_expr R X (fst (s_cf R S X p) +
          fst (s_cf R S X q)) e \<noteq> \<zero>) =
         (\<exists>j\<le>fst (s_cf R S X p) + fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>)",
        thin_tac "p \<cdot>\<^sub>r q =
         polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e",
        thin_tac "polyn_expr R X (fst (s_cf R S X p) + fst (s_cf R S X q)) e
         \<in> carrier R",
        thin_tac "snd (s_cf R S X p) (fst (s_cf R S X p)) \<in> carrier S",
        thin_tac "snd (s_cf R S X q) (fst (s_cf R S X q)) \<in> carrier S")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; fst e = fst (s_cf R S X p) + fst (s_cf R S X q); snd e (fst (s_cf R S X p) + fst (s_cf R S X q)) = snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)); snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> \<exists>j\<le>fst (s_cf R S X p) + fst (s_cf R S X q). snd e j \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (drule sym, drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; Ring S; pol_coeff S (s_cf R S X p); pol_coeff S (s_cf R S X q); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X q) (fst (s_cf R S X q)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S e; snd e (fst e) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) + fst (s_cf R S X q) = fst e; snd (s_cf R S X p) (fst (s_cf R S X p)) \<cdot>\<^sub>r\<^bsub>S\<^esub> snd (s_cf R S X q) (fst (s_cf R S X q)) = snd e (fst e)\<rbrakk> \<Longrightarrow> \<exists>j\<le>fst e. snd e j \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (cut_tac n = "fst e" in le_refl, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) deg_mult_pols1:"\<lbrakk>Idomain S; p \<in> carrier R; q \<in> carrier R\<rbrakk>
       \<Longrightarrow>
          deg R S X (p \<cdot>\<^sub>r q) = deg R S X p + deg R S X q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; q \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X (p \<cdot>\<^sub>r q) = deg R S X p + deg R S X q
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp add:ring_times_0_x, simp add:deg_def,
       rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; \<zero> \<in> carrier R; q \<in> carrier R; p = \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> - \<infinity> = - \<infinity> + an (deg_n R S X q)
 2. \<lbrakk>Idomain S; p \<in> carrier R; q \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<cdot>\<^sub>r q) = deg R S X p + deg R S X q
[PROOF STEP]
apply (simp add:an_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; q \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<cdot>\<^sub>r q) = deg R S X p + deg R S X q
[PROOF STEP]
apply (case_tac "q = \<zero>\<^bsub>R\<^esub>", simp add:ring_times_x_0, simp add:deg_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; p \<in> carrier R; \<zero> \<in> carrier R; p \<noteq> \<zero>; q = \<zero>\<rbrakk> \<Longrightarrow> - \<infinity> = an (deg_n R S X p) + - \<infinity>
 2. \<lbrakk>Idomain S; p \<in> carrier R; q \<in> carrier R; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<cdot>\<^sub>r q) = deg R S X p + deg R S X q
[PROOF STEP]
apply (simp add:an_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; q \<in> carrier R; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<cdot>\<^sub>r q) = deg R S X p + deg R S X q
[PROOF STEP]
apply (frule deg_mult_pols[of p q], assumption+, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; q \<in> carrier R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<cdot>\<^sub>r q \<noteq> \<zero>; deg_n R S X (p \<cdot>\<^sub>r q) = deg_n R S X p + deg_n R S X q\<rbrakk> \<Longrightarrow> deg R S X (p \<cdot>\<^sub>r q) = deg R S X p + deg R S X q
[PROOF STEP]
apply (frule Idomain.idom_is_ring[of "S"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; q \<in> carrier R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<cdot>\<^sub>r q \<noteq> \<zero>; deg_n R S X (p \<cdot>\<^sub>r q) = deg_n R S X p + deg_n R S X q; Ring S\<rbrakk> \<Longrightarrow> deg R S X (p \<cdot>\<^sub>r q) = deg R S X p + deg R S X q
[PROOF STEP]
apply (frule ring_tOp_closed[of p q], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; q \<in> carrier R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<cdot>\<^sub>r q \<noteq> \<zero>; deg_n R S X (p \<cdot>\<^sub>r q) = deg_n R S X p + deg_n R S X q; Ring S; p \<cdot>\<^sub>r q \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X (p \<cdot>\<^sub>r q) = deg R S X p + deg R S X q
[PROOF STEP]
apply (simp add:deg_an an_def a_zpz)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) const_times_polyn:"\<lbrakk>Idomain S; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>;
       p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (c \<cdot>\<^sub>r p) \<noteq> \<zero>  \<and>
       deg_n R S X (c \<cdot>\<^sub>r p) = deg_n R S X p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> c \<cdot>\<^sub>r p \<noteq> \<zero> \<and> deg_n R S X (c \<cdot>\<^sub>r p) = deg_n R S X p
[PROOF STEP]
apply (frule Idomain.idom_is_ring[of "S"],
       cut_tac subring,
       frule mem_subring_mem_ring[of S c], assumption+,
       simp add:Subring_zero_ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; c \<in> carrier S; c \<noteq> \<zero>; p \<in> carrier R; p \<noteq> \<zero>; Ring S; Subring R S; c \<in> carrier R\<rbrakk> \<Longrightarrow> c \<cdot>\<^sub>r p \<noteq> \<zero> \<and> deg_n R S X (c \<cdot>\<^sub>r p) = deg_n R S X p
[PROOF STEP]
apply (frule deg_mult_pols[of c p], assumption+,
       erule conjE, simp,
       simp add:pol_of_deg0[THEN sym, of "c"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) p_times_monomial_nonzero:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
                                                          (X^\<^bsup>R j\<^esup>) \<cdot>\<^sub>r p \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> X^\<^bsup>R j\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S\<rbrakk> \<Longrightarrow> X^\<^bsup>R j\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> X^\<^bsup>R j\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>
[PROOF STEP]
apply (frule low_deg_terms_zero1[THEN sym, of "s_cf R S X p" j])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; X^\<^bsup>R j\<^esup> \<cdot>\<^sub>r polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = polyn_expr R X (fst (s_cf R S X p) + j) (ext_cf S j (s_cf R S X p))\<rbrakk> \<Longrightarrow> X^\<^bsup>R j\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>
[PROOF STEP]
apply (drule sym, simp,
        thin_tac "X^\<^bsup>R j\<^esup> \<cdot>\<^sub>r p =
     polyn_expr R X (fst (s_cf R S X p) + j) (ext_cf S j (s_cf R S X p))",
         thin_tac "polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = p")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> polyn_expr R X (fst (s_cf R S X p) + j) (ext_cf S j (s_cf R S X p)) \<noteq> \<zero>
[PROOF STEP]
apply (frule ext_cf_pol_coeff[of "s_cf R S X p" j])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S j (s_cf R S X p))\<rbrakk> \<Longrightarrow> polyn_expr R X (fst (s_cf R S X p) + j) (ext_cf S j (s_cf R S X p)) \<noteq> \<zero>
[PROOF STEP]
apply(frule coeff_nonzero_polyn_nonzero[of "ext_cf S j (s_cf R S X p)"
                                      "fst (ext_cf S j (s_cf R S X p))"],
       simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S j (s_cf R S X p)); (polyn_expr R X (fst (ext_cf S j (s_cf R S X p))) (ext_cf S j (s_cf R S X p)) \<noteq> \<zero>) = (\<exists>ja\<le>fst (ext_cf S j (s_cf R S X p)). snd (ext_cf S j (s_cf R S X p)) ja \<noteq> \<zero>\<^bsub>S\<^esub>)\<rbrakk> \<Longrightarrow> polyn_expr R X (fst (s_cf R S X p) + j) (ext_cf S j (s_cf R S X p)) \<noteq> \<zero>
[PROOF STEP]
apply (simp add:ext_cf_len add.commute[of j],
     thin_tac "(polyn_expr R X (fst (s_cf R S X p) + j)
         (ext_cf S j (s_cf R S X p)) \<noteq> \<zero>) =
     (\<exists>ja\<le>fst (s_cf R S X p) + j. snd (ext_cf S j (s_cf R S X p)) ja \<noteq> \<zero>\<^bsub>S\<^esub>)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S j (s_cf R S X p))\<rbrakk> \<Longrightarrow> \<exists>ja\<le>fst (s_cf R S X p) + j. snd (ext_cf S j (s_cf R S X p)) ja \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (cut_tac ext_cf_hi[of "s_cf R S X p" j], simp,
        thin_tac "snd (s_cf R S X p) (fst (s_cf R S X p)) =
        snd (ext_cf S j (s_cf R S X p)) (j + fst (s_cf R S X p))",
        simp add:add.commute[of _ j])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; pol_coeff S (s_cf R S X p); snd (ext_cf S j (s_cf R S X p)) (j + fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S j (s_cf R S X p))\<rbrakk> \<Longrightarrow> \<exists>ja\<le>j + fst (s_cf R S X p). snd (ext_cf S j (s_cf R S X p)) ja \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S j (s_cf R S X p))\<rbrakk> \<Longrightarrow> pol_coeff S (s_cf R S X p)
[PROOF STEP]
apply (cut_tac n = "j + fst (s_cf R S X p)" in le_refl, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; pol_coeff S (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; pol_coeff S (ext_cf S j (s_cf R S X p))\<rbrakk> \<Longrightarrow> pol_coeff S (s_cf R S X p)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) p_times_monomial_nonzero1:"\<lbrakk>Idomain S; p \<in> carrier R;
       p \<noteq> \<zero>; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow>(c \<cdot>\<^sub>r (X^\<^bsup>R j\<^esup>)) \<cdot>\<^sub>r p \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> c \<cdot>\<^sub>r X^\<^bsup>R j\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>
[PROOF STEP]
apply (frule Idomain.idom_is_ring[of "S"],
       cut_tac subring,
       cut_tac X_mem_R ,
       frule mem_subring_mem_ring[of S c], assumption+,
       frule npClose[of X j])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; p \<noteq> \<zero>; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>; Ring S; Subring R S; X \<in> carrier R; c \<in> carrier R; X^\<^bsup>R j\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> c \<cdot>\<^sub>r X^\<^bsup>R j\<^esup> \<cdot>\<^sub>r p \<noteq> \<zero>
[PROOF STEP]
apply (simp add:ring_tOp_commute[of c],
       simp add:ring_tOp_assoc,
       frule const_times_polyn[of c p], assumption+,
       erule conjE,
       frule ring_tOp_closed[of c p], assumption+,
       simp add:p_times_monomial_nonzero[of "c \<cdot>\<^sub>r p"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) polyn_ring_integral:"Idomain S = Idomain R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Idomain S = Idomain R
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Subring R S; Ring S\<rbrakk> \<Longrightarrow> Idomain S = Idomain R
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Subring R S; Ring S; Idomain S\<rbrakk> \<Longrightarrow> Idomain R
 2. \<lbrakk>Subring R S; Ring S; Idomain R\<rbrakk> \<Longrightarrow> Idomain S
[PROOF STEP]
apply (subst Idomain_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Subring R S; Ring S; Idomain S\<rbrakk> \<Longrightarrow> Ring R \<and> Idomain_axioms R
 2. \<lbrakk>Subring R S; Ring S; Idomain R\<rbrakk> \<Longrightarrow> Idomain S
[PROOF STEP]
apply (cut_tac Ring, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Subring R S; Ring S; Idomain S; Ring R\<rbrakk> \<Longrightarrow> Idomain_axioms R
 2. \<lbrakk>Subring R S; Ring S; Idomain R\<rbrakk> \<Longrightarrow> Idomain S
[PROOF STEP]
apply (rule Idomain_axioms.intro,
        rule contrapos_pp, simp+, erule conjE,
        frule_tac p = a and q = b in deg_mult_pols,
       assumption+, erule conjE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Subring R S; Ring S; Idomain R\<rbrakk> \<Longrightarrow> Idomain S
[PROOF STEP]
apply (subst Idomain_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Subring R S; Ring S; Idomain R\<rbrakk> \<Longrightarrow> Ring S \<and> Idomain_axioms S
[PROOF STEP]
apply (cut_tac Ring, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Subring R S; Ring S; Idomain R; Ring R\<rbrakk> \<Longrightarrow> Idomain_axioms S
[PROOF STEP]
apply (rule Idomain_axioms.intro,
        rule contrapos_pp, simp+, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Subring R S; Ring S; Idomain R; Ring R; a \<in> carrier S; b \<in> carrier S; a \<cdot>\<^sub>r\<^bsub>S\<^esub> b = \<zero>\<^bsub>S\<^esub>; a \<noteq> \<zero>\<^bsub>S\<^esub>; b \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:Subring_tOp_ring_tOp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Subring R S; Ring S; Idomain R; Ring R; a \<in> carrier S; b \<in> carrier S; a \<cdot>\<^sub>r b = \<zero>\<^bsub>S\<^esub>; a \<noteq> \<zero>\<^bsub>S\<^esub>; b \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = a in mem_subring_mem_ring[of S], assumption,
        frule_tac x = b in mem_subring_mem_ring[of S], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Subring R S; Ring S; Idomain R; Ring R; a \<in> carrier S; b \<in> carrier S; a \<cdot>\<^sub>r b = \<zero>\<^bsub>S\<^esub>; a \<noteq> \<zero>\<^bsub>S\<^esub>; b \<noteq> \<zero>\<^bsub>S\<^esub>; a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac a = a and b = b in Idomain.idom[of R], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Subring R S; Ring S; Idomain R; Ring R; a \<in> carrier S; b \<in> carrier S; a \<cdot>\<^sub>r b = \<zero>\<^bsub>S\<^esub>; a \<noteq> \<zero>\<^bsub>S\<^esub>; b \<noteq> \<zero>\<^bsub>S\<^esub>; a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b = \<zero>
 2. \<And>a b. \<lbrakk>Subring R S; Ring S; Idomain R; Ring R; a \<in> carrier S; b \<in> carrier S; a \<cdot>\<^sub>r b = \<zero>\<^bsub>S\<^esub>; a \<noteq> \<zero>\<^bsub>S\<^esub>; b \<noteq> \<zero>\<^bsub>S\<^esub>; a \<in> carrier R; b \<in> carrier R; a = \<zero> \<or> b = \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:Subring_zero_ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Subring R S; Ring S; Idomain R; Ring R; a \<in> carrier S; b \<in> carrier S; a \<cdot>\<^sub>r b = \<zero>\<^bsub>S\<^esub>; a \<noteq> \<zero>\<^bsub>S\<^esub>; b \<noteq> \<zero>\<^bsub>S\<^esub>; a \<in> carrier R; b \<in> carrier R; a = \<zero> \<or> b = \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule disjE, simp add:Subring_zero_ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Subring R S; Ring S; Idomain R; Ring R; a \<in> carrier S; b \<in> carrier S; a \<cdot>\<^sub>r b = \<zero>\<^bsub>S\<^esub>; a \<noteq> \<zero>\<^bsub>S\<^esub>; b \<noteq> \<zero>\<^bsub>S\<^esub>; a \<in> carrier R; b \<in> carrier R; b = \<zero>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:Subring_zero_ring_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) deg_to_X_d:"Idomain S \<Longrightarrow>  deg_n R S X (X^\<^bsup>R d\<^esup>) = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Idomain S \<Longrightarrow> deg_n R S X (X^\<^bsup>R d\<^esup>) = d
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       cut_tac polyn_ring_S_nonzero,
       cut_tac X_mem_R,
       cut_tac polyn_ring_X_nonzero,
       cut_tac polyn_ring_integral)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; Subring R S; Ring S; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; X \<in> carrier R; X \<noteq> \<zero>; Idomain S = Idomain R\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R d\<^esup>) = d
[PROOF STEP]
apply (induct_tac d)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; Subring R S; Ring S; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; X \<in> carrier R; X \<noteq> \<zero>; Idomain S = Idomain R\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R 0\<^esup>) = 0
 2. \<And>n. \<lbrakk>Idomain S; Subring R S; Ring S; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; X \<in> carrier R; X \<noteq> \<zero>; Idomain S = Idomain R; deg_n R S X (X^\<^bsup>R n\<^esup>) = n\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R Suc n\<^esup>) = Suc n
[PROOF STEP]
apply (cut_tac ring_one,
        simp add:Subring_one_ring_one[THEN sym],
        simp add:Subring_zero_ring_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; Subring R S; Ring S; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R\<rbrakk> \<Longrightarrow> deg_n R S X 1\<^sub>r\<^bsub>S\<^esub> = 0
 2. \<And>n. \<lbrakk>Idomain S; Subring R S; Ring S; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; X \<in> carrier R; X \<noteq> \<zero>; Idomain S = Idomain R; deg_n R S X (X^\<^bsup>R n\<^esup>) = n\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R Suc n\<^esup>) = Suc n
[PROOF STEP]
apply (subst pol_of_deg0[of "1\<^sub>r\<^bsub>S\<^esub>"], assumption+, simp add:Ring.ring_one[of S])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain S; Subring R S; Ring S; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; X \<in> carrier R; X \<noteq> \<zero>; Idomain S = Idomain R; deg_n R S X (X^\<^bsup>R n\<^esup>) = n\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R Suc n\<^esup>) = Suc n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Subring R S; Ring S; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; deg_n R S X (X^\<^bsup>R n\<^esup>) = n\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X) = Suc n
[PROOF STEP]
apply (subst deg_mult_pols, assumption+,
        simp add:npClose,
        rule Idomain.idom_potent_nonzero, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Subring R S; Ring S; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; deg_n R S X (X^\<^bsup>R n\<^esup>) = n\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R n\<^esup>) + deg_n R S X X = Suc n
[PROOF STEP]
apply (simp add:deg_n_of_X)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) nonzero_deg_pos:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
                                                 0 \<le> deg R S X p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 \<le> deg R S X p
[PROOF STEP]
by (simp add:deg_def)


[STATEMENT]
lemma (in PolynRg) deg_minf_pol_0:"p \<in> carrier R \<Longrightarrow>
                    (deg R S X p = -\<infinity>) = (p = \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> carrier R \<Longrightarrow> (deg R S X p = - \<infinity>) = (p = \<zero>)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p = - \<infinity>\<rbrakk> \<Longrightarrow> p = \<zero>
 2. \<lbrakk>p \<in> carrier R; p = \<zero>\<rbrakk> \<Longrightarrow> deg R S X p = - \<infinity>
[PROOF STEP]
apply (rule contrapos_pp, simp+,
        frule nonzero_deg_pos[of p], assumption+,
        simp add:deg_def an_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p = \<zero>\<rbrakk> \<Longrightarrow> deg R S X p = - \<infinity>
[PROOF STEP]
apply (simp add:deg_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pol_nonzero:"p \<in> carrier R \<Longrightarrow>
             (0 \<le> deg R S X p) = (p \<noteq> \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> carrier R \<Longrightarrow> (0 \<le> deg R S X p) = (p \<noteq> \<zero>)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; 0 \<le> deg R S X p\<rbrakk> \<Longrightarrow> p \<noteq> \<zero>
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 \<le> deg R S X p
[PROOF STEP]
apply (rule contrapos_pp, simp+, simp add:deg_def,
       cut_tac minf_le_any[of "0"], frule ale_antisym[of "0" "-\<infinity>"],
       assumption+,
       simp only:an_0[THEN sym], simp only:an_def, simp del:of_nat_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 \<le> deg R S X p
[PROOF STEP]
apply (simp add:deg_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) minus_deg_in_aug_minf:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
                   - (deg R S X p) \<in> Z\<^sub>-\<^sub>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> - deg R S X p \<in> Z\<^sub>-\<^sub>\<infinity>
[PROOF STEP]
apply (frule deg_in_aug_minf[of p],
      frule pol_nonzero[THEN sym, of p],
      simp add:aug_minf_def,
      rule contrapos_pp, simp+,
      cut_tac a_minus_minus[of "deg R S X p"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; 0 \<le> deg R S X p; deg R S X p \<noteq> \<infinity>; p \<noteq> \<zero>; - deg R S X p = \<infinity>; - \<infinity> = deg R S X p\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (thin_tac "- deg R S X p = \<infinity>", frule sym,
       thin_tac "- \<infinity> = deg R S X p",
       frule deg_minf_pol_0[of p], simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) deg_of_X:"deg R S X X = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg R S X X = 1
[PROOF STEP]
(* the degree of the polyn. X *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg R S X X = 1
[PROOF STEP]
apply (cut_tac X_mem_R,
       cut_tac polyn_ring_X_nonzero,
       cut_tac subring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> carrier R; X \<noteq> \<zero>; Subring R S\<rbrakk> \<Longrightarrow> deg R S X X = 1
[PROOF STEP]
apply (simp add:deg_def, simp only:an_1[THEN sym],
       rule nat_eq_an_eq, simp add:deg_n_of_X)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pol_deg_0:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk>
                   \<Longrightarrow>  (deg R S X p = 0) = (p \<in> carrier S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (deg R S X p = 0) = (p \<in> carrier S)
[PROOF STEP]
apply (simp add:deg_def, simp only:an_0[THEN sym],
       rule iffI,
       frule an_inj[of "deg_n R S X p" "0"], simp,
       simp add:pol_of_deg0,
       rule nat_eq_an_eq, simp add:pol_of_deg0[of p])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) deg_of_X2n:"Idomain S \<Longrightarrow> deg R S X (X^\<^bsup>R n\<^esup>) = an n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Idomain S \<Longrightarrow> deg R S X (X^\<^bsup>R n\<^esup>) = an n
[PROOF STEP]
apply (frule Idomain.idom_is_ring[of "S"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; Ring S\<rbrakk> \<Longrightarrow> deg R S X (X^\<^bsup>R n\<^esup>) = an n
[PROOF STEP]
apply (cut_tac subring,
       cut_tac X_mem_R,
       cut_tac polyn_ring_X_nonzero,
       cut_tac polyn_ring_integral, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S\<rbrakk> \<Longrightarrow> deg R S X (X^\<^bsup>R n\<^esup>) = an n
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S\<rbrakk> \<Longrightarrow> deg R S X (X^\<^bsup>R 0\<^esup>) = an 0
 2. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; deg R S X (X^\<^bsup>R n\<^esup>) = an n\<rbrakk> \<Longrightarrow> deg R S X (X^\<^bsup>R Suc n\<^esup>) = an (Suc n)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S\<rbrakk> \<Longrightarrow> deg R S X 1\<^sub>r = 0
 2. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; deg R S X (X^\<^bsup>R n\<^esup>) = an n\<rbrakk> \<Longrightarrow> deg R S X (X^\<^bsup>R Suc n\<^esup>) = an (Suc n)
[PROOF STEP]
apply (simp add:Subring_one_ring_one[THEN sym, of "S"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S\<rbrakk> \<Longrightarrow> deg R S X 1\<^sub>r\<^bsub>S\<^esub> = 0
 2. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; deg R S X (X^\<^bsup>R n\<^esup>) = an n\<rbrakk> \<Longrightarrow> deg R S X (X^\<^bsup>R Suc n\<^esup>) = an (Suc n)
[PROOF STEP]
apply (subst pol_deg_0[of "1\<^sub>r\<^bsub>S\<^esub>"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier R
 2. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>
 3. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S
 4. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; deg R S X (X^\<^bsup>R n\<^esup>) = an n\<rbrakk> \<Longrightarrow> deg R S X (X^\<^bsup>R Suc n\<^esup>) = an (Suc n)
[PROOF STEP]
apply (simp add:Subring_one_ring_one, simp add:ring_one)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>
 2. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S
 3. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; deg R S X (X^\<^bsup>R n\<^esup>) = an n\<rbrakk> \<Longrightarrow> deg R S X (X^\<^bsup>R Suc n\<^esup>) = an (Suc n)
[PROOF STEP]
apply (simp add:Subring_one_ring_one[of S] polyn_ring_nonzero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>S\<^esub> \<in> carrier S
 2. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; deg R S X (X^\<^bsup>R n\<^esup>) = an n\<rbrakk> \<Longrightarrow> deg R S X (X^\<^bsup>R Suc n\<^esup>) = an (Suc n)
[PROOF STEP]
apply (simp add:Ring.ring_one[of S])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; deg R S X (X^\<^bsup>R n\<^esup>) = an n\<rbrakk> \<Longrightarrow> deg R S X (X^\<^bsup>R Suc n\<^esup>) = an (Suc n)
[PROOF STEP]
apply (frule_tac n = n in npClose[of X])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; deg R S X (X^\<^bsup>R n\<^esup>) = an n; X^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X (X^\<^bsup>R Suc n\<^esup>) = an (Suc n)
[PROOF STEP]
apply (simp add:deg_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; (if X^\<^bsup>R n\<^esup> = \<zero> then - \<infinity> else an (deg_n R S X (X^\<^bsup>R n\<^esup>))) = an n; X^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X = \<zero> \<longrightarrow> - \<infinity> = an (Suc n)) \<and> (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X \<noteq> \<zero> \<longrightarrow> an (deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X)) = an (Suc n))
[PROOF STEP]
apply (simp add:Idomain.idom_potent_nonzero,
       frule_tac n = "Suc n" in Idomain.idom_potent_nonzero[of R X],
       assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; an (deg_n R S X (X^\<^bsup>R n\<^esup>)) = an n; X^\<^bsup>R n\<^esup> \<in> carrier R; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X \<noteq> \<zero>\<rbrakk> \<Longrightarrow> an (deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X)) = an (Suc n)
[PROOF STEP]
apply (rule nat_eq_an_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; an (deg_n R S X (X^\<^bsup>R n\<^esup>)) = an n; X^\<^bsup>R n\<^esup> \<in> carrier R; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X) = Suc n
[PROOF STEP]
apply (frule_tac n = n in Idomain.idom_potent_nonzero[of R X], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; an (deg_n R S X (X^\<^bsup>R n\<^esup>)) = an n; X^\<^bsup>R n\<^esup> \<in> carrier R; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X) = Suc n
[PROOF STEP]
apply (frule_tac n = "deg_n R S X (X^\<^bsup>R n\<^esup>)" and m = n in an_inj,
       thin_tac "an (deg_n R S X (X^\<^bsup>R n\<^esup>)) = an n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; X^\<^bsup>R n\<^esup> \<in> carrier R; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<noteq> \<zero>; deg_n R S X (X^\<^bsup>R n\<^esup>) = n\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X) = Suc n
[PROOF STEP]
apply (cut_tac deg_of_X)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; X^\<^bsup>R n\<^esup> \<in> carrier R; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<noteq> \<zero>; deg_n R S X (X^\<^bsup>R n\<^esup>) = n; deg R S X X = 1\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X) = Suc n
[PROOF STEP]
apply (simp add:deg_def, simp only:an_1[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; X^\<^bsup>R n\<^esup> \<in> carrier R; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<noteq> \<zero>; deg_n R S X (X^\<^bsup>R n\<^esup>) = n; an (deg_n R S X X) = an 1\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X) = Suc n
[PROOF STEP]
apply (frule_tac n = "deg_n R S X X" and m = 1 in an_inj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Idomain R; Ring S; Subring R S; X \<in> carrier R; X \<noteq> \<zero>; Idomain S; X^\<^bsup>R n\<^esup> \<in> carrier R; X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X \<noteq> \<zero>; X^\<^bsup>R n\<^esup> \<noteq> \<zero>; deg_n R S X (X^\<^bsup>R n\<^esup>) = n; an (deg_n R S X X) = an 1; deg_n R S X X = 1\<rbrakk> \<Longrightarrow> deg_n R S X (X^\<^bsup>R n\<^esup> \<cdot>\<^sub>r X) = Suc n
[PROOF STEP]
apply (simp add:deg_mult_pols)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) add_pols_nonzero:"\<lbrakk>p \<in> carrier R; q \<in> carrier R;
      (deg R S X p) \<noteq> (deg R S X q)\<rbrakk>  \<Longrightarrow>  p \<plusminus> q \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<noteq> deg R S X q\<rbrakk> \<Longrightarrow> p \<plusminus> q \<noteq> \<zero>
[PROOF STEP]
apply (cut_tac ring_is_ag,
       cut_tac subring,
       frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<noteq> deg R S X q; aGroup R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> p \<plusminus> q \<noteq> \<zero>
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp add:deg_minf_pol_0[THEN sym],
       simp add:aGroup.ag_l_zero, rule contrapos_pp, simp+,
       case_tac "q = \<zero>\<^bsub>R\<^esub>", simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<noteq> deg R S X q; aGroup R; Subring R S; Ring S; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> p \<plusminus> q \<noteq> \<zero>
[PROOF STEP]
apply (simp add:deg_def,
       simp only:aneq_natneq[of "deg_n R S X p" "deg_n R S X q"],
       cut_tac less_linear[of "deg_n R S X p" "deg_n R S X q"], simp,
       erule disjE,
       rule less_deg_add_nonzero[of p q],
         assumption+,
       frule less_deg_add_nonzero[of q p], assumption+,
       simp add:aGroup.ag_pOp_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) deg_pols_add1:"\<lbrakk>p \<in> carrier R; q \<in> carrier R;
                (deg R S X p) < (deg R S X q)\<rbrakk>  \<Longrightarrow>
                              deg R S X (p \<plusminus> q) = deg R S X q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p < deg R S X q\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) = deg R S X q
[PROOF STEP]
apply (cut_tac ring_is_ag,
       case_tac "p = \<zero>\<^bsub>R\<^esub>", simp add:deg_def aGroup.ag_l_zero,
       case_tac "q = \<zero>\<^bsub>R\<^esub>", simp add:deg_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; \<zero> \<in> carrier R; an (deg_n R S X p) < - \<infinity>; aGroup R; p \<noteq> \<zero>; q = \<zero>\<rbrakk> \<Longrightarrow> p \<plusminus> \<zero> \<noteq> \<zero> \<longrightarrow> an (deg_n R S X (p \<plusminus> \<zero>)) = - \<infinity>
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p < deg R S X q; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) = deg R S X q
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; \<zero> \<in> carrier R; an (deg_n R S X p) < - \<infinity>; aGroup R; p \<noteq> \<zero>; q = \<zero>; p \<plusminus> \<zero> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> an (deg_n R S X (p \<plusminus> \<zero>)) = - \<infinity>
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p < deg R S X q; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) = deg R S X q
[PROOF STEP]
apply (simp add:an_def z_neq_minf)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; \<zero> \<in> carrier R; ant (int (deg_n R S X p)) < - \<infinity>; aGroup R; p \<noteq> \<zero>; q = \<zero>; p \<plusminus> \<zero> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p < deg R S X q; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) = deg R S X q
[PROOF STEP]
apply (fold an_def,
        frule aless_imp_le[of "an (deg_n R S X p)" " - \<infinity>"],
        cut_tac minf_le_any[of "an (deg_n R S X p)"],
        frule ale_antisym[of "an (deg_n R S X p)" "- \<infinity>"], assumption+,
        simp add:an_neq_minf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p < deg R S X q; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) = deg R S X q
[PROOF STEP]
apply (simp add:deg_def, simp add:aless_nat_less,
       frule less_deg_add_nonzero[of p q], assumption+,
       simp, frule polyn_deg_add1[of p q], assumption+, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) deg_pols_add2:"\<lbrakk>p \<in> carrier R; q \<in> carrier R;
       (deg R S X p) = (deg R S X q)\<rbrakk>  \<Longrightarrow>
               deg R S X (p \<plusminus> q) \<le> (deg R S X q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p = deg R S X q\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> deg R S X q
[PROOF STEP]
apply (cut_tac ring_is_ag,
       cut_tac subring, frule subring_Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p = deg R S X q; aGroup R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> deg R S X q
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p = deg R S X q; aGroup R; Subring R S; Ring S; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> deg R S X q
[PROOF STEP]
apply (case_tac "q = \<zero>\<^bsub>R\<^esub>", simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p = deg R S X q; aGroup R; Subring R S; Ring S; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> deg R S X q
[PROOF STEP]
apply (simp add:deg_def,
       frule an_inj[of "deg_n R S X p" "deg_n R S X q"], simp,
       rule impI, subst ale_natle, simp add:polyn_deg_add2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) deg_pols_add3:"\<lbrakk>p \<in> carrier R; q \<in> carrier R;
       (deg R S X p) \<le> an n; (deg R S X q) \<le> an n\<rbrakk>  \<Longrightarrow>
                  deg R S X (p \<plusminus> q) \<le> an n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an n; deg R S X q \<le> an n\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> an n
[PROOF STEP]
apply (case_tac "(deg R S X p) = (deg R S X q)",
       frule deg_pols_add2[of p q], assumption+,
       simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an n; deg R S X q \<le> an n; deg R S X p \<noteq> deg R S X q\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> an n
[PROOF STEP]
apply (cut_tac aless_linear[of "deg R S X p" "deg R S X q"],
       simp, thin_tac "deg R S X p \<noteq> deg R S X q",
       erule disjE, simp add:deg_pols_add1,
       cut_tac ring_is_ag, simp add:aGroup.ag_pOp_commute[of "R" "p" "q"],
       simp add:deg_pols_add1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) const_times_polyn1:"\<lbrakk>Idomain S; p\<in> carrier R; c \<in> carrier S;
            c \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> deg R S X (c \<cdot>\<^sub>r p) = deg R S X p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> deg R S X (c \<cdot>\<^sub>r p) = deg R S X p
[PROOF STEP]
apply (frule Idomain.idom_is_ring,
       cut_tac subring,
       frule mem_subring_mem_ring[of S c], assumption,
       simp add:Subring_zero_ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; p \<in> carrier R; c \<in> carrier S; c \<noteq> \<zero>; Ring S; Subring R S; c \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X (c \<cdot>\<^sub>r p) = deg R S X p
[PROOF STEP]
apply (subst deg_mult_pols1[of c p], assumption+,
       simp add: pol_deg_0[THEN sym, of "c"],
       simp add:aadd_0_l)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) cf_h_len:"\<lbrakk>PolynRg A B Y; f \<in> rHom S B;
                   pol_coeff S c\<rbrakk> \<Longrightarrow> fst (cf_h f c) = fst c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> rHom S B; pol_coeff S c\<rbrakk> \<Longrightarrow> fst (cf_h f c) = fst c
[PROOF STEP]
by (simp add:cf_h_def)


[STATEMENT]
lemma (in PolynRg) cf_h_coeff:"\<lbrakk>PolynRg A B Y; f \<in> rHom S B;
                   pol_coeff S c\<rbrakk> \<Longrightarrow>  pol_coeff B (cf_h f c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> rHom S B; pol_coeff S c\<rbrakk> \<Longrightarrow> pol_coeff B (cf_h f c)
[PROOF STEP]
apply (subst pol_coeff_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> rHom S B; pol_coeff S c\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (cf_h f c). snd (cf_h f c) j \<in> carrier B
[PROOF STEP]
apply (rule allI, rule impI, simp add:cf_h_len cf_h_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; f \<in> rHom S B; pol_coeff S c; j \<le> fst c\<rbrakk> \<Longrightarrow> cmp f (snd c) j \<in> carrier B
[PROOF STEP]
apply (frule_tac j = j in pol_coeff_mem[of c], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; f \<in> rHom S B; pol_coeff S c; j \<le> fst c; snd c j \<in> carrier S\<rbrakk> \<Longrightarrow> cmp f (snd c) j \<in> carrier B
[PROOF STEP]
apply (simp add:cmp_def rHom_mem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) cf_h_cmp:"\<lbrakk>PolynRg A B Y; pol_coeff S (n, f); h \<in> rHom S B;
                    j \<le> n\<rbrakk> \<Longrightarrow>
                 (snd (cf_h h (n, f))) j = (cmp h f) j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; pol_coeff S (n, f); h \<in> rHom S B; j \<le> n\<rbrakk> \<Longrightarrow> snd (cf_h h (n, f)) j = cmp h f j
[PROOF STEP]
by (simp add:cf_h_def)


[STATEMENT]
lemma (in PolynRg) cf_h_special_cf:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B\<rbrakk> \<Longrightarrow>
       polyn_expr A Y (Suc 0) (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) =
         polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B\<rbrakk> \<Longrightarrow> polyn_expr A Y (Suc 0) (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) = polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B))
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule PolynRg.is_Ring[of A B Y],
       frule PolynRg.subring[of A B Y],
       frule Ring.subring_Ring[of A B], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B\<rbrakk> \<Longrightarrow> polyn_expr A Y (Suc 0) (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) = polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B))
[PROOF STEP]
apply (cut_tac special_cf_pol_coeff,
       frule ext_cf_pol_coeff[of "C\<^sub>0 S" "Suc 0"],
       frule cf_h_coeff[of A B Y h "ext_cf S (Suc 0) (C\<^sub>0 S)"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff B (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S)))\<rbrakk> \<Longrightarrow> polyn_expr A Y (Suc 0) (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) = polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B))
[PROOF STEP]
apply (frule PolynRg.special_cf_pol_coeff,
       frule PolynRg.ext_cf_pol_coeff[of A B Y "C\<^sub>0 B" "Suc 0"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff B (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))); pol_coeff B (C\<^sub>0 B); pol_coeff B (ext_cf B (Suc 0) (C\<^sub>0 B))\<rbrakk> \<Longrightarrow> polyn_expr A Y (Suc 0) (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) = polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B))
[PROOF STEP]
apply (frule PolynRg.pol_expr_unique2[of A B Y
             "cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))" "ext_cf B (Suc 0) (C\<^sub>0 B)"],
       assumption+,
       simp add:cf_h_len PolynRg.ext_cf_len,
       simp add:ext_cf_len special_cf_len PolynRg.special_cf_len,
       simp add:cf_h_len PolynRg.ext_cf_len,
       simp add:ext_cf_len special_cf_len PolynRg.special_cf_len,
       thin_tac "(polyn_expr A Y (Suc 0) (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) =
                   polyn_expr A Y (Suc 0) (ext_cf B (Suc 0) (C\<^sub>0 B))) =
                (\<forall>j\<le>Suc 0.
                  snd (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) j =
                  snd (ext_cf B (Suc 0) (C\<^sub>0 B)) j)",
       thin_tac "pol_coeff S (C\<^sub>0 S)",
       thin_tac "pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S))",
       thin_tac "pol_coeff B (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S)))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff B (C\<^sub>0 B); pol_coeff B (ext_cf B (Suc 0) (C\<^sub>0 B))\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc 0. snd (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) j = snd (ext_cf B (Suc 0) (C\<^sub>0 B)) j
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff B (C\<^sub>0 B); pol_coeff B (ext_cf B (Suc 0) (C\<^sub>0 B)); j \<le> Suc 0\<rbrakk> \<Longrightarrow> snd (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) j = snd (ext_cf B (Suc 0) (C\<^sub>0 B)) j
[PROOF STEP]
apply (case_tac "j = 0", simp add:cf_h_def cmp_def ext_cf_def sliden_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff B (C\<^sub>0 B); pol_coeff B (Suc (fst (C\<^sub>0 B)), \<lambda>i. if Suc 0 \<le> i then snd (C\<^sub>0 B) (sliden (Suc 0) i) else \<zero>\<^bsub>B\<^esub>); j = 0\<rbrakk> \<Longrightarrow> h \<zero>\<^bsub>S\<^esub> = \<zero>\<^bsub>B\<^esub>
 2. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff B (C\<^sub>0 B); pol_coeff B (ext_cf B (Suc 0) (C\<^sub>0 B)); j \<le> Suc 0; j \<noteq> 0\<rbrakk> \<Longrightarrow> snd (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) j = snd (ext_cf B (Suc 0) (C\<^sub>0 B)) j
[PROOF STEP]
apply (simp add:rHom_0_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff B (C\<^sub>0 B); pol_coeff B (ext_cf B (Suc 0) (C\<^sub>0 B)); j \<le> Suc 0; j \<noteq> 0\<rbrakk> \<Longrightarrow> snd (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) j = snd (ext_cf B (Suc 0) (C\<^sub>0 B)) j
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff B (C\<^sub>0 B); pol_coeff B (ext_cf B (Suc 0) (C\<^sub>0 B)); j \<le> Suc 0; 0 < j\<rbrakk> \<Longrightarrow> snd (cf_h h (ext_cf S (Suc 0) (C\<^sub>0 S))) j = snd (ext_cf B (Suc 0) (C\<^sub>0 B)) j
[PROOF STEP]
apply (frule_tac n = j in Suc_leI[of 0],
        frule_tac m = j and n = "Suc 0" in le_antisym, assumption+,
        thin_tac "j \<le> Suc 0", thin_tac "Suc 0 \<le> j",
        simp add:cf_h_def cmp_def ext_cf_def sliden_def special_cf_def,
        simp add:rHom_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) polyn_Hom_coeff_to_coeff:
     "\<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S c\<rbrakk>
        \<Longrightarrow>  pol_coeff B (cf_h f c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S c\<rbrakk> \<Longrightarrow> pol_coeff B (cf_h f c)
[PROOF STEP]
apply (subst pol_coeff_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S c\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (cf_h f c). snd (cf_h f c) j \<in> carrier B
[PROOF STEP]
apply (rule allI, rule impI, simp add:cf_h_len cf_h_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S c; j \<le> fst c\<rbrakk> \<Longrightarrow> cmp f (snd c) j \<in> carrier B
[PROOF STEP]
apply (frule_tac j = j in pol_coeff_mem[of c], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S c; j \<le> fst c; snd c j \<in> carrier S\<rbrakk> \<Longrightarrow> cmp f (snd c) j \<in> carrier B
[PROOF STEP]
apply (simp add:cmp_def polyn_Hom_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; pol_coeff S c; j \<le> fst c; snd c j \<in> carrier S; f \<in> rHom R A; f ` carrier S \<subseteq> carrier B; f X = Y\<rbrakk> \<Longrightarrow> f (snd c j) \<in> carrier B
[PROOF STEP]
apply (simp add:image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; pol_coeff S c; j \<le> fst c; snd c j \<in> carrier S; f \<in> rHom R A; {y. \<exists>x\<in>carrier S. y = f x} \<subseteq> carrier B; f X = Y\<rbrakk> \<Longrightarrow> f (snd c j) \<in> carrier B
[PROOF STEP]
apply (rule subsetD[of "{y. \<exists>x\<in>carrier S. y = f x}" "carrier B"], assumption,
        simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; pol_coeff S c; j \<le> fst c; snd c j \<in> carrier S; f \<in> rHom R A; {y. \<exists>x\<in>carrier S. y = f x} \<subseteq> carrier B; f X = Y\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier S. f (snd c j) = f x
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) cf_h_len1:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B;
        f \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. f x = h x; pol_coeff S c\<rbrakk> \<Longrightarrow>
        fst (cf_h f c) = fst (cf_h h c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; f \<in> pHom R S X, A B Y; \<forall>x\<in>carrier S. f x = h x; pol_coeff S c\<rbrakk> \<Longrightarrow> fst (cf_h f c) = fst (cf_h h c)
[PROOF STEP]
by (simp add:cf_h_def)


[STATEMENT]
lemma (in PolynRg) cf_h_len2:"\<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y;
          pol_coeff S c\<rbrakk> \<Longrightarrow> fst (cf_h f c) = fst c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S c\<rbrakk> \<Longrightarrow> fst (cf_h f c) = fst c
[PROOF STEP]
by (simp add:cf_h_def)


[STATEMENT]
lemma (in PolynRg) cmp_pol_coeff:"\<lbrakk>f \<in> rHom S B;
       pol_coeff S (n, c)\<rbrakk>  \<Longrightarrow> pol_coeff B (n,(cmp f c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> rHom S B; pol_coeff S (n, c)\<rbrakk> \<Longrightarrow> pol_coeff B (n, cmp f c)
[PROOF STEP]
apply (simp add:pol_coeff_def,
      rule allI, rule impI, simp add:cmp_def,
      frule_tac a = j in forall_spec, simp,
      thin_tac "\<forall>j\<le>n. c j \<in> carrier S")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>f \<in> rHom S B; j \<le> n; c j \<in> carrier S\<rbrakk> \<Longrightarrow> f (c j) \<in> carrier B
[PROOF STEP]
apply (simp add:rHom_mem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) cmp_pol_coeff_e:"\<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y;
         pol_coeff S (n, c)\<rbrakk> \<Longrightarrow> pol_coeff B (n, (cmp f c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S (n, c)\<rbrakk> \<Longrightarrow> pol_coeff B (n, cmp f c)
[PROOF STEP]
apply (subst pol_coeff_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S (n, c)\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (n, cmp f c). snd (n, cmp f c) j \<in> carrier B
[PROOF STEP]
apply (rule allI, rule impI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S (n, c); j \<le> n\<rbrakk> \<Longrightarrow> cmp f c j \<in> carrier B
[PROOF STEP]
apply (frule_tac j = j in pol_coeff_mem[of "(n, c)"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S (n, c); j \<le> n; snd (n, c) j \<in> carrier S\<rbrakk> \<Longrightarrow> cmp f c j \<in> carrier B
[PROOF STEP]
apply (simp add:polyn_Hom_def cmp_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; pol_coeff S (n, c); j \<le> n; c j \<in> carrier S; f \<in> rHom R A; f ` carrier S \<subseteq> carrier B; f X = Y\<rbrakk> \<Longrightarrow> f (c j) \<in> carrier B
[PROOF STEP]
apply (simp add:image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; pol_coeff S (n, c); j \<le> n; c j \<in> carrier S; f \<in> rHom R A; {y. \<exists>x\<in>carrier S. y = f x} \<subseteq> carrier B; f X = Y\<rbrakk> \<Longrightarrow> f (c j) \<in> carrier B
[PROOF STEP]
apply (rule_tac c = "f (c j)" in subsetD[of "{y. \<exists>x\<in>carrier S. y = f x}"
                                  "carrier B"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>PolynRg A B Y; pol_coeff S (n, c); j \<le> n; c j \<in> carrier S; f \<in> rHom R A; {y. \<exists>x\<in>carrier S. y = f x} \<subseteq> carrier B; f X = Y\<rbrakk> \<Longrightarrow> f (c j) \<in> {y. \<exists>x\<in>carrier S. y = f x}
[PROOF STEP]
apply (simp, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) cf_h_pol_coeff:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B;
      pol_coeff S (n, f)\<rbrakk> \<Longrightarrow> cf_h h (n, f) = (n, cmp h f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, f)\<rbrakk> \<Longrightarrow> cf_h h (n, f) = (n, cmp h f)
[PROOF STEP]
by (simp add:cf_h_def)


[STATEMENT]
lemma (in PolynRg) cf_h_polyn:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B;
      pol_coeff S (n, f)\<rbrakk> \<Longrightarrow>
      polyn_expr A Y n (cf_h h (n, f)) = polyn_expr A Y n (n, (cmp h f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, f)\<rbrakk> \<Longrightarrow> polyn_expr A Y n (cf_h h (n, f)) = polyn_expr A Y n (n, cmp h f)
[PROOF STEP]
apply (frule cf_h_coeff[of A B Y h "(n, f)"], assumption+,
       frule cmp_pol_coeff[of h B n f], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S (n, f); pol_coeff B (cf_h h (n, f)); pol_coeff B (n, cmp h f)\<rbrakk> \<Longrightarrow> polyn_expr A Y n (cf_h h (n, f)) = polyn_expr A Y n (n, cmp h f)
[PROOF STEP]
apply (rule PolynRg.polyn_exprs_eq[of A B Y  "cf_h h (n, f)" "(n, cmp h f)" n],
       assumption+,
       simp add:cf_h_len,
       rule allI, rule impI,
       simp add:cf_h_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pHom_rHom:"\<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow>
                                 f \<in> rHom R A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow> f \<in> rHom R A
[PROOF STEP]
by (simp add:polyn_Hom_def)


[STATEMENT]
lemma (in PolynRg) pHom_X_Y:"\<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow>
                                 f X = Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow> f X = Y
[PROOF STEP]
by (simp add:polyn_Hom_def)


[STATEMENT]
lemma (in PolynRg) pHom_memTr:"\<lbrakk>PolynRg A B Y;
      f \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow>
      \<forall>c. pol_coeff S (n, c) \<longrightarrow>
          f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y\<rbrakk> \<Longrightarrow> \<forall>c. pol_coeff S (n, c) \<longrightarrow> f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule PolynRg.is_Ring[of A B Y],
       frule PolynRg.subring[of A B Y],
       frule Ring.subring_Ring[of A B], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B\<rbrakk> \<Longrightarrow> \<forall>c. pol_coeff S (n, c) \<longrightarrow> f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B\<rbrakk> \<Longrightarrow> \<forall>c. pol_coeff S (0, c) \<longrightarrow> f (polyn_expr R X 0 (0, c)) = polyn_expr A Y 0 (0, cmp f c)
 2. \<And>n. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; \<forall>c. pol_coeff S (n, c) \<longrightarrow> f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)\<rbrakk> \<Longrightarrow> \<forall>c. pol_coeff S (Suc n, c) \<longrightarrow> f (polyn_expr R X (Suc n) (Suc n, c)) = polyn_expr A Y (Suc n) (Suc n, cmp f c)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (0, c)\<rbrakk> \<Longrightarrow> f (polyn_expr R X 0 (0, c)) = polyn_expr A Y 0 (0, cmp f c)
 2. \<And>n. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; \<forall>c. pol_coeff S (n, c) \<longrightarrow> f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)\<rbrakk> \<Longrightarrow> \<forall>c. pol_coeff S (Suc n, c) \<longrightarrow> f (polyn_expr R X (Suc n) (Suc n, c)) = polyn_expr A Y (Suc n) (Suc n, cmp f c)
[PROOF STEP]
apply (simp add:polyn_expr_def cmp_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (0, c)\<rbrakk> \<Longrightarrow> f (c 0 \<cdot>\<^sub>r 1\<^sub>r) = f (c 0) \<cdot>\<^sub>r\<^bsub>A\<^esub> 1\<^sub>r\<^bsub>A\<^esub>
 2. \<And>n. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; \<forall>c. pol_coeff S (n, c) \<longrightarrow> f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)\<rbrakk> \<Longrightarrow> \<forall>c. pol_coeff S (Suc n, c) \<longrightarrow> f (polyn_expr R X (Suc n) (Suc n, c)) = polyn_expr A Y (Suc n) (Suc n, cmp f c)
[PROOF STEP]
apply (frule_tac c = "(0, c)" and j = 0 in pol_coeff_mem,
           simp, simp,
       frule_tac x = "c 0" in mem_subring_mem_ring, assumption+,
       simp add:polyn_Hom_def, (erule conjE)+,
       frule rHom_func[of f R A],
       frule_tac x = "c 0" in funcset_mem[of f "carrier R" "carrier A"],
              assumption+,
       simp add:ring_r_one, simp add:Ring.ring_r_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; \<forall>c. pol_coeff S (n, c) \<longrightarrow> f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)\<rbrakk> \<Longrightarrow> \<forall>c. pol_coeff S (Suc n, c) \<longrightarrow> f (polyn_expr R X (Suc n) (Suc n, c)) = polyn_expr A Y (Suc n) (Suc n, cmp f c)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; \<forall>c. pol_coeff S (n, c) \<longrightarrow> f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); pol_coeff S (Suc n, c)\<rbrakk> \<Longrightarrow> f (polyn_expr R X (Suc n) (Suc n, c)) = polyn_expr A Y (Suc n) (Suc n, cmp f c)
[PROOF STEP]
apply (cut_tac n = n and f = c in pol_coeff_pre, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; \<forall>c. pol_coeff S (n, c) \<longrightarrow> f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); pol_coeff S (Suc n, c); pol_coeff S (n, c)\<rbrakk> \<Longrightarrow> f (polyn_expr R X (Suc n) (Suc n, c)) = polyn_expr A Y (Suc n) (Suc n, cmp f c)
[PROOF STEP]
apply (
       drule_tac a = c in forall_spec, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)\<rbrakk> \<Longrightarrow> f (polyn_expr R X (Suc n) (Suc n, c)) = polyn_expr A Y (Suc n) (Suc n, cmp f c)
[PROOF STEP]
apply (cut_tac n = n and c = "(Suc n, c)" in polyn_Suc, simp,
        simp del:npow_suc,
        thin_tac "polyn_expr R X (Suc n) (Suc n, c) =
           polyn_expr R X n (Suc n, c) \<plusminus> c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R (Suc n)\<^esup>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)\<rbrakk> \<Longrightarrow> f (polyn_expr R X n (Suc n, c) \<plusminus> c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y (Suc n) (Suc n, cmp f c)
[PROOF STEP]
apply (frule_tac c = "(Suc n, c)" and k = n in polyn_expr_short, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); polyn_expr R X n (Suc n, c) = polyn_expr R X n (n, snd (Suc n, c))\<rbrakk> \<Longrightarrow> f (polyn_expr R X n (Suc n, c) \<plusminus> c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y (Suc n) (Suc n, cmp f c)
[PROOF STEP]
apply (simp del:npow_suc,
       thin_tac "polyn_expr R X n (Suc n, c) = polyn_expr R X n (n, c)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)\<rbrakk> \<Longrightarrow> f (polyn_expr R X n (n, c) \<plusminus> c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y (Suc n) (Suc n, cmp f c)
[PROOF STEP]
apply (frule_tac c = "(Suc n, c)" in polyn_Hom_coeff_to_coeff[of A B Y f],
       assumption+, simp del:npow_suc add:cf_h_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); pol_coeff B (Suc n, cmp f c)\<rbrakk> \<Longrightarrow> f (polyn_expr R X n (n, c) \<plusminus> c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y (Suc n) (Suc n, cmp f c)
[PROOF STEP]
apply (frule_tac c = "(Suc n, cmp f c)" and n = n in
                  PolynRg.polyn_Suc[of A B Y], simp, simp del:npow_suc,
       thin_tac "polyn_expr A Y (Suc n) (Suc n, cmp f c) =
        polyn_expr A Y n (Suc n, cmp f c) \<plusminus>\<^bsub>A\<^esub>  cmp f c (Suc n) \<cdot>\<^sub>r\<^bsub>A\<^esub> Y^\<^bsup>A (Suc n)\<^esup>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); pol_coeff B (Suc n, cmp f c)\<rbrakk> \<Longrightarrow> f (polyn_expr R X n (n, c) \<plusminus> c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y n (Suc n, cmp f c) \<plusminus>\<^bsub>A\<^esub> cmp f c (Suc n) \<cdot>\<^sub>r\<^bsub>A\<^esub> Y^\<^bsup>A Suc n\<^esup>
[PROOF STEP]
apply (frule_tac k = n and c = "(n, c)" in polyn_mem, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); pol_coeff B (Suc n, cmp f c); polyn_expr R X n (n, c) \<in> carrier R\<rbrakk> \<Longrightarrow> f (polyn_expr R X n (n, c) \<plusminus> c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y n (Suc n, cmp f c) \<plusminus>\<^bsub>A\<^esub> cmp f c (Suc n) \<cdot>\<^sub>r\<^bsub>A\<^esub> Y^\<^bsup>A Suc n\<^esup>
[PROOF STEP]
apply (frule_tac c = "(Suc n, c)" in monomial_mem,
       drule_tac a = "Suc n" in forall_spec, simp, simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); pol_coeff B (Suc n, cmp f c); polyn_expr R X n (n, c) \<in> carrier R; c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> f (polyn_expr R X n (n, c) \<plusminus> c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y n (Suc n, cmp f c) \<plusminus>\<^bsub>A\<^esub> cmp f c (Suc n) \<cdot>\<^sub>r\<^bsub>A\<^esub> Y^\<^bsup>A Suc n\<^esup>
[PROOF STEP]
apply (frule pHom_rHom[of A B Y f], assumption+,
                                       simp del:npow_suc add:rHom_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); pol_coeff B (Suc n, cmp f c); polyn_expr R X n (n, c) \<in> carrier R; c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup> \<in> carrier R; f \<in> rHom R A\<rbrakk> \<Longrightarrow> polyn_expr A Y n (n, cmp f c) \<plusminus>\<^bsub>A\<^esub> f (c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y n (Suc n, cmp f c) \<plusminus>\<^bsub>A\<^esub> cmp f c (Suc n) \<cdot>\<^sub>r\<^bsub>A\<^esub> Y^\<^bsup>A Suc n\<^esup>
[PROOF STEP]
apply (frule_tac c = "(Suc n, c)" and j = "Suc n" in pol_coeff_mem_R, simp,
         simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); pol_coeff B (Suc n, cmp f c); polyn_expr R X n (n, c) \<in> carrier R; c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup> \<in> carrier R; f \<in> rHom R A; c (Suc n) \<in> carrier R\<rbrakk> \<Longrightarrow> polyn_expr A Y n (n, cmp f c) \<plusminus>\<^bsub>A\<^esub> f (c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y n (Suc n, cmp f c) \<plusminus>\<^bsub>A\<^esub> cmp f c (Suc n) \<cdot>\<^sub>r\<^bsub>A\<^esub> Y^\<^bsup>A Suc n\<^esup>
[PROOF STEP]
apply (cut_tac X_mem_R,
       frule_tac n = "Suc n" in npClose[of X],
       cut_tac Ring,
       subst rHom_tOp[of R A _ _ f], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); pol_coeff B (Suc n, cmp f c); polyn_expr R X n (n, c) \<in> carrier R; c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup> \<in> carrier R; f \<in> rHom R A; c (Suc n) \<in> carrier R; X \<in> carrier R; X^\<^bsup>R Suc n\<^esup> \<in> carrier R; Ring R\<rbrakk> \<Longrightarrow> polyn_expr A Y n (n, cmp f c) \<plusminus>\<^bsub>A\<^esub> f (c (Suc n)) \<cdot>\<^sub>r\<^bsub>A\<^esub> f (X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y n (Suc n, cmp f c) \<plusminus>\<^bsub>A\<^esub> cmp f c (Suc n) \<cdot>\<^sub>r\<^bsub>A\<^esub> Y^\<^bsup>A Suc n\<^esup>
[PROOF STEP]
apply (frule_tac c = "(Suc n, cmp f c)" and k = n in
        PolynRg.polyn_expr_short[of A B Y], assumption+, simp,
        simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); pol_coeff B (Suc n, cmp f c); polyn_expr R X n (n, c) \<in> carrier R; c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup> \<in> carrier R; f \<in> rHom R A; c (Suc n) \<in> carrier R; X \<in> carrier R; X^\<^bsup>R Suc n\<^esup> \<in> carrier R; Ring R; polyn_expr A Y n (Suc n, cmp f c) = polyn_expr A Y n (n, cmp f c)\<rbrakk> \<Longrightarrow> polyn_expr A Y n (n, cmp f c) \<plusminus>\<^bsub>A\<^esub> f (c (Suc n)) \<cdot>\<^sub>r\<^bsub>A\<^esub> f (X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y n (n, cmp f c) \<plusminus>\<^bsub>A\<^esub> cmp f c (Suc n) \<cdot>\<^sub>r\<^bsub>A\<^esub> Y^\<^bsup>A Suc n\<^esup>
[PROOF STEP]
apply (cut_tac c = "(Suc n, cmp f c)" and n = n in
        PolynRg.pol_coeff_le[of A B Y], assumption+, simp,
        simp del:npow_suc add:PolynRg.pol_coeff_le[of A B Y])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; Subring R S; Ring S; Ring A; Subring A B; Ring B; pol_coeff S (Suc n, c); pol_coeff S (n, c); f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c); pol_coeff B (Suc n, cmp f c); polyn_expr R X n (n, c) \<in> carrier R; c (Suc n) \<cdot>\<^sub>r X^\<^bsup>R Suc n\<^esup> \<in> carrier R; f \<in> rHom R A; c (Suc n) \<in> carrier R; X \<in> carrier R; X^\<^bsup>R Suc n\<^esup> \<in> carrier R; Ring R; polyn_expr A Y n (Suc n, cmp f c) = polyn_expr A Y n (n, cmp f c); pol_coeff B (n, cmp f c)\<rbrakk> \<Longrightarrow> polyn_expr A Y n (n, cmp f c) \<plusminus>\<^bsub>A\<^esub> f (c (Suc n)) \<cdot>\<^sub>r\<^bsub>A\<^esub> f (X^\<^bsup>R Suc n\<^esup>) = polyn_expr A Y n (n, cmp f c) \<plusminus>\<^bsub>A\<^esub> cmp f c (Suc n) \<cdot>\<^sub>r\<^bsub>A\<^esub> Y^\<^bsup>A Suc n\<^esup>
[PROOF STEP]
apply (subst rHom_npow[of R A X f], assumption+,
       simp del:npow_suc add:pHom_X_Y cmp_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pHom_mem:"\<lbrakk>PolynRg A B Y;
      f \<in> pHom R S X, A B Y; pol_coeff S (n, c)\<rbrakk> \<Longrightarrow>
      f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S (n, c)\<rbrakk> \<Longrightarrow> f (polyn_expr R X n (n, c)) = polyn_expr A Y n (n, cmp f c)
[PROOF STEP]
apply (simp add:pHom_memTr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pHom_memc:"\<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y;
      pol_coeff S c\<rbrakk> \<Longrightarrow>
      f (polyn_expr R X (fst c) c) = polyn_expr A Y (fst c) (cf_h f c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; pol_coeff S c\<rbrakk> \<Longrightarrow> f (polyn_expr R X (fst c) c) = polyn_expr A Y (fst c) (cf_h f c)
[PROOF STEP]
by (cases c) (simp add: cf_h_def pHom_mem)


[STATEMENT]
lemma (in PolynRg) pHom_mem1:"\<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y;
       p \<in> carrier R\<rbrakk> \<Longrightarrow>  f p \<in> carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R\<rbrakk> \<Longrightarrow> f p \<in> carrier A
[PROOF STEP]
apply (simp add:polyn_Hom_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; p \<in> carrier R; f \<in> rHom R A; f ` carrier S \<subseteq> carrier B; f X = Y\<rbrakk> \<Longrightarrow> f p \<in> carrier A
[PROOF STEP]
apply (simp add:rHom_mem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pHom_pol_mem:"\<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y;
      p \<in> carrier R; p \<noteq> \<zero>\<rbrakk>  \<Longrightarrow>
      f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p))
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> f p = polyn_expr A Y (deg_n R S X p) (cf_h f (s_cf R S X p))
[PROOF STEP]
apply (subst s_cf_deg[of p], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> f p = polyn_expr A Y (fst (s_cf R S X p)) (cf_h f (s_cf R S X p))
[PROOF STEP]
apply (subst pHom_memc[THEN sym, of A B Y f], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; f \<in> pHom R S X, A B Y; p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> f p = f (polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p))
[PROOF STEP]
apply (drule sym, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) erh_rHom_coeff:"\<lbrakk>PolynRg A B Y; h \<in> rHom S B;
       pol_coeff S c\<rbrakk>  \<Longrightarrow>  erh R S X A B Y h 0 c = (cmp h (snd c)) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c\<rbrakk> \<Longrightarrow> erh R S X A B Y h 0 c = cmp h (snd c) 0
[PROOF STEP]
apply (cut_tac subring,
       frule subring_Ring,
       frule PolynRg.is_Ring[of A B Y],
       frule PolynRg.subring[of A B Y],
       frule Ring.subring_Ring[of A B], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; Subring R S; Ring S; Ring A; Subring A B; Ring B\<rbrakk> \<Longrightarrow> erh R S X A B Y h 0 c = cmp h (snd c) 0
[PROOF STEP]
apply (simp add:erh_def polyn_expr_def cf_h_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; Subring R S; Ring S; Ring A; Subring A B; Ring B\<rbrakk> \<Longrightarrow> cmp h (snd c) 0 \<cdot>\<^sub>r\<^bsub>A\<^esub> 1\<^sub>r\<^bsub>A\<^esub> = cmp h (snd c) 0
[PROOF STEP]
apply (frule pol_coeff_mem [of c 0], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; Subring R S; Ring S; Ring A; Subring A B; Ring B; snd c 0 \<in> carrier S\<rbrakk> \<Longrightarrow> cmp h (snd c) 0 \<cdot>\<^sub>r\<^bsub>A\<^esub> 1\<^sub>r\<^bsub>A\<^esub> = cmp h (snd c) 0
[PROOF STEP]
apply (simp add:cmp_def, frule rHom_mem[of h S B "snd c 0"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PolynRg A B Y; h \<in> rHom S B; pol_coeff S c; Subring R S; Ring S; Ring A; Subring A B; Ring B; snd c 0 \<in> carrier S; h (snd c 0) \<in> carrier B\<rbrakk> \<Longrightarrow> h (snd c 0) \<cdot>\<^sub>r\<^bsub>A\<^esub> 1\<^sub>r\<^bsub>A\<^esub> = h (snd c 0)
[PROOF STEP]
apply (frule Ring.mem_subring_mem_ring[of A B "h (snd c 0)"], assumption+,
        simp add:Ring.ring_r_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done