[STATEMENT]
theorem herbrand'_contra:
  assumes finite_cs: "finite Cs" "\<forall>C\<in>Cs. finite C"
  assumes unsat: "\<forall>G. \<not>eval\<^sub>c\<^sub>s HFun G Cs"
  shows "\<exists>T. \<forall>G. branch G T \<longrightarrow> closed_branch G T Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T. anybranch T (\<lambda>G. closed_branch G T Cs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>T. anybranch T (\<lambda>G. closed_branch G T Cs)
[PROOF STEP]
from finite_cs unsat
[PROOF STATE]
proof (chain)
picking this:
finite Cs
\<forall>C\<in>Cs. finite C
\<forall>G. \<not> eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
have "(\<forall>T. \<exists>G. open_branch G T Cs) \<longrightarrow> (\<exists>G. eval\<^sub>c\<^sub>s HFun G Cs)"
[PROOF STATE]
proof (prove)
using this:
finite Cs
\<forall>C\<in>Cs. finite C
\<forall>G. \<not> eval\<^sub>c\<^sub>s HFun G Cs

goal (1 subgoal):
 1. (\<forall>T. \<exists>G. branch G T \<and> \<not> falsifies\<^sub>c\<^sub>s G Cs) \<longrightarrow> (\<exists>G. eval\<^sub>c\<^sub>s HFun G Cs)
[PROOF STEP]
using herbrand'
[PROOF STATE]
proof (prove)
using this:
finite Cs
\<forall>C\<in>Cs. finite C
\<forall>G. \<not> eval\<^sub>c\<^sub>s HFun G Cs
\<lbrakk>\<forall>T. \<exists>G. branch G T \<and> \<not> falsifies\<^sub>c\<^sub>s G ?Cs; finite ?Cs; \<forall>C\<in>?Cs. finite C\<rbrakk> \<Longrightarrow> \<exists>G. eval\<^sub>c\<^sub>s HFun G ?Cs

goal (1 subgoal):
 1. (\<forall>T. \<exists>G. branch G T \<and> \<not> falsifies\<^sub>c\<^sub>s G Cs) \<longrightarrow> (\<exists>G. eval\<^sub>c\<^sub>s HFun G Cs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>T. \<exists>G. branch G T \<and> \<not> falsifies\<^sub>c\<^sub>s G Cs) \<longrightarrow> (\<exists>G. eval\<^sub>c\<^sub>s HFun G Cs)

goal (1 subgoal):
 1. \<exists>T. anybranch T (\<lambda>G. closed_branch G T Cs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<forall>T. \<exists>G. branch G T \<and> \<not> falsifies\<^sub>c\<^sub>s G Cs) \<longrightarrow> (\<exists>G. eval\<^sub>c\<^sub>s HFun G Cs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<forall>T. \<exists>G. branch G T \<and> \<not> falsifies\<^sub>c\<^sub>s G Cs) \<longrightarrow> (\<exists>G. eval\<^sub>c\<^sub>s HFun G Cs)

goal (1 subgoal):
 1. \<exists>T. anybranch T (\<lambda>G. closed_branch G T Cs)
[PROOF STEP]
using unsat
[PROOF STATE]
proof (prove)
using this:
(\<forall>T. \<exists>G. branch G T \<and> \<not> falsifies\<^sub>c\<^sub>s G Cs) \<longrightarrow> (\<exists>G. eval\<^sub>c\<^sub>s HFun G Cs)
\<forall>G. \<not> eval\<^sub>c\<^sub>s HFun G Cs

goal (1 subgoal):
 1. \<exists>T. anybranch T (\<lambda>G. closed_branch G T Cs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>T. anybranch T (\<lambda>G. closed_branch G T Cs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem herbrand:
  assumes unsat: "\<forall>G. \<not>eval\<^sub>c\<^sub>s HFun G Cs"
  assumes finite_cs: "finite Cs" "\<forall>C\<in>Cs. finite C"
  shows "\<exists>T. closed_tree T Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T. closed_tree T Cs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>T. closed_tree T Cs
[PROOF STEP]
from unsat finite_cs
[PROOF STATE]
proof (chain)
picking this:
\<forall>G. \<not> eval\<^sub>c\<^sub>s HFun G Cs
finite Cs
\<forall>C\<in>Cs. finite C
[PROOF STEP]
obtain T where "anybranch T (\<lambda>b. closed_branch b T Cs)"
[PROOF STATE]
proof (prove)
using this:
\<forall>G. \<not> eval\<^sub>c\<^sub>s HFun G Cs
finite Cs
\<forall>C\<in>Cs. finite C

goal (1 subgoal):
 1. (\<And>T. anybranch T (\<lambda>p. closed_branch p T Cs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using herbrand'_contra[of Cs]
[PROOF STATE]
proof (prove)
using this:
\<forall>G. \<not> eval\<^sub>c\<^sub>s HFun G Cs
finite Cs
\<forall>C\<in>Cs. finite C
\<lbrakk>finite Cs; \<forall>C\<in>Cs. finite C; \<forall>G. \<not> eval\<^sub>c\<^sub>s HFun G Cs\<rbrakk> \<Longrightarrow> \<exists>T. anybranch T (\<lambda>G. closed_branch G T Cs)

goal (1 subgoal):
 1. (\<And>T. anybranch T (\<lambda>p. closed_branch p T Cs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
anybranch T (\<lambda>p. closed_branch p T Cs)

goal (1 subgoal):
 1. \<exists>T. closed_tree T Cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
anybranch T (\<lambda>p. closed_branch p T Cs)
[PROOF STEP]
have "\<exists>T. anybranch T (\<lambda>p. falsifies\<^sub>c\<^sub>s p Cs) \<and> anyinternal T (\<lambda>p. \<not> falsifies\<^sub>c\<^sub>s p Cs)"
[PROOF STATE]
proof (prove)
using this:
anybranch T (\<lambda>p. closed_branch p T Cs)

goal (1 subgoal):
 1. \<exists>T. anybranch T (\<lambda>p. falsifies\<^sub>c\<^sub>s p Cs) \<and> anyinternal T (\<lambda>p. \<not> falsifies\<^sub>c\<^sub>s p Cs)
[PROOF STEP]
using cutoff_branch_internal[of T "\<lambda>p. falsifies\<^sub>c\<^sub>s p Cs"]
[PROOF STATE]
proof (prove)
using this:
anybranch T (\<lambda>p. closed_branch p T Cs)
anybranch T (\<lambda>p. falsifies\<^sub>c\<^sub>s p Cs) \<Longrightarrow> \<exists>T'. anyinternal T' (\<lambda>p. \<not> falsifies\<^sub>c\<^sub>s p Cs) \<and> anybranch T' (\<lambda>p. falsifies\<^sub>c\<^sub>s p Cs)

goal (1 subgoal):
 1. \<exists>T. anybranch T (\<lambda>p. falsifies\<^sub>c\<^sub>s p Cs) \<and> anyinternal T (\<lambda>p. \<not> falsifies\<^sub>c\<^sub>s p Cs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>T. anybranch T (\<lambda>p. falsifies\<^sub>c\<^sub>s p Cs) \<and> anyinternal T (\<lambda>p. \<not> falsifies\<^sub>c\<^sub>s p Cs)

goal (1 subgoal):
 1. \<exists>T. closed_tree T Cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>T. anybranch T (\<lambda>p. falsifies\<^sub>c\<^sub>s p Cs) \<and> anyinternal T (\<lambda>p. \<not> falsifies\<^sub>c\<^sub>s p Cs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>T. anybranch T (\<lambda>p. falsifies\<^sub>c\<^sub>s p Cs) \<and> anyinternal T (\<lambda>p. \<not> falsifies\<^sub>c\<^sub>s p Cs)

goal (1 subgoal):
 1. \<exists>T. closed_tree T Cs
[PROOF STEP]
unfolding closed_tree_def
[PROOF STATE]
proof (prove)
using this:
\<exists>T. anybranch T (\<lambda>p. falsifies\<^sub>c\<^sub>s p Cs) \<and> anyinternal T (\<lambda>p. \<not> falsifies\<^sub>c\<^sub>s p Cs)

goal (1 subgoal):
 1. \<exists>T. anybranch T (\<lambda>p. closed_branch p T Cs) \<and> anyinternal T (\<lambda>p. \<not> falsifies\<^sub>c\<^sub>s p Cs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>T. closed_tree T Cs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rat_int_poly_step_agree :
  assumes "coeff (pCons b c2) (degree q) mod coeff q (degree q) = 0"
  shows "(rp a1,rp a2) = (div_rat_poly_step (rp q) \<circ> rat_of_int) b (rp c1,rp c2)
         \<longleftrightarrow> Some (a1,a2) = div_int_poly_step q b (Some (c1,c2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
have coeffs: "coeff (pCons b c2) (degree q) mod coeff q (degree q) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (pCons b c2) (degree q) mod lead_coeff q = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
coeff (pCons b c2) (degree q) mod lead_coeff q = 0

goal (1 subgoal):
 1. coeff (pCons b c2) (degree q) mod lead_coeff q = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeff (pCons b c2) (degree q) mod lead_coeff q = 0

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
let ?ri = "rat_of_int"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
let ?withDiv1 = "pCons (?ri (coeff (pCons b c2) (degree q) div coeff q (degree q))) (rp c1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
let ?withSls1 = "pCons (coeff (pCons (?ri b) (rp c2)) (degree q) / coeff (rp q) (degree q)) (rp c1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
let ?ident1 = "?withDiv1 = ?withSls1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
let ?withDiv2 = "rp (pCons b c2 - smult (coeff (pCons b c2) (degree q) div coeff q (degree q)) q)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
let ?withSls2 = "pCons (?ri b) (rp c2) - smult (coeff (pCons (?ri b) (rp c2)) (degree q) / coeff (rp q) (degree q)) (rp q)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
let ?ident2 = "?withDiv2 = ?withSls2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
note simps = div_int_poly_step_def option.simps Let_def prod.simps
[PROOF STATE]
proof (state)
this:
div_int_poly_step ?q = (\<lambda>a sro. case sro of None \<Rightarrow> None | Some (s, r) \<Rightarrow> let ar = pCons a r; (b, m) = divmod_int (coeff ar (degree ?q)) (lead_coeff ?q) in if m = 0 then Some (pCons b s, ar - smult b ?q) else None)
(Some ?x2.0 = Some ?y2.0) = (?x2.0 = ?y2.0)
None \<noteq> Some ?x2.0
Some ?x2.0 \<noteq> None
(case None of None \<Rightarrow> ?f1.0 | Some x \<Rightarrow> ?f2.0 x) = ?f1.0
(case Some ?x2.0 of None \<Rightarrow> ?f1.0 | Some x \<Rightarrow> ?f2.0 x) = ?f2.0 ?x2.0
rec_option ?f1.0 ?f2.0 None = ?f1.0
rec_option ?f1.0 ?f2.0 (Some ?x2.0) = ?f2.0 ?x2.0
map_option ?f None = None
map_option ?f (Some ?x2.0) = Some (?f ?x2.0)
rel_option ?R None None
rel_option ?R (Some ?x2.0) (Some ?y2.0) = ?R ?x2.0 ?y2.0
\<not> rel_option ?R None (Some ?y2.0)
\<not> rel_option ?R (Some ?y2.0) None
set_option None = {}
set_option (Some ?x2.0) = {?x2.0}
Let ?s ?f \<equiv> ?f ?s
((?x1.0, ?x2.0) = (?y1.0, ?y2.0)) = (?x1.0 = ?y1.0 \<and> ?x2.0 = ?y2.0)
(case (?x1.0, ?x2.0) of (x, xa) \<Rightarrow> ?f x xa) = ?f ?x1.0 ?x2.0
old.rec_prod ?f1.0 (?a, ?b) = ?f1.0 ?a ?b

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
have id1:"?ri (coeff (pCons b c2) (degree q) div coeff q (degree q)) =
            ?ri (coeff (pCons b c2) (degree q)) / ?ri (coeff q (degree q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (coeff (pCons b c2) (degree q) div lead_coeff q) = rat_of_int (coeff (pCons b c2) (degree q)) / rat_of_int (lead_coeff q)
[PROOF STEP]
using coeffs
[PROOF STATE]
proof (prove)
using this:
coeff (pCons b c2) (degree q) mod lead_coeff q = 0

goal (1 subgoal):
 1. rat_of_int (coeff (pCons b c2) (degree q) div lead_coeff q) = rat_of_int (coeff (pCons b c2) (degree q)) / rat_of_int (lead_coeff q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rat_of_int (coeff (pCons b c2) (degree q) div lead_coeff q) = rat_of_int (coeff (pCons b c2) (degree q)) / rat_of_int (lead_coeff q)

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
have id2:"?ident1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pCons (rat_of_int (coeff (pCons b c2) (degree q) div lead_coeff q)) (of_int_poly c1) = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1)
[PROOF STEP]
unfolding id1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pCons (rat_of_int (coeff (pCons b c2) (degree q)) / rat_of_int (lead_coeff q)) (of_int_poly c1) = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1)
[PROOF STEP]
by (simp, fold of_int_hom.coeff_map_poly_hom of_int_hom.map_poly_pCons_hom, simp)
[PROOF STATE]
proof (state)
this:
pCons (rat_of_int (coeff (pCons b c2) (degree q) div lead_coeff q)) (of_int_poly c1) = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1)

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
hence id3:"?ident2"
[PROOF STATE]
proof (prove)
using this:
pCons (rat_of_int (coeff (pCons b c2) (degree q) div lead_coeff q)) (of_int_poly c1) = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1)

goal (1 subgoal):
 1. of_int_poly (pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q)
[PROOF STEP]
using id2
[PROOF STATE]
proof (prove)
using this:
pCons (rat_of_int (coeff (pCons b c2) (degree q) div lead_coeff q)) (of_int_poly c1) = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1)
pCons (rat_of_int (coeff (pCons b c2) (degree q) div lead_coeff q)) (of_int_poly c1) = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1)

goal (1 subgoal):
 1. of_int_poly (pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q)
[PROOF STEP]
by (auto simp: hom_distribs)
[PROOF STATE]
proof (state)
this:
of_int_poly (pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q)

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
have c1:"((rp (pCons (coeff (pCons b c2) (degree q) div coeff q (degree q)) c1)
            ,rp (pCons b c2 - smult (coeff (pCons b c2) (degree q) div coeff q (degree q)) q))
           = div_rat_poly_step (rp q) (?ri b) (rp c1,rp c2)) \<longleftrightarrow> (?ident1 \<and> ?ident2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((of_int_poly (pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1), of_int_poly (pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q)) = div_rat_poly_step (of_int_poly q) (rat_of_int b) (of_int_poly c1, of_int_poly c2)) = (pCons (rat_of_int (coeff (pCons b c2) (degree q) div lead_coeff q)) (of_int_poly c1) = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1) \<and> of_int_poly (pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q))
[PROOF STEP]
unfolding div_rat_poly_step_def simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int_poly (pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1) = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)) (of_int_poly c1) \<and> of_int_poly (pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)) (of_int_poly q)) = (pCons (rat_of_int (coeff (pCons b c2) (degree q) div lead_coeff q)) (of_int_poly c1) = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1) \<and> of_int_poly (pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q))
[PROOF STEP]
by (simp add: hom_distribs)
[PROOF STATE]
proof (state)
this:
((of_int_poly (pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1), of_int_poly (pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q)) = div_rat_poly_step (of_int_poly q) (rat_of_int b) (of_int_poly c1, of_int_poly c2)) = (pCons (rat_of_int (coeff (pCons b c2) (degree q) div lead_coeff q)) (of_int_poly c1) = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1) \<and> of_int_poly (pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q))

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
have "((rp a1, rp a2) = (div_rat_poly_step (rp q) \<circ> rat_of_int) b (rp c1, rp c2)) \<longleftrightarrow>
             (rp a1 = ?withSls1 \<and> rp a2 = ?withSls2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (of_int_poly a1 = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1) \<and> of_int_poly a2 = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q))
[PROOF STEP]
unfolding div_rat_poly_step_def simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = ((\<lambda>a (s, r). (pCons (coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)) s, pCons a r - smult (coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)) (of_int_poly q))) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (of_int_poly a1 = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1) \<and> of_int_poly a2 = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (of_int_poly a1 = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1) \<and> of_int_poly a2 = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q))

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (of_int_poly a1 = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1) \<and> of_int_poly a2 = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q))

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
have "\<dots> \<longleftrightarrow>
      ((a1 = pCons (coeff (pCons b c2) (degree q) div coeff q (degree q)) c1) \<and>
       (a2 = pCons b c2 - smult (coeff (pCons b c2) (degree q) div coeff q (degree q)) q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int_poly a1 = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1) \<and> of_int_poly a2 = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q)) = (a1 = pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1 \<and> a2 = pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q)
[PROOF STEP]
by (fold id2 id3 of_int_hom.map_poly_pCons_hom, unfold of_int_poly_hom.eq_iff, auto)
[PROOF STATE]
proof (state)
this:
(of_int_poly a1 = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1) \<and> of_int_poly a2 = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q)) = (a1 = pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1 \<and> a2 = pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q)

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(of_int_poly a1 = pCons (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly c1) \<and> of_int_poly a2 = pCons (rat_of_int b) (of_int_poly c2) - smult (coeff (pCons (rat_of_int b) (of_int_poly c2)) (degree q) / coeff (of_int_poly q) (degree q)) (of_int_poly q)) = (a1 = pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1 \<and> a2 = pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q)

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
have c0:"\<dots> \<longleftrightarrow> Some (a1,a2) = div_int_poly_step q b (Some (c1,c2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a1 = pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1 \<and> a2 = pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
unfolding divmod_int_def div_int_poly_step_def option.simps Let_def prod.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a1 = pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1 \<and> a2 = pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) = (Some (a1, a2) = (if coeff (pCons b c2) (degree q) mod lead_coeff q = 0 then Some (pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1, pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) else None))
[PROOF STEP]
using coeffs
[PROOF STATE]
proof (prove)
using this:
coeff (pCons b c2) (degree q) mod lead_coeff q = 0

goal (1 subgoal):
 1. (a1 = pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1 \<and> a2 = pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) = (Some (a1, a2) = (if coeff (pCons b c2) (degree q) mod lead_coeff q = 0 then Some (pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1, pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) else None))
[PROOF STEP]
by (auto split: option.splits prod.splits if_splits)
[PROOF STATE]
proof (state)
this:
(a1 = pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1 \<and> a2 = pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))

goal (1 subgoal):
 1. ((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)) = (Some (a1, a2) = div_int_poly_step q b (Some (c1, c2)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma int_step_then_rat_poly_step :
  assumes Some:"Some (a1,a2) = div_int_poly_step q b (Some (c1,c2))"
  shows "(rp a1,rp a2) = (div_rat_poly_step (rp q) \<circ> rat_of_int) b (rp c1,rp c2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)
[PROOF STEP]
note simps = div_int_poly_step_def option.simps Let_def divmod_int_def prod.simps
[PROOF STATE]
proof (state)
this:
div_int_poly_step ?q = (\<lambda>a sro. case sro of None \<Rightarrow> None | Some (s, r) \<Rightarrow> let ar = pCons a r; (b, m) = divmod_int (coeff ar (degree ?q)) (lead_coeff ?q) in if m = 0 then Some (pCons b s, ar - smult b ?q) else None)
(Some ?x2.0 = Some ?y2.0) = (?x2.0 = ?y2.0)
None \<noteq> Some ?x2.0
Some ?x2.0 \<noteq> None
(case None of None \<Rightarrow> ?f1.0 | Some x \<Rightarrow> ?f2.0 x) = ?f1.0
(case Some ?x2.0 of None \<Rightarrow> ?f1.0 | Some x \<Rightarrow> ?f2.0 x) = ?f2.0 ?x2.0
rec_option ?f1.0 ?f2.0 None = ?f1.0
rec_option ?f1.0 ?f2.0 (Some ?x2.0) = ?f2.0 ?x2.0
map_option ?f None = None
map_option ?f (Some ?x2.0) = Some (?f ?x2.0)
rel_option ?R None None
rel_option ?R (Some ?x2.0) (Some ?y2.0) = ?R ?x2.0 ?y2.0
\<not> rel_option ?R None (Some ?y2.0)
\<not> rel_option ?R (Some ?y2.0) None
set_option None = {}
set_option (Some ?x2.0) = {?x2.0}
Let ?s ?f \<equiv> ?f ?s
divmod_int ?n ?m = (?n div ?m, ?n mod ?m)
((?x1.0, ?x2.0) = (?y1.0, ?y2.0)) = (?x1.0 = ?y1.0 \<and> ?x2.0 = ?y2.0)
(case (?x1.0, ?x2.0) of (x, xa) \<Rightarrow> ?f x xa) = ?f ?x1.0 ?x2.0
old.rec_prod ?f1.0 (?a, ?b) = ?f1.0 ?a ?b

goal (1 subgoal):
 1. (of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)
[PROOF STEP]
from Some[unfolded simps]
[PROOF STATE]
proof (chain)
picking this:
Some (a1, a2) = (if coeff (pCons b c2) (degree q) mod lead_coeff q = 0 then Some (pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1, pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) else None)
[PROOF STEP]
have mod0: "coeff (pCons b c2) (degree q) mod coeff q (degree q) = 0"
[PROOF STATE]
proof (prove)
using this:
Some (a1, a2) = (if coeff (pCons b c2) (degree q) mod lead_coeff q = 0 then Some (pCons (coeff (pCons b c2) (degree q) div lead_coeff q) c1, pCons b c2 - smult (coeff (pCons b c2) (degree q) div lead_coeff q) q) else None)

goal (1 subgoal):
 1. coeff (pCons b c2) (degree q) mod lead_coeff q = 0
[PROOF STEP]
by (auto split: option.splits prod.splits if_splits)
[PROOF STATE]
proof (state)
this:
coeff (pCons b c2) (degree q) mod lead_coeff q = 0

goal (1 subgoal):
 1. (of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
coeff (pCons b c2) (degree q) mod lead_coeff q = 0

goal (1 subgoal):
 1. (of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)
[PROOF STEP]
using assms rat_int_poly_step_agree
[PROOF STATE]
proof (prove)
using this:
coeff (pCons b c2) (degree q) mod lead_coeff q = 0
Some (a1, a2) = div_int_poly_step q b (Some (c1, c2))
coeff (pCons ?b ?c2.0) (degree ?q) mod lead_coeff ?q = 0 \<Longrightarrow> ((of_int_poly ?a1.0, of_int_poly ?a2.0) = (div_rat_poly_step (of_int_poly ?q) \<circ> rat_of_int) ?b (of_int_poly ?c1.0, of_int_poly ?c2.0)) = (Some (?a1.0, ?a2.0) = div_int_poly_step ?q ?b (Some (?c1.0, ?c2.0)))

goal (1 subgoal):
 1. (of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (of_int_poly c1, of_int_poly c2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_int_rat_division :
  assumes "y \<noteq> 0"
  shows "is_int_rat (rat_of_int x / rat_of_int y) \<longleftrightarrow> x mod y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_int_rat (rat_of_int x / rat_of_int y) = (x mod y = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_int_rat (rat_of_int x / rat_of_int y) \<Longrightarrow> x mod y = 0
 2. x mod y = 0 \<Longrightarrow> is_int_rat (rat_of_int x / rat_of_int y)
[PROOF STEP]
assume "is_int_rat (rat_of_int x / rat_of_int y)"
[PROOF STATE]
proof (state)
this:
is_int_rat (rat_of_int x / rat_of_int y)

goal (2 subgoals):
 1. is_int_rat (rat_of_int x / rat_of_int y) \<Longrightarrow> x mod y = 0
 2. x mod y = 0 \<Longrightarrow> is_int_rat (rat_of_int x / rat_of_int y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_int_rat (rat_of_int x / rat_of_int y)
[PROOF STEP]
obtain v where v_def:"rat_of_int v = rat_of_int x / rat_of_int y"
[PROOF STATE]
proof (prove)
using this:
is_int_rat (rat_of_int x / rat_of_int y)

goal (1 subgoal):
 1. (\<And>v. rat_of_int v = rat_of_int x / rat_of_int y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using int_of_rat(2) is_int_rat
[PROOF STATE]
proof (prove)
using this:
is_int_rat (rat_of_int x / rat_of_int y)
?z \<in> \<int> \<Longrightarrow> rat_of_int (int_of_rat ?z) = ?z
is_int_rat ?x = (?x \<in> \<int>)

goal (1 subgoal):
 1. (\<And>v. rat_of_int v = rat_of_int x / rat_of_int y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
rat_of_int v = rat_of_int x / rat_of_int y

goal (2 subgoals):
 1. is_int_rat (rat_of_int x / rat_of_int y) \<Longrightarrow> x mod y = 0
 2. x mod y = 0 \<Longrightarrow> is_int_rat (rat_of_int x / rat_of_int y)
[PROOF STEP]
hence "v = \<lfloor>rat_of_int x / rat_of_int y\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
rat_of_int v = rat_of_int x / rat_of_int y

goal (1 subgoal):
 1. v = \<lfloor>rat_of_int x / rat_of_int y\<rfloor>
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
v = \<lfloor>rat_of_int x / rat_of_int y\<rfloor>

goal (2 subgoals):
 1. is_int_rat (rat_of_int x / rat_of_int y) \<Longrightarrow> x mod y = 0
 2. x mod y = 0 \<Longrightarrow> is_int_rat (rat_of_int x / rat_of_int y)
[PROOF STEP]
hence "v * y = x - x mod y"
[PROOF STATE]
proof (prove)
using this:
v = \<lfloor>rat_of_int x / rat_of_int y\<rfloor>

goal (1 subgoal):
 1. v * y = x - x mod y
[PROOF STEP]
using div_is_floor_divide_rat mod_div_equality_int
[PROOF STATE]
proof (prove)
using this:
v = \<lfloor>rat_of_int x / rat_of_int y\<rfloor>
?n div ?y = \<lfloor>rat_of_int ?n / rat_of_int ?y\<rfloor>
?n div ?x * ?x = ?n - ?n mod ?x

goal (1 subgoal):
 1. v * y = x - x mod y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v * y = x - x mod y

goal (2 subgoals):
 1. is_int_rat (rat_of_int x / rat_of_int y) \<Longrightarrow> x mod y = 0
 2. x mod y = 0 \<Longrightarrow> is_int_rat (rat_of_int x / rat_of_int y)
[PROOF STEP]
hence "rat_of_int v * rat_of_int y = rat_of_int x - rat_of_int (x mod y)"
[PROOF STATE]
proof (prove)
using this:
v * y = x - x mod y

goal (1 subgoal):
 1. rat_of_int v * rat_of_int y = rat_of_int x - rat_of_int (x mod y)
[PROOF STEP]
by (fold hom_distribs, unfold of_int_hom.eq_iff)
[PROOF STATE]
proof (state)
this:
rat_of_int v * rat_of_int y = rat_of_int x - rat_of_int (x mod y)

goal (2 subgoals):
 1. is_int_rat (rat_of_int x / rat_of_int y) \<Longrightarrow> x mod y = 0
 2. x mod y = 0 \<Longrightarrow> is_int_rat (rat_of_int x / rat_of_int y)
[PROOF STEP]
hence "(rat_of_int x / rat_of_int y) * rat_of_int y = rat_of_int x - rat_of_int (x mod y)"
[PROOF STATE]
proof (prove)
using this:
rat_of_int v * rat_of_int y = rat_of_int x - rat_of_int (x mod y)

goal (1 subgoal):
 1. rat_of_int x / rat_of_int y * rat_of_int y = rat_of_int x - rat_of_int (x mod y)
[PROOF STEP]
using v_def
[PROOF STATE]
proof (prove)
using this:
rat_of_int v * rat_of_int y = rat_of_int x - rat_of_int (x mod y)
rat_of_int v = rat_of_int x / rat_of_int y

goal (1 subgoal):
 1. rat_of_int x / rat_of_int y * rat_of_int y = rat_of_int x - rat_of_int (x mod y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rat_of_int x / rat_of_int y * rat_of_int y = rat_of_int x - rat_of_int (x mod y)

goal (2 subgoals):
 1. is_int_rat (rat_of_int x / rat_of_int y) \<Longrightarrow> x mod y = 0
 2. x mod y = 0 \<Longrightarrow> is_int_rat (rat_of_int x / rat_of_int y)
[PROOF STEP]
hence "rat_of_int x = rat_of_int x - rat_of_int (x mod y)"
[PROOF STATE]
proof (prove)
using this:
rat_of_int x / rat_of_int y * rat_of_int y = rat_of_int x - rat_of_int (x mod y)

goal (1 subgoal):
 1. rat_of_int x = rat_of_int x - rat_of_int (x mod y)
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
rat_of_int x = rat_of_int x - rat_of_int (x mod y)

goal (2 subgoals):
 1. is_int_rat (rat_of_int x / rat_of_int y) \<Longrightarrow> x mod y = 0
 2. x mod y = 0 \<Longrightarrow> is_int_rat (rat_of_int x / rat_of_int y)
[PROOF STEP]
thus "x mod y = 0"
[PROOF STATE]
proof (prove)
using this:
rat_of_int x = rat_of_int x - rat_of_int (x mod y)

goal (1 subgoal):
 1. x mod y = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x mod y = 0

goal (1 subgoal):
 1. x mod y = 0 \<Longrightarrow> is_int_rat (rat_of_int x / rat_of_int y)
[PROOF STEP]
qed (force)


[STATEMENT]
lemma pCons_of_rp_contains_ints :
  assumes "rp a = pCons b c"
    shows "is_int_rat b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_int_rat b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_int_rat b
[PROOF STEP]
have "\<And> b n. rp a = b \<Longrightarrow> is_int_rat (coeff b n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b n. of_int_poly a = b \<Longrightarrow> is_int_rat (coeff b n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int_poly a = ?b \<Longrightarrow> is_int_rat (coeff ?b ?n)

goal (1 subgoal):
 1. is_int_rat b
[PROOF STEP]
hence "rp a = pCons b c \<Longrightarrow> is_int_rat (coeff (pCons b c) 0)"
[PROOF STATE]
proof (prove)
using this:
of_int_poly a = ?b \<Longrightarrow> is_int_rat (coeff ?b ?n)

goal (1 subgoal):
 1. of_int_poly a = pCons b c \<Longrightarrow> is_int_rat (coeff (pCons b c) 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
of_int_poly a = pCons b c \<Longrightarrow> is_int_rat (coeff (pCons b c) 0)

goal (1 subgoal):
 1. is_int_rat b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
of_int_poly a = pCons b c \<Longrightarrow> is_int_rat (coeff (pCons b c) 0)

goal (1 subgoal):
 1. is_int_rat b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
of_int_poly a = pCons b c \<Longrightarrow> is_int_rat (coeff (pCons b c) 0)
of_int_poly a = pCons b c

goal (1 subgoal):
 1. is_int_rat b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_int_rat b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rat_step_then_int_poly_step :
  assumes "q \<noteq> 0"
      and "(rp a1,rp a2) = (div_rat_poly_step (rp q) \<circ> rat_of_int) b2 (rp c1,rp c2)"
  shows "Some (a1,a2) = div_int_poly_step q b2 (Some (c1,c2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
let ?mustbeint = "rat_of_int (coeff (pCons b2 c2) (degree q)) / rat_of_int (coeff q (degree q))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
let ?mustbeint2 = "coeff (pCons (rat_of_int b2) (rp c2)) (degree (rp q))
    / coeff (rp q) (degree (rp q))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
have mustbeint : "?mustbeint = ?mustbeint2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int (coeff (pCons b2 c2) (degree q)) / rat_of_int (lead_coeff q) = coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)
[PROOF STEP]
by (fold hom_distribs of_int_hom.coeff_map_poly_hom, simp)
[PROOF STATE]
proof (state)
this:
rat_of_int (coeff (pCons b2 c2) (degree q)) / rat_of_int (lead_coeff q) = coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)

goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
note simps = div_int_poly_step_def option.simps Let_def divmod_int_def prod.simps
[PROOF STATE]
proof (state)
this:
div_int_poly_step ?q = (\<lambda>a sro. case sro of None \<Rightarrow> None | Some (s, r) \<Rightarrow> let ar = pCons a r; (b, m) = divmod_int (coeff ar (degree ?q)) (lead_coeff ?q) in if m = 0 then Some (pCons b s, ar - smult b ?q) else None)
(Some ?x2.0 = Some ?y2.0) = (?x2.0 = ?y2.0)
None \<noteq> Some ?x2.0
Some ?x2.0 \<noteq> None
(case None of None \<Rightarrow> ?f1.0 | Some x \<Rightarrow> ?f2.0 x) = ?f1.0
(case Some ?x2.0 of None \<Rightarrow> ?f1.0 | Some x \<Rightarrow> ?f2.0 x) = ?f2.0 ?x2.0
rec_option ?f1.0 ?f2.0 None = ?f1.0
rec_option ?f1.0 ?f2.0 (Some ?x2.0) = ?f2.0 ?x2.0
map_option ?f None = None
map_option ?f (Some ?x2.0) = Some (?f ?x2.0)
rel_option ?R None None
rel_option ?R (Some ?x2.0) (Some ?y2.0) = ?R ?x2.0 ?y2.0
\<not> rel_option ?R None (Some ?y2.0)
\<not> rel_option ?R (Some ?y2.0) None
set_option None = {}
set_option (Some ?x2.0) = {?x2.0}
Let ?s ?f \<equiv> ?f ?s
divmod_int ?n ?m = (?n div ?m, ?n mod ?m)
((?x1.0, ?x2.0) = (?y1.0, ?y2.0)) = (?x1.0 = ?y1.0 \<and> ?x2.0 = ?y2.0)
(case (?x1.0, ?x2.0) of (x, xa) \<Rightarrow> ?f x xa) = ?f ?x1.0 ?x2.0
old.rec_prod ?f1.0 (?a, ?b) = ?f1.0 ?a ?b

goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
from assms leading_coeff_neq_0[of q]
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> 0
(of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b2 (of_int_poly c1, of_int_poly c2)
q \<noteq> 0 \<Longrightarrow> lead_coeff q \<noteq> 0
[PROOF STEP]
have q0:"coeff q (degree q) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
q \<noteq> 0
(of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b2 (of_int_poly c1, of_int_poly c2)
q \<noteq> 0 \<Longrightarrow> lead_coeff q \<noteq> 0

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

goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
have "rp a1 = pCons ?mustbeint2 (rp c1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly a1 = pCons (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)) (of_int_poly c1)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b2 (of_int_poly c1, of_int_poly c2)

goal (1 subgoal):
 1. of_int_poly a1 = pCons (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)) (of_int_poly c1)
[PROOF STEP]
unfolding div_rat_poly_step_def
[PROOF STATE]
proof (prove)
using this:
(of_int_poly a1, of_int_poly a2) = ((\<lambda>a (s, r). let b = coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q) in (pCons b s, pCons a r - smult b (of_int_poly q))) \<circ> rat_of_int) b2 (of_int_poly c1, of_int_poly c2)

goal (1 subgoal):
 1. of_int_poly a1 = pCons (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)) (of_int_poly c1)
[PROOF STEP]
by (simp add:div_int_poly_step_def Let_def)
[PROOF STATE]
proof (state)
this:
of_int_poly a1 = pCons (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)) (of_int_poly c1)

goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
hence "is_int_rat ?mustbeint2"
[PROOF STATE]
proof (prove)
using this:
of_int_poly a1 = pCons (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)) (of_int_poly c1)

goal (1 subgoal):
 1. is_int_rat (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q))
[PROOF STEP]
unfolding div_rat_poly_step_def
[PROOF STATE]
proof (prove)
using this:
of_int_poly a1 = pCons (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)) (of_int_poly c1)

goal (1 subgoal):
 1. is_int_rat (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q))
[PROOF STEP]
using pCons_of_rp_contains_ints
[PROOF STATE]
proof (prove)
using this:
of_int_poly a1 = pCons (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)) (of_int_poly c1)
of_int_poly ?a = pCons ?b ?c \<Longrightarrow> is_int_rat ?b

goal (1 subgoal):
 1. is_int_rat (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_int_rat (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q))

goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
hence "is_int_rat ?mustbeint"
[PROOF STATE]
proof (prove)
using this:
is_int_rat (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q))

goal (1 subgoal):
 1. is_int_rat (rat_of_int (coeff (pCons b2 c2) (degree q)) / rat_of_int (lead_coeff q))
[PROOF STEP]
unfolding mustbeint
[PROOF STATE]
proof (prove)
using this:
is_int_rat (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q))

goal (1 subgoal):
 1. is_int_rat (coeff (pCons (rat_of_int b2) (of_int_poly c2)) (degree (of_int_poly q)) / lead_coeff (of_int_poly q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_int_rat (rat_of_int (coeff (pCons b2 c2) (degree q)) / rat_of_int (lead_coeff q))

goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
hence "coeff (pCons b2 c2) (degree q) mod coeff q (degree q) = 0"
[PROOF STATE]
proof (prove)
using this:
is_int_rat (rat_of_int (coeff (pCons b2 c2) (degree q)) / rat_of_int (lead_coeff q))

goal (1 subgoal):
 1. coeff (pCons b2 c2) (degree q) mod lead_coeff q = 0
[PROOF STEP]
using is_int_rat_division q0
[PROOF STATE]
proof (prove)
using this:
is_int_rat (rat_of_int (coeff (pCons b2 c2) (degree q)) / rat_of_int (lead_coeff q))
?y \<noteq> 0 \<Longrightarrow> is_int_rat (rat_of_int ?x / rat_of_int ?y) = (?x mod ?y = 0)
lead_coeff q \<noteq> 0

goal (1 subgoal):
 1. coeff (pCons b2 c2) (degree q) mod lead_coeff q = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coeff (pCons b2 c2) (degree q) mod lead_coeff q = 0

goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
coeff (pCons b2 c2) (degree q) mod lead_coeff q = 0

goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
using rat_int_poly_step_agree assms
[PROOF STATE]
proof (prove)
using this:
coeff (pCons b2 c2) (degree q) mod lead_coeff q = 0
coeff (pCons ?b ?c2.0) (degree ?q) mod lead_coeff ?q = 0 \<Longrightarrow> ((of_int_poly ?a1.0, of_int_poly ?a2.0) = (div_rat_poly_step (of_int_poly ?q) \<circ> rat_of_int) ?b (of_int_poly ?c1.0, of_int_poly ?c2.0)) = (Some (?a1.0, ?a2.0) = div_int_poly_step ?q ?b (Some (?c1.0, ?c2.0)))
q \<noteq> 0
(of_int_poly a1, of_int_poly a2) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b2 (of_int_poly c1, of_int_poly c2)

goal (1 subgoal):
 1. Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some (a1, a2) = div_int_poly_step q b2 (Some (c1, c2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma div_int_poly_step_surjective : "Some a = div_int_poly_step q b c \<Longrightarrow> \<exists> c'. c = Some c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some a = div_int_poly_step q b c \<Longrightarrow> \<exists>c'. c = Some c'
[PROOF STEP]
unfolding div_int_poly_step_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some a = (case c of None \<Rightarrow> None | Some (s, r) \<Rightarrow> let ar = pCons b r; (b, m) = divmod_int (coeff ar (degree q)) (lead_coeff q) in if m = 0 then Some (pCons b s, ar - smult b q) else None) \<Longrightarrow> \<exists>c'. c = Some c'
[PROOF STEP]
by(cases c, simp_all)


[STATEMENT]
lemma  div_mod_int_poly_then_pdivmod:
  assumes "div_mod_int_poly p q = Some (r,m)"
  shows   "(rp p div rp q, rp p mod rp q) = (rp r, rp m)"
    and   "q \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m) &&& q \<noteq> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
 2. q \<noteq> 0
[PROOF STEP]
let ?rpp = "(\<lambda> (a,b). (rp a,rp b))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
 2. q \<noteq> 0
[PROOF STEP]
let ?p = "rp p"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
 2. q \<noteq> 0
[PROOF STEP]
let ?q = "rp q"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
 2. q \<noteq> 0
[PROOF STEP]
let ?r = "rp r"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
 2. q \<noteq> 0
[PROOF STEP]
let ?m = "rp m"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
 2. q \<noteq> 0
[PROOF STEP]
let ?div_rat_step = "div_rat_poly_step ?q"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
 2. q \<noteq> 0
[PROOF STEP]
let ?div_int_step = "div_int_poly_step q"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
 2. q \<noteq> 0
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
show q0 : "q \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
div_mod_int_poly p q = Some (r, m)

goal (1 subgoal):
 1. q \<noteq> 0
[PROOF STEP]
using div_mod_int_poly_def
[PROOF STATE]
proof (prove)
using this:
div_mod_int_poly p q = Some (r, m)
div_mod_int_poly ?p ?q = (if ?q = 0 then None else let n = degree ?q; qn = coeff ?q n in fold_coeffs (div_int_poly_step ?q) ?p (Some (0, 0)))

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

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
hence "div_mod_int_poly p q = Some (r,m) \<longleftrightarrow> Some (r,m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))"
[PROOF STATE]
proof (prove)
using this:
q \<noteq> 0

goal (1 subgoal):
 1. (div_mod_int_poly p q = Some (r, m)) = (Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0)))
[PROOF STEP]
unfolding div_mod_int_poly_def fold_coeffs_def
[PROOF STATE]
proof (prove)
using this:
q \<noteq> 0

goal (1 subgoal):
 1. ((if q = 0 then None else let n = degree q; qn = coeff q n in foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))) = Some (r, m)) = (Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0)))
[PROOF STEP]
by (auto split: option.splits prod.splits if_splits)
[PROOF STATE]
proof (state)
this:
(div_mod_int_poly p q = Some (r, m)) = (Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0)))

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
hence innerRes: "Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0, 0))"
[PROOF STATE]
proof (prove)
using this:
(div_mod_int_poly p q = Some (r, m)) = (Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0)))

goal (1 subgoal):
 1. Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(div_mod_int_poly p q = Some (r, m)) = (Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0)))
div_mod_int_poly p q = Some (r, m)

goal (1 subgoal):
 1. Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
fix oldRes res :: "int poly \<times> int poly"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
fix lst :: "int list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
have "Some res = foldr ?div_int_step lst (Some oldRes) \<Longrightarrow>
          ?rpp res = foldr (?div_rat_step \<circ> rat_of_int) lst (?rpp oldRes)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some res = foldr (div_int_poly_step q) lst (Some oldRes) \<Longrightarrow> (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
using foldr_cong_plus[of "set lst" Some ?div_int_step ?rpp "?div_rat_step \<circ> rat_of_int"
        lst res oldRes] int_step_then_rat_poly_step div_int_poly_step_surjective
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>a b c. \<lbrakk>b \<in> set lst; Some a = div_int_poly_step q b (Some c)\<rbrakk> \<Longrightarrow> (case a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (case c of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)); \<And>a b. Some a = Some b \<Longrightarrow> a = b; \<And>a b c. Some a = div_int_poly_step q b c \<Longrightarrow> \<exists>c'. c = Some c'; set lst \<subseteq> set lst; Some res = foldr (div_int_poly_step q) lst (Some oldRes)\<rbrakk> \<Longrightarrow> (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
Some (?a1.0, ?a2.0) = div_int_poly_step ?q ?b (Some (?c1.0, ?c2.0)) \<Longrightarrow> (of_int_poly ?a1.0, of_int_poly ?a2.0) = (div_rat_poly_step (of_int_poly ?q) \<circ> rat_of_int) ?b (of_int_poly ?c1.0, of_int_poly ?c2.0)
Some ?a = div_int_poly_step ?q ?b ?c \<Longrightarrow> \<exists>c'. ?c = Some c'

goal (1 subgoal):
 1. Some res = foldr (div_int_poly_step q) lst (Some oldRes) \<Longrightarrow> (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some res = foldr (div_int_poly_step q) lst (Some oldRes) \<Longrightarrow> (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
hence "Some res = foldr ?div_int_step lst (Some oldRes)
      \<Longrightarrow> ?rpp res = foldr ?div_rat_step (map rat_of_int lst) (?rpp oldRes)"
[PROOF STATE]
proof (prove)
using this:
Some res = foldr (div_int_poly_step q) lst (Some oldRes) \<Longrightarrow> (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))

goal (1 subgoal):
 1. Some res = foldr (div_int_poly_step q) lst (Some oldRes) \<Longrightarrow> (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int lst) (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
using foldr_map[of ?div_rat_step rat_of_int lst]
[PROOF STATE]
proof (prove)
using this:
Some res = foldr (div_int_poly_step q) lst (Some oldRes) \<Longrightarrow> (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int lst) ?a = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst ?a

goal (1 subgoal):
 1. Some res = foldr (div_int_poly_step q) lst (Some oldRes) \<Longrightarrow> (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int lst) (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some res = foldr (div_int_poly_step q) lst (Some oldRes) \<Longrightarrow> (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int lst) (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Some ?res2 = foldr (div_int_poly_step q) ?lst2 (Some ?oldRes2) \<Longrightarrow> (case ?res2 of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int ?lst2) (case ?oldRes2 of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
hence equal_foldr : "Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0,0))
    \<Longrightarrow> ?rpp (r,m) = foldr (?div_rat_step) (map rat_of_int (coeffs p)) (?rpp (0,0))"
[PROOF STATE]
proof (prove)
using this:
Some ?res2 = foldr (div_int_poly_step q) ?lst2 (Some ?oldRes2) \<Longrightarrow> (case ?res2 of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int ?lst2) (case ?oldRes2 of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))

goal (1 subgoal):
 1. Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0)) \<Longrightarrow> (case (r, m) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int (coeffs p)) (case (0, 0) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0)) \<Longrightarrow> (case (r, m) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int (coeffs p)) (case (0, 0) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
have "(map rat_of_int (coeffs p) = coeffs ?p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map rat_of_int (coeffs p) = coeffs (of_int_poly p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map rat_of_int (coeffs p) = coeffs (of_int_poly p)

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
hence "(?r,?m) = (foldr (?div_rat_step) (coeffs ?p) (0,0))"
[PROOF STATE]
proof (prove)
using this:
map rat_of_int (coeffs p) = coeffs (of_int_poly p)

goal (1 subgoal):
 1. (of_int_poly r, of_int_poly m) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p)) (0, 0)
[PROOF STEP]
using equal_foldr innerRes
[PROOF STATE]
proof (prove)
using this:
map rat_of_int (coeffs p) = coeffs (of_int_poly p)
Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0)) \<Longrightarrow> (case (r, m) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int (coeffs p)) (case (0, 0) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))

goal (1 subgoal):
 1. (of_int_poly r, of_int_poly m) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p)) (0, 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(of_int_poly r, of_int_poly m) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p)) (0, 0)

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
thus "(?p div ?q, ?p mod ?q) = (?r,?m)"
[PROOF STATE]
proof (prove)
using this:
(of_int_poly r, of_int_poly m) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p)) (0, 0)

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
using fold_coeffs_def [of "?div_rat_step" ?p] q0
      div_mod_fold_coeffs [of ?p ?q]
[PROOF STATE]
proof (prove)
using this:
(of_int_poly r, of_int_poly m) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p)) (0, 0)
fold_coeffs (div_rat_poly_step (of_int_poly q)) (of_int_poly p) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p))
q \<noteq> 0
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (if of_int_poly q = 0 then (0, of_int_poly p) else fold_coeffs (\<lambda>a (s, r). let b = coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q) in (pCons b s, pCons a r - smult b (of_int_poly q))) (of_int_poly p) (0, 0))

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
unfolding div_rat_poly_step_def
[PROOF STATE]
proof (prove)
using this:
(of_int_poly r, of_int_poly m) = foldr (\<lambda>a (s, r). let b = coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q) in (pCons b s, pCons a r - smult b (of_int_poly q))) (coeffs (of_int_poly p)) (0, 0)
fold_coeffs (\<lambda>a (s, r). let b = coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q) in (pCons b s, pCons a r - smult b (of_int_poly q))) (of_int_poly p) = foldr (\<lambda>a (s, r). let b = coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q) in (pCons b s, pCons a r - smult b (of_int_poly q))) (coeffs (of_int_poly p))
q \<noteq> 0
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (if of_int_poly q = 0 then (0, of_int_poly p) else fold_coeffs (\<lambda>a (s, r). let b = coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q) in (pCons b s, pCons a r - smult b (of_int_poly q))) (of_int_poly p) (0, 0))

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma div_rat_poly_step_sur:
 assumes "(case a of (a, b) \<Rightarrow> (rp a, rp b)) = (div_rat_poly_step (rp q) \<circ> rat_of_int) x pair"
   shows "\<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (rp a, rp b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
obtain b1 b2 where pair: "pair = (b1, b2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b1 b2. pair = (b1, b2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases pair) simp
[PROOF STATE]
proof (state)
this:
pair = (b1, b2)

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
define p12 where "p12 = coeff (pCons (rat_of_int x) b2) (degree (rp q)) / coeff (rp q) (degree (rp q))"
[PROOF STATE]
proof (state)
this:
p12 = coeff (pCons (rat_of_int x) b2) (degree (of_int_poly q)) / lead_coeff (of_int_poly q)

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
obtain a1 a2 where "a = (a1, a2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a1 a2. a = (a1, a2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases a) simp
[PROOF STATE]
proof (state)
this:
a = (a1, a2)

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
with assms pair
[PROOF STATE]
proof (chain)
picking this:
(case a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) x pair
pair = (b1, b2)
a = (a1, a2)
[PROOF STEP]
have "(rp a1, rp a2) = div_rat_poly_step (rp q) (rat_of_int x) (b1, b2)"
[PROOF STATE]
proof (prove)
using this:
(case a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) x pair
pair = (b1, b2)
a = (a1, a2)

goal (1 subgoal):
 1. (of_int_poly a1, of_int_poly a2) = div_rat_poly_step (of_int_poly q) (rat_of_int x) (b1, b2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(of_int_poly a1, of_int_poly a2) = div_rat_poly_step (of_int_poly q) (rat_of_int x) (b1, b2)

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(of_int_poly a1, of_int_poly a2) = div_rat_poly_step (of_int_poly q) (rat_of_int x) (b1, b2)
[PROOF STEP]
have a1: "rp a1 = pCons p12 b1"
    and "rp a2 = pCons (rat_of_int x) b2 - smult p12 (rp q)"
[PROOF STATE]
proof (prove)
using this:
(of_int_poly a1, of_int_poly a2) = div_rat_poly_step (of_int_poly q) (rat_of_int x) (b1, b2)

goal (1 subgoal):
 1. of_int_poly a1 = pCons p12 b1 &&& of_int_poly a2 = pCons (rat_of_int x) b2 - smult p12 (of_int_poly q)
[PROOF STEP]
by (auto split: prod.splits simp add: Let_def div_rat_poly_step_def p12_def)
[PROOF STATE]
proof (state)
this:
of_int_poly a1 = pCons p12 b1
of_int_poly a2 = pCons (rat_of_int x) b2 - smult p12 (of_int_poly q)

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
of_int_poly a1 = pCons p12 b1
of_int_poly a2 = pCons (rat_of_int x) b2 - smult p12 (of_int_poly q)
[PROOF STEP]
obtain p21 p22 where "rp p21 = pCons p22 b2"
[PROOF STATE]
proof (prove)
using this:
of_int_poly a1 = pCons p12 b1
of_int_poly a2 = pCons (rat_of_int x) b2 - smult p12 (of_int_poly q)

goal (1 subgoal):
 1. (\<And>p21 p22. of_int_poly p21 = pCons p22 b2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: field_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p21 p22. of_int_poly p21 = pCons p22 b2 \<Longrightarrow> thesis; of_int_poly a1 = pCons p12 b1; of_int_poly a2 + smult p12 (of_int_poly q) = pCons (rat_of_int x) b2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (metis coeff_pCons_0 of_int_hom.map_poly_hom_add of_int_hom.map_poly_hom_smult of_int_hom.coeff_map_poly_hom)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
of_int_poly p21 = pCons p22 b2

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
of_int_poly p21 = pCons p22 b2

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
obtain p21' p21q where "p21 = pCons p21' p21q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p21' p21q. p21 = pCons p21' p21q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule pCons_cases)
[PROOF STATE]
proof (state)
this:
p21 = pCons p21' p21q

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
of_int_poly p21 = pCons p22 b2
p21 = pCons p21' p21q
[PROOF STEP]
obtain p2 where "b2 = rp p2 "
[PROOF STATE]
proof (prove)
using this:
of_int_poly p21 = pCons p22 b2
p21 = pCons p21' p21q

goal (1 subgoal):
 1. (\<And>p2. b2 = of_int_poly p2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: hom_distribs)
[PROOF STATE]
proof (state)
this:
b2 = of_int_poly p2

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b2 = of_int_poly p2

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
obtain a1' a1q where "a1 = pCons a1' a1q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a1' a1q. a1 = pCons a1' a1q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule pCons_cases)
[PROOF STATE]
proof (state)
this:
a1 = pCons a1' a1q

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
with a1
[PROOF STATE]
proof (chain)
picking this:
of_int_poly a1 = pCons p12 b1
a1 = pCons a1' a1q
[PROOF STEP]
obtain p1 where "b1 = rp p1"
[PROOF STATE]
proof (prove)
using this:
of_int_poly a1 = pCons p12 b1
a1 = pCons a1' a1q

goal (1 subgoal):
 1. (\<And>p1. b1 = of_int_poly p1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: hom_distribs)
[PROOF STATE]
proof (state)
this:
b1 = of_int_poly p1

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b2 = of_int_poly p2
b1 = of_int_poly p1
[PROOF STEP]
have "pair = (rp p1, rp p2)"
[PROOF STATE]
proof (prove)
using this:
b2 = of_int_poly p2
b1 = of_int_poly p1

goal (1 subgoal):
 1. pair = (of_int_poly p1, of_int_poly p2)
[PROOF STEP]
using pair
[PROOF STATE]
proof (prove)
using this:
b2 = of_int_poly p2
b1 = of_int_poly p1
pair = (b1, b2)

goal (1 subgoal):
 1. pair = (of_int_poly p1, of_int_poly p2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pair = (of_int_poly p1, of_int_poly p2)

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pair = (of_int_poly p1, of_int_poly p2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pair = (of_int_poly p1, of_int_poly p2)

goal (1 subgoal):
 1. \<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>c'. pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  pdivmod_then_div_mod_int_poly:
  assumes q0: "q \<noteq> 0" and "(rp p div rp q, rp p mod rp q) = (rp r, rp m)"
  shows   "div_mod_int_poly p q = Some (r,m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
let ?rpp = "(\<lambda> (a,b). (rp a,rp b))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
(* rp pair *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
let ?p = "rp p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
let ?q = "rp q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
let ?r = "rp r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
let ?m = "rp m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
let ?div_rat_step = "div_rat_poly_step ?q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
let ?div_int_step = "div_int_poly_step q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
fix oldRes res :: "int poly \<times> int poly"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
fix lst :: "int list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
have inj: "(\<And>a b. (case a of (a, b) \<Rightarrow> (rp a, rp b)) = (case b of (a, b) \<Rightarrow> (rp a, rp b)) \<Longrightarrow> a = b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (case a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (case b of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> a = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(case ?a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (case ?b of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
have "(\<And>a b c. b \<in> set lst \<Longrightarrow>
              (case a of (a, b) \<Rightarrow> (map_poly rat_of_int a, map_poly rat_of_int b)) =
              (div_rat_poly_step (map_poly rat_of_int q) \<circ> rat_of_int) b
               (case c of (a, b) \<Rightarrow> (map_poly rat_of_int a, map_poly rat_of_int b)) \<Longrightarrow>
              Some a = div_int_poly_step q b (Some c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>b \<in> set lst; (case a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (case c of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))\<rbrakk> \<Longrightarrow> Some a = div_int_poly_step q b (Some c)
[PROOF STEP]
using rat_step_then_int_poly_step[OF q0]
[PROOF STATE]
proof (prove)
using this:
(of_int_poly ?a1.0, of_int_poly ?a2.0) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) ?b2.0 (of_int_poly ?c1.0, of_int_poly ?c2.0) \<Longrightarrow> Some (?a1.0, ?a2.0) = div_int_poly_step q ?b2.0 (Some (?c1.0, ?c2.0))

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>b \<in> set lst; (case a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (case c of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))\<rbrakk> \<Longrightarrow> Some a = div_int_poly_step q b (Some c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?b \<in> set lst; (case ?a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) ?b (case ?c of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))\<rbrakk> \<Longrightarrow> Some ?a = div_int_poly_step q ?b (Some ?c)

goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
hence "?rpp res = foldr (?div_rat_step \<circ> rat_of_int) lst (?rpp oldRes)
          \<Longrightarrow> Some res = foldr ?div_int_step lst (Some oldRes)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?b \<in> set lst; (case ?a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) ?b (case ?c of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))\<rbrakk> \<Longrightarrow> Some ?a = div_int_poly_step q ?b (Some ?c)

goal (1 subgoal):
 1. (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some res = foldr (div_int_poly_step q) lst (Some oldRes)
[PROOF STEP]
using foldr_cong_plus[of "set lst" ?rpp "?div_rat_step \<circ> rat_of_int" Some ?div_int_step lst res oldRes]
            div_rat_poly_step_sur inj
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?b \<in> set lst; (case ?a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) ?b (case ?c of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))\<rbrakk> \<Longrightarrow> Some ?a = div_int_poly_step q ?b (Some ?c)
\<lbrakk>\<And>a b c. \<lbrakk>b \<in> set lst; (case a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b (case c of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))\<rbrakk> \<Longrightarrow> Some a = div_int_poly_step q b (Some c); \<And>a b. (case a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (case b of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> a = b; \<And>a b c. (case a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) b c \<Longrightarrow> \<exists>c'. c = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)); set lst \<subseteq> set lst; (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))\<rbrakk> \<Longrightarrow> Some res = foldr (div_int_poly_step q) lst (Some oldRes)
(case ?a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (div_rat_poly_step (of_int_poly ?q) \<circ> rat_of_int) ?x ?pair \<Longrightarrow> \<exists>c'. ?pair = (case c' of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b))
(case ?a of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = (case ?b of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some res = foldr (div_int_poly_step q) lst (Some oldRes)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some res = foldr (div_int_poly_step q) lst (Some oldRes)

goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
hence "?rpp res = foldr ?div_rat_step (map rat_of_int lst) (?rpp oldRes)
       \<Longrightarrow> Some res = foldr ?div_int_step lst (Some oldRes)"
[PROOF STATE]
proof (prove)
using this:
(case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some res = foldr (div_int_poly_step q) lst (Some oldRes)

goal (1 subgoal):
 1. (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int lst) (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some res = foldr (div_int_poly_step q) lst (Some oldRes)
[PROOF STEP]
using foldr_map[of ?div_rat_step rat_of_int lst]
[PROOF STATE]
proof (prove)
using this:
(case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some res = foldr (div_int_poly_step q) lst (Some oldRes)
foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int lst) ?a = foldr (div_rat_poly_step (of_int_poly q) \<circ> rat_of_int) lst ?a

goal (1 subgoal):
 1. (case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int lst) (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some res = foldr (div_int_poly_step q) lst (Some oldRes)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(case res of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int lst) (case oldRes of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some res = foldr (div_int_poly_step q) lst (Some oldRes)

goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(case ?res2 of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int ?lst2) (case ?oldRes2 of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some ?res2 = foldr (div_int_poly_step q) ?lst2 (Some ?oldRes2)

goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
hence equal_foldr : "?rpp (r,m) = foldr (?div_rat_step) (map rat_of_int (coeffs p)) (?rpp (0,0))
                   \<Longrightarrow> Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0,0))"
[PROOF STATE]
proof (prove)
using this:
(case ?res2 of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int ?lst2) (case ?oldRes2 of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some ?res2 = foldr (div_int_poly_step q) ?lst2 (Some ?oldRes2)

goal (1 subgoal):
 1. (case (r, m) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int (coeffs p)) (case (0, 0) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(case (r, m) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int (coeffs p)) (case (0, 0) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))

goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
have "(?r,?m) = (foldr (?div_rat_step) (coeffs ?p) (0,0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int_poly r, of_int_poly m) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p)) (0, 0)
[PROOF STEP]
using fold_coeffs_def[of "?div_rat_step" ?p] assms
      div_mod_fold_coeffs [of ?p ?q]
[PROOF STATE]
proof (prove)
using this:
fold_coeffs (div_rat_poly_step (of_int_poly q)) (of_int_poly p) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p))
q \<noteq> 0
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (if of_int_poly q = 0 then (0, of_int_poly p) else fold_coeffs (\<lambda>a (s, r). let b = coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q) in (pCons b s, pCons a r - smult b (of_int_poly q))) (of_int_poly p) (0, 0))

goal (1 subgoal):
 1. (of_int_poly r, of_int_poly m) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p)) (0, 0)
[PROOF STEP]
unfolding div_rat_poly_step_def
[PROOF STATE]
proof (prove)
using this:
fold_coeffs (\<lambda>a (s, r). let b = coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q) in (pCons b s, pCons a r - smult b (of_int_poly q))) (of_int_poly p) = foldr (\<lambda>a (s, r). let b = coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q) in (pCons b s, pCons a r - smult b (of_int_poly q))) (coeffs (of_int_poly p))
q \<noteq> 0
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly m)
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (if of_int_poly q = 0 then (0, of_int_poly p) else fold_coeffs (\<lambda>a (s, r). let b = coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q) in (pCons b s, pCons a r - smult b (of_int_poly q))) (of_int_poly p) (0, 0))

goal (1 subgoal):
 1. (of_int_poly r, of_int_poly m) = foldr (\<lambda>a (s, r). let b = coeff (pCons a r) (degree (of_int_poly q)) / lead_coeff (of_int_poly q) in (pCons b s, pCons a r - smult b (of_int_poly q))) (coeffs (of_int_poly p)) (0, 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(of_int_poly r, of_int_poly m) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p)) (0, 0)

goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
hence "Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0,0))"
[PROOF STATE]
proof (prove)
using this:
(of_int_poly r, of_int_poly m) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p)) (0, 0)

goal (1 subgoal):
 1. Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))
[PROOF STEP]
using equal_foldr
[PROOF STATE]
proof (prove)
using this:
(of_int_poly r, of_int_poly m) = foldr (div_rat_poly_step (of_int_poly q)) (coeffs (of_int_poly p)) (0, 0)
(case (r, m) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) = foldr (div_rat_poly_step (of_int_poly q)) (map rat_of_int (coeffs p)) (case (0, 0) of (a, b) \<Rightarrow> (of_int_poly a, of_int_poly b)) \<Longrightarrow> Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))

goal (1 subgoal):
 1. Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))

goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))

goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
using q0
[PROOF STATE]
proof (prove)
using this:
Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))
q \<noteq> 0

goal (1 subgoal):
 1. div_mod_int_poly p q = Some (r, m)
[PROOF STEP]
unfolding div_mod_int_poly_def
[PROOF STATE]
proof (prove)
using this:
Some (r, m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))
q \<noteq> 0

goal (1 subgoal):
 1. (if q = 0 then None else let n = degree q; qn = coeff q n in fold_coeffs (div_int_poly_step q) p (Some (0, 0))) = Some (r, m)
[PROOF STEP]
by (simp add: fold_coeffs_def)
[PROOF STATE]
proof (state)
this:
div_mod_int_poly p q = Some (r, m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma div_int_then_rqp:
  assumes "div_int_poly p q = Some r"
  shows "r * q = p"
    and "q \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * q = p &&& q \<noteq> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
let ?rpp = "(\<lambda> (a,b). (rp a,rp b))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
(* rp pair *)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
let ?p = "rp p"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
let ?q = "rp q"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
let ?r = "rp r"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
have "Some (r,0) = div_mod_int_poly p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (r, 0) = div_mod_int_poly p q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
div_int_poly p q = Some r

goal (1 subgoal):
 1. Some (r, 0) = div_mod_int_poly p q
[PROOF STEP]
unfolding div_int_poly_def
[PROOF STATE]
proof (prove)
using this:
(case div_mod_int_poly p q of None \<Rightarrow> None | Some (d, m) \<Rightarrow> if m = 0 then Some d else None) = Some r

goal (1 subgoal):
 1. Some (r, 0) = div_mod_int_poly p q
[PROOF STEP]
by (auto split:  option.splits prod.splits if_splits)
[PROOF STATE]
proof (state)
this:
Some (r, 0) = div_mod_int_poly p q

goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
with div_mod_int_poly_then_pdivmod[of p q r 0]
[PROOF STATE]
proof (chain)
picking this:
div_mod_int_poly p q = Some (r, 0) \<Longrightarrow> (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly 0)
div_mod_int_poly p q = Some (r, 0) \<Longrightarrow> q \<noteq> 0
Some (r, 0) = div_mod_int_poly p q
[PROOF STEP]
have "?p div ?q = ?r \<and> ?p mod ?q = 0"
[PROOF STATE]
proof (prove)
using this:
div_mod_int_poly p q = Some (r, 0) \<Longrightarrow> (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly 0)
div_mod_int_poly p q = Some (r, 0) \<Longrightarrow> q \<noteq> 0
Some (r, 0) = div_mod_int_poly p q

goal (1 subgoal):
 1. of_int_poly p div of_int_poly q = of_int_poly r \<and> of_int_poly p mod of_int_poly q = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_int_poly p div of_int_poly q = of_int_poly r \<and> of_int_poly p mod of_int_poly q = 0

goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
with div_mult_mod_eq[of ?p ?q]
[PROOF STATE]
proof (chain)
picking this:
of_int_poly p div of_int_poly q * of_int_poly q + of_int_poly p mod of_int_poly q = of_int_poly p
of_int_poly p div of_int_poly q = of_int_poly r \<and> of_int_poly p mod of_int_poly q = 0
[PROOF STEP]
have "?p = ?r * ?q"
[PROOF STATE]
proof (prove)
using this:
of_int_poly p div of_int_poly q * of_int_poly q + of_int_poly p mod of_int_poly q = of_int_poly p
of_int_poly p div of_int_poly q = of_int_poly r \<and> of_int_poly p mod of_int_poly q = 0

goal (1 subgoal):
 1. of_int_poly p = of_int_poly r * of_int_poly q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int_poly p = of_int_poly r * of_int_poly q

goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int_poly p = of_int_poly r * of_int_poly q

goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
have "\<dots> = rp (r * q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly r * of_int_poly q = of_int_poly (r * q)
[PROOF STEP]
by (simp add: hom_distribs)
[PROOF STATE]
proof (state)
this:
of_int_poly r * of_int_poly q = of_int_poly (r * q)

goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_int_poly p = of_int_poly (r * q)
[PROOF STEP]
have "?p = rp (r * q)"
[PROOF STATE]
proof (prove)
using this:
of_int_poly p = of_int_poly (r * q)

goal (1 subgoal):
 1. of_int_poly p = of_int_poly (r * q)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
of_int_poly p = of_int_poly (r * q)

goal (2 subgoals):
 1. r * q = p
 2. q \<noteq> 0
[PROOF STEP]
thus "r * q = p"
[PROOF STATE]
proof (prove)
using this:
of_int_poly p = of_int_poly (r * q)

goal (1 subgoal):
 1. r * q = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r * q = p

goal (1 subgoal):
 1. q \<noteq> 0
[PROOF STEP]
show "q \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
div_int_poly p q = Some r

goal (1 subgoal):
 1. q \<noteq> 0
[PROOF STEP]
unfolding div_int_poly_def div_mod_int_poly_def
[PROOF STATE]
proof (prove)
using this:
(case if q = 0 then None else let n = degree q; qn = coeff q n in fold_coeffs (div_int_poly_step q) p (Some (0, 0)) of None \<Rightarrow> None | Some (d, m) \<Rightarrow> if m = 0 then Some d else None) = Some r

goal (1 subgoal):
 1. q \<noteq> 0
[PROOF STEP]
by (auto split: option.splits prod.splits if_splits)
[PROOF STATE]
proof (state)
this:
q \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rqp_then_div_int:
  assumes "r * q = p"
      and q0:"q \<noteq> 0"
  shows "div_int_poly p q = Some r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
let ?rpp = "(\<lambda> (a,b). (rp a,rp b))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
(* rp pair *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
let ?p = "rp p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
let ?q = "rp q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
let ?r = "rp r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
have "?p = ?r * ?q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly p = of_int_poly r * of_int_poly q
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
r * q = p

goal (1 subgoal):
 1. of_int_poly p = of_int_poly r * of_int_poly q
[PROOF STEP]
by (auto simp: hom_distribs)
[PROOF STATE]
proof (state)
this:
of_int_poly p = of_int_poly r * of_int_poly q

goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
hence "?p div ?q = ?r" and "?p mod ?q = 0"
[PROOF STATE]
proof (prove)
using this:
of_int_poly p = of_int_poly r * of_int_poly q

goal (1 subgoal):
 1. of_int_poly p div of_int_poly q = of_int_poly r &&& of_int_poly p mod of_int_poly q = 0
[PROOF STEP]
using q0
[PROOF STATE]
proof (prove)
using this:
of_int_poly p = of_int_poly r * of_int_poly q
q \<noteq> 0

goal (1 subgoal):
 1. of_int_poly p div of_int_poly q = of_int_poly r &&& of_int_poly p mod of_int_poly q = 0
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
of_int_poly p div of_int_poly q = of_int_poly r
of_int_poly p mod of_int_poly q = 0

goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
hence "(rp p div rp q, rp p mod rp q) = (rp r, 0)"
[PROOF STATE]
proof (prove)
using this:
of_int_poly p div of_int_poly q = of_int_poly r
of_int_poly p mod of_int_poly q = 0

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, 0)
[PROOF STEP]
by (auto split: prod.splits)
[PROOF STATE]
proof (state)
this:
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, 0)

goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
hence "(rp p div rp q, rp p mod rp q) = (rp r, rp 0)"
[PROOF STATE]
proof (prove)
using this:
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, 0)

goal (1 subgoal):
 1. (of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly 0)

goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
hence "Some (r,0) = div_mod_int_poly p q"
[PROOF STATE]
proof (prove)
using this:
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly 0)

goal (1 subgoal):
 1. Some (r, 0) = div_mod_int_poly p q
[PROOF STEP]
using pdivmod_then_div_mod_int_poly[OF q0,of p r 0]
[PROOF STATE]
proof (prove)
using this:
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly 0)
(of_int_poly p div of_int_poly q, of_int_poly p mod of_int_poly q) = (of_int_poly r, of_int_poly 0) \<Longrightarrow> div_mod_int_poly p q = Some (r, 0)

goal (1 subgoal):
 1. Some (r, 0) = div_mod_int_poly p q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some (r, 0) = div_mod_int_poly p q

goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Some (r, 0) = div_mod_int_poly p q

goal (1 subgoal):
 1. div_int_poly p q = Some r
[PROOF STEP]
unfolding div_mod_int_poly_def div_int_poly_def
[PROOF STATE]
proof (prove)
using this:
Some (r, 0) = (if q = 0 then None else let n = degree q; qn = coeff q n in fold_coeffs (div_int_poly_step q) p (Some (0, 0)))

goal (1 subgoal):
 1. (case if q = 0 then None else let n = degree q; qn = coeff q n in fold_coeffs (div_int_poly_step q) p (Some (0, 0)) of None \<Rightarrow> None | Some (d, m) \<Rightarrow> if m = 0 then Some d else None) = Some r
[PROOF STEP]
using q0
[PROOF STATE]
proof (prove)
using this:
Some (r, 0) = (if q = 0 then None else let n = degree q; qn = coeff q n in fold_coeffs (div_int_poly_step q) p (Some (0, 0)))
q \<noteq> 0

goal (1 subgoal):
 1. (case if q = 0 then None else let n = degree q; qn = coeff q n in fold_coeffs (div_int_poly_step q) p (Some (0, 0)) of None \<Rightarrow> None | Some (d, m) \<Rightarrow> if m = 0 then Some d else None) = Some r
[PROOF STEP]
by (metis (mono_tags, lifting) option.simps(5) split_conv)
[PROOF STATE]
proof (state)
this:
div_int_poly p q = Some r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma div_int_poly: "(div_int_poly p q = Some r) \<longleftrightarrow> (q \<noteq> 0 \<and> p = r * q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (div_int_poly p q = Some r) = (q \<noteq> 0 \<and> p = r * q)
[PROOF STEP]
using div_int_then_rqp rqp_then_div_int
[PROOF STATE]
proof (prove)
using this:
div_int_poly ?p ?q = Some ?r \<Longrightarrow> ?r * ?q = ?p
div_int_poly ?p ?q = Some ?r \<Longrightarrow> ?q \<noteq> 0
\<lbrakk>?r * ?q = ?p; ?q \<noteq> 0\<rbrakk> \<Longrightarrow> div_int_poly ?p ?q = Some ?r

goal (1 subgoal):
 1. (div_int_poly p q = Some r) = (q \<noteq> 0 \<and> p = r * q)
[PROOF STEP]
by blast


[STATEMENT]
lemma dvd_int_poly[simp]: "dvd_int_poly q p = (q dvd p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dvd_int_poly q p = (q dvd p)
[PROOF STEP]
unfolding dvd_def dvd_int_poly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if q = 0 then p = 0 else div_int_poly p q \<noteq> None) = (\<exists>k. p = q * k)
[PROOF STEP]
using div_int_poly[of p q]
[PROOF STATE]
proof (prove)
using this:
(div_int_poly p q = Some ?r) = (q \<noteq> 0 \<and> p = ?r * q)

goal (1 subgoal):
 1. (if q = 0 then p = 0 else div_int_poly p q \<noteq> None) = (\<exists>k. p = q * k)
[PROOF STEP]
by (cases "q = 0", auto)


[STATEMENT]
lemma dvd_int_poly_non_0[simp]: "q \<noteq> 0 \<Longrightarrow> dvd_int_poly_non_0 q p = (q dvd p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<noteq> 0 \<Longrightarrow> dvd_int_poly_non_0 q p = (q dvd p)
[PROOF STEP]
unfolding dvd_def dvd_int_poly_non_0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<noteq> 0 \<Longrightarrow> (div_int_poly p q \<noteq> None) = (\<exists>k. p = q * k)
[PROOF STEP]
using div_int_poly[of p q]
[PROOF STATE]
proof (prove)
using this:
(div_int_poly p q = Some ?r) = (q \<noteq> 0 \<and> p = ?r * q)

goal (1 subgoal):
 1. q \<noteq> 0 \<Longrightarrow> (div_int_poly p q \<noteq> None) = (\<exists>k. p = q * k)
[PROOF STEP]
by auto


[STATEMENT]
lemma [code_unfold]: "p dvd q \<longleftrightarrow> dvd_int_poly p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p dvd q) = dvd_int_poly p q
[PROOF STEP]
by simp