[STATEMENT]
lemma fst_uses'_phis': "uses' g = lookup_multimap (fst (uses'_phis' g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uses' g = lookup_multimap (fst (uses'_phis' g))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. uses' g x = lookup_multimap (fst (uses'_phis' g)) x
[PROOF STEP]
apply (simp add: uses'_phis'_def Let_def split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. uses' g x = lookup_multimap (fst (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) x
[PROOF STEP]
apply (case_tac "x \<in> set (\<alpha>n g)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set (\<alpha>n g) \<Longrightarrow> uses' g x = lookup_multimap (fst (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) x
 2. \<And>x. x \<notin> set (\<alpha>n g) \<Longrightarrow> uses' g x = lookup_multimap (fst (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) x
[PROOF STEP]
apply (rule foldr_aux_2(1)[OF _ _ surjective_pairing]; auto simp: lookup_empty intro: \<alpha>n_distinct; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<notin> set (\<alpha>n g) \<Longrightarrow> uses' g x = lookup_multimap (fst (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) x
[PROOF STEP]
unfolding lookup_multimap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<notin> set (\<alpha>n g) \<Longrightarrow> uses' g x = (case Mapping.lookup (fst (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) x of None \<Rightarrow> {} | Some x \<Rightarrow> id x)
[PROOF STEP]
apply (subst foldr_aux_2(2)[OF _ _ surjective_pairing]; auto simp: lookup_empty uses_in_\<alpha>n uses'_def intro: \<alpha>n_distinct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fst_uses'_phis'_in_\<alpha>n: "Mapping.keys (fst (uses'_phis' g)) \<subseteq> set (\<alpha>n g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.keys (fst (uses'_phis' g)) \<subseteq> set (\<alpha>n g)
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Mapping.keys (fst (uses'_phis' g)) \<Longrightarrow> x \<in> set (\<alpha>n g)
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> Mapping.keys (fst (uses'_phis' g)); x \<notin> set (\<alpha>n g)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add: uses'_phis'_def Let_def split_def keys_dom_lookup dom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<exists>y. Mapping.lookup (fst (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) x = Some y; x \<notin> set (\<alpha>n g)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subst(asm) foldr_aux_2(2)[OF _ _ surjective_pairing]; auto intro: \<alpha>n_distinct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma snd_uses'_phis': "phis'_code g = snd (uses'_phis' g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phis'_code g = snd (uses'_phis' g)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phis'_code g = snd (uses'_phis' g)
[PROOF STEP]
have a: "\<And>n v. (THE k. (\<lambda>p. (fst p, snd p, fst p, PhiDef)) -` {(n, v, n, PhiDef)} = {k}) = (n,v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n v. (THE k. (\<lambda>p. (fst p, snd p, fst p, PhiDef)) -` {(n, v, n, PhiDef)} = {k}) = (n, v)
[PROOF STEP]
by (rule the1_equality) (auto simp: vimage_def)
[PROOF STATE]
proof (state)
this:
(THE k. (\<lambda>p. (fst p, snd p, fst p, PhiDef)) -` {(?n2, ?v2, ?n2, PhiDef)} = {k}) = (?n2, ?v2)

goal (1 subgoal):
 1. phis'_code g = snd (uses'_phis' g)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phis'_code g = snd (uses'_phis' g)
[PROOF STEP]
apply (subst Mapping_eq_lookup)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (phis'_code g) = Mapping.lookup (snd (uses'_phis' g))
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g. phis' g = Mapping.lookup (snd (uses'_phis' g))
[PROOF STEP]
apply (simp add: phis'_def uses'_phis'_def Let_def split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g. (\<lambda>p. if defNode (snd p) = fst p \<and> fst p \<in> phiDefNodes g (fst (snd p)) \<and> fst (snd p) \<in> vars g \<and> defKind (snd p) = PhiDef then Some (map (\<lambda>m. lookupDef g m (fst (snd p))) (predecessors g (fst p))) else None) = Mapping.lookup (map_keys (\<lambda>p. (fst p, snd p, fst p, PhiDef)) (snd (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))))
[PROOF STEP]
apply (auto simp: lookup_map_keys a intro!: ext)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>g a aa. \<lbrakk>a \<in> phiDefNodes g aa; aa \<in> vars g; (\<lambda>p. (fst p, snd p, fst p, PhiDef)) -` {(a, aa, a, PhiDef)} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>g a aa. \<lbrakk>a \<in> phiDefNodes g aa; aa \<in> vars g\<rbrakk> \<Longrightarrow> Some (map (\<lambda>m. lookupDef g m aa) (predecessors g a)) = Mapping.lookup (snd (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) (a, aa)
 3. \<And>g ac ba. \<lbrakk>None \<noteq> Mapping.lookup (snd (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) (ac, ba); ba \<notin> vars g\<rbrakk> \<Longrightarrow> False
 4. \<And>g ac ba. \<lbrakk>None \<noteq> Mapping.lookup (snd (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) (ac, ba); ac \<notin> phiDefNodes g ba\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a_ \<in> phiDefNodes g_ aa_; aa_ \<in> vars g_; (\<lambda>p. (fst p, snd p, fst p, PhiDef)) -` {(a_, aa_, a_, PhiDef)} = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto simp: vimage_def)[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>g a aa. \<lbrakk>a \<in> phiDefNodes g aa; aa \<in> vars g\<rbrakk> \<Longrightarrow> Some (map (\<lambda>m. lookupDef g m aa) (predecessors g a)) = Mapping.lookup (snd (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) (a, aa)
 2. \<And>g ac ba. \<lbrakk>None \<noteq> Mapping.lookup (snd (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) (ac, ba); ba \<notin> vars g\<rbrakk> \<Longrightarrow> False
 3. \<And>g ac ba. \<lbrakk>None \<noteq> Mapping.lookup (snd (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) (ac, ba); ac \<notin> phiDefNodes g ba\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a_ \<in> phiDefNodes g_ aa_; aa_ \<in> vars g_\<rbrakk> \<Longrightarrow> Some (map (\<lambda>m. lookupDef g_ m aa_) (predecessors g_ a_)) = Mapping.lookup (snd (foldr (aux_2 g_) (\<alpha>n g_) (Mapping.empty, Mapping.empty))) (a_, aa_)
[PROOF STEP]
apply (subst foldr_aux_2(3)[OF _ _ surjective_pairing, symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a_ \<in> phiDefNodes g_ aa_; aa_ \<in> vars g_\<rbrakk> \<Longrightarrow> set (\<alpha>n g_) \<subseteq> set (\<alpha>n g_)
 2. \<lbrakk>a_ \<in> phiDefNodes g_ aa_; aa_ \<in> vars g_\<rbrakk> \<Longrightarrow> distinct (\<alpha>n g_)
 3. \<lbrakk>a_ \<in> phiDefNodes g_ aa_; aa_ \<in> vars g_\<rbrakk> \<Longrightarrow> Some (map (\<lambda>m. lookupDef g_ m aa_) (predecessors g_ a_)) = (if \<exists>n\<in>set (\<alpha>n g_). a_ \<in> phiDefNodes_aux g_ aa_ (\<alpha>n g_) n \<and> aa_ \<in> uses g_ n then Some (map (\<lambda>m. lookupDef g_ m aa_) (predecessors g_ a_)) else None)
[PROOF STEP]
by (auto simp: phiDefNodes_def vimage_def elim!: fold_union_elem intro!: \<alpha>n_distinct split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>g ac ba. \<lbrakk>None \<noteq> Mapping.lookup (snd (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) (ac, ba); ba \<notin> vars g\<rbrakk> \<Longrightarrow> False
 2. \<And>g ac ba. \<lbrakk>None \<noteq> Mapping.lookup (snd (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) (ac, ba); ac \<notin> phiDefNodes g ba\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>None \<noteq> Mapping.lookup (snd (foldr (aux_2 g_) (\<alpha>n g_) (Mapping.empty, Mapping.empty))) (ac_, ba_); ba_ \<notin> vars g_\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subst(asm) foldr_aux_2(3)[OF _ _ surjective_pairing, symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ba_ \<notin> vars g_ \<Longrightarrow> set (\<alpha>n g_) \<subseteq> set (\<alpha>n g_)
 2. ba_ \<notin> vars g_ \<Longrightarrow> distinct (\<alpha>n g_)
 3. \<lbrakk>None \<noteq> (if \<exists>n\<in>set (\<alpha>n g_). ac_ \<in> phiDefNodes_aux g_ ba_ (\<alpha>n g_) n \<and> ba_ \<in> uses g_ n then Some (map (\<lambda>m. lookupDef g_ m ba_) (predecessors g_ ac_)) else None); ba_ \<notin> vars g_\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto simp: phiDefNodes_def vimage_def elim!: fold_union_elem intro!: \<alpha>n_distinct split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g ac ba. \<lbrakk>None \<noteq> Mapping.lookup (snd (foldr (aux_2 g) (\<alpha>n g) (Mapping.empty, Mapping.empty))) (ac, ba); ac \<notin> phiDefNodes g ba\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>None \<noteq> Mapping.lookup (snd (foldr (aux_2 g_) (\<alpha>n g_) (Mapping.empty, Mapping.empty))) (ac_, ba_); ac_ \<notin> phiDefNodes g_ ba_\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subst(asm) foldr_aux_2(3)[OF _ _ surjective_pairing, symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ac_ \<notin> phiDefNodes g_ ba_ \<Longrightarrow> set (\<alpha>n g_) \<subseteq> set (\<alpha>n g_)
 2. ac_ \<notin> phiDefNodes g_ ba_ \<Longrightarrow> distinct (\<alpha>n g_)
 3. \<lbrakk>None \<noteq> (if \<exists>n\<in>set (\<alpha>n g_). ac_ \<in> phiDefNodes_aux g_ ba_ (\<alpha>n g_) n \<and> ba_ \<in> uses g_ n then Some (map (\<lambda>m. lookupDef g_ m ba_) (predecessors g_ ac_)) else None); ac_ \<notin> phiDefNodes g_ ba_\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto simp: phiDefNodes_def vimage_def elim!: fold_union_elem intro!: \<alpha>n_distinct fold_union_elemI split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
phis'_code g = snd (uses'_phis' g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma square_free_separable_GFp: fixes f :: "'a :: prime_card mod_ring poly"
  assumes card: "CARD('a) > degree f"
  and sf: "square_free f"
  shows "separable f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. separable f
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> separable f \<Longrightarrow> False
[PROOF STEP]
assume "\<not> separable f"
[PROOF STATE]
proof (state)
this:
\<not> separable f

goal (1 subgoal):
 1. \<not> separable f \<Longrightarrow> False
[PROOF STEP]
with square_free_separable_main[OF sf]
[PROOF STATE]
proof (chain)
picking this:
\<not> separable f \<Longrightarrow> \<exists>g k. f = g * k \<and> degree g \<noteq> 0 \<and> pderiv g = 0
\<not> separable f
[PROOF STEP]
obtain g k where *: "f = g * k" "degree g \<noteq> 0" and g0: "pderiv g = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> separable f \<Longrightarrow> \<exists>g k. f = g * k \<and> degree g \<noteq> 0 \<and> pderiv g = 0
\<not> separable f

goal (1 subgoal):
 1. (\<And>g k. \<lbrakk>f = g * k; degree g \<noteq> 0; pderiv g = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f = g * k
degree g \<noteq> 0
pderiv g = 0

goal (1 subgoal):
 1. \<not> separable f \<Longrightarrow> False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
degree f < CARD('a)
square_free f
[PROOF STEP]
have f: "f \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
degree f < CARD('a)
square_free f

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

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

goal (1 subgoal):
 1. \<not> separable f \<Longrightarrow> False
[PROOF STEP]
have "degree f = degree g + degree k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree f = degree g + degree k
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
f \<noteq> 0

goal (1 subgoal):
 1. degree f = degree g + degree k
[PROOF STEP]
unfolding *(1)
[PROOF STATE]
proof (prove)
using this:
g * k \<noteq> 0

goal (1 subgoal):
 1. degree (g * k) = degree g + degree k
[PROOF STEP]
by (subst degree_mult_eq, auto)
[PROOF STATE]
proof (state)
this:
degree f = degree g + degree k

goal (1 subgoal):
 1. \<not> separable f \<Longrightarrow> False
[PROOF STEP]
with card
[PROOF STATE]
proof (chain)
picking this:
degree f < CARD('a)
degree f = degree g + degree k
[PROOF STEP]
have card: "degree g < CARD('a)"
[PROOF STATE]
proof (prove)
using this:
degree f < CARD('a)
degree f = degree g + degree k

goal (1 subgoal):
 1. degree g < CARD('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree g < CARD('a)

goal (1 subgoal):
 1. \<not> separable f \<Longrightarrow> False
[PROOF STEP]
from *(2)
[PROOF STATE]
proof (chain)
picking this:
degree g \<noteq> 0
[PROOF STEP]
obtain n where deg: "degree g = Suc n"
[PROOF STATE]
proof (prove)
using this:
degree g \<noteq> 0

goal (1 subgoal):
 1. (\<And>n. degree g = Suc n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "degree g", auto)
[PROOF STATE]
proof (state)
this:
degree g = Suc n

goal (1 subgoal):
 1. \<not> separable f \<Longrightarrow> False
[PROOF STEP]
from *(2)
[PROOF STATE]
proof (chain)
picking this:
degree g \<noteq> 0
[PROOF STEP]
have cg: "coeff g (degree g) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
degree g \<noteq> 0

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

goal (1 subgoal):
 1. \<not> separable f \<Longrightarrow> False
[PROOF STEP]
from g0
[PROOF STATE]
proof (chain)
picking this:
pderiv g = 0
[PROOF STEP]
have "coeff (pderiv g) n = 0"
[PROOF STATE]
proof (prove)
using this:
pderiv g = 0

goal (1 subgoal):
 1. poly.coeff (pderiv g) n = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff (pderiv g) n = 0

goal (1 subgoal):
 1. \<not> separable f \<Longrightarrow> False
[PROOF STEP]
from this[unfolded coeff_pderiv, folded deg] cg
[PROOF STATE]
proof (chain)
picking this:
of_nat (degree g) * lead_coeff g = 0
lead_coeff g \<noteq> 0
[PROOF STEP]
have "of_nat (degree g) = (0 :: 'a mod_ring)"
[PROOF STATE]
proof (prove)
using this:
of_nat (degree g) * lead_coeff g = 0
lead_coeff g \<noteq> 0

goal (1 subgoal):
 1. of_nat (degree g) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_nat (degree g) = 0

goal (1 subgoal):
 1. \<not> separable f \<Longrightarrow> False
[PROOF STEP]
from of_nat_0_mod_ring_dvd[OF this]
[PROOF STATE]
proof (chain)
picking this:
CARD('a) dvd degree g
[PROOF STEP]
have "CARD('a) dvd degree g"
[PROOF STATE]
proof (prove)
using this:
CARD('a) dvd degree g

goal (1 subgoal):
 1. CARD('a) dvd degree g
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
CARD('a) dvd degree g

goal (1 subgoal):
 1. \<not> separable f \<Longrightarrow> False
[PROOF STEP]
with card
[PROOF STATE]
proof (chain)
picking this:
degree g < CARD('a)
CARD('a) dvd degree g
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
degree g < CARD('a)
CARD('a) dvd degree g

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: deg nat_dvd_not_less)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma square_free_iff_separable_GFp: assumes "degree f < CARD('a)"
  shows "square_free (f :: 'a :: prime_card mod_ring poly) = separable f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free f = separable f
[PROOF STEP]
using separable_imp_square_free[of f] square_free_separable_GFp[OF assms]
[PROOF STATE]
proof (prove)
using this:
separable f \<Longrightarrow> square_free f
square_free f \<Longrightarrow> separable f

goal (1 subgoal):
 1. square_free f = separable f
[PROOF STEP]
by auto


[STATEMENT]
lemma (in prime_field_gen) separable_impl:
  shows "separable_impl_main p ff_ops f \<Longrightarrow> square_free_m f"
  "p > degree_m f \<Longrightarrow> p > separable_bound f \<Longrightarrow> square_free f
   \<Longrightarrow> separable_impl_main p ff_ops f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (separable_impl_main p ff_ops f \<Longrightarrow> square_free_m f) &&& (\<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_impl_main p ff_ops f)
[PROOF STEP]
unfolding separable_impl_main_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f) &&& (\<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
define F where F: "(F :: 'a mod_ring poly) = of_int_poly (Mp f)"
[PROOF STATE]
proof (state)
this:
F = of_int_poly (Mp f)

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
let ?f' = "of_int_poly_i ff_ops (Mp f)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
define f'' where "f'' \<equiv> of_int_poly (Mp f) :: 'a mod_ring poly"
[PROOF STATE]
proof (state)
this:
f'' \<equiv> of_int_poly (Mp f)

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
have rel_f[transfer_rule]: "poly_rel ?f' f''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (of_int_poly_i ff_ops (Mp f)) f''
[PROOF STEP]
by (rule poly_rel_of_int_poly[OF refl], simp add: f''_def)
[PROOF STATE]
proof (state)
this:
poly_rel (of_int_poly_i ff_ops (Mp f)) f''

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
have "separable_i ff_ops ?f' \<longleftrightarrow> gcd f'' (pderiv f'') = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = (gcd f'' (pderiv f'') = 1)
[PROOF STEP]
unfolding separable_i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gcd_poly_i ff_ops (of_int_poly_i ff_ops (Mp f)) (pderiv_i ff_ops (of_int_poly_i ff_ops (Mp f))) = one_poly_i ff_ops) = (gcd f'' (pderiv f'') = 1)
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = (gcd f'' (pderiv f'') = 1)

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = (gcd f'' (pderiv f'') = 1)

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
have "\<dots> \<longleftrightarrow> coprime f'' (pderiv f'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gcd f'' (pderiv f'') = 1) = comm_monoid_mult_class.coprime f'' (pderiv f'')
[PROOF STEP]
by (auto simp add: gcd_eq_1_imp_coprime)
[PROOF STATE]
proof (state)
this:
(gcd f'' (pderiv f'') = 1) = comm_monoid_mult_class.coprime f'' (pderiv f'')

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = comm_monoid_mult_class.coprime f'' (pderiv f'')
[PROOF STEP]
have id: "separable_i ff_ops ?f' \<longleftrightarrow> separable f''"
[PROOF STATE]
proof (prove)
using this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = comm_monoid_mult_class.coprime f'' (pderiv f'')

goal (1 subgoal):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = separable f''
[PROOF STEP]
unfolding separable_def coprime_iff_coprime
[PROOF STATE]
proof (prove)
using this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = algebraic_semidom_class.coprime f'' (pderiv f'')

goal (1 subgoal):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = algebraic_semidom_class.coprime f'' (pderiv f'')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = separable f''

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
have Mprel [transfer_rule]: "MP_Rel (Mp f) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MP_Rel (Mp f) F
[PROOF STEP]
unfolding F MP_Rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mp (Mp f) = to_int_poly (of_int_poly (Mp f))
[PROOF STEP]
by (simp add: Mp_f_representative)
[PROOF STATE]
proof (state)
this:
MP_Rel (Mp f) F

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
have "square_free f'' = square_free F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free f'' = square_free F
[PROOF STEP]
unfolding f''_def F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free (of_int_poly (Mp f)) = square_free (of_int_poly (Mp f))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
square_free f'' = square_free F

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
square_free f'' = square_free F

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
have "\<dots> = square_free_m (Mp f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free F = square_free_m (Mp f)
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
square_free F = square_free_m (Mp f)

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
square_free F = square_free_m (Mp f)

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
have "\<dots> = square_free_m f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free_m (Mp f) = square_free_m f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
square_free_m (Mp f) = square_free_m f

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
square_free f'' = square_free_m f
[PROOF STEP]
have id2: "square_free f'' = square_free_m f"
[PROOF STATE]
proof (prove)
using this:
square_free f'' = square_free_m f

goal (1 subgoal):
 1. square_free f'' = square_free_m f
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
square_free f'' = square_free_m f

goal (2 subgoals):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
 2. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
from separable_imp_square_free[of f'']
[PROOF STATE]
proof (chain)
picking this:
separable f'' \<Longrightarrow> square_free f''
[PROOF STEP]
show "separable_i ff_ops ?f' \<Longrightarrow> square_free_m f"
[PROOF STATE]
proof (prove)
using this:
separable f'' \<Longrightarrow> square_free f''

goal (1 subgoal):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f
[PROOF STEP]
unfolding id id2
[PROOF STATE]
proof (prove)
using this:
separable f'' \<Longrightarrow> square_free_m f

goal (1 subgoal):
 1. separable f'' \<Longrightarrow> square_free_m f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) \<Longrightarrow> square_free_m f

goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
let ?m = "map_poly (of_int :: int \<Rightarrow> 'a mod_ring)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
let ?f = "?m f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
assume "p > degree_m f" and bnd: "p > separable_bound f" and sf: "square_free f"
[PROOF STATE]
proof (state)
this:
int (degree_m f) < p
separable_bound f < p
square_free f

goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
with rel_funD[OF degree_MP_Rel Mprel, folded p]
[PROOF STATE]
proof (chain)
picking this:
degree_m (Mp f) = degree F
int (degree_m f) < p
separable_bound f < p
square_free f
[PROOF STEP]
have "p > degree F"
[PROOF STATE]
proof (prove)
using this:
degree_m (Mp f) = degree F
int (degree_m f) < p
separable_bound f < p
square_free f

goal (1 subgoal):
 1. int (degree F) < p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int (degree F) < p

goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
hence "CARD('a) > degree f''"
[PROOF STATE]
proof (prove)
using this:
int (degree F) < p

goal (1 subgoal):
 1. degree f'' < CARD('a)
[PROOF STEP]
unfolding f''_def F p
[PROOF STATE]
proof (prove)
using this:
int (degree (of_int_poly (poly_mod.Mp (int CARD('a)) f))) < int CARD('a)

goal (1 subgoal):
 1. degree (of_int_poly (poly_mod.Mp (int CARD('a)) f)) < CARD('a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree f'' < CARD('a)

goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
from square_free_iff_separable_GFp[OF this]
[PROOF STATE]
proof (chain)
picking this:
square_free f'' = separable f''
[PROOF STEP]
have "separable_i ff_ops ?f' = square_free f''"
[PROOF STATE]
proof (prove)
using this:
square_free f'' = separable f''

goal (1 subgoal):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = square_free f''
[PROOF STEP]
unfolding id id2
[PROOF STATE]
proof (prove)
using this:
square_free_m f = separable f''

goal (1 subgoal):
 1. separable f'' = square_free_m f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = square_free f''

goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f)) = square_free f''

goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
have "\<dots> = square_free F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free f'' = square_free F
[PROOF STEP]
unfolding f''_def F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free (of_int_poly (Mp f)) = square_free (of_int_poly (Mp f))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
square_free f'' = square_free F

goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
square_free f'' = square_free F

goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
have "F = ?f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = of_int_poly f
[PROOF STEP]
unfolding F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly (Mp f) = of_int_poly f
[PROOF STEP]
by (rule poly_eqI, (subst coeff_map_poly, force)+, unfold Mp_coeff,
    auto simp: M_def, transfer, auto simp: p)
[PROOF STATE]
proof (state)
this:
F = of_int_poly f

goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
F = of_int_poly f

goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
have "square_free ?f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free (of_int_poly f)
[PROOF STEP]
using square_free_int_imp_square_free_mod_ring[where 'a = 'a, OF sf] bnd m
[PROOF STATE]
proof (prove)
using this:
separable_bound f < int CARD('a) \<Longrightarrow> square_free (of_int_poly f)
separable_bound f < p
p = int CARD('a)

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

goal (1 subgoal):
 1. \<lbrakk>int (degree_m f) < p; separable_bound f < p; square_free f\<rbrakk> \<Longrightarrow> separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
show "separable_i ff_ops ?f'"
[PROOF STATE]
proof (prove)
using this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f))

goal (1 subgoal):
 1. separable_i ff_ops (of_int_poly_i ff_ops (Mp f))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
separable_i ff_ops (of_int_poly_i ff_ops (Mp f))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma square_free_mod_imp_square_free: assumes
  p: "prime p" and sf: "poly_mod.square_free_m p f"
  and cop: "coprime (lead_coeff f) p"
  shows "square_free f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. square_free f
[PROOF STEP]
interpret poly_mod p
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. square_free f
[PROOF STEP]
from sf[unfolded square_free_m_def]
[PROOF STATE]
proof (chain)
picking this:
Mp f \<noteq> Mp 0 \<and> (\<forall>g. degree_m g \<noteq> 0 \<longrightarrow> \<not> g * g dvdm f)
[PROOF STEP]
have f0: "Mp f \<noteq> 0" and ndvd: "\<And> g. degree_m g > 0 \<Longrightarrow> \<not> (g * g) dvdm f"
[PROOF STATE]
proof (prove)
using this:
Mp f \<noteq> Mp 0 \<and> (\<forall>g. degree_m g \<noteq> 0 \<longrightarrow> \<not> g * g dvdm f)

goal (1 subgoal):
 1. Mp f \<noteq> 0 &&& (\<And>g. 0 < degree_m g \<Longrightarrow> \<not> g * g dvdm f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Mp f \<noteq> 0
0 < degree_m ?g \<Longrightarrow> \<not> ?g * ?g dvdm f

goal (1 subgoal):
 1. square_free f
[PROOF STEP]
from f0
[PROOF STATE]
proof (chain)
picking this:
Mp f \<noteq> 0
[PROOF STEP]
have ff0: "f \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
Mp f \<noteq> 0

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

goal (1 subgoal):
 1. square_free f
[PROOF STEP]
show "square_free f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_free f
[PROOF STEP]
unfolding square_free_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<noteq> 0 \<and> (\<forall>q. 0 < degree q \<longrightarrow> \<not> q * q dvd f)
[PROOF STEP]
proof (intro conjI[OF ff0] allI impI notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume deg: "degree g > 0" and dvd: "g * g dvd f"
[PROOF STATE]
proof (state)
this:
0 < degree g
g * g dvd f

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < degree g
g * g dvd f
[PROOF STEP]
obtain h where f: "f = g * g * h"
[PROOF STATE]
proof (prove)
using this:
0 < degree g
g * g dvd f

goal (1 subgoal):
 1. (\<And>h. f = g * g * h \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
0 < degree g
\<exists>k. f = g * g * k

goal (1 subgoal):
 1. (\<And>h. f = g * g * h \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f = g * g * h

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from arg_cong[OF this, of Mp]
[PROOF STATE]
proof (chain)
picking this:
f =m g * g * h
[PROOF STEP]
have "(g * g) dvdm f"
[PROOF STATE]
proof (prove)
using this:
f =m g * g * h

goal (1 subgoal):
 1. g * g dvdm f
[PROOF STEP]
unfolding dvdm_def
[PROOF STATE]
proof (prove)
using this:
f =m g * g * h

goal (1 subgoal):
 1. \<exists>h. f =m g * g * h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g * g dvdm f

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with ndvd[of g]
[PROOF STATE]
proof (chain)
picking this:
0 < degree_m g \<Longrightarrow> \<not> g * g dvdm f
g * g dvdm f
[PROOF STEP]
have deg0: "degree_m g = 0"
[PROOF STATE]
proof (prove)
using this:
0 < degree_m g \<Longrightarrow> \<not> g * g dvdm f
g * g dvdm f

goal (1 subgoal):
 1. degree_m g = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree_m g = 0

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence g0: "M (lead_coeff g) = 0"
[PROOF STATE]
proof (prove)
using this:
degree_m g = 0

goal (1 subgoal):
 1. M (lead_coeff g) = 0
[PROOF STEP]
unfolding Mp_def
[PROOF STATE]
proof (prove)
using this:
degree (map_poly M g) = 0

goal (1 subgoal):
 1. M (lead_coeff g) = 0
[PROOF STEP]
using deg
[PROOF STATE]
proof (prove)
using this:
degree (map_poly M g) = 0
0 < degree g

goal (1 subgoal):
 1. M (lead_coeff g) = 0
[PROOF STEP]
by (metis M_def deg0 p poly_mod.degree_m_eq prime_gt_1_int neq0_conv)
[PROOF STATE]
proof (state)
this:
M (lead_coeff g) = 0

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
prime p
[PROOF STEP]
have p0: "p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
prime p

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

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from arg_cong[OF f, of lead_coeff]
[PROOF STATE]
proof (chain)
picking this:
lead_coeff f = lead_coeff (g * g * h)
[PROOF STEP]
have "lead_coeff f = lead_coeff g * lead_coeff g * lead_coeff h"
[PROOF STATE]
proof (prove)
using this:
lead_coeff f = lead_coeff (g * g * h)

goal (1 subgoal):
 1. lead_coeff f = lead_coeff g * lead_coeff g * lead_coeff h
[PROOF STEP]
by (auto simp: lead_coeff_mult)
[PROOF STATE]
proof (state)
this:
lead_coeff f = lead_coeff g * lead_coeff g * lead_coeff h

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "lead_coeff g dvd lead_coeff f"
[PROOF STATE]
proof (prove)
using this:
lead_coeff f = lead_coeff g * lead_coeff g * lead_coeff h

goal (1 subgoal):
 1. lead_coeff g dvd lead_coeff f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lead_coeff g dvd lead_coeff f

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with cop
[PROOF STATE]
proof (chain)
picking this:
comm_monoid_mult_class.coprime (lead_coeff f) p
lead_coeff g dvd lead_coeff f
[PROOF STEP]
have cop: "coprime (lead_coeff g) p"
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime (lead_coeff f) p
lead_coeff g dvd lead_coeff f

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff g) p
[PROOF STEP]
by (auto elim: coprime_imp_coprime intro: dvd_trans)
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime (lead_coeff g) p

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with p0
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> 0
comm_monoid_mult_class.coprime (lead_coeff g) p
[PROOF STEP]
have "coprime (lead_coeff g mod p) p"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0
comm_monoid_mult_class.coprime (lead_coeff g) p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff g mod p) p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime (lead_coeff g mod p) p

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime (lead_coeff g mod p) p

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "lead_coeff g mod p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_coeff g mod p = 0
[PROOF STEP]
using M_def g0
[PROOF STATE]
proof (prove)
using this:
M ?x = ?x mod p
M (lead_coeff g) = 0

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

goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < degree q; q * q dvd f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
comm_monoid_mult_class.coprime 0 p
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime 0 p

goal (1 subgoal):
 1. False
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime 0 p
prime p

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding prime_int_iff
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime 0 p
1 < p \<and> (\<forall>m. 0 \<le> m \<and> m dvd p \<longrightarrow> m = 1 \<or> m = p)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: prime_int_iff)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
square_free f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coprime_lead_coeff_large_prime: assumes prime: "prime (p :: int)"
  and large: "p > abs (lead_coeff f)"
  and f: "f \<noteq> 0"
  shows "coprime (lead_coeff f) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
fix lc
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
assume "0 < lc" "lc < p"
[PROOF STATE]
proof (state)
this:
0 < lc
lc < p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < lc
lc < p
[PROOF STEP]
have "\<not> p dvd lc"
[PROOF STATE]
proof (prove)
using this:
0 < lc
lc < p

goal (1 subgoal):
 1. \<not> p dvd lc
[PROOF STEP]
by (simp add: zdvd_not_zless)
[PROOF STATE]
proof (state)
this:
\<not> p dvd lc

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
with \<open>prime p\<close>
[PROOF STATE]
proof (chain)
picking this:
prime p
\<not> p dvd lc
[PROOF STEP]
have "coprime p lc"
[PROOF STATE]
proof (prove)
using this:
prime p
\<not> p dvd lc

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime p lc
[PROOF STEP]
by (auto intro: prime_imp_coprime)
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime p lc

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
comm_monoid_mult_class.coprime p lc
[PROOF STEP]
have "coprime lc p"
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime p lc

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime lc p
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime lc p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?lc2; ?lc2 < p\<rbrakk> \<Longrightarrow> comm_monoid_mult_class.coprime ?lc2 p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
note main = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?lc2; ?lc2 < p\<rbrakk> \<Longrightarrow> comm_monoid_mult_class.coprime ?lc2 p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
define lc where "lc = lead_coeff f"
[PROOF STATE]
proof (state)
this:
lc = lead_coeff f

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
f \<noteq> 0
[PROOF STEP]
have lc0: "lc \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
f \<noteq> 0

goal (1 subgoal):
 1. lc \<noteq> 0
[PROOF STEP]
unfolding lc_def
[PROOF STATE]
proof (prove)
using this:
f \<noteq> 0

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

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
from large
[PROOF STATE]
proof (chain)
picking this:
\<bar>lead_coeff f\<bar> < p
[PROOF STEP]
have large: "p > abs lc"
[PROOF STATE]
proof (prove)
using this:
\<bar>lead_coeff f\<bar> < p

goal (1 subgoal):
 1. \<bar>lc\<bar> < p
[PROOF STEP]
unfolding lc_def
[PROOF STATE]
proof (prove)
using this:
\<bar>lead_coeff f\<bar> < p

goal (1 subgoal):
 1. \<bar>lead_coeff f\<bar> < p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>lc\<bar> < p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
have "coprime lc p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm_monoid_mult_class.coprime lc p
[PROOF STEP]
proof (cases "lc > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < lc \<Longrightarrow> comm_monoid_mult_class.coprime lc p
 2. \<not> 0 < lc \<Longrightarrow> comm_monoid_mult_class.coprime lc p
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < lc

goal (2 subgoals):
 1. 0 < lc \<Longrightarrow> comm_monoid_mult_class.coprime lc p
 2. \<not> 0 < lc \<Longrightarrow> comm_monoid_mult_class.coprime lc p
[PROOF STEP]
from large
[PROOF STATE]
proof (chain)
picking this:
\<bar>lc\<bar> < p
[PROOF STEP]
have "p > lc"
[PROOF STATE]
proof (prove)
using this:
\<bar>lc\<bar> < p

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

goal (2 subgoals):
 1. 0 < lc \<Longrightarrow> comm_monoid_mult_class.coprime lc p
 2. \<not> 0 < lc \<Longrightarrow> comm_monoid_mult_class.coprime lc p
[PROOF STEP]
from main[OF True this]
[PROOF STATE]
proof (chain)
picking this:
comm_monoid_mult_class.coprime lc p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime lc p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime lc p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime lc p

goal (1 subgoal):
 1. \<not> 0 < lc \<Longrightarrow> comm_monoid_mult_class.coprime lc p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < lc \<Longrightarrow> comm_monoid_mult_class.coprime lc p
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 < lc

goal (1 subgoal):
 1. \<not> 0 < lc \<Longrightarrow> comm_monoid_mult_class.coprime lc p
[PROOF STEP]
let ?mlc = "- lc"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < lc \<Longrightarrow> comm_monoid_mult_class.coprime lc p
[PROOF STEP]
from large False lc0
[PROOF STATE]
proof (chain)
picking this:
\<bar>lc\<bar> < p
\<not> 0 < lc
lc \<noteq> 0
[PROOF STEP]
have "?mlc > 0" "p > ?mlc"
[PROOF STATE]
proof (prove)
using this:
\<bar>lc\<bar> < p
\<not> 0 < lc
lc \<noteq> 0

goal (1 subgoal):
 1. 0 < - lc &&& - lc < p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < - lc
- lc < p

goal (1 subgoal):
 1. \<not> 0 < lc \<Longrightarrow> comm_monoid_mult_class.coprime lc p
[PROOF STEP]
from main[OF this]
[PROOF STATE]
proof (chain)
picking this:
comm_monoid_mult_class.coprime (- lc) p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime (- lc) p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime lc p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime lc p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime lc p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime lc p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
unfolding lc_def
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime (lead_coeff f) p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime (lead_coeff f) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_for_berlekamp_zassenhaus_exists: assumes sf: "square_free f"
  shows "\<exists> p. prime p \<and> (coprime (lead_coeff f) p \<and> separable_impl p f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
square_free f
[PROOF STEP]
have f0: "f \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
square_free f

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

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

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
define n where "n = max (max (abs (lead_coeff f)) (degree f)) (separable_bound f)"
[PROOF STATE]
proof (state)
this:
n = max (max \<bar>lead_coeff f\<bar> (int (degree f))) (separable_bound f)

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
assume contr: "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
fix p :: int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
assume prime: "prime p" and n: "p > n"
[PROOF STATE]
proof (state)
this:
prime p
n < p

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prime p
n < p
[PROOF STEP]
interpret poly_mod_prime p
[PROOF STATE]
proof (prove)
using this:
prime p
n < p

goal (1 subgoal):
 1. poly_mod_prime p
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
n < p
[PROOF STEP]
have large: "p > abs (lead_coeff f)" "nat p > degree f" "nat p > separable_bound f"
[PROOF STATE]
proof (prove)
using this:
n < p

goal (1 subgoal):
 1. \<bar>lead_coeff f\<bar> < p &&& degree f < nat p &&& separable_bound f < int (nat p)
[PROOF STEP]
unfolding n_def
[PROOF STATE]
proof (prove)
using this:
max (max \<bar>lead_coeff f\<bar> (int (degree f))) (separable_bound f) < p

goal (1 subgoal):
 1. \<bar>lead_coeff f\<bar> < p &&& degree f < nat p &&& separable_bound f < int (nat p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>lead_coeff f\<bar> < p
degree f < nat p
separable_bound f < int (nat p)

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
from coprime_lead_coeff_large_prime[OF prime large(1) f0]
[PROOF STATE]
proof (chain)
picking this:
comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
have cop: "coprime (lead_coeff f) p"
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime (lead_coeff f) p

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime (lead_coeff f) p

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
with prime contr
[PROOF STATE]
proof (chain)
picking this:
prime p
\<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f
comm_monoid_mult_class.coprime (lead_coeff f) p
[PROOF STEP]
have nsf: "\<not> separable_impl p f"
[PROOF STATE]
proof (prove)
using this:
prime p
\<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f
comm_monoid_mult_class.coprime (lead_coeff f) p

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

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
from large(2)
[PROOF STATE]
proof (chain)
picking this:
degree f < nat p
[PROOF STEP]
have "nat p > degree_m f"
[PROOF STATE]
proof (prove)
using this:
degree f < nat p

goal (1 subgoal):
 1. degree_m f < nat p
[PROOF STEP]
using degree_m_le[of f]
[PROOF STATE]
proof (prove)
using this:
degree f < nat p
degree_m f \<le> degree f

goal (1 subgoal):
 1. degree_m f < nat p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree_m f < nat p

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
from separable_impl(2)[OF this large(3) sf] nsf
[PROOF STATE]
proof (chain)
picking this:
separable_impl p f
\<not> separable_impl p f
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
separable_impl p f
\<not> separable_impl p f

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

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>prime ?p2; n < ?p2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
hence no_large_prime: "\<And> p. prime p \<Longrightarrow> p > n \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime ?p2; n < ?p2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>p. \<lbrakk>prime p; n < p\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>prime ?p; n < ?p\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
from bigger_prime[of "nat n"]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. prime p \<and> nat n < p
[PROOF STEP]
obtain p where *: "prime p" "p > nat n"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. prime p \<and> nat n < p

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; nat n < p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime p
nat n < p

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
define q where "q \<equiv> int p"
[PROOF STATE]
proof (state)
this:
q \<equiv> int p

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
prime p
nat n < p
[PROOF STEP]
have "prime q" "q > n"
[PROOF STATE]
proof (prove)
using this:
prime p
nat n < p

goal (1 subgoal):
 1. prime q &&& n < q
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
using this:
prime p
nat n < p

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

goal (1 subgoal):
 1. \<nexists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<Longrightarrow> False
[PROOF STEP]
from no_large_prime[OF this]
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. False
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next_primes: assumes res: "next_primes n = (m,ps)"
  and n: "candidate_invariant n"
  shows "candidate_invariant m" "sorted ps" "distinct ps" "n < m"
  "set ps = {i. prime i \<and> n \<le> i \<and> i < m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (candidate_invariant m &&& sorted ps) &&& distinct ps &&& n < m &&& set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. candidate_invariant m
 2. sorted ps
 3. distinct ps
 4. n < m
 5. set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
have "candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and>
    set ps = {i. prime i \<and> n \<le> i \<and> i < m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
 2. n \<noteq> 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
 2. n \<noteq> 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
with res[unfolded next_primes_def]
[PROOF STATE]
proof (chain)
picking this:
(if n = 0 then next_candidates 0 else let (m, ps) = next_candidates n in (m, filter prime ps)) = (m, ps)
n = 0
[PROOF STEP]
have nc: "next_candidates 0 = (m,ps)"
[PROOF STATE]
proof (prove)
using this:
(if n = 0 then next_candidates 0 else let (m, ps) = next_candidates n in (m, filter prime ps)) = (m, ps)
n = 0

goal (1 subgoal):
 1. next_candidates 0 = (m, ps)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
next_candidates 0 = (m, ps)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
 2. n \<noteq> 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
from this[unfolded next_candidates_def]
[PROOF STATE]
proof (chain)
picking this:
(if 0 = 0 then (1001, primes_1000) else (0 + 30, [0, 0 + 2, 0 + 6, 0 + 8, 0 + 12, 0 + 18, 0 + 20, 0 + 26])) = (m, ps)
[PROOF STEP]
have ps: "ps = primes_1000" and m: "m = 1001"
[PROOF STATE]
proof (prove)
using this:
(if 0 = 0 then (1001, primes_1000) else (0 + 30, [0, 0 + 2, 0 + 6, 0 + 8, 0 + 12, 0 + 18, 0 + 20, 0 + 26])) = (m, ps)

goal (1 subgoal):
 1. ps = primes_1000 &&& m = 1001
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ps = primes_1000
m = 1001

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
 2. n \<noteq> 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
have ps: "set ps = {i. prime i \<and> n \<le> i \<and> i < m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
unfolding m True ps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set primes_1000 = {i. prime i \<and> 0 \<le> i \<and> i < 1001}
[PROOF STEP]
by (auto simp: primes_1000)
[PROOF STATE]
proof (state)
this:
set ps = {i. prime i \<and> n \<le> i \<and> i < m}

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
 2. n \<noteq> 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
with next_candidates[OF nc n[unfolded True]] True
[PROOF STATE]
proof (chain)
picking this:
candidate_invariant m
sorted ps
{i. prime i \<and> 0 \<le> i \<and> i < m} \<subseteq> set ps
set ps \<subseteq> {2..} \<inter> {0..<m}
distinct ps
ps \<noteq> []
0 < m
n = 0
set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
candidate_invariant m
sorted ps
{i. prime i \<and> 0 \<le> i \<and> i < m} \<subseteq> set ps
set ps \<subseteq> {2..} \<inter> {0..<m}
distinct ps
ps \<noteq> []
0 < m
n = 0
set ps = {i. prime i \<and> n \<le> i \<and> i < m}

goal (1 subgoal):
 1. candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
with res[unfolded next_primes_def Let_def]
[PROOF STATE]
proof (chain)
picking this:
(if n = 0 then next_candidates 0 else case next_candidates n of (m, ps) \<Rightarrow> (m, filter prime ps)) = (m, ps)
n \<noteq> 0
[PROOF STEP]
obtain qs where nc: "next_candidates n = (m, qs)"
      and ps: "ps = filter prime qs"
[PROOF STATE]
proof (prove)
using this:
(if n = 0 then next_candidates 0 else case next_candidates n of (m, ps) \<Rightarrow> (m, filter prime ps)) = (m, ps)
n \<noteq> 0

goal (1 subgoal):
 1. (\<And>qs. \<lbrakk>next_candidates n = (m, qs); ps = filter prime qs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "next_candidates n", auto)
[PROOF STATE]
proof (state)
this:
next_candidates n = (m, qs)
ps = filter prime qs

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
have "sorted qs \<Longrightarrow> sorted ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted qs \<Longrightarrow> sorted ps
[PROOF STEP]
unfolding ps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted qs \<Longrightarrow> sorted (filter prime qs)
[PROOF STEP]
using sorted_filter[of id qs prime]
[PROOF STATE]
proof (prove)
using this:
sorted (map id qs) \<Longrightarrow> sorted (map id (filter prime qs))

goal (1 subgoal):
 1. sorted qs \<Longrightarrow> sorted (filter prime qs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sorted qs \<Longrightarrow> sorted ps

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
with next_candidates[OF nc n]
[PROOF STATE]
proof (chain)
picking this:
candidate_invariant m
sorted qs
{i. prime i \<and> n \<le> i \<and> i < m} \<subseteq> set qs
set qs \<subseteq> {2..} \<inter> {n..<m}
distinct qs
qs \<noteq> []
n < m
sorted qs \<Longrightarrow> sorted ps
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
candidate_invariant m
sorted qs
{i. prime i \<and> n \<le> i \<and> i < m} \<subseteq> set qs
set qs \<subseteq> {2..} \<inter> {n..<m}
distinct qs
qs \<noteq> []
n < m
sorted qs \<Longrightarrow> sorted ps

goal (1 subgoal):
 1. candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
unfolding ps
[PROOF STATE]
proof (prove)
using this:
candidate_invariant m
sorted qs
{i. prime i \<and> n \<le> i \<and> i < m} \<subseteq> set qs
set qs \<subseteq> {2..} \<inter> {n..<m}
distinct qs
qs \<noteq> []
n < m
sorted qs \<Longrightarrow> sorted (filter prime qs)

goal (1 subgoal):
 1. candidate_invariant m \<and> sorted (filter prime qs) \<and> distinct (filter prime qs) \<and> n < m \<and> set (filter prime qs) = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}

goal (5 subgoals):
 1. candidate_invariant m
 2. sorted ps
 3. distinct ps
 4. n < m
 5. set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
thus "candidate_invariant m" "sorted ps" "distinct ps" "n < m"
    "set ps = {i. prime i \<and> n \<le> i \<and> i < m}"
[PROOF STATE]
proof (prove)
using this:
candidate_invariant m \<and> sorted ps \<and> distinct ps \<and> n < m \<and> set ps = {i. prime i \<and> n \<le> i \<and> i < m}

goal (1 subgoal):
 1. (candidate_invariant m &&& sorted ps) &&& distinct ps &&& n < m &&& set ps = {i. prime i \<and> n \<le> i \<and> i < m}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
candidate_invariant m
sorted ps
distinct ps
n < m
set ps = {i. prime i \<and> n \<le> i \<and> i < m}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_prime: assumes "\<exists> n. prime n \<and> f n"
  shows "prime (find_prime f) \<and> f (find_prime f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (find_prime f) \<and> f (find_prime f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime (find_prime f) \<and> f (find_prime f)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. prime n \<and> f n
[PROOF STEP]
obtain n where fn: "prime n" "f n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. prime n \<and> f n

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>prime n; f n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime n
f n

goal (1 subgoal):
 1. prime (find_prime f) \<and> f (find_prime f)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
prime n
f n

goal (1 subgoal):
 1. prime (find_prime f) \<and> f (find_prime f)
[PROOF STEP]
fix i ps m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime (find_prime f) \<and> f (find_prime f)
[PROOF STEP]
assume "candidate_invariant i"
      and "n \<in> set ps \<or> n \<ge> i"
      and "m = (Suc n - i, length ps)"
      and "\<And> p. p \<in> set ps \<Longrightarrow> prime p"
[PROOF STATE]
proof (state)
this:
candidate_invariant i
n \<in> set ps \<or> i \<le> n
m = (Suc n - i, length ps)
?p \<in> set ps \<Longrightarrow> prime ?p

goal (1 subgoal):
 1. prime (find_prime f) \<and> f (find_prime f)
[PROOF STEP]
hence "prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)"
[PROOF STATE]
proof (prove)
using this:
candidate_invariant i
n \<in> set ps \<or> i \<le> n
m = (Suc n - i, length ps)
?p \<in> set ps \<Longrightarrow> prime ?p

goal (1 subgoal):
 1. prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
proof (induct m arbitrary: i ps rule: wf_induct[OF wf_measures[of "[fst, snd]"]])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x i ps. \<lbrakk>\<forall>y. (y, x) \<in> measures [fst, snd] \<longrightarrow> (\<forall>x. candidate_invariant x \<longrightarrow> (\<forall>xa. n \<in> set xa \<or> x \<le> n \<longrightarrow> y = (Suc n - x, length xa) \<longrightarrow> (\<forall>x. x \<in> set xa \<longrightarrow> prime x) \<longrightarrow> prime (find_prime_main f x xa) \<and> f (find_prime_main f x xa))); candidate_invariant i; n \<in> set ps \<or> i \<le> n; x = (Suc n - i, length ps); \<And>p. p \<in> set ps \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
case (1 m i ps)
[PROOF STATE]
proof (state)
this:
\<forall>y. (y, m) \<in> measures [fst, snd] \<longrightarrow> (\<forall>x. candidate_invariant x \<longrightarrow> (\<forall>xa. n \<in> set xa \<or> x \<le> n \<longrightarrow> y = (Suc n - x, length xa) \<longrightarrow> (\<forall>x. x \<in> set xa \<longrightarrow> prime x) \<longrightarrow> prime (find_prime_main f x xa) \<and> f (find_prime_main f x xa)))
candidate_invariant i
n \<in> set ps \<or> i \<le> n
m = (Suc n - i, length ps)
?p \<in> set ps \<Longrightarrow> prime ?p

goal (1 subgoal):
 1. \<And>x i ps. \<lbrakk>\<forall>y. (y, x) \<in> measures [fst, snd] \<longrightarrow> (\<forall>x. candidate_invariant x \<longrightarrow> (\<forall>xa. n \<in> set xa \<or> x \<le> n \<longrightarrow> y = (Suc n - x, length xa) \<longrightarrow> (\<forall>x. x \<in> set xa \<longrightarrow> prime x) \<longrightarrow> prime (find_prime_main f x xa) \<and> f (find_prime_main f x xa))); candidate_invariant i; n \<in> set ps \<or> i \<le> n; x = (Suc n - i, length ps); \<And>p. p \<in> set ps \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
note IH = 1(1)[rule_format]
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?y, m) \<in> measures [fst, snd]; candidate_invariant ?x; n \<in> set ?xa \<or> ?x \<le> n; ?y = (Suc n - ?x, length ?xa); \<And>x. x \<in> set ?xa \<Longrightarrow> prime x\<rbrakk> \<Longrightarrow> prime (find_prime_main f ?x ?xa) \<and> f (find_prime_main f ?x ?xa)

goal (1 subgoal):
 1. \<And>x i ps. \<lbrakk>\<forall>y. (y, x) \<in> measures [fst, snd] \<longrightarrow> (\<forall>x. candidate_invariant x \<longrightarrow> (\<forall>xa. n \<in> set xa \<or> x \<le> n \<longrightarrow> y = (Suc n - x, length xa) \<longrightarrow> (\<forall>x. x \<in> set xa \<longrightarrow> prime x) \<longrightarrow> prime (find_prime_main f x xa) \<and> f (find_prime_main f x xa))); candidate_invariant i; n \<in> set ps \<or> i \<le> n; x = (Suc n - i, length ps); \<And>p. p \<in> set ps \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
note can = 1(2)
[PROOF STATE]
proof (state)
this:
candidate_invariant i

goal (1 subgoal):
 1. \<And>x i ps. \<lbrakk>\<forall>y. (y, x) \<in> measures [fst, snd] \<longrightarrow> (\<forall>x. candidate_invariant x \<longrightarrow> (\<forall>xa. n \<in> set xa \<or> x \<le> n \<longrightarrow> y = (Suc n - x, length xa) \<longrightarrow> (\<forall>x. x \<in> set xa \<longrightarrow> prime x) \<longrightarrow> prime (find_prime_main f x xa) \<and> f (find_prime_main f x xa))); candidate_invariant i; n \<in> set ps \<or> i \<le> n; x = (Suc n - i, length ps); \<And>p. p \<in> set ps \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
note n = 1(3)
[PROOF STATE]
proof (state)
this:
n \<in> set ps \<or> i \<le> n

goal (1 subgoal):
 1. \<And>x i ps. \<lbrakk>\<forall>y. (y, x) \<in> measures [fst, snd] \<longrightarrow> (\<forall>x. candidate_invariant x \<longrightarrow> (\<forall>xa. n \<in> set xa \<or> x \<le> n \<longrightarrow> y = (Suc n - x, length xa) \<longrightarrow> (\<forall>x. x \<in> set xa \<longrightarrow> prime x) \<longrightarrow> prime (find_prime_main f x xa) \<and> f (find_prime_main f x xa))); candidate_invariant i; n \<in> set ps \<or> i \<le> n; x = (Suc n - i, length ps); \<And>p. p \<in> set ps \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
note m = 1(4)
[PROOF STATE]
proof (state)
this:
m = (Suc n - i, length ps)

goal (1 subgoal):
 1. \<And>x i ps. \<lbrakk>\<forall>y. (y, x) \<in> measures [fst, snd] \<longrightarrow> (\<forall>x. candidate_invariant x \<longrightarrow> (\<forall>xa. n \<in> set xa \<or> x \<le> n \<longrightarrow> y = (Suc n - x, length xa) \<longrightarrow> (\<forall>x. x \<in> set xa \<longrightarrow> prime x) \<longrightarrow> prime (find_prime_main f x xa) \<and> f (find_prime_main f x xa))); candidate_invariant i; n \<in> set ps \<or> i \<le> n; x = (Suc n - i, length ps); \<And>p. p \<in> set ps \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
note ps = 1(5)
[PROOF STATE]
proof (state)
this:
?p \<in> set ps \<Longrightarrow> prime ?p

goal (1 subgoal):
 1. \<And>x i ps. \<lbrakk>\<forall>y. (y, x) \<in> measures [fst, snd] \<longrightarrow> (\<forall>x. candidate_invariant x \<longrightarrow> (\<forall>xa. n \<in> set xa \<or> x \<le> n \<longrightarrow> y = (Suc n - x, length xa) \<longrightarrow> (\<forall>x. x \<in> set xa \<longrightarrow> prime x) \<longrightarrow> prime (find_prime_main f x xa) \<and> f (find_prime_main f x xa))); candidate_invariant i; n \<in> set ps \<or> i \<le> n; x = (Suc n - i, length ps); \<And>p. p \<in> set ps \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
note simps [simp] = find_prime_main.simps[of f i ps]
[PROOF STATE]
proof (state)
this:
find_prime_main f i ps = (case ps of [] \<Rightarrow> let (np', ps') = next_primes i in find_prime_main f np' ps' | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps)

goal (1 subgoal):
 1. \<And>x i ps. \<lbrakk>\<forall>y. (y, x) \<in> measures [fst, snd] \<longrightarrow> (\<forall>x. candidate_invariant x \<longrightarrow> (\<forall>xa. n \<in> set xa \<or> x \<le> n \<longrightarrow> y = (Suc n - x, length xa) \<longrightarrow> (\<forall>x. x \<in> set xa \<longrightarrow> prime x) \<longrightarrow> prime (find_prime_main f x xa) \<and> f (find_prime_main f x xa))); candidate_invariant i; n \<in> set ps \<or> i \<le> n; x = (Suc n - i, length ps); \<And>p. p \<in> set ps \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
proof (cases ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ps = [] \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
 2. \<And>a list. ps = a # list \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ps = []

goal (2 subgoals):
 1. ps = [] \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
 2. \<And>a list. ps = a # list \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
with n
[PROOF STATE]
proof (chain)
picking this:
n \<in> set ps \<or> i \<le> n
ps = []
[PROOF STEP]
have i_n: "i \<le> n"
[PROOF STATE]
proof (prove)
using this:
n \<in> set ps \<or> i \<le> n
ps = []

goal (1 subgoal):
 1. i \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<le> n

goal (2 subgoals):
 1. ps = [] \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
 2. \<And>a list. ps = a # list \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
obtain j qs where np: "next_primes i = (j,qs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j qs. next_primes i = (j, qs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
next_primes i = (j, qs)

goal (2 subgoals):
 1. ps = [] \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
 2. \<And>a list. ps = a # list \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
note j = next_primes[OF np can]
[PROOF STATE]
proof (state)
this:
candidate_invariant j
sorted qs
distinct qs
i < j
set qs = {i. prime i \<and> i \<le> i \<and> i < j}

goal (2 subgoals):
 1. ps = [] \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
 2. \<And>a list. ps = a # list \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
from j(4) i_n m
[PROOF STATE]
proof (chain)
picking this:
i < j
i \<le> n
m = (Suc n - i, length ps)
[PROOF STEP]
have meas: "((Suc n - j, length qs), m) \<in> measures [fst, snd]"
[PROOF STATE]
proof (prove)
using this:
i < j
i \<le> n
m = (Suc n - i, length ps)

goal (1 subgoal):
 1. ((Suc n - j, length qs), m) \<in> measures [fst, snd]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((Suc n - j, length qs), m) \<in> measures [fst, snd]

goal (2 subgoals):
 1. ps = [] \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
 2. \<And>a list. ps = a # list \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
have n: "n \<in> set qs \<or> j \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> set qs \<or> j \<le> n
[PROOF STEP]
unfolding j(5)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> {i. prime i \<and> i \<le> i \<and> i < j} \<or> j \<le> n
[PROOF STEP]
using i_n fn
[PROOF STATE]
proof (prove)
using this:
i \<le> n
prime n
f n

goal (1 subgoal):
 1. n \<in> {i. prime i \<and> i \<le> i \<and> i < j} \<or> j \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> set qs \<or> j \<le> n

goal (2 subgoals):
 1. ps = [] \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
 2. \<And>a list. ps = a # list \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
unfolding simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps) \<and> f (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps)
[PROOF STEP]
using IH[OF meas j(1) n refl] j(5)
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> set qs \<Longrightarrow> prime x) \<Longrightarrow> prime (find_prime_main f j qs) \<and> f (find_prime_main f j qs)
set qs = {i. prime i \<and> i \<le> i \<and> i < j}

goal (1 subgoal):
 1. prime (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps) \<and> f (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps)
[PROOF STEP]
by (simp add: Nil np)
[PROOF STATE]
proof (state)
this:
prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)

goal (1 subgoal):
 1. \<And>a list. ps = a # list \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ps = a # list \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
case (Cons p qs)
[PROOF STATE]
proof (state)
this:
ps = p # qs

goal (1 subgoal):
 1. \<And>a list. ps = a # list \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
proof (cases "f p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f p \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
 2. \<not> f p \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f p

goal (2 subgoals):
 1. f p \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
 2. \<not> f p \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f p

goal (1 subgoal):
 1. prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
unfolding simps
[PROOF STATE]
proof (prove)
using this:
f p

goal (1 subgoal):
 1. prime (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps) \<and> f (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps)
[PROOF STEP]
using ps
[PROOF STATE]
proof (prove)
using this:
f p
?p \<in> set ps \<Longrightarrow> prime ?p

goal (1 subgoal):
 1. prime (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps) \<and> f (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps)
[PROOF STEP]
unfolding Cons
[PROOF STATE]
proof (prove)
using this:
f p
?p \<in> set (p # qs) \<Longrightarrow> prime ?p

goal (1 subgoal):
 1. prime (case p # qs of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps) \<and> f (case p # qs of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)

goal (1 subgoal):
 1. \<not> f p \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> f p \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> f p

goal (1 subgoal):
 1. \<not> f p \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
have m: "((Suc n - i, length qs), m) \<in> measures [fst, snd]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((Suc n - i, length qs), m) \<in> measures [fst, snd]
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
m = (Suc n - i, length ps)

goal (1 subgoal):
 1. ((Suc n - i, length qs), m) \<in> measures [fst, snd]
[PROOF STEP]
unfolding Cons
[PROOF STATE]
proof (prove)
using this:
m = (Suc n - i, length (p # qs))

goal (1 subgoal):
 1. ((Suc n - i, length qs), m) \<in> measures [fst, snd]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((Suc n - i, length qs), m) \<in> measures [fst, snd]

goal (1 subgoal):
 1. \<not> f p \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
have n: "n \<in> set qs \<or> i \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> set qs \<or> i \<le> n
[PROOF STEP]
using False n fn
[PROOF STATE]
proof (prove)
using this:
\<not> f p
n \<in> set ps \<or> i \<le> n
prime n
f n

goal (1 subgoal):
 1. n \<in> set qs \<or> i \<le> n
[PROOF STEP]
by (auto simp: Cons)
[PROOF STATE]
proof (state)
this:
n \<in> set qs \<or> i \<le> n

goal (1 subgoal):
 1. \<not> f p \<Longrightarrow> prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
from IH[OF m can n refl ps]
[PROOF STATE]
proof (chain)
picking this:
(\<And>x. x \<in> set qs \<Longrightarrow> x \<in> set ps) \<Longrightarrow> prime (find_prime_main f i qs) \<and> f (find_prime_main f i qs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> set qs \<Longrightarrow> x \<in> set ps) \<Longrightarrow> prime (find_prime_main f i qs) \<and> f (find_prime_main f i qs)

goal (1 subgoal):
 1. prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)
[PROOF STEP]
unfolding simps
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> set qs \<Longrightarrow> x \<in> set ps) \<Longrightarrow> prime (find_prime_main f i qs) \<and> f (find_prime_main f i qs)

goal (1 subgoal):
 1. prime (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps) \<and> f (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps)
[PROOF STEP]
using Cons False
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> set qs \<Longrightarrow> x \<in> set ps) \<Longrightarrow> prime (find_prime_main f i qs) \<and> f (find_prime_main f i qs)
ps = p # qs
\<not> f p

goal (1 subgoal):
 1. prime (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps) \<and> f (case ps of [] \<Rightarrow> let (x, y) = next_primes i in find_prime_main f x y | p # ps \<Rightarrow> if f p then p else find_prime_main f i ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime (find_prime_main f i ps) \<and> f (find_prime_main f i ps)

goal (1 subgoal):
 1. prime (find_prime f) \<and> f (find_prime f)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>candidate_invariant ?i2; n \<in> set ?ps2 \<or> ?i2 \<le> n; ?m2 = (Suc n - ?i2, length ?ps2); \<And>p. p \<in> set ?ps2 \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f ?i2 ?ps2) \<and> f (find_prime_main f ?i2 ?ps2)

goal (1 subgoal):
 1. prime (find_prime f) \<and> f (find_prime f)
[PROOF STEP]
note main = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>candidate_invariant ?i2; n \<in> set ?ps2 \<or> ?i2 \<le> n; ?m2 = (Suc n - ?i2, length ?ps2); \<And>p. p \<in> set ?ps2 \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f ?i2 ?ps2) \<and> f (find_prime_main f ?i2 ?ps2)

goal (1 subgoal):
 1. prime (find_prime f) \<and> f (find_prime f)
[PROOF STEP]
have "candidate_invariant 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. candidate_invariant 0
[PROOF STEP]
by (simp add: candidate_invariant_def)
[PROOF STATE]
proof (state)
this:
candidate_invariant 0

goal (1 subgoal):
 1. prime (find_prime f) \<and> f (find_prime f)
[PROOF STEP]
from main[OF this _ refl, of Nil]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>n \<in> set [] \<or> 0 \<le> n; \<And>p. p \<in> set [] \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f 0 []) \<and> f (find_prime_main f 0 [])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n \<in> set [] \<or> 0 \<le> n; \<And>p. p \<in> set [] \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f 0 []) \<and> f (find_prime_main f 0 [])

goal (1 subgoal):
 1. prime (find_prime f) \<and> f (find_prime f)
[PROOF STEP]
unfolding find_prime_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n \<in> set [] \<or> 0 \<le> n; \<And>p. p \<in> set [] \<Longrightarrow> prime p\<rbrakk> \<Longrightarrow> prime (find_prime_main f 0 []) \<and> f (find_prime_main f 0 [])

goal (1 subgoal):
 1. prime (find_prime_main f 0 []) \<and> f (find_prime_main f 0 [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime (find_prime f) \<and> f (find_prime f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma suitable_prime_bz: assumes sf: "square_free f" and p: "p = suitable_prime_bz f"
  shows "prime p" "coprime (lead_coeff f) p" "poly_mod.square_free_m p f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p &&& comm_monoid_mult_class.coprime (lead_coeff f) p &&& poly_mod.square_free_m p f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. prime p
 2. comm_monoid_mult_class.coprime (lead_coeff f) p
 3. poly_mod.square_free_m p f
[PROOF STEP]
let ?lc = "lead_coeff f"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. prime p
 2. comm_monoid_mult_class.coprime (lead_coeff f) p
 3. poly_mod.square_free_m p f
[PROOF STEP]
from prime_for_berlekamp_zassenhaus_exists[OF sf, unfolded Let_def]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f
[PROOF STEP]
obtain P where *: "prime P \<and> coprime ?lc P \<and> separable_impl P f"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f

goal (1 subgoal):
 1. (\<And>P. prime P \<and> comm_monoid_mult_class.coprime (lead_coeff f) P \<and> separable_impl P f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime P \<and> comm_monoid_mult_class.coprime (lead_coeff f) P \<and> separable_impl P f

goal (3 subgoals):
 1. prime p
 2. comm_monoid_mult_class.coprime (lead_coeff f) p
 3. poly_mod.square_free_m p f
[PROOF STEP]
hence "prime (nat P)"
[PROOF STATE]
proof (prove)
using this:
prime P \<and> comm_monoid_mult_class.coprime (lead_coeff f) P \<and> separable_impl P f

goal (1 subgoal):
 1. prime (nat P)
[PROOF STEP]
using prime_int_nat_transfer
[PROOF STATE]
proof (prove)
using this:
prime P \<and> comm_monoid_mult_class.coprime (lead_coeff f) P \<and> separable_impl P f
prime ?k = (0 \<le> ?k \<and> prime (nat ?k))

goal (1 subgoal):
 1. prime (nat P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prime (nat P)

goal (3 subgoals):
 1. prime p
 2. comm_monoid_mult_class.coprime (lead_coeff f) p
 3. poly_mod.square_free_m p f
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
prime P \<and> comm_monoid_mult_class.coprime (lead_coeff f) P \<and> separable_impl P f
prime (nat P)
[PROOF STEP]
have "\<exists> p. prime p \<and> coprime ?lc (int p) \<and> separable_impl p f"
[PROOF STATE]
proof (prove)
using this:
prime P \<and> comm_monoid_mult_class.coprime (lead_coeff f) P \<and> separable_impl P f
prime (nat P)

goal (1 subgoal):
 1. \<exists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) (int p) \<and> separable_impl (int p) f
[PROOF STEP]
by (intro exI [of _ "nat P"]) (auto dest: prime_gt_0_int)
[PROOF STATE]
proof (state)
this:
\<exists>p. prime p \<and> comm_monoid_mult_class.coprime (lead_coeff f) (int p) \<and> separable_impl (int p) f

goal (3 subgoals):
 1. prime p
 2. comm_monoid_mult_class.coprime (lead_coeff f) p
 3. poly_mod.square_free_m p f
[PROOF STEP]
from find_prime[OF this]
[PROOF STATE]
proof (chain)
picking this:
prime (find_prime (\<lambda>p. comm_monoid_mult_class.coprime (lead_coeff f) (int p) \<and> separable_impl (int p) f)) \<and> comm_monoid_mult_class.coprime (lead_coeff f) (int (find_prime (\<lambda>p. comm_monoid_mult_class.coprime (lead_coeff f) (int p) \<and> separable_impl (int p) f))) \<and> separable_impl (int (find_prime (\<lambda>p. comm_monoid_mult_class.coprime (lead_coeff f) (int p) \<and> separable_impl (int p) f))) f
[PROOF STEP]
have prime: "prime p" and cop: "coprime ?lc p" and sf: "separable_impl p f"
[PROOF STATE]
proof (prove)
using this:
prime (find_prime (\<lambda>p. comm_monoid_mult_class.coprime (lead_coeff f) (int p) \<and> separable_impl (int p) f)) \<and> comm_monoid_mult_class.coprime (lead_coeff f) (int (find_prime (\<lambda>p. comm_monoid_mult_class.coprime (lead_coeff f) (int p) \<and> separable_impl (int p) f))) \<and> separable_impl (int (find_prime (\<lambda>p. comm_monoid_mult_class.coprime (lead_coeff f) (int p) \<and> separable_impl (int p) f))) f

goal (1 subgoal):
 1. prime p &&& comm_monoid_mult_class.coprime (lead_coeff f) p &&& separable_impl p f
[PROOF STEP]
unfolding p suitable_prime_bz_def Let_def
[PROOF STATE]
proof (prove)
using this:
prime (find_prime (\<lambda>p. comm_monoid_mult_class.coprime (lead_coeff f) (int p) \<and> separable_impl (int p) f)) \<and> comm_monoid_mult_class.coprime (lead_coeff f) (int (find_prime (\<lambda>p. comm_monoid_mult_class.coprime (lead_coeff f) (int p) \<and> separable_impl (int p) f))) \<and> separable_impl (int (find_prime (\<lambda>p. comm_monoid_mult_class.coprime (lead_coeff f) (int p) \<and> separable_impl (int p) f))) f

goal (1 subgoal):
 1. prime (int (find_prime (\<lambda>n. comm_monoid_mult_class.coprime (lead_coeff f) (int n) \<and> separable_impl (int n) f))) &&& comm_monoid_mult_class.coprime (lead_coeff f) (int (find_prime (\<lambda>n. comm_monoid_mult_class.coprime (lead_coeff f) (int n) \<and> separable_impl (int n) f))) &&& separable_impl (int (find_prime (\<lambda>n. comm_monoid_mult_class.coprime (lead_coeff f) (int n) \<and> separable_impl (int n) f))) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime p
comm_monoid_mult_class.coprime (lead_coeff f) p
separable_impl p f

goal (3 subgoals):
 1. prime p
 2. comm_monoid_mult_class.coprime (lead_coeff f) p
 3. poly_mod.square_free_m p f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prime p
comm_monoid_mult_class.coprime (lead_coeff f) p
separable_impl p f
[PROOF STEP]
interpret poly_mod_prime p
[PROOF STATE]
proof (prove)
using this:
prime p
comm_monoid_mult_class.coprime (lead_coeff f) p
separable_impl p f

goal (1 subgoal):
 1. poly_mod_prime p
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. prime p
 2. comm_monoid_mult_class.coprime (lead_coeff f) p
 3. square_free_m f
[PROOF STEP]
from prime cop separable_impl(1)[OF sf]
[PROOF STATE]
proof (chain)
picking this:
prime p
comm_monoid_mult_class.coprime (lead_coeff f) p
square_free_m f
[PROOF STEP]
show "prime p" "coprime ?lc p" "square_free_m f"
[PROOF STATE]
proof (prove)
using this:
prime p
comm_monoid_mult_class.coprime (lead_coeff f) p
square_free_m f

goal (1 subgoal):
 1. prime p &&& comm_monoid_mult_class.coprime (lead_coeff f) p &&& square_free_m f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime p
comm_monoid_mult_class.coprime (lead_coeff f) p
square_free_m f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_Some_D: "find f xs = Some y \<Longrightarrow> y \<in> set xs \<and> f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find f xs = Some y \<Longrightarrow> y \<in> set xs \<and> f y
[PROOF STEP]
unfolding find_Some_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i<length xs. f (xs ! i) \<and> y = xs ! i \<and> (\<forall>j<i. \<not> f (xs ! j)) \<Longrightarrow> y \<in> set xs \<and> f y
[PROOF STEP]
by auto


[STATEMENT]
lemma square_free_heuristic: assumes "square_free_heuristic f = Some p"
  shows "coprime (lead_coeff f) p \<and> separable_impl p f \<and> prime p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<and> prime p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<and> prime p
[PROOF STEP]
from find_Some_D[OF assms[unfolded square_free_heuristic_def Let_def]]
[PROOF STATE]
proof (chain)
picking this:
p \<in> set [2, 3, 5, 7, 11, 13, 17, 19, 23] \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> set [2, 3, 5, 7, 11, 13, 17, 19, 23] \<and> comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<and> prime p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime (lead_coeff f) p \<and> separable_impl p f \<and> prime p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma summandsInput[simp]:
  fixes a :: name
  and   x :: name
  and   P :: pi

  shows "summands (a<x>.P) = {a<x>.P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summands (a<x>.P) = {a<x>.P}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summands (a<x>.P) = {a<x>.P}
[PROOF STEP]
obtain y where yineqa: "y \<noteq> a" and yFreshP: "y \<sharp> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<noteq> a; y \<sharp> P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(force intro: name_exists_fresh[of "(a, P)"] simp add: fresh_prod)
[PROOF STATE]
proof (state)
this:
y \<noteq> a
y \<sharp> P

goal (1 subgoal):
 1. summands (a<x>.P) = {a<x>.P}
[PROOF STEP]
from yFreshP
[PROOF STATE]
proof (chain)
picking this:
y \<sharp> P
[PROOF STEP]
have "a<x>.P = a<y>.([(x, y)] \<bullet> P)"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> P

goal (1 subgoal):
 1. a<x>.P = a<y>.([(x, y)] \<bullet> P)
[PROOF STEP]
by(simp add: alphaInput)
[PROOF STATE]
proof (state)
this:
a<x>.P = a<y>.([(x, y)] \<bullet> P)

goal (1 subgoal):
 1. summands (a<x>.P) = {a<x>.P}
[PROOF STEP]
with yineqa
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> a
a<x>.P = a<y>.([(x, y)] \<bullet> P)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<noteq> a
a<x>.P = a<y>.([(x, y)] \<bullet> P)

goal (1 subgoal):
 1. summands (a<x>.P) = {a<x>.P}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
summands (a<x>.P) = {a<x>.P}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finiteSummands:
  fixes P :: pi

  shows "finite(summands P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (summands P)
[PROOF STEP]
by(induct P rule: pi.induct) auto