[STATEMENT]
lemma (in PolynRg) pol_of_deg0:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk>
      \<Longrightarrow>  (deg_n 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_n R S X p = 0) = (p \<in> carrier S)
[PROOF STEP]
apply (cut_tac subring,
       frule subring_Ring,
       cut_tac ring_is_ag,
       frule Ring.ring_is_ag[of S])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S\<rbrakk> \<Longrightarrow> (deg_n R S X p = 0) = (p \<in> carrier S)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; deg_n R S X p = 0\<rbrakk> \<Longrightarrow> p \<in> carrier S
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier S\<rbrakk> \<Longrightarrow> deg_n R S X p = 0
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; deg_n R S X p = 0; pol_coeff S (s_cf R S X p) \<and> p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) \<and> snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> p \<in> carrier S
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier S\<rbrakk> \<Longrightarrow> deg_n R S X p = 0
[PROOF STEP]
apply (simp add:s_cf_deg, (erule conjE)+, simp add:polyn_expr_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; fst (s_cf R S X p) = 0; pol_coeff S (s_cf R S X p); p = snd (s_cf R S X p) 0 \<cdot>\<^sub>r 1\<^sub>r; snd (s_cf R S X p) 0 \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> p \<in> carrier S
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier S\<rbrakk> \<Longrightarrow> deg_n R S X p = 0
[PROOF STEP]
apply (frule pol_coeff_mem[of "s_cf R S X p" 0], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; fst (s_cf R S X p) = 0; pol_coeff S (s_cf R S X p); p = snd (s_cf R S X p) 0 \<cdot>\<^sub>r 1\<^sub>r; snd (s_cf R S X p) 0 \<noteq> \<zero>\<^bsub>S\<^esub>; snd (s_cf R S X p) 0 \<in> carrier S\<rbrakk> \<Longrightarrow> p \<in> carrier S
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier S\<rbrakk> \<Longrightarrow> deg_n R S X p = 0
[PROOF STEP]
apply (cut_tac mem_subring_mem_ring[of S "snd (s_cf R S X p) 0"],
        simp add:ring_r_one, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier S\<rbrakk> \<Longrightarrow> deg_n R S X p = 0
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption+, (erule conjE)+,
       simp add:s_cf_deg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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> fst (s_cf R S X p) = 0
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "pol_coeff S (0, (\<lambda>j. p)) \<and>
                      p = polyn_expr R X 0 (0, (\<lambda>j. p))", erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p); pol_coeff S (0, \<lambda>j. p); p = polyn_expr R X 0 (0, \<lambda>j. p)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (cut_tac a = "polyn_expr R X 0 (0, \<lambda>j. p)" and
               b = "polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)" in
               aGroup.ag_eq_diffzero[of R],  assumption+, simp, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p); pol_coeff S (0, \<lambda>j. p); p = polyn_expr R X 0 (0, \<lambda>j. p); (polyn_expr R X 0 (0, \<lambda>j. p) = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)) = (polyn_expr R X 0 (0, \<lambda>j. p) \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = \<zero>)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (frule_tac c = "polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)" in
         box_equation[of p "polyn_expr R X 0 (0, \<lambda>j. p)"], assumption,
        thin_tac "p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)",
        thin_tac "p = polyn_expr R X 0 (0, \<lambda>j. p)", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p); pol_coeff S (0, \<lambda>j. p); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) = \<zero>; polyn_expr R X 0 (0, \<lambda>j. p) = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (simp only:polyn_minus_m_cf)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p); pol_coeff S (0, \<lambda>j. p); polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) \<plusminus> polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p)) = \<zero>; polyn_expr R X 0 (0, \<lambda>j. p) = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (rotate_tac -2, drule sym, simp,
        thin_tac "polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) =
                 polyn_expr R X 0 (0, \<lambda>j. p)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>polyn_expr R X 0 (0, \<lambda>j. p) \<plusminus> polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p)) = \<zero>; p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p); pol_coeff S (0, \<lambda>j. p)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (frule_tac c = "s_cf R S X p" in m_cf_pol_coeff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>polyn_expr R X 0 (0, \<lambda>j. p) \<plusminus> polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p)) = \<zero>; p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p); pol_coeff S (0, \<lambda>j. p); pol_coeff S (m_cf S (s_cf R S X p))\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (frule_tac d = "m_cf S (s_cf R S X p)" in polyn_add1[of "(0, \<lambda>j. p)"],
        assumption,
        simp add:m_cf_len,
        thin_tac "polyn_expr R X 0 (0, \<lambda>j. p) \<plusminus>
     polyn_expr R X (fst (s_cf R S X p)) (m_cf S (s_cf R S X p)) =
     polyn_expr R X (fst (s_cf R S X p))
      (add_cf S (0, \<lambda>j. p) (m_cf S (s_cf R S X p)))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> polyn_expr R X (fst (s_cf R S X p)) (add_cf S (0, \<lambda>j. p) (m_cf S (s_cf R S X p))); Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p); pol_coeff S (0, \<lambda>j. p); pol_coeff S (m_cf S (s_cf R S X p)); \<zero> = polyn_expr R X (fst (s_cf R S X p)) (add_cf S (0, \<lambda>j. p) (m_cf S (s_cf R S X p)))\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (rotate_tac -1, drule sym, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p); pol_coeff S (0, \<lambda>j. p); pol_coeff S (m_cf S (s_cf R S X p)); polyn_expr R X (fst (s_cf R S X p)) (add_cf S (0, \<lambda>j. p) (m_cf S (s_cf R S X p))) = \<zero>\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (frule_tac d = "m_cf S (s_cf R S X p)" in
                      add_cf_pol_coeff[of "(0, \<lambda>j. p)"], assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p); pol_coeff S (0, \<lambda>j. p); pol_coeff S (m_cf S (s_cf R S X p)); polyn_expr R X (fst (s_cf R S X p)) (add_cf S (0, \<lambda>j. p) (m_cf S (s_cf R S X p))) = \<zero>; pol_coeff S (add_cf S (0, \<lambda>j. p) (m_cf S (s_cf R S X p)))\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (frule_tac c1 = "add_cf S (0, \<lambda>j. p) (m_cf S (s_cf R S X p))" and
        k1 = "fst (s_cf R S X p)" in
         coeff_0_pol_0[THEN sym],
       simp add:add_cf_len m_cf_len, simp,
       thin_tac "pol_coeff S (add_cf S (0, \<lambda>j. p) (m_cf S (s_cf R S X p)))",
       thin_tac "polyn_expr R X (fst (s_cf R S X p))
      (add_cf S (0, \<lambda>j. p) (m_cf S (s_cf R S X p))) = \<zero>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p); pol_coeff S (0, \<lambda>j. p); pol_coeff S (m_cf S (s_cf R S X p)); \<forall>j\<le>fst (s_cf R S X p). snd (add_cf S (0, \<lambda>j. p) (m_cf S (s_cf R S X p))) j = \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (drule_tac a = "fst (s_cf R S X p)" in forall_spec, simp,
        simp add:add_cf_def m_cf_len m_cf_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p); pol_coeff S (0, \<lambda>j. p); pol_coeff S (fst (s_cf R S X p), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (s_cf R S X p) j); -\<^sub>a\<^bsub>S\<^esub> snd (s_cf R S X p) (fst (s_cf R S X p)) = \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (frule_tac c = "s_cf R S X p" and j = "fst (s_cf R S X p)" in
        pol_coeff_mem, simp,
        frule_tac x = "snd (s_cf R S X p) (fst (s_cf R S X p))" in
        aGroup.ag_inv_inv[of S],
        assumption, simp add:aGroup.ag_inv_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p) \<and> p = polyn_expr R X 0 (0, \<lambda>j. p)
[PROOF STEP]
apply (subst polyn_expr_def, simp add:ring_r_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; Subring R S; Ring S; aGroup R; aGroup S; p \<in> carrier 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>; 0 < fst (s_cf R S X p)\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. p)
[PROOF STEP]
apply (simp add:pol_coeff_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pols_const:"\<lbrakk>p \<in> carrier R; (deg R S X p) \<le> 0\<rbrakk>  \<Longrightarrow>
                         p \<in> carrier S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> 0\<rbrakk> \<Longrightarrow> p \<in> carrier S
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> 0; p = \<zero>\<rbrakk> \<Longrightarrow> p \<in> carrier S
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> 0; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> p \<in> carrier S
[PROOF STEP]
apply (cut_tac subring)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> 0; p = \<zero>; Subring R S\<rbrakk> \<Longrightarrow> p \<in> carrier S
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> 0; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> p \<in> carrier S
[PROOF STEP]
apply (frule Subring_zero_ring_zero[THEN sym, of S], simp,
       cut_tac subring,
       frule subring_Ring[of S],
       rule Ring.ring_zero[of S], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> 0; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> p \<in> carrier S
[PROOF STEP]
apply (subst pol_of_deg0[THEN sym], assumption+,
       simp add:deg_def,
       simp only:an_0[THEN sym],
       simp add:an_inj)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) less_deg_add_nonzero:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>;
       q \<in> carrier R; q \<noteq> \<zero>;
       (deg_n R S X p) < (deg_n R S X q)\<rbrakk>  \<Longrightarrow> p \<plusminus> q \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; deg_n R S X p < deg_n R S X q\<rbrakk> \<Longrightarrow> p \<plusminus> q \<noteq> \<zero>
[PROOF STEP]
apply (frule ex_polyn_expr[of p], erule exE, erule conjE,
       frule ex_polyn_expr[of q], erule exE, erule conjE,
       rename_tac c d)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; deg_n R S X p < deg_n R S X q; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d\<rbrakk> \<Longrightarrow> p \<plusminus> q \<noteq> \<zero>
[PROOF STEP]
apply (frule_tac c = c in pol_deg_eq_c_max[of p], assumption+,
       frule_tac c = d in pol_deg_eq_c_max[of q], assumption+,
       frule_tac c = c in coeff_max_bddTr,
       frule_tac c = d in coeff_max_bddTr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; deg_n R S X p < deg_n R S X q; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d; deg_n R S X p = c_max S c; deg_n R S X q = c_max S d; c_max S c \<le> fst c; c_max S d \<le> fst d\<rbrakk> \<Longrightarrow> p \<plusminus> q \<noteq> \<zero>
[PROOF STEP]
apply (frule_tac c = c and n = "c_max S c" in pol_coeff_le, assumption,
       frule_tac c = d and n = "c_max S d" in pol_coeff_le, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; deg_n R S X p < deg_n R S X q; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d; deg_n R S X p = c_max S c; deg_n R S X q = c_max S d; c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d)\<rbrakk> \<Longrightarrow> p \<plusminus> q \<noteq> \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; polyn_expr R X (fst d) d \<in> carrier R; polyn_expr R X (fst d) d \<noteq> \<zero>; c_max S c < c_max S d; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d; deg_n R S X (polyn_expr R X (fst c) c) = c_max S c; deg_n R S X (polyn_expr R X (fst d) d) = c_max S d; c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d)\<rbrakk> \<Longrightarrow> polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d \<noteq> \<zero>
[PROOF STEP]
apply (subst polyn_c_max, assumption,
       subst polyn_c_max, assumption,
       subst polyn_expr_short, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; polyn_expr R X (fst d) d \<in> carrier R; polyn_expr R X (fst d) d \<noteq> \<zero>; c_max S c < c_max S d; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d; deg_n R S X (polyn_expr R X (fst c) c) = c_max S c; deg_n R S X (polyn_expr R X (fst d) d) = c_max S d; c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d)\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S c) (c_max S c, snd c) \<plusminus> polyn_expr R X (c_max S d) d \<noteq> \<zero>
[PROOF STEP]
apply (frule_tac c = d and k = "c_max S d" in polyn_expr_short, assumption+,
       simp,
       thin_tac "polyn_expr R X (c_max S d) d =
           polyn_expr R X (c_max S d) (c_max S d, snd d)",
       thin_tac "deg_n R S X (polyn_expr R X (fst c) c) = c_max S c",
       thin_tac "deg_n R S X (polyn_expr R X (fst d) d) = c_max S d")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; polyn_expr R X (fst d) d \<in> carrier R; polyn_expr R X (fst d) d \<noteq> \<zero>; c_max S c < c_max S d; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d; c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d)\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S c) (c_max S c, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>
[PROOF STEP]
apply (subst polyn_add, assumption+, simp add: max.absorb1 max.absorb2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; polyn_expr R X (fst d) d \<in> carrier R; polyn_expr R X (fst d) d \<noteq> \<zero>; c_max S c < c_max S d; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d; c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d)\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)) \<noteq> \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+,
         frule_tac c = "(c_max S c, snd c)" and d = "(c_max S d, snd d)" in
         add_cf_pol_coeff, assumption+,
         frule_tac c1 = "add_cf S (c_max S c, snd c) (c_max S d, snd d)" and
         k1 = "c_max S d" in coeff_0_pol_0[THEN sym],
         simp add:add_cf_len, simp,
       thin_tac "pol_coeff S (add_cf S (c_max S c, snd c) (c_max S d, snd d))",
       thin_tac "polyn_expr R X (c_max S d)
            (add_cf S (c_max S c, snd c) (c_max S d, snd d)) = \<zero>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; polyn_expr R X (fst d) d \<in> carrier R; polyn_expr R X (fst d) d \<noteq> \<zero>; c_max S c < c_max S d; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d; c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d); \<forall>j\<le>c_max S d. snd (add_cf S (c_max S c, snd c) (c_max S d, snd d)) j = \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac a = "c_max S d" in forall_spec, simp,
         simp add:add_cf_def,
         frule_tac c = d and k = "fst d" in coeff_nonzero_polyn_nonzero,
         simp, simp,
         frule_tac c = d in coeff_max_nonzeroTr, assumption+, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) polyn_deg_add1:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R;
      q \<noteq> \<zero>; (deg_n R S X p) < (deg_n R S X q)\<rbrakk>  \<Longrightarrow>
            deg_n R S X (p \<plusminus> q) = (deg_n R S X q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; deg_n R S X p < deg_n R S X q\<rbrakk> \<Longrightarrow> deg_n R S X (p \<plusminus> q) = deg_n R S X q
[PROOF STEP]
apply (cut_tac subring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; deg_n R S X p < deg_n R S X q; Subring R S\<rbrakk> \<Longrightarrow> deg_n R S X (p \<plusminus> q) = deg_n R S X q
[PROOF STEP]
apply (frule less_deg_add_nonzero[of p q], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; deg_n R S X p < deg_n R S X q; Subring R S; p \<plusminus> q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg_n R S X (p \<plusminus> q) = deg_n R S X q
[PROOF STEP]
apply (frule ex_polyn_expr[of p], erule exE, erule conjE,
       frule ex_polyn_expr[of q], erule exE, erule conjE,
       rename_tac c d)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; deg_n R S X p < deg_n R S X q; Subring R S; p \<plusminus> q \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d\<rbrakk> \<Longrightarrow> deg_n R S X (p \<plusminus> q) = deg_n R S X q
[PROOF STEP]
apply (simp only:pol_deg_eq_c_max)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; polyn_expr R X (fst d) d \<in> carrier R; polyn_expr R X (fst d) d \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d) = c_max S d
[PROOF STEP]
apply (frule_tac c = c in coeff_max_bddTr,
       frule_tac c = d in coeff_max_bddTr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; polyn_expr R X (fst d) d \<in> carrier R; polyn_expr R X (fst d) d \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d; c_max S c \<le> fst c; c_max S d \<le> fst d\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d) = c_max S d
[PROOF STEP]
apply (frule_tac c = c and n = "c_max S c" in pol_coeff_le, assumption,
       frule_tac c = d and n = "c_max S d" in pol_coeff_le, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; polyn_expr R X (fst d) d \<in> carrier R; polyn_expr R X (fst d) d \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d; c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d) = c_max S d
[PROOF STEP]
apply (simp add:polyn_c_max)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S c) c \<in> carrier R; polyn_expr R X (c_max S c) c \<noteq> \<zero>; polyn_expr R X (c_max S d) d \<in> carrier R; polyn_expr R X (c_max S d) d \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (c_max S c) c \<plusminus> polyn_expr R X (c_max S d) d \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (c_max S c) c; pol_coeff S d; q = polyn_expr R X (c_max S d) d; c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S c) c \<plusminus> polyn_expr R X (c_max S d) d) = c_max S d
[PROOF STEP]
apply (frule_tac c = c and k = "c_max S c" in polyn_expr_short, simp,
       frule_tac c = d and k = "c_max S d" in polyn_expr_short, simp,
       simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S c) (c_max S c, snd c) \<in> carrier R; polyn_expr R X (c_max S c) (c_max S c, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (c_max S c) (c_max S c, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (c_max S c) (c_max S c, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d); polyn_expr R X (c_max S c) c = polyn_expr R X (c_max S c) (c_max S c, snd c); polyn_expr R X (c_max S d) d = polyn_expr R X (c_max S d) (c_max S d, snd d)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S c) (c_max S c, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d)) = c_max S d
[PROOF STEP]
apply (frule_tac c = "(c_max S c, snd c)" and d = "(c_max S d, snd d)" in
         polyn_add1, assumption+, simp,
        thin_tac "polyn_expr R X (c_max S c) c =
           polyn_expr R X (c_max S c) (c_max S c, snd c)",
        thin_tac "polyn_expr R X (c_max S d) d =
           polyn_expr R X (c_max S d) (c_max S d, snd d)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S c) (c_max S c, snd c) \<in> carrier R; polyn_expr R X (c_max S c) (c_max S c, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)) \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (c_max S c) (c_max S c, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d); polyn_expr R X (c_max S c) (c_max S c, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d) = polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d))) = c_max S d
[PROOF STEP]
apply (frule_tac c = "(c_max S c, snd c)" and d = "(c_max S d, snd d)" in
                  add_cf_pol_coeff, assumption+,
         rule_tac p = "polyn_expr R X (c_max S d)
            (add_cf S (c_max S c, snd c) (c_max S d, snd d))" and
          c = "add_cf S (c_max S c, snd c) (c_max S d, snd d)" and
          n = "c_max S d" in pol_deg_n)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S c) (c_max S c, snd c) \<in> carrier R; polyn_expr R X (c_max S c) (c_max S c, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)) \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (c_max S c) (c_max S c, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d); polyn_expr R X (c_max S c) (c_max S c, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d) = polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)); pol_coeff S (add_cf S (c_max S c, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)) \<in> carrier R
 2. \<And>c d. \<lbrakk>polyn_expr R X (c_max S c) (c_max S c, snd c) \<in> carrier R; polyn_expr R X (c_max S c) (c_max S c, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)) \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (c_max S c) (c_max S c, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d); polyn_expr R X (c_max S c) (c_max S c, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d) = polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)); pol_coeff S (add_cf S (c_max S c, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (c_max S c, snd c) (c_max S d, snd d))
 3. \<And>c d. \<lbrakk>polyn_expr R X (c_max S c) (c_max S c, snd c) \<in> carrier R; polyn_expr R X (c_max S c) (c_max S c, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)) \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (c_max S c) (c_max S c, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d); polyn_expr R X (c_max S c) (c_max S c, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d) = polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)); pol_coeff S (add_cf S (c_max S c, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> c_max S d \<le> fst (add_cf S (c_max S c, snd c) (c_max S d, snd d))
 4. \<And>c d. \<lbrakk>polyn_expr R X (c_max S c) (c_max S c, snd c) \<in> carrier R; polyn_expr R X (c_max S c) (c_max S c, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)) \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (c_max S c) (c_max S c, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d); polyn_expr R X (c_max S c) (c_max S c, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d) = polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)); pol_coeff S (add_cf S (c_max S c, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)) = polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d))
 5. \<And>c d. \<lbrakk>polyn_expr R X (c_max S c) (c_max S c, snd c) \<in> carrier R; polyn_expr R X (c_max S c) (c_max S c, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)) \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (c_max S c) (c_max S c, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d); polyn_expr R X (c_max S c) (c_max S c, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d) = polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)); pol_coeff S (add_cf S (c_max S c, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> snd (add_cf S (c_max S c, snd c) (c_max S d, snd d)) (c_max S d) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (rule_tac polyn_mem, simp, simp add:add_cf_len,
         assumption,
         simp add:add_cf_len, simp,
         subst add_cf_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S c) (c_max S c, snd c) \<in> carrier R; polyn_expr R X (c_max S c) (c_max S c, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; c_max S c < c_max S d; Subring R S; polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)) \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (c_max S c) (c_max S c, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d); polyn_expr R X (c_max S c) (c_max S c, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d) = polyn_expr R X (c_max S d) (add_cf S (c_max S c, snd c) (c_max S d, snd d)); pol_coeff S (add_cf S (c_max S c, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> snd d (c_max S d) \<noteq> \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (frule_tac c1 = "(c_max S d, snd d)" and k1 = "c_max S d" in
         coeff_0_pol_0[THEN sym], simp, simp,
         rule coeff_max_nonzeroTr, assumption+,
         erule exE, erule conjE,
         frule_tac i = j and j = "c_max S d" and k = "fst d" in
                le_trans, assumption+, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) polyn_deg_add2:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R;
      q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; (deg_n R S X p) = (deg_n R S X q)\<rbrakk>  \<Longrightarrow>
          deg_n R S X (p \<plusminus> q) \<le> (deg_n R S X q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; deg_n R S X p = deg_n R S X q\<rbrakk> \<Longrightarrow> deg_n R S X (p \<plusminus> q) \<le> deg_n R S X q
[PROOF STEP]
apply (cut_tac subring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; deg_n R S X p = deg_n R S X q; Subring R S\<rbrakk> \<Longrightarrow> deg_n R S X (p \<plusminus> q) \<le> deg_n R S X q
[PROOF STEP]
apply (frule ex_polyn_expr[of p], erule exE, erule conjE,
       frule ex_polyn_expr[of q], erule exE, erule conjE,
       rename_tac c d)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; q \<in> carrier R; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; deg_n R S X p = deg_n R S X q; Subring R S; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d\<rbrakk> \<Longrightarrow> deg_n R S X (p \<plusminus> q) \<le> deg_n R S X q
[PROOF STEP]
apply (simp only:pol_deg_eq_c_max)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; polyn_expr R X (fst d) d \<in> carrier R; polyn_expr R X (fst d) d \<noteq> \<zero>; polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d) \<le> c_max S d
[PROOF STEP]
apply (frule_tac c = c in coeff_max_bddTr,
       frule_tac c = d in coeff_max_bddTr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; polyn_expr R X (fst d) d \<in> carrier R; polyn_expr R X (fst d) d \<noteq> \<zero>; polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d; c_max S c \<le> fst c; c_max S d \<le> fst d\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d) \<le> c_max S d
[PROOF STEP]
apply (frule_tac c = c and n = "c_max S c" in pol_coeff_le, assumption,
       frule_tac c = d and n = "c_max S d" in pol_coeff_le, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; polyn_expr R X (fst d) d \<in> carrier R; polyn_expr R X (fst d) d \<noteq> \<zero>; polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (fst c) c; pol_coeff S d; q = polyn_expr R X (fst d) d; c_max S c \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S c, snd c); pol_coeff S (c_max S d, snd d)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (fst c) c \<plusminus> polyn_expr R X (fst d) d) \<le> c_max S d
[PROOF STEP]
apply (simp add:polyn_c_max)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) c \<in> carrier R; polyn_expr R X (c_max S d) c \<noteq> \<zero>; polyn_expr R X (c_max S d) d \<in> carrier R; polyn_expr R X (c_max S d) d \<noteq> \<zero>; polyn_expr R X (c_max S d) c \<plusminus> polyn_expr R X (c_max S d) d \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) c; pol_coeff S d; q = polyn_expr R X (c_max S d) d; c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S d) c \<plusminus> polyn_expr R X (c_max S d) d) \<le> c_max S d
[PROOF STEP]
apply (frule_tac c = c and k = "c_max S c" in polyn_expr_short, simp,
       frule_tac c = d and k = "c_max S d" in polyn_expr_short, simp,
       simp,
       frule_tac c = "(c_max S d, snd c)" and d = "(c_max S d, snd d)" in
         polyn_add1, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); polyn_expr R X (c_max S d) c = polyn_expr R X (c_max S d) (c_max S d, snd c); polyn_expr R X (c_max S d) d = polyn_expr R X (c_max S d) (c_max S d, snd d); polyn_expr R X (fst (c_max S d, snd c)) (c_max S d, snd c) \<plusminus> polyn_expr R X (fst (c_max S d, snd d)) (c_max S d, snd d) = polyn_expr R X (max (fst (c_max S d, snd c)) (fst (c_max S d, snd d))) (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S d) (c_max S d, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d)) \<le> c_max S d
[PROOF STEP]
apply (thin_tac "polyn_expr R X (c_max S d) d =
           polyn_expr R X (c_max S d) (c_max S d, snd d)",
        thin_tac "polyn_expr R X (c_max S d) c =
           polyn_expr R X (c_max S d) (c_max S d, snd c)", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); polyn_expr R X (c_max S d) (c_max S d, snd c) \<plusminus> polyn_expr R X (c_max S d) (c_max S d, snd d) = polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d))) \<le> c_max S d
[PROOF STEP]
apply (thin_tac "polyn_expr R X (c_max S d) (c_max S d, snd c) \<plusminus>
           polyn_expr R X (c_max S d) (c_max S d, snd d) =
           polyn_expr R X (c_max S d)
            (add_cf S (c_max S d, snd c) (c_max S d, snd d))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d))) \<le> c_max S d
[PROOF STEP]
apply (frule_tac c = "(c_max S d, snd c)" and d = "(c_max S d, snd d)" in
                  add_cf_pol_coeff, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d))) \<le> c_max S d
[PROOF STEP]
apply (cut_tac p = "polyn_expr R X (c_max S d)
                (add_cf S (c_max S d, snd c) (c_max S d, snd d))"
        and c = "add_cf S (c_max S d, snd c) (c_max S d, snd d)" in
        pol_deg_eq_c_max)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<in> carrier R
 2. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d))
 3. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) = polyn_expr R X (fst (add_cf S (c_max S d, snd c) (c_max S d, snd d))) (add_cf S (c_max S d, snd c) (c_max S d, snd d))
 4. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d)); deg_n R S X (polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d))) = c_max S (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d))) \<le> c_max S d
[PROOF STEP]
apply (rule_tac polyn_mem, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> c_max S d \<le> fst (add_cf S (c_max S d, snd c) (c_max S d, snd d))
 2. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d))
 3. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) = polyn_expr R X (fst (add_cf S (c_max S d, snd c) (c_max S d, snd d))) (add_cf S (c_max S d, snd c) (c_max S d, snd d))
 4. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d)); deg_n R S X (polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d))) = c_max S (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d))) \<le> c_max S d
[PROOF STEP]
apply (simp add:add_cf_len,
              assumption,
             simp add:add_cf_len, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d)); deg_n R S X (polyn_expr R X (c_max S d) (add_cf S (c_max S d, snd c) (c_max S d, snd d))) = c_max S (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> c_max S (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<le> c_max S d
[PROOF STEP]
apply (thin_tac "deg_n R S X
            (polyn_expr R X (c_max S d)
              (add_cf S (c_max S d, snd c) (c_max S d, snd d))) =
           c_max S (add_cf S (c_max S d, snd c) (c_max S d, snd d))",
             thin_tac "polyn_expr R X (c_max S d)
            (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<noteq>
           \<zero>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> c_max S (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<le> c_max S d
[PROOF STEP]
apply (frule_tac c = "add_cf S (c_max S d, snd c) (c_max S d, snd d)" in
         coeff_max_bddTr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c d. \<lbrakk>polyn_expr R X (c_max S d) (c_max S d, snd c) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd c) \<noteq> \<zero>; polyn_expr R X (c_max S d) (c_max S d, snd d) \<in> carrier R; polyn_expr R X (c_max S d) (c_max S d, snd d) \<noteq> \<zero>; c_max S c = c_max S d; Subring R S; pol_coeff S c; p = polyn_expr R X (c_max S d) (c_max S d, snd c); pol_coeff S d; q = polyn_expr R X (c_max S d) (c_max S d, snd d); c_max S d \<le> fst c; c_max S d \<le> fst d; pol_coeff S (c_max S d, snd c); pol_coeff S (c_max S d, snd d); pol_coeff S (add_cf S (c_max S d, snd c) (c_max S d, snd d)); c_max S (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<le> fst (add_cf S (c_max S d, snd c) (c_max S d, snd d))\<rbrakk> \<Longrightarrow> c_max S (add_cf S (c_max S d, snd c) (c_max S d, snd d)) \<le> c_max S d
[PROOF STEP]
apply (simp add:add_cf_len)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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


[STATEMENT]
lemma (in PolynRg) polyn_deg_add4:"\<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 (cut_tac ring_is_ag)
[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; aGroup R\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> an n
[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 \<le> an n; deg R S X q \<le> an n; aGroup R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> an n
[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 \<le> an n; deg R S X q \<le> an n; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> an n
[PROOF STEP]
apply (case_tac "p \<plusminus>\<^bsub>R\<^esub> q = \<zero>\<^bsub>R\<^esub>", simp add:deg_def)
[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; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> an n
[PROOF STEP]
apply (frule aGroup.ag_pOp_closed[of R p q], assumption+)
[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; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; p \<plusminus> q \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> an n
[PROOF STEP]
apply (simp add:deg_an)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; an (deg_n R S X p) \<le> an n; an (deg_n R S X q) \<le> an n; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; p \<plusminus> q \<in> carrier R\<rbrakk> \<Longrightarrow> an (deg_n R S X (p \<plusminus> q)) \<le> an n
[PROOF STEP]
apply (simp only:ale_natle)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg_n R S X p \<le> n; deg_n R S X q \<le> n; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; p \<plusminus> q \<noteq> \<zero>; p \<plusminus> q \<in> carrier R\<rbrakk> \<Longrightarrow> deg_n R S X (p \<plusminus> q) \<le> n
[PROOF STEP]
apply (simp add:polyn_deg_add3)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) polyn_deg_add5:"\<lbrakk>p \<in> carrier R; q \<in> carrier R;
       (deg R S X p) \<le> a; (deg R S X q) \<le> a\<rbrakk>  \<Longrightarrow>
                                deg R S X (p \<plusminus> q) \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> a; deg R S X q \<le> a\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> a
[PROOF STEP]
apply (case_tac "a = \<infinity>", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> a; deg R S X q \<le> a; a \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> a
[PROOF STEP]
apply (cut_tac ring_is_ag,
       case_tac "p = \<zero>\<^bsub>R\<^esub>", simp add:aGroup.ag_l_zero[of R],
       case_tac "q = \<zero>\<^bsub>R\<^esub>", simp add:aGroup.ag_r_zero,
       simp add:deg_an[of p])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; an (deg_n R S X p) \<le> a; deg R S X q \<le> a; a \<noteq> \<infinity>; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> a
[PROOF STEP]
apply (cut_tac an_nat_pos[of "deg_n R S X p"],
       frule ale_trans[of "0" "an (deg_n R S X p)" "a"], assumption+,
       subgoal_tac "an (deg_n R S X p) \<le> an (na a)",
       simp only:ale_natle[of "deg_n R S X p" "na a"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; an (deg_n R S X p) \<le> a; deg R S X q \<le> a; a \<noteq> \<infinity>; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; 0 \<le> an (deg_n R S X p); 0 \<le> a; deg_n R S X p \<le> na a\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> a
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; an (deg_n R S X p) \<le> a; deg R S X q \<le> a; a \<noteq> \<infinity>; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; 0 \<le> an (deg_n R S X p); 0 \<le> a\<rbrakk> \<Longrightarrow> an (deg_n R S X p) \<le> an (na a)
[PROOF STEP]
apply (simp add:deg_an[of q])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; an (deg_n R S X p) \<le> a; an (deg_n R S X q) \<le> a; a \<noteq> \<infinity>; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; 0 \<le> a; deg_n R S X p \<le> na a\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> a
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; an (deg_n R S X p) \<le> a; deg R S X q \<le> a; a \<noteq> \<infinity>; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; 0 \<le> an (deg_n R S X p); 0 \<le> a\<rbrakk> \<Longrightarrow> an (deg_n R S X p) \<le> an (na a)
[PROOF STEP]
apply (cut_tac an_nat_pos[of "deg_n R S X q"],
       frule ale_trans[of "0" "an (deg_n R S X q)" "a"], assumption+,
       subgoal_tac "an (deg_n R S X q) \<le> an (na a)",
       simp only:ale_natle[of "deg_n R S X q" "na a"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; an (deg_n R S X p) \<le> a; an (deg_n R S X q) \<le> a; a \<noteq> \<infinity>; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; True; deg_n R S X p \<le> na a; 0 \<le> an (deg_n R S X q); 0 \<le> a; deg_n R S X q \<le> na a\<rbrakk> \<Longrightarrow> deg R S X (p \<plusminus> q) \<le> a
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; an (deg_n R S X p) \<le> a; an (deg_n R S X q) \<le> a; a \<noteq> \<infinity>; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; 0 \<le> a; deg_n R S X p \<le> na a; 0 \<le> an (deg_n R S X q); 0 \<le> a\<rbrakk> \<Longrightarrow> an (deg_n R S X q) \<le> an (na a)
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; an (deg_n R S X p) \<le> a; deg R S X q \<le> a; a \<noteq> \<infinity>; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; 0 \<le> an (deg_n R S X p); 0 \<le> a\<rbrakk> \<Longrightarrow> an (deg_n R S X p) \<le> an (na a)
[PROOF STEP]
apply (frule polyn_deg_add4[of p q "na a"], assumption+,
       simp add:an_na, simp add:deg_an,
       simp add:deg_an an_na, simp add:an_na)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; an (deg_n R S X p) \<le> a; an (deg_n R S X q) \<le> a; a \<noteq> \<infinity>; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; 0 \<le> a; deg_n R S X p \<le> na a; 0 \<le> an (deg_n R S X q); 0 \<le> a\<rbrakk> \<Longrightarrow> an (deg_n R S X q) \<le> an (na a)
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; an (deg_n R S X p) \<le> a; deg R S X q \<le> a; a \<noteq> \<infinity>; aGroup R; p \<noteq> \<zero>; q \<noteq> \<zero>; 0 \<le> an (deg_n R S X p); 0 \<le> a\<rbrakk> \<Longrightarrow> an (deg_n R S X p) \<le> an (na a)
[PROOF STEP]
apply (simp add:deg_an an_na, simp add:deg_an an_na)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) lower_deg_part:"\<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < deg_n R S X p\<rbrakk>
      \<Longrightarrow>
 deg R S X (polyn_expr R X (deg_n R S X p - Suc 0)(SOME f. cf_sol R S X p f))
                       < deg R S X p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < deg_n R S X p\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f)) < deg R S X p
[PROOF STEP]
apply (case_tac "polyn_expr R X (deg_n R S X p - Suc 0)
                              (SOME f. cf_sol R S X p f) = \<zero>\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < deg_n R S X p; polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f) = \<zero>\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f)) < deg R S X p
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < deg_n R S X p; polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f)) < deg R S X p
[PROOF STEP]
apply (simp add:deg_def, cut_tac minf_le_any[of "an (deg_n R S X p)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < deg_n R S X p; polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f) = \<zero>; - \<infinity> \<le> an (deg_n R S X p)\<rbrakk> \<Longrightarrow> - \<infinity> < an (deg_n R S X p)
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < deg_n R S X p; polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f)) < deg R S X p
[PROOF STEP]
apply (subst less_le, simp, simp add:an_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < deg_n R S X p; polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f) = \<zero>\<rbrakk> \<Longrightarrow> - \<infinity> \<noteq> ant (int (deg_n R S X p))
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < deg_n R S X p; polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f)) < deg R S X p
[PROOF STEP]
apply (rule not_sym, rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < deg_n R S X p; polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg R S X (polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f)) < deg R S X p
[PROOF STEP]
apply (simp add:deg_def, simp add:aless_natless)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < deg_n R S X p; polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (deg_n R S X p - Suc 0) (Eps (cf_sol R S X p))) < deg_n R S X p
[PROOF STEP]
apply (frule pol_SOME_2[of p], erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < deg_n R S X p; polyn_expr R X (deg_n R S X p - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (deg_n R S X p - Suc 0) (Eps (cf_sol R S X p))) < deg_n R S X p
[PROOF STEP]
apply (simp add:pol_deg_eq_c_max[of p "SOME c. cf_sol R S X p c"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p))) < c_max S (SOME c. cf_sol R S X p c)
[PROOF STEP]
apply (frule_tac c = "SOME c. cf_sol R S X p c" in coeff_max_bddTr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c)\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p))) < c_max S (SOME c. cf_sol R S X p c)
[PROOF STEP]
apply (cut_tac
  p = "polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0)
          (Eps (cf_sol R S X p))" and c = "(c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))" in pol_deg_eq_c_max)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c)\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p)) \<in> carrier R
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c)\<rbrakk> \<Longrightarrow> pol_coeff S (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c)\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p)) = polyn_expr R X (fst (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))) (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c); deg_n R S X (polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p))) = c_max S (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p))) < c_max S (SOME c. cf_sol R S X p c)
[PROOF STEP]
apply (rule polyn_mem, simp, arith)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c)\<rbrakk> \<Longrightarrow> pol_coeff S (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c)\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p)) = polyn_expr R X (fst (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))) (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c); deg_n R S X (polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p))) = c_max S (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p))) < c_max S (SOME c. cf_sol R S X p c)
[PROOF STEP]
apply (rule pol_coeff_le, assumption, arith)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c)\<rbrakk> \<Longrightarrow> polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p)) = polyn_expr R X (fst (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))) (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c); deg_n R S X (polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p))) = c_max S (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p))) < c_max S (SOME c. cf_sol R S X p c)
[PROOF STEP]
apply (subst polyn_expr_short, arith, arith, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c); deg_n R S X (polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p))) = c_max S (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))\<rbrakk> \<Longrightarrow> deg_n R S X (polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p))) < c_max S (SOME c. cf_sol R S X p c)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; 0 < c_max S (SOME c. cf_sol R S X p c); polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (SOME f. cf_sol R S X p f) \<noteq> \<zero>; pol_coeff S (SOME c. cf_sol R S X p c); p = polyn_expr R X (fst (SOME c. cf_sol R S X p c)) (SOME c. cf_sol R S X p c); c_max S (SOME c. cf_sol R S X p c) \<le> fst (SOME c. cf_sol R S X p c); deg_n R S X (polyn_expr R X (c_max S (SOME c. cf_sol R S X p c) - Suc 0) (Eps (cf_sol R S X p))) = c_max S (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c))\<rbrakk> \<Longrightarrow> c_max S (c_max S (SOME c. cf_sol R S X p c) - Suc 0, snd (SOME c. cf_sol R S X p c)) < c_max S (SOME c. cf_sol R S X p c)
[PROOF STEP]
apply (cut_tac c = "(c_max S (SOME c. cf_sol R S X p c) - Suc 0,
         snd (SOME c. cf_sol R S X p c))" in coeff_max_bddTr,
         rule pol_coeff_le, assumption, arith, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) ldeg_p_mem:"\<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d) \<rbrakk> \<Longrightarrow>
                      ldeg_p R S X d p \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> ldeg_p R S X d p \<in> carrier R
[PROOF STEP]
apply (frule scf_d_pol[of "p" "Suc d"], assumption+,
       erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d \<and> p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> ldeg_p R S X d p \<in> carrier R
[PROOF STEP]
apply (simp add:ldeg_p_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d \<and> p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X p (Suc d)) \<in> carrier R
[PROOF STEP]
apply (rule polyn_mem[of "scf_d R S X p (Suc d)" d],
         assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d \<and> p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> d \<le> fst (scf_d R S X p (Suc d))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) ldeg_p_zero:"p = \<zero>\<^bsub>R\<^esub> \<Longrightarrow> ldeg_p R S X d p = \<zero>\<^bsub>R\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = \<zero> \<Longrightarrow> ldeg_p R S X d p = \<zero>
[PROOF STEP]
apply (subgoal_tac "deg R S X p \<le> an (Suc d)",
       subgoal_tac "p \<in> carrier R")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; deg R S X p \<le> an (Suc d); p \<in> carrier R\<rbrakk> \<Longrightarrow> ldeg_p R S X d p = \<zero>
 2. \<lbrakk>p = \<zero>; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. p = \<zero> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (frule scf_d_pol[of "p" "Suc d"], assumption+,
       erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; deg R S X p \<le> an (Suc d); p \<in> carrier R; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d \<and> p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> ldeg_p R S X d p = \<zero>
 2. \<lbrakk>p = \<zero>; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. p = \<zero> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; deg R S X \<zero> \<le> an (Suc d); \<zero> \<in> carrier R; pol_coeff S (scf_d R S X \<zero> (Suc d)); fst (scf_d R S X \<zero> (Suc d)) = Suc d \<and> \<zero> = polyn_expr R X (Suc d) (scf_d R S X \<zero> (Suc d))\<rbrakk> \<Longrightarrow> ldeg_p R S X d \<zero> = \<zero>
 2. \<lbrakk>p = \<zero>; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. p = \<zero> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (frule coeff_0_pol_0[of "scf_d R S X \<zero> (Suc d)" "Suc d"], simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; deg R S X \<zero> \<le> an (Suc d); \<zero> \<in> carrier R; pol_coeff S (scf_d R S X \<zero> (Suc d)); fst (scf_d R S X \<zero> (Suc d)) = Suc d \<and> \<zero> = polyn_expr R X (Suc d) (scf_d R S X \<zero> (Suc d)); (\<forall>j\<le>Suc d. snd (scf_d R S X \<zero> (Suc d)) j = \<zero>\<^bsub>S\<^esub>) = (polyn_expr R X (Suc d) (scf_d R S X \<zero> (Suc d)) = \<zero>)\<rbrakk> \<Longrightarrow> ldeg_p R S X d \<zero> = \<zero>
 2. \<lbrakk>p = \<zero>; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. p = \<zero> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (simp add:ldeg_p_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; deg R S X \<zero> \<le> an (Suc d); \<zero> \<in> carrier R; pol_coeff S (scf_d R S X \<zero> (Suc d)); fst (scf_d R S X \<zero> (Suc d)) = Suc d \<and> \<zero> = polyn_expr R X (Suc d) (scf_d R S X \<zero> (Suc d)); \<forall>j\<le>Suc d. snd (scf_d R S X \<zero> (Suc d)) j = \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> polyn_expr R X d (scf_d R S X \<zero> (Suc d)) = \<zero>
 2. \<lbrakk>p = \<zero>; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. p = \<zero> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (subst coeff_0_pol_0[THEN sym, of "scf_d R S X \<zero> (Suc d)"],
        assumption+, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; deg R S X \<zero> \<le> an (Suc d); \<zero> \<in> carrier R; pol_coeff S (scf_d R S X \<zero> (Suc d)); fst (scf_d R S X \<zero> (Suc d)) = Suc d \<and> \<zero> = polyn_expr R X (Suc d) (scf_d R S X \<zero> (Suc d)); \<forall>j\<le>Suc d. snd (scf_d R S X \<zero> (Suc d)) j = \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> \<forall>j\<le>d. snd (scf_d R S X \<zero> (Suc d)) j = \<zero>\<^bsub>S\<^esub>
 2. \<lbrakk>p = \<zero>; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. p = \<zero> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (rule allI, rule impI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p = \<zero>; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 2. p = \<zero> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (simp, simp add:ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = \<zero> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (simp add:deg_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) hdeg_p_mem:"\<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow>
                      hdeg_p R S X (Suc d) p \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<in> carrier R
[PROOF STEP]
apply (frule scf_d_pol[of p "Suc d"], assumption+, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d \<and> p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<in> carrier R
[PROOF STEP]
apply (simp only:hdeg_p_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> \<in> carrier R
[PROOF STEP]
apply (cut_tac Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); Ring R\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> \<in> carrier R
[PROOF STEP]
apply (rule Ring.ring_tOp_closed[of "R"], assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); Ring R\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier R
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); Ring R\<rbrakk> \<Longrightarrow> X^\<^bsup>R Suc d\<^esup> \<in> carrier R
[PROOF STEP]
apply (frule pol_coeff_mem[of "scf_d R S X p (Suc d)" "Suc d"], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); Ring R; snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier S\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier R
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); Ring R\<rbrakk> \<Longrightarrow> X^\<^bsup>R Suc d\<^esup> \<in> carrier R
[PROOF STEP]
apply (cut_tac subring)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); Ring R; snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier S; Subring R S\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier R
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); Ring R\<rbrakk> \<Longrightarrow> X^\<^bsup>R Suc d\<^esup> \<in> carrier R
[PROOF STEP]
apply (simp add:Ring.mem_subring_mem_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); Ring R\<rbrakk> \<Longrightarrow> X^\<^bsup>R Suc d\<^esup> \<in> carrier R
[PROOF STEP]
apply (rule Ring.npClose[of "R"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); Ring R\<rbrakk> \<Longrightarrow> X \<in> carrier R
[PROOF STEP]
apply (rule X_mem_R)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) hdeg_p_zero:"p = \<zero> \<Longrightarrow> hdeg_p R S X (Suc d) p = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = \<zero> \<Longrightarrow> hdeg_p R S X (Suc d) p = \<zero>
[PROOF STEP]
apply (cut_tac X_mem_R)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p = \<zero>
[PROOF STEP]
apply (subgoal_tac "deg R S X p \<le> an (Suc d)",
       subgoal_tac "p \<in> carrier R")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X p \<le> an (Suc d); p \<in> carrier R\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p = \<zero>
 2. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. \<lbrakk>p = \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (frule scf_d_pol[of p "Suc d"], assumption+, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X p \<le> an (Suc d); p \<in> carrier R; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d \<and> p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p = \<zero>
 2. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. \<lbrakk>p = \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X \<zero> \<le> an (Suc d); \<zero> \<in> carrier R; pol_coeff S (scf_d R S X \<zero> (Suc d)); fst (scf_d R S X \<zero> (Suc d)) = Suc d \<and> \<zero> = polyn_expr R X (Suc d) (scf_d R S X \<zero> (Suc d))\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) \<zero> = \<zero>
 2. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. \<lbrakk>p = \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (frule coeff_0_pol_0[of "scf_d R S X \<zero> (Suc d)" "Suc d"],
        (erule conjE)+, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X \<zero> \<le> an (Suc d); \<zero> \<in> carrier R; pol_coeff S (scf_d R S X \<zero> (Suc d)); fst (scf_d R S X \<zero> (Suc d)) = Suc d \<and> \<zero> = polyn_expr R X (Suc d) (scf_d R S X \<zero> (Suc d)); (\<forall>j\<le>Suc d. snd (scf_d R S X \<zero> (Suc d)) j = \<zero>\<^bsub>S\<^esub>) = (polyn_expr R X (Suc d) (scf_d R S X \<zero> (Suc d)) = \<zero>)\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) \<zero> = \<zero>
 2. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. \<lbrakk>p = \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (simp only:hdeg_p_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X \<zero> \<le> an (Suc d); \<zero> \<in> carrier R; pol_coeff S (scf_d R S X \<zero> (Suc d)); fst (scf_d R S X \<zero> (Suc d)) = Suc d \<and> \<zero> = polyn_expr R X (Suc d) (scf_d R S X \<zero> (Suc d)); (\<forall>j\<le>Suc d. snd (scf_d R S X \<zero> (Suc d)) j = \<zero>\<^bsub>S\<^esub>) = (\<zero> = \<zero>)\<rbrakk> \<Longrightarrow> snd (scf_d R S X \<zero> (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = \<zero>
 2. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. \<lbrakk>p = \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (rotate_tac -1, drule sym, simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X \<zero> \<le> an (Suc d); \<zero> \<in> carrier R; pol_coeff S (scf_d R S X \<zero> (Suc d)); fst (scf_d R S X \<zero> (Suc d)) = Suc d \<and> \<zero> = polyn_expr R X (Suc d) (scf_d R S X \<zero> (Suc d)); \<forall>j\<le>Suc d. snd (scf_d R S X \<zero> (Suc d)) j = \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>S\<^esub> \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = \<zero>
 2. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 3. \<lbrakk>p = \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (cut_tac subring,
       simp del:npow_suc add:Subring_zero_ring_zero,
       rule ring_times_0_x, rule npClose, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p = \<zero>; X \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> p \<in> carrier R
 2. \<lbrakk>p = \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (simp add:ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = \<zero>; X \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X p \<le> an (Suc d)
[PROOF STEP]
apply (simp add:deg_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done