[STATEMENT]
lemma (in PolynRg) P_mod_diffxxx5_4:"\<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>;
      maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R;
  g \<in> carrier R; h \<in> carrier R;
  deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
   (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g);
  deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R'
                (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f;
    0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
        (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g);
    0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
        (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h);
  rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
          (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)
          (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h);
  P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r h))\<rbrakk> \<Longrightarrow>
       deg R S X (fst (Hpr\<^bsub>R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and>
       deg R S X (snd (Hpr\<^bsub>R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
       frule Ring.maximal_ideal_ideal[of S "S \<diamondsuit>\<^sub>p t"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t)\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (case_tac "m = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m = 0\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
 2. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m \<noteq> 0\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m = 0\<rbrakk> \<Longrightarrow> deg R S X h \<le> deg R S X f
 2. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m \<noteq> 0\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (frule aless_imp_le[of "0" "deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
          (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m = 0; 0 \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)\<rbrakk> \<Longrightarrow> deg R S X h \<le> deg R S X f
 2. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m \<noteq> 0\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (frule aadd_le_mono[of "0" "deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
       (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)" "deg R S X h"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m = 0; 0 \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 + deg R S X h \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) + deg R S X h\<rbrakk> \<Longrightarrow> deg R S X h \<le> deg R S X f
 2. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m \<noteq> 0\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (simp add:aadd_0_l, simp add:aadd_commute[of  _ "deg R S X h"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m \<noteq> 0\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (frule P_mod_diffxxx5_1[of t R' Y f g h "m - Suc 0"],
        assumption+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m \<noteq> 0; Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0) \<in> carrier R \<times> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)); deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (m - Suc 0)\<^esup>)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))) \<le> deg R S X f; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (m - Suc 0)\<^esup>)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus> -\<^sub>a snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (Suc (m - Suc 0))\<^esup>)) (f \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)) \<cdot>\<^sub>r snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (thin_tac "deg R S X g
     \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
        (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m \<noteq> 0; Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0) \<in> carrier R \<times> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)); deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (m - Suc 0)\<^esup>)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))) \<le> deg R S X f; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (m - Suc 0)\<^esup>)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus> -\<^sub>a snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (Suc (m - Suc 0))\<^esup>)) (f \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)) \<cdot>\<^sub>r snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (thin_tac "deg R S X h +  deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
      (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m \<noteq> 0; Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0) \<in> carrier R \<times> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)); deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (m - Suc 0)\<^esup>)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))) \<le> deg R S X f; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (m - Suc 0)\<^esup>)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus> -\<^sub>a snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (Suc (m - Suc 0))\<^esup>)) (f \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)) \<cdot>\<^sub>r snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (thin_tac "rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
      (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)
      (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h)",
       thin_tac "P_mod R S X (S \<diamondsuit>\<^sub>p t) ( f \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r h))",
       thin_tac "P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc (m - Suc 0))\<^esup>))
        (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus>
         -\<^sub>a (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))))",
       thin_tac "P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc (m - Suc 0))\<^esup>))
      ( snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus>
          -\<^sub>a (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))))",
       thin_tac "P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc (Suc (m - Suc 0)))\<^esup>))
      (f \<plusminus>
       -\<^sub>a (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)) \<cdot>\<^sub>r
           snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); m \<noteq> 0; Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0) \<in> carrier R \<times> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)); deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))) \<le> deg R S X f\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (simp del:npow_suc Hpr_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (thin_tac "erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t))
         (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) =
         erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g",
        thin_tac "erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t))
        (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) =
        erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (frule_tac p = g in pHom_dec_deg[of R' "(S /\<^sub>r (S \<diamondsuit>\<^sub>p t))" Y
         "erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t))"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y
 2. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f\<rbrakk> \<Longrightarrow> g \<in> carrier R
 3. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X g\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (frule Ring.qring_ring[of "S" "S \<diamondsuit>\<^sub>p t"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; Ring (S /\<^sub>r (S \<diamondsuit>\<^sub>p t))\<rbrakk> \<Longrightarrow> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) \<in> pHom R S X, R' S /\<^sub>r (S \<diamondsuit>\<^sub>p t) Y
 2. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f\<rbrakk> \<Longrightarrow> g \<in> carrier R
 3. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X g\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (rule erH_rHom[of R' "(S /\<^sub>r (S \<diamondsuit>\<^sub>p t))" Y "pj S (S \<diamondsuit>\<^sub>p t)"], assumption+,
       simp add:pj_Hom, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X g\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (frule ale_trans[of "deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m))"
        "deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
         (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)" "deg R S X g"],
       assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X g; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g\<rbrakk> \<Longrightarrow> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X g; deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g\<rbrakk> \<Longrightarrow> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (thin_tac "deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m))
                  \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
                    (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)",
      thin_tac "deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
         (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X g",
      thin_tac "deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X g")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f\<rbrakk> \<Longrightarrow> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (frule aless_imp_le[of "0" "deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
          (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)\<rbrakk> \<Longrightarrow> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (frule aadd_le_mono[of "0" "deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
              (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)"
           "deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m))"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); Subring R S; Ring S; ideal S (S \<diamondsuit>\<^sub>p t); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R; deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 + deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) + deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m))\<rbrakk> \<Longrightarrow> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m)) \<le> deg R S X f
[PROOF STEP]
apply (simp add:aadd_0_l, simp add:aadd_commute[of  _
                "deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m))"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma root_primitive_part [simp]:
  fixes p :: "'a :: {semiring_gcd, semiring_no_zero_divisors} poly"
  shows  "poly (primitive_part p) x = 0 \<longleftrightarrow> poly p x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
[PROOF STEP]
proof(cases "p = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = 0 \<Longrightarrow> (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
 2. p \<noteq> 0 \<Longrightarrow> (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p = 0

goal (2 subgoals):
 1. p = 0 \<Longrightarrow> (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
 2. p \<noteq> 0 \<Longrightarrow> (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = 0

goal (1 subgoal):
 1. (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
[PROOF STEP]
have "poly p x = content p * poly (primitive_part p) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly p x = content p * poly (primitive_part p) x
[PROOF STEP]
by (metis content_times_primitive_part poly_smult)
[PROOF STATE]
proof (state)
this:
poly p x = content p * poly (primitive_part p) x

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poly p x = content p * poly (primitive_part p) x

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
[PROOF STEP]
have "\<dots> = 0 \<longleftrightarrow> poly (primitive_part p) x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (content p * poly (primitive_part p) x = (0::'a)) = (poly (primitive_part p) x = (0::'a))
[PROOF STEP]
by (simp add: False)
[PROOF STATE]
proof (state)
this:
(content p * poly (primitive_part p) x = (0::'a)) = (poly (primitive_part p) x = (0::'a))

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(poly p x = (0::'a)) = (poly (primitive_part p) x = (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(poly p x = (0::'a)) = (poly (primitive_part p) x = (0::'a))

goal (1 subgoal):
 1. (poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(poly (primitive_part p) x = (0::'a)) = (poly p x = (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma irreducible_primitive_part:
  assumes "irreducible p" and "degree p > 0"
  shows "primitive_part p = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primitive_part p = p
[PROOF STEP]
using irreducible_content[OF assms(1), unfolded primitive_iff_content_eq_1] assms(2)
[PROOF STATE]
proof (prove)
using this:
degree p = 0 \<or> content p = (1::'a)
0 < degree p

goal (1 subgoal):
 1. primitive_part p = p
[PROOF STEP]
by (auto simp: primitive_part_def abs_poly_def)


[STATEMENT]
lemma count_roots_interval_iff: "square_free p \<Longrightarrow> count_roots_interval p = count_roots_interval_sf p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free p \<Longrightarrow> count_roots_interval p = count_roots_interval_sf p
[PROOF STEP]
unfolding count_roots_interval_def count_roots_interval_sf_def sturm_squarefree_def
    square_free_iff_separable separable_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. algebraic_semidom_class.coprime p (pderiv p) \<Longrightarrow> (let ps = sturm p in (\<lambda>a b. sign_changes ps a - sign_changes ps b + (if poly p a = 0 then 1 else 0), \<lambda>a. sign_changes_neg_inf ps - sign_changes ps a)) = (let ps = sturm (p div gcd p (pderiv p)) in (\<lambda>a b. sign_changes ps a - sign_changes ps b + (if poly p a = 0 then 1 else 0), \<lambda>a. sign_changes_neg_inf ps - sign_changes ps a))
[PROOF STEP]
by (cases "p = 0", auto)


[STATEMENT]
lemma count_roots_interval_sf: assumes p: "p \<noteq> 0"
  and cr: "count_roots_interval_sf p = (cr,nr)"
  shows "a \<le> b \<Longrightarrow> cr a b = (card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0})"
    "nr a = card {x. x \<le> a \<and> poly p x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b \<Longrightarrow> cr a b = card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0}) &&& nr a = card {x. x \<le> a \<and> poly p x = 0}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> cr a b = card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0}
 2. nr a = card {x. x \<le> a \<and> poly p x = 0}
[PROOF STEP]
have id: "a \<le> b \<Longrightarrow> { x. a \<le> x \<and> x \<le> b \<and> poly p x = 0} =
    { x. a < x \<and> x \<le> b \<and> poly p x = 0} \<union> (if poly p a = 0 then {a} else {})"
    (is "_ \<Longrightarrow> _ = ?R \<union> ?S")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0} = {x. a < x \<and> x \<le> b \<and> poly p x = 0} \<union> (if poly p a = 0 then {a} else {})
[PROOF STEP]
using not_less
[PROOF STATE]
proof (prove)
using this:
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0} = {x. a < x \<and> x \<le> b \<and> poly p x = 0} \<union> (if poly p a = 0 then {a} else {})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a \<le> b \<Longrightarrow> {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0} = {x. a < x \<and> x \<le> b \<and> poly p x = 0} \<union> (if poly p a = 0 then {a} else {})

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> cr a b = card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0}
 2. nr a = card {x. x \<le> a \<and> poly p x = 0}
[PROOF STEP]
have RS: "finite ?R" "finite ?S" "?R \<inter> ?S = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. a < x \<and> x \<le> b \<and> poly p x = 0} &&& finite (if poly p a = 0 then {a} else {}) &&& {x. a < x \<and> x \<le> b \<and> poly p x = 0} \<inter> (if poly p a = 0 then {a} else {}) = {}
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0

goal (1 subgoal):
 1. finite {x. a < x \<and> x \<le> b \<and> poly p x = 0} &&& finite (if poly p a = 0 then {a} else {}) &&& {x. a < x \<and> x \<le> b \<and> poly p x = 0} \<inter> (if poly p a = 0 then {a} else {}) = {}
[PROOF STEP]
by (auto simp: poly_roots_finite)
[PROOF STATE]
proof (state)
this:
finite {x. a < x \<and> x \<le> b \<and> poly p x = 0}
finite (if poly p a = 0 then {a} else {})
{x. a < x \<and> x \<le> b \<and> poly p x = 0} \<inter> (if poly p a = 0 then {a} else {}) = {}

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> cr a b = card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0}
 2. nr a = card {x. x \<le> a \<and> poly p x = 0}
[PROOF STEP]
show "a \<le> b \<Longrightarrow> cr a b = (card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0})"
    "nr a = card {x. x \<le> a \<and> poly p x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b \<Longrightarrow> cr a b = card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0}) &&& nr a = card {x. x \<le> a \<and> poly p x = 0}
[PROOF STEP]
using cr
[PROOF STATE]
proof (prove)
using this:
count_roots_interval_sf p = (cr, nr)

goal (1 subgoal):
 1. (a \<le> b \<Longrightarrow> cr a b = card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0}) &&& nr a = card {x. x \<le> a \<and> poly p x = 0}
[PROOF STEP]
unfolding arg_cong[OF id, of card] card_Un_disjoint[OF RS]
    count_roots_interval_sf_def count_roots_between_correct[symmetric]
    count_roots_below_correct[symmetric] count_roots_below_def
    count_roots_between_def Let_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>a b. sign_changes (sturm_squarefree p) a - sign_changes (sturm_squarefree p) b + (if poly p a = 0 then 1 else 0), \<lambda>a. sign_changes_neg_inf (sturm_squarefree p) - sign_changes (sturm_squarefree p) a) = (cr, nr)

goal (1 subgoal):
 1. (a \<le> b \<Longrightarrow> cr a b = (if a \<le> b \<and> p \<noteq> 0 then sign_changes (sturm_squarefree p) a - sign_changes (sturm_squarefree p) b else 0) + card (if poly p a = 0 then {a} else {})) &&& nr a = (if p = 0 then 0 else sign_changes_neg_inf (sturm_squarefree p) - sign_changes (sturm_squarefree p) a)
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
(\<lambda>a b. sign_changes (sturm_squarefree p) a - sign_changes (sturm_squarefree p) b + (if poly p a = 0 then 1 else 0), \<lambda>a. sign_changes_neg_inf (sturm_squarefree p) - sign_changes (sturm_squarefree p) a) = (cr, nr)
p \<noteq> 0

goal (1 subgoal):
 1. (a \<le> b \<Longrightarrow> cr a b = (if a \<le> b \<and> p \<noteq> 0 then sign_changes (sturm_squarefree p) a - sign_changes (sturm_squarefree p) b else 0) + card (if poly p a = 0 then {a} else {})) &&& nr a = (if p = 0 then 0 else sign_changes_neg_inf (sturm_squarefree p) - sign_changes (sturm_squarefree p) a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<le> b \<Longrightarrow> cr a b = card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0}
nr a = card {x. x \<le> a \<and> poly p x = 0}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma count_roots_interval: assumes cr: "count_roots_interval p = (cr,nr)"
  and sf: "square_free p"
  shows "a \<le> b \<Longrightarrow> cr a b = (card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0})"
    "nr a = card {x. x \<le> a \<and> poly p x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b \<Longrightarrow> cr a b = card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0}) &&& nr a = card {x. x \<le> a \<and> poly p x = 0}
[PROOF STEP]
using count_roots_interval_sf[OF _ cr[unfolded count_roots_interval_iff[OF sf]]]
    sf[unfolded square_free_def]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p \<noteq> 0; ?a \<le> ?b\<rbrakk> \<Longrightarrow> cr ?a ?b = card {x. ?a \<le> x \<and> x \<le> ?b \<and> poly p x = 0}
p \<noteq> 0 \<Longrightarrow> nr ?a = card {x. x \<le> ?a \<and> poly p x = 0}
p \<noteq> 0 \<and> (\<forall>q. 0 < degree q \<longrightarrow> \<not> q * q dvd p)

goal (1 subgoal):
 1. (a \<le> b \<Longrightarrow> cr a b = card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0}) &&& nr a = card {x. x \<le> a \<and> poly p x = 0}
[PROOF STEP]
by blast+


[STATEMENT]
lemma root_info_condD: "root_info_cond ri p \<Longrightarrow> a \<le> b \<Longrightarrow> root_info.l_r ri a b = card {x. root_cond (p,a,b) x}"
  "root_info_cond ri p \<Longrightarrow> root_info.number_root ri a = card {x. x \<le> real_of_rat a \<and> ipoly p x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>root_info_cond ri p; a \<le> b\<rbrakk> \<Longrightarrow> root_info.l_r ri a b = card {x. root_cond (p, a, b) x}) &&& (root_info_cond ri p \<Longrightarrow> root_info.number_root ri a = card {x. x \<le> real_of_rat a \<and> poly (real_of_int_poly p) x = 0})
[PROOF STEP]
unfolding root_info_cond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>(\<forall>a b. a \<le> b \<longrightarrow> root_info.l_r ri a b = card {x. root_cond (p, a, b) x}) \<and> (\<forall>a. root_info.number_root ri a = card {x. x \<le> real_of_rat a \<and> poly (real_of_int_poly p) x = 0}); a \<le> b\<rbrakk> \<Longrightarrow> root_info.l_r ri a b = card {x. root_cond (p, a, b) x}) &&& ((\<forall>a b. a \<le> b \<longrightarrow> root_info.l_r ri a b = card {x. root_cond (p, a, b) x}) \<and> (\<forall>a. root_info.number_root ri a = card {x. x \<le> real_of_rat a \<and> poly (real_of_int_poly p) x = 0}) \<Longrightarrow> root_info.number_root ri a = card {x. x \<le> real_of_rat a \<and> poly (real_of_int_poly p) x = 0})
[PROOF STEP]
by auto


[STATEMENT]
lemma count_roots_interval_sf_rat: assumes p: "p \<noteq> 0"
  shows "root_info_cond (count_roots_interval_sf_rat p) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_info_cond (count_roots_interval_sf_rat p) p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. root_info_cond (count_roots_interval_sf_rat p) p
[PROOF STEP]
let ?p = "real_of_int_poly p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. root_info_cond (count_roots_interval_sf_rat p) p
[PROOF STEP]
let ?r = real_of_rat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. root_info_cond (count_roots_interval_sf_rat p) p
[PROOF STEP]
let ?ri = "count_roots_interval_sf_rat p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. root_info_cond (count_roots_interval_sf_rat p) p
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> 0
[PROOF STEP]
have p: "?p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0

goal (1 subgoal):
 1. real_of_int_poly p \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int_poly p \<noteq> 0

goal (1 subgoal):
 1. root_info_cond (count_roots_interval_sf_rat p) p
[PROOF STEP]
obtain cr nr where cr: "count_roots_interval_sf ?p = (cr,nr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cr nr. count_roots_interval_sf (real_of_int_poly p) = (cr, nr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
count_roots_interval_sf (real_of_int_poly p) = (cr, nr)

goal (1 subgoal):
 1. root_info_cond (count_roots_interval_sf_rat p) p
[PROOF STEP]
have "?ri = Root_Info (\<lambda>a b. cr (?r a) (?r b)) (\<lambda>a. nr (?r a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_roots_interval_sf_rat p = Root_Info (\<lambda>a b. cr (real_of_rat a) (real_of_rat b)) (\<lambda>a. nr (real_of_rat a))
[PROOF STEP]
unfolding count_roots_interval_sf_rat_def Let_def cr
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (cr, nr) of (cr, nr) \<Rightarrow> Root_Info (\<lambda>a b. cr (real_of_rat a) (real_of_rat b)) (\<lambda>a. nr (real_of_rat a))) = Root_Info (\<lambda>a b. cr (real_of_rat a) (real_of_rat b)) (\<lambda>a. nr (real_of_rat a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
count_roots_interval_sf_rat p = Root_Info (\<lambda>a b. cr (real_of_rat a) (real_of_rat b)) (\<lambda>a. nr (real_of_rat a))

goal (1 subgoal):
 1. root_info_cond (count_roots_interval_sf_rat p) p
[PROOF STEP]
hence id: "root_info.l_r ?ri = (\<lambda>a b. cr (?r a) (?r b))" "root_info.number_root ?ri = (\<lambda>a. nr (?r a))"
[PROOF STATE]
proof (prove)
using this:
count_roots_interval_sf_rat p = Root_Info (\<lambda>a b. cr (real_of_rat a) (real_of_rat b)) (\<lambda>a. nr (real_of_rat a))

goal (1 subgoal):
 1. root_info.l_r (count_roots_interval_sf_rat p) = (\<lambda>a b. cr (real_of_rat a) (real_of_rat b)) &&& root_info.number_root (count_roots_interval_sf_rat p) = (\<lambda>a. nr (real_of_rat a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
root_info.l_r (count_roots_interval_sf_rat p) = (\<lambda>a b. cr (real_of_rat a) (real_of_rat b))
root_info.number_root (count_roots_interval_sf_rat p) = (\<lambda>a. nr (real_of_rat a))

goal (1 subgoal):
 1. root_info_cond (count_roots_interval_sf_rat p) p
[PROOF STEP]
note cr = count_roots_interval_sf[OF p cr]
[PROOF STATE]
proof (state)
this:
?a \<le> ?b \<Longrightarrow> cr ?a ?b = card {x. ?a \<le> x \<and> x \<le> ?b \<and> poly (real_of_int_poly p) x = 0}
nr ?a = card {x. x \<le> ?a \<and> poly (real_of_int_poly p) x = 0}

goal (1 subgoal):
 1. root_info_cond (count_roots_interval_sf_rat p) p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_info_cond (count_roots_interval_sf_rat p) p
[PROOF STEP]
unfolding root_info_cond_def id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a b. a \<le> b \<longrightarrow> cr (real_of_rat a) (real_of_rat b) = card {x. root_cond (p, a, b) x}) \<and> (\<forall>a. nr (real_of_rat a) = card {x. x \<le> real_of_rat a \<and> poly (real_of_int_poly p) x = 0})
[PROOF STEP]
proof (intro conjI impI allI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. a \<le> b \<Longrightarrow> cr (real_of_rat a) (real_of_rat b) = card {x. root_cond (p, a, b) x}
 2. \<And>a. nr (real_of_rat a) = card {x. x \<le> real_of_rat a \<and> poly (real_of_int_poly p) x = 0}
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. a \<le> b \<Longrightarrow> cr (real_of_rat a) (real_of_rat b) = card {x. root_cond (p, a, b) x}
 2. \<And>a. nr (real_of_rat a) = card {x. x \<le> real_of_rat a \<and> poly (real_of_int_poly p) x = 0}
[PROOF STEP]
show "nr (?r a) = card {x. x \<le> (?r a) \<and> ipoly p x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nr (real_of_rat a) = card {x. x \<le> real_of_rat a \<and> poly (real_of_int_poly p) x = 0}
[PROOF STEP]
using cr(2)[of "?r a"]
[PROOF STATE]
proof (prove)
using this:
nr (real_of_rat a) = card {x. x \<le> real_of_rat a \<and> poly (real_of_int_poly p) x = 0}

goal (1 subgoal):
 1. nr (real_of_rat a) = card {x. x \<le> real_of_rat a \<and> poly (real_of_int_poly p) x = 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nr (real_of_rat a) = card {x. x \<le> real_of_rat a \<and> poly (real_of_int_poly p) x = 0}

goal (1 subgoal):
 1. \<And>a b. a \<le> b \<Longrightarrow> cr (real_of_rat a) (real_of_rat b) = card {x. root_cond (p, a, b) x}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. a \<le> b \<Longrightarrow> cr (real_of_rat a) (real_of_rat b) = card {x. root_cond (p, a, b) x}
[PROOF STEP]
fix a b :: rat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. a \<le> b \<Longrightarrow> cr (real_of_rat a) (real_of_rat b) = card {x. root_cond (p, a, b) x}
[PROOF STEP]
assume ab: "a \<le> b"
[PROOF STATE]
proof (state)
this:
a \<le> b

goal (1 subgoal):
 1. \<And>a b. a \<le> b \<Longrightarrow> cr (real_of_rat a) (real_of_rat b) = card {x. root_cond (p, a, b) x}
[PROOF STEP]
from ab
[PROOF STATE]
proof (chain)
picking this:
a \<le> b
[PROOF STEP]
have ab: "?r a \<le> ?r b"
[PROOF STATE]
proof (prove)
using this:
a \<le> b

goal (1 subgoal):
 1. real_of_rat a \<le> real_of_rat b
[PROOF STEP]
by (simp add: of_rat_less_eq)
[PROOF STATE]
proof (state)
this:
real_of_rat a \<le> real_of_rat b

goal (1 subgoal):
 1. \<And>a b. a \<le> b \<Longrightarrow> cr (real_of_rat a) (real_of_rat b) = card {x. root_cond (p, a, b) x}
[PROOF STEP]
from cr(1)[OF this]
[PROOF STATE]
proof (chain)
picking this:
cr (real_of_rat a) (real_of_rat b) = card {x. real_of_rat a \<le> x \<and> x \<le> real_of_rat b \<and> poly (real_of_int_poly p) x = 0}
[PROOF STEP]
show "cr (?r a) (?r b) = card (Collect (root_cond (p, a, b)))"
[PROOF STATE]
proof (prove)
using this:
cr (real_of_rat a) (real_of_rat b) = card {x. real_of_rat a \<le> x \<and> x \<le> real_of_rat b \<and> poly (real_of_int_poly p) x = 0}

goal (1 subgoal):
 1. cr (real_of_rat a) (real_of_rat b) = card (Collect (root_cond (p, a, b)))
[PROOF STEP]
unfolding root_cond_def[abs_def] split
[PROOF STATE]
proof (prove)
using this:
cr (real_of_rat a) (real_of_rat b) = card {x. real_of_rat a \<le> x \<and> x \<le> real_of_rat b \<and> poly (real_of_int_poly p) x = 0}

goal (1 subgoal):
 1. cr (real_of_rat a) (real_of_rat b) = card {x. real_of_rat a \<le> x \<and> x \<le> real_of_rat b \<and> poly (real_of_int_poly p) x = 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cr (real_of_rat a) (real_of_rat b) = card (Collect (root_cond (p, a, b)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
root_info_cond (count_roots_interval_sf_rat p) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_rat_of_int_poly: "map_poly of_rat (of_int_poly p) = of_int_poly p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_poly of_rat (of_int_poly p) = of_int_poly p
[PROOF STEP]
by (subst map_poly_map_poly, auto simp: o_def)


[STATEMENT]
lemma square_free_of_int_poly: assumes "square_free p"
  shows "square_free (of_int_poly p :: 'a :: {field_gcd, field_char_0} poly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free (of_int_poly p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. square_free (of_int_poly p)
[PROOF STEP]
have "square_free (map_poly of_rat (of_int_poly p) :: 'a poly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free (map_poly of_rat (of_int_poly p))
[PROOF STEP]
unfolding of_rat_hom.square_free_map_poly
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free (of_int_poly p)
[PROOF STEP]
by (rule square_free_int_rat[OF assms])
[PROOF STATE]
proof (state)
this:
square_free (map_poly of_rat (of_int_poly p))

goal (1 subgoal):
 1. square_free (of_int_poly p)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
square_free (map_poly of_rat (of_int_poly p))

goal (1 subgoal):
 1. square_free (of_int_poly p)
[PROOF STEP]
unfolding of_rat_of_int_poly
[PROOF STATE]
proof (prove)
using this:
square_free (of_int_poly p)

goal (1 subgoal):
 1. square_free (of_int_poly p)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
square_free (of_int_poly p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma count_roots_interval_rat: assumes sf: "square_free p"
  shows "root_info_cond (count_roots_interval_rat p) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_info_cond (count_roots_interval_rat p) p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. root_info_cond (count_roots_interval_rat p) p
[PROOF STEP]
from sf
[PROOF STATE]
proof (chain)
picking this:
square_free p
[PROOF STEP]
have sf: "square_free (real_of_int_poly p)"
[PROOF STATE]
proof (prove)
using this:
square_free p

goal (1 subgoal):
 1. square_free (real_of_int_poly p)
[PROOF STEP]
by (rule square_free_of_int_poly)
[PROOF STATE]
proof (state)
this:
square_free (real_of_int_poly p)

goal (1 subgoal):
 1. root_info_cond (count_roots_interval_rat p) p
[PROOF STEP]
from sf
[PROOF STATE]
proof (chain)
picking this:
square_free (real_of_int_poly p)
[PROOF STEP]
have p: "p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
square_free (real_of_int_poly p)

goal (1 subgoal):
 1. p \<noteq> 0
[PROOF STEP]
unfolding square_free_def
[PROOF STATE]
proof (prove)
using this:
real_of_int_poly p \<noteq> 0 \<and> (\<forall>q. 0 < degree q \<longrightarrow> \<not> q * q dvd real_of_int_poly p)

goal (1 subgoal):
 1. p \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

goal (1 subgoal):
 1. root_info_cond (count_roots_interval_rat p) p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_info_cond (count_roots_interval_rat p) p
[PROOF STEP]
using count_roots_interval_sf_rat[OF p]
[PROOF STATE]
proof (prove)
using this:
root_info_cond (count_roots_interval_sf_rat p) p

goal (1 subgoal):
 1. root_info_cond (count_roots_interval_rat p) p
[PROOF STEP]
unfolding count_roots_interval_rat_def count_roots_interval_sf_rat_def
    Let_def count_roots_interval_iff[OF sf]
[PROOF STATE]
proof (prove)
using this:
root_info_cond (case count_roots_interval_sf (real_of_int_poly p) of (cr, nr) \<Rightarrow> Root_Info (\<lambda>a b. cr (real_of_rat a) (real_of_rat b)) (\<lambda>a. nr (real_of_rat a))) p

goal (1 subgoal):
 1. root_info_cond (case count_roots_interval_sf (real_of_int_poly p) of (cr, nr) \<Rightarrow> Root_Info (\<lambda>a b. cr (real_of_rat a) (real_of_rat b)) (\<lambda>a. nr (real_of_rat a))) p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
root_info_cond (count_roots_interval_rat p) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma count_roots_rat: "count_roots_rat p = card {x. ipoly p x = (0 :: real)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_roots_rat p = card {x. poly (real_of_int_poly p) x = 0}
[PROOF STEP]
unfolding count_roots_rat_def count_roots_correct
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {x. poly (real_of_int_poly p) x = 0} = card {x. poly (real_of_int_poly p) x = 0}
[PROOF STEP]
..


[STATEMENT]
lemma sturm_aux_rat: "sturm_aux (real_of_rat_poly p) (real_of_rat_poly q) =
  map real_of_rat_poly (sturm_aux_rat p q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sturm_aux (real_of_rat_poly p) (real_of_rat_poly q) = map real_of_rat_poly (sturm_aux_rat p q)
[PROOF STEP]
proof (induct p q rule: sturm_aux_rat.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p q. (degree q \<noteq> 0 \<Longrightarrow> sturm_aux (real_of_rat_poly q) (real_of_rat_poly (- (p mod q))) = map real_of_rat_poly (sturm_aux_rat q (- (p mod q)))) \<Longrightarrow> sturm_aux (real_of_rat_poly p) (real_of_rat_poly q) = map real_of_rat_poly (sturm_aux_rat p q)
[PROOF STEP]
case (1 p q)
[PROOF STATE]
proof (state)
this:
degree q \<noteq> 0 \<Longrightarrow> sturm_aux (real_of_rat_poly q) (real_of_rat_poly (- (p mod q))) = map real_of_rat_poly (sturm_aux_rat q (- (p mod q)))

goal (1 subgoal):
 1. \<And>p q. (degree q \<noteq> 0 \<Longrightarrow> sturm_aux (real_of_rat_poly q) (real_of_rat_poly (- (p mod q))) = map real_of_rat_poly (sturm_aux_rat q (- (p mod q)))) \<Longrightarrow> sturm_aux (real_of_rat_poly p) (real_of_rat_poly q) = map real_of_rat_poly (sturm_aux_rat p q)
[PROOF STEP]
interpret map_poly_inj_idom_hom of_rat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_poly_inj_idom_hom of_rat
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p q. (degree q \<noteq> 0 \<Longrightarrow> sturm_aux (real_of_rat_poly q) (real_of_rat_poly (- (p mod q))) = map real_of_rat_poly (sturm_aux_rat q (- (p mod q)))) \<Longrightarrow> sturm_aux (real_of_rat_poly p) (real_of_rat_poly q) = map real_of_rat_poly (sturm_aux_rat p q)
[PROOF STEP]
note deg = of_int_hom.degree_map_poly_hom
[PROOF STATE]
proof (state)
this:
degree (of_int_poly ?p) = degree ?p

goal (1 subgoal):
 1. \<And>p q. (degree q \<noteq> 0 \<Longrightarrow> sturm_aux (real_of_rat_poly q) (real_of_rat_poly (- (p mod q))) = map real_of_rat_poly (sturm_aux_rat q (- (p mod q)))) \<Longrightarrow> sturm_aux (real_of_rat_poly p) (real_of_rat_poly q) = map real_of_rat_poly (sturm_aux_rat p q)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sturm_aux (real_of_rat_poly p) (real_of_rat_poly q) = map real_of_rat_poly (sturm_aux_rat p q)
[PROOF STEP]
unfolding sturm_aux.simps[of "real_of_rat_poly p"] sturm_aux_rat.simps[of p]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if degree (real_of_rat_poly q) = 0 then [real_of_rat_poly p, real_of_rat_poly q] else real_of_rat_poly p # sturm_aux (real_of_rat_poly q) (- (real_of_rat_poly p mod real_of_rat_poly q))) = map real_of_rat_poly (if degree q = 0 then [p, q] else p # sturm_aux_rat q (- (p mod q)))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
degree q \<noteq> 0 \<Longrightarrow> sturm_aux (real_of_rat_poly q) (real_of_rat_poly (- (p mod q))) = map real_of_rat_poly (sturm_aux_rat q (- (p mod q)))

goal (1 subgoal):
 1. (if degree (real_of_rat_poly q) = 0 then [real_of_rat_poly p, real_of_rat_poly q] else real_of_rat_poly p # sturm_aux (real_of_rat_poly q) (- (real_of_rat_poly p mod real_of_rat_poly q))) = map real_of_rat_poly (if degree q = 0 then [p, q] else p # sturm_aux_rat q (- (p mod q)))
[PROOF STEP]
by (cases "degree q = 0"; simp add: hom_distribs)
[PROOF STATE]
proof (state)
this:
sturm_aux (real_of_rat_poly p) (real_of_rat_poly q) = map real_of_rat_poly (sturm_aux_rat p q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sturm_rat: "sturm (real_of_rat_poly p) = map real_of_rat_poly (sturm_rat p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sturm (real_of_rat_poly p) = map real_of_rat_poly (sturm_rat p)
[PROOF STEP]
unfolding sturm_rat_def sturm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sturm_aux (real_of_rat_poly p) (pderiv (real_of_rat_poly p)) = map real_of_rat_poly (sturm_aux_rat p (pderiv p))
[PROOF STEP]
apply (fold of_rat_hom.map_poly_pderiv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sturm_aux (real_of_rat_poly p) (real_of_rat_poly (pderiv p)) = map real_of_rat_poly (sturm_aux_rat p (pderiv p))
[PROOF STEP]
unfolding sturm_aux_rat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map real_of_rat_poly (sturm_aux_rat p (pderiv p)) = map real_of_rat_poly (sturm_aux_rat p (pderiv p))
[PROOF STEP]
..


[STATEMENT]
lemma poly_number_rootat: "poly_inf (real_of_rat_poly p) = real_of_rat (poly_number_rootat p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_inf (real_of_rat_poly p) = real_of_rat (poly_number_rootat p)
[PROOF STEP]
unfolding poly_inf_def poly_number_rootat_def of_int_hom.degree_map_poly_hom of_rat_hom.coeff_map_poly_hom
    real_of_rat_sgn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat (sgn (coeff p (degree (real_of_rat_poly p)))) = real_of_rat (sgn (lead_coeff p))
[PROOF STEP]
by simp


[STATEMENT]
lemma poly_neg_number_rootat: "poly_neg_inf (real_of_rat_poly p) = real_of_rat (poly_neg_number_rootat p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_neg_inf (real_of_rat_poly p) = real_of_rat (poly_neg_number_rootat p)
[PROOF STEP]
unfolding poly_neg_inf_def poly_neg_number_rootat_def of_int_hom.degree_map_poly_hom of_rat_hom.coeff_map_poly_hom
    real_of_rat_sgn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if even (degree (real_of_rat_poly p)) then real_of_rat (sgn (coeff p (degree (real_of_rat_poly p)))) else - real_of_rat (sgn (coeff p (degree (real_of_rat_poly p))))) = real_of_rat (if even (degree p) then sgn (lead_coeff p) else - sgn (lead_coeff p))
[PROOF STEP]
by (simp add:hom_distribs)


[STATEMENT]
lemma real_of_rat_list_neq: "list_neq (map real_of_rat xs) 0
  = map real_of_rat (list_neq xs 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_neq (map real_of_rat xs) 0 = map real_of_rat (list_neq xs 0)
[PROOF STEP]
by (induct xs, auto)


[STATEMENT]
lemma real_of_rat_remdups_adj: "remdups_adj (map real_of_rat xs) = map real_of_rat (remdups_adj xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remdups_adj (map real_of_rat xs) = map real_of_rat (remdups_adj xs)
[PROOF STEP]
by (induct xs rule: remdups_adj.induct, auto)


[STATEMENT]
lemma sign_changes_rat: "sign_changes (map real_of_rat_poly ps) (real_of_rat x)
  = sign_changes_rat ps x" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_changes (map real_of_rat_poly ps) (real_of_rat x) = sign_changes_rat ps x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sign_changes (map real_of_rat_poly ps) (real_of_rat x) = sign_changes_rat ps x
[PROOF STEP]
define xs where "xs = list_neq (map (\<lambda>p. sgn (poly p x)) ps) 0"
[PROOF STATE]
proof (state)
this:
xs = list_neq (map (\<lambda>p. sgn (poly p x)) ps) 0

goal (1 subgoal):
 1. sign_changes (map real_of_rat_poly ps) (real_of_rat x) = sign_changes_rat ps x
[PROOF STEP]
have "?l = length (remdups_adj (list_neq (map real_of_rat (map (\<lambda>xa.  (sgn (poly xa x))) ps)) 0)) - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_changes (map real_of_rat_poly ps) (real_of_rat x) = length (remdups_adj (list_neq (map real_of_rat (map (\<lambda>xa. sgn (poly xa x)) ps)) 0)) - 1
[PROOF STEP]
by (simp add: sign_changes_def real_of_rat_sgn o_def)
[PROOF STATE]
proof (state)
this:
sign_changes (map real_of_rat_poly ps) (real_of_rat x) = length (remdups_adj (list_neq (map real_of_rat (map (\<lambda>xa. sgn (poly xa x)) ps)) 0)) - 1

goal (1 subgoal):
 1. sign_changes (map real_of_rat_poly ps) (real_of_rat x) = sign_changes_rat ps x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sign_changes (map real_of_rat_poly ps) (real_of_rat x) = length (remdups_adj (list_neq (map real_of_rat (map (\<lambda>xa. sgn (poly xa x)) ps)) 0)) - 1

goal (1 subgoal):
 1. sign_changes (map real_of_rat_poly ps) (real_of_rat x) = sign_changes_rat ps x
[PROOF STEP]
have "\<dots> = ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remdups_adj (list_neq (map real_of_rat (map (\<lambda>xa. sgn (poly xa x)) ps)) 0)) - 1 = sign_changes_rat ps x
[PROOF STEP]
unfolding sign_changes_rat_def real_of_rat_list_neq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remdups_adj (map real_of_rat (list_neq (map (\<lambda>xa. sgn (poly xa x)) ps) 0))) - 1 = length (remdups_adj (list_neq (map (\<lambda>p. sgn (poly p x)) ps) 0)) - 1
[PROOF STEP]
unfolding real_of_rat_remdups_adj
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map real_of_rat (remdups_adj (list_neq (map (\<lambda>xa. sgn (poly xa x)) ps) 0))) - 1 = length (remdups_adj (list_neq (map (\<lambda>p. sgn (poly p x)) ps) 0)) - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remdups_adj (list_neq (map real_of_rat (map (\<lambda>xa. sgn (poly xa x)) ps)) 0)) - 1 = sign_changes_rat ps x

goal (1 subgoal):
 1. sign_changes (map real_of_rat_poly ps) (real_of_rat x) = sign_changes_rat ps x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sign_changes (map real_of_rat_poly ps) (real_of_rat x) = sign_changes_rat ps x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sign_changes (map real_of_rat_poly ps) (real_of_rat x) = sign_changes_rat ps x

goal (1 subgoal):
 1. sign_changes (map real_of_rat_poly ps) (real_of_rat x) = sign_changes_rat ps x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sign_changes (map real_of_rat_poly ps) (real_of_rat x) = sign_changes_rat ps x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sign_changes_neg_number_rootat: "sign_changes_neg_inf (map real_of_rat_poly ps)
  =  sign_changes_neg_number_rootat ps" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_changes_neg_inf (map real_of_rat_poly ps) = sign_changes_neg_number_rootat ps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sign_changes_neg_inf (map real_of_rat_poly ps) = sign_changes_neg_number_rootat ps
[PROOF STEP]
have "?l = length (remdups_adj (list_neq (map real_of_rat (map poly_neg_number_rootat ps)) 0)) - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_changes_neg_inf (map real_of_rat_poly ps) = length (remdups_adj (list_neq (map real_of_rat (map poly_neg_number_rootat ps)) 0)) - 1
[PROOF STEP]
by (simp add: sign_changes_neg_inf_def o_def real_of_rat_sgn poly_neg_number_rootat)
[PROOF STATE]
proof (state)
this:
sign_changes_neg_inf (map real_of_rat_poly ps) = length (remdups_adj (list_neq (map real_of_rat (map poly_neg_number_rootat ps)) 0)) - 1

goal (1 subgoal):
 1. sign_changes_neg_inf (map real_of_rat_poly ps) = sign_changes_neg_number_rootat ps
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sign_changes_neg_inf (map real_of_rat_poly ps) = length (remdups_adj (list_neq (map real_of_rat (map poly_neg_number_rootat ps)) 0)) - 1

goal (1 subgoal):
 1. sign_changes_neg_inf (map real_of_rat_poly ps) = sign_changes_neg_number_rootat ps
[PROOF STEP]
have "\<dots> = ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remdups_adj (list_neq (map real_of_rat (map poly_neg_number_rootat ps)) 0)) - 1 = sign_changes_neg_number_rootat ps
[PROOF STEP]
unfolding sign_changes_neg_number_rootat_def real_of_rat_list_neq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remdups_adj (map real_of_rat (list_neq (map poly_neg_number_rootat ps) 0))) - 1 = length (remdups_adj (list_neq (map poly_neg_number_rootat ps) 0)) - 1
[PROOF STEP]
unfolding real_of_rat_remdups_adj
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map real_of_rat (remdups_adj (list_neq (map poly_neg_number_rootat ps) 0))) - 1 = length (remdups_adj (list_neq (map poly_neg_number_rootat ps) 0)) - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remdups_adj (list_neq (map real_of_rat (map poly_neg_number_rootat ps)) 0)) - 1 = sign_changes_neg_number_rootat ps

goal (1 subgoal):
 1. sign_changes_neg_inf (map real_of_rat_poly ps) = sign_changes_neg_number_rootat ps
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sign_changes_neg_inf (map real_of_rat_poly ps) = sign_changes_neg_number_rootat ps
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sign_changes_neg_inf (map real_of_rat_poly ps) = sign_changes_neg_number_rootat ps

goal (1 subgoal):
 1. sign_changes_neg_inf (map real_of_rat_poly ps) = sign_changes_neg_number_rootat ps
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sign_changes_neg_inf (map real_of_rat_poly ps) = sign_changes_neg_number_rootat ps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sign_changes_number_rootat: "sign_changes_inf (map real_of_rat_poly ps)
  =  sign_changes_number_rootat ps" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_changes_inf (map real_of_rat_poly ps) = sign_changes_number_rootat ps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sign_changes_inf (map real_of_rat_poly ps) = sign_changes_number_rootat ps
[PROOF STEP]
have "?l = length (remdups_adj (list_neq (map real_of_rat (map poly_number_rootat ps)) 0)) - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_changes_inf (map real_of_rat_poly ps) = length (remdups_adj (list_neq (map real_of_rat (map poly_number_rootat ps)) 0)) - 1
[PROOF STEP]
unfolding sign_changes_inf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remdups_adj (list_neq (map poly_inf (map real_of_rat_poly ps)) 0)) - 1 = length (remdups_adj (list_neq (map real_of_rat (map poly_number_rootat ps)) 0)) - 1
[PROOF STEP]
unfolding map_map o_def real_of_rat_sgn poly_number_rootat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remdups_adj (list_neq (map (\<lambda>x. real_of_rat (poly_number_rootat x)) ps) 0)) - 1 = length (remdups_adj (list_neq (map (\<lambda>x. real_of_rat (poly_number_rootat x)) ps) 0)) - 1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sign_changes_inf (map real_of_rat_poly ps) = length (remdups_adj (list_neq (map real_of_rat (map poly_number_rootat ps)) 0)) - 1

goal (1 subgoal):
 1. sign_changes_inf (map real_of_rat_poly ps) = sign_changes_number_rootat ps
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sign_changes_inf (map real_of_rat_poly ps) = length (remdups_adj (list_neq (map real_of_rat (map poly_number_rootat ps)) 0)) - 1

goal (1 subgoal):
 1. sign_changes_inf (map real_of_rat_poly ps) = sign_changes_number_rootat ps
[PROOF STEP]
have "\<dots> = ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remdups_adj (list_neq (map real_of_rat (map poly_number_rootat ps)) 0)) - 1 = sign_changes_number_rootat ps
[PROOF STEP]
unfolding sign_changes_number_rootat_def real_of_rat_list_neq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remdups_adj (map real_of_rat (list_neq (map poly_number_rootat ps) 0))) - 1 = length (remdups_adj (list_neq (map poly_number_rootat ps) 0)) - 1
[PROOF STEP]
unfolding real_of_rat_remdups_adj
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map real_of_rat (remdups_adj (list_neq (map poly_number_rootat ps) 0))) - 1 = length (remdups_adj (list_neq (map poly_number_rootat ps) 0)) - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remdups_adj (list_neq (map real_of_rat (map poly_number_rootat ps)) 0)) - 1 = sign_changes_number_rootat ps

goal (1 subgoal):
 1. sign_changes_inf (map real_of_rat_poly ps) = sign_changes_number_rootat ps
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sign_changes_inf (map real_of_rat_poly ps) = sign_changes_number_rootat ps
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sign_changes_inf (map real_of_rat_poly ps) = sign_changes_number_rootat ps

goal (1 subgoal):
 1. sign_changes_inf (map real_of_rat_poly ps) = sign_changes_number_rootat ps
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sign_changes_inf (map real_of_rat_poly ps) = sign_changes_number_rootat ps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma count_roots_interval_rat_code[code]:
  "count_roots_interval_rat p = (let rp = map_poly rat_of_int p; ps = sturm_rat rp
    in Root_Info
      (\<lambda> a b. sign_changes_rat ps a - sign_changes_rat ps b + (if poly rp a = 0 then 1 else 0))
      (\<lambda> a. sign_changes_neg_number_rootat ps - sign_changes_rat ps a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_roots_interval_rat p = (let rp = of_int_poly p; ps = sturm_rat rp in Root_Info (\<lambda>a b. sign_changes_rat ps a - sign_changes_rat ps b + (if poly rp a = 0 then 1 else 0)) (\<lambda>a. sign_changes_neg_number_rootat ps - sign_changes_rat ps a))
[PROOF STEP]
unfolding count_roots_interval_rat_def Let_def count_roots_interval_def split of_rat_of_int_poly[symmetric, where 'a = real]
    sturm_rat sign_changes_rat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Root_Info (\<lambda>a b. sign_changes_rat (sturm_rat (of_int_poly p)) a - sign_changes_rat (sturm_rat (of_int_poly p)) b + (if poly (real_of_rat_poly (of_int_poly p)) (real_of_rat a) = 0 then 1 else 0)) (\<lambda>a. sign_changes_neg_inf (map real_of_rat_poly (sturm_rat (of_int_poly p))) - sign_changes_rat (sturm_rat (of_int_poly p)) a) = Root_Info (\<lambda>a b. sign_changes_rat (sturm_rat (of_int_poly p)) a - sign_changes_rat (sturm_rat (of_int_poly p)) b + (if ipoly p a = 0 then 1 else 0)) (\<lambda>a. sign_changes_neg_number_rootat (sturm_rat (of_int_poly p)) - sign_changes_rat (sturm_rat (of_int_poly p)) a)
[PROOF STEP]
by (simp add: sign_changes_neg_number_rootat)


[STATEMENT]
lemma count_roots_rat_code[code]:
  "count_roots_rat p = (let rp = map_poly rat_of_int p in if p = 0 then 0 else let ps = sturm_rat rp
    in sign_changes_neg_number_rootat ps - sign_changes_number_rootat ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_roots_rat p = (let rp = of_int_poly p in if p = 0 then 0 else let ps = sturm_rat rp in sign_changes_neg_number_rootat ps - sign_changes_number_rootat ps)
[PROOF STEP]
unfolding count_roots_rat_def Let_def sturm_rat count_roots_code of_rat_of_int_poly[symmetric, where 'a = real]
    sign_changes_neg_number_rootat sign_changes_number_rootat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if real_of_rat_poly (of_int_poly p) = 0 then 0 else sign_changes_neg_number_rootat (sturm_rat (of_int_poly p)) - sign_changes_number_rootat (sturm_rat (of_int_poly p))) = (if p = 0 then 0 else sign_changes_neg_number_rootat (sturm_rat (of_int_poly p)) - sign_changes_number_rootat (sturm_rat (of_int_poly p)))
[PROOF STEP]
by simp