[STATEMENT]
lemma power_poly_f_mod_i: assumes m: "(poly_rel ===> poly_rel) m (\<lambda> x'. x' mod m')"
  shows "poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
from m
[PROOF STATE]
proof (chain)
picking this:
(poly_rel ===> poly_rel) m (\<lambda>x'. x' mod m')
[PROOF STEP]
have m: "\<And> x x'. poly_rel x x' \<Longrightarrow> poly_rel (m x) (x' mod m')"
[PROOF STATE]
proof (prove)
using this:
(poly_rel ===> poly_rel) m (\<lambda>x'. x' mod m')

goal (1 subgoal):
 1. \<And>x x'. poly_rel x x' \<Longrightarrow> poly_rel (m x) (x' mod m')
[PROOF STEP]
unfolding rel_fun_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. poly_rel x y \<longrightarrow> poly_rel (m x) (y mod m')

goal (1 subgoal):
 1. \<And>x x'. poly_rel x x' \<Longrightarrow> poly_rel (m x) (x' mod m')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly_rel ?x ?x' \<Longrightarrow> poly_rel (m ?x) (?x' mod m')

goal (1 subgoal):
 1. poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
show "poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
proof (induct n arbitrary: f f' rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x f f'. \<lbrakk>\<And>y f f'. \<lbrakk>y < x; poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f y) (power_poly_f_mod m' f' y); poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f x) (power_poly_f_mod m' f' x)
[PROOF STEP]
case (less n f f')
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y < n; poly_rel ?f ?f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m ?f ?y) (power_poly_f_mod m' ?f' ?y)
poly_rel f f'

goal (1 subgoal):
 1. \<And>x f f'. \<lbrakk>\<And>y f f'. \<lbrakk>y < x; poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f y) (power_poly_f_mod m' f' y); poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f x) (power_poly_f_mod m' f' x)
[PROOF STEP]
note f[transfer_rule] = less(2)
[PROOF STATE]
proof (state)
this:
poly_rel f f'

goal (1 subgoal):
 1. \<And>x f f'. \<lbrakk>\<And>y f f'. \<lbrakk>y < x; poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f y) (power_poly_f_mod m' f' y); poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f x) (power_poly_f_mod m' f' x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
 2. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
 2. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
by (simp add: True power_poly_f_mod_i.simps power_poly_f_mod_binary, 
          rule m[OF poly_rel_one])
[PROOF STATE]
proof (state)
this:
poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
hence n: "(n = 0) = False"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. (n = 0) = False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(n = 0) = False

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
obtain q r where div: "Euclidean_Division.divmod_nat n 2 = (q,r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q r. Euclidean_Division.divmod_nat n 2 = (q, r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Euclidean_Division.divmod_nat n 2 = (q, r)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
from this[unfolded Euclidean_Division.divmod_nat_def] n
[PROOF STATE]
proof (chain)
picking this:
(n div 2, n mod 2) = (q, r)
(n = 0) = False
[PROOF STEP]
have "q < n"
[PROOF STATE]
proof (prove)
using this:
(n div 2, n mod 2) = (q, r)
(n = 0) = False

goal (1 subgoal):
 1. q < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q < n

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
note IH = less(1)[OF this]
[PROOF STATE]
proof (state)
this:
poly_rel ?f ?f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m ?f q) (power_poly_f_mod m' ?f' q)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
have rec: "poly_rel (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) 
        (power_poly_f_mod m' (f' * f' mod m') q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) (power_poly_f_mod m' (f' * f' mod m') q)
[PROOF STEP]
by (rule IH, rule m, transfer_prover)
[PROOF STATE]
proof (state)
this:
poly_rel (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) (power_poly_f_mod m' (f' * f' mod m') q)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
have other: "poly_rel 
        (m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f))
        (power_poly_f_mod m' (f' * f' mod m') q * f' mod m')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f)) (power_poly_f_mod m' (f' * f' mod m') q * f' mod m')
[PROOF STEP]
by (rule m, rule poly_rel_times[unfolded rel_fun_def, rule_format, OF rec f])
[PROOF STATE]
proof (state)
this:
poly_rel (m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f)) (power_poly_f_mod m' (f' * f' mod m') q * f' mod m')

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
unfolding power_poly_f_mod_i.simps[of _ _ _ n] Let_def 
        power_poly_f_mod_binary[of _ _ n] div split n if_False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (if r = 0 then power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q else m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f)) (if r = 0 then power_poly_f_mod m' (f' * f' mod m') q else power_poly_f_mod m' (f' * f' mod m') q * f' mod m')
[PROOF STEP]
using rec other
[PROOF STATE]
proof (prove)
using this:
poly_rel (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) (power_poly_f_mod m' (f' * f' mod m') q)
poly_rel (m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f)) (power_poly_f_mod m' (f' * f' mod m') q * f' mod m')

goal (1 subgoal):
 1. poly_rel (if r = 0 then power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q else m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f)) (if r = 0 then power_poly_f_mod m' (f' * f' mod m') q else power_poly_f_mod m' (f' * f' mod m') q * f' mod m')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)

goal:
No subgoals!
[PROOF STEP]
qed