Theory PAC_Polynomials_Operations

```theory PAC_Polynomials_Operations
imports PAC_Polynomials_Term PAC_Checker_Specification
begin

text ‹In this section, we refine the polynomials to list. These lists will be used in our checker
to represent the polynomials and execute operations.

There is one ∗‹key› difference between the list representation and the usual representation: in the
former, coefficients can be zero and monomials can appear several times. This makes it easier to
reason on intermediate representation where this has not yet been sanitized.
›

fun add_poly_l' :: ‹llist_polynomial × llist_polynomial ⇒ llist_polynomial› where
‹add_poly_l' (p, []) = p› |
‹add_poly_l' ([], q) = q› |
‹add_poly_l' ((xs, n) # p, (ys, m) # q) =
(if xs = ys then if n + m = 0 then add_poly_l' (p, q) else
let pq = add_poly_l' (p, q) in
((xs, n + m) # pq)
else if (xs, ys) ∈ term_order_rel
then
let pq = add_poly_l' (p, (ys, m) # q) in
((xs, n) # pq)
else
let pq = add_poly_l' ((xs, n) # p, q) in
((ys, m) # pq)
)›

definition add_poly_l :: ‹llist_polynomial × llist_polynomial ⇒ llist_polynomial nres› where
case (p,q) of
(p, []) ⇒ RETURN p
| ([], q) ⇒ RETURN q
| ((xs, n) # p, (ys, m) # q) ⇒
(if xs = ys then if n + m = 0 then add_poly_l (p, q) else
do {
RETURN ((xs, n + m) # pq)
}
else if (xs, ys) ∈ term_order_rel
then do {
pq ← add_poly_l (p, (ys, m) # q);
RETURN ((xs, n) # pq)
}
else do {
pq ← add_poly_l ((xs, n) # p, q);
RETURN ((ys, m) # pq)
}))›

definition nonzero_coeffs where
‹nonzero_coeffs a ⟷ 0 ∉# snd `# a›

lemma nonzero_coeffs_simps[simp]:
‹nonzero_coeffs {#}›
‹nonzero_coeffs (add_mset (xs, n) a) ⟷ nonzero_coeffs a ∧ n ≠ 0›
by (auto simp: nonzero_coeffs_def)

lemma nonzero_coeffsD:
‹nonzero_coeffs a ⟹ (x, n) ∈# a ⟹ n ≠ 0›
by (auto simp: nonzero_coeffs_def)

lemma sorted_poly_list_rel_ConsD:
‹((ys, n) # p, a) ∈ sorted_poly_list_rel S ⟹ (p, remove1_mset (mset ys, n) a) ∈ sorted_poly_list_rel S ∧
(mset ys, n) ∈# a ∧ (∀x ∈ set p. S ys (fst x)) ∧ sorted_wrt (rel2p var_order_rel) ys ∧
distinct ys ∧ ys ∉ set (map fst p) ∧ n ≠ 0 ∧ nonzero_coeffs a›
unfolding sorted_poly_list_rel_wrt_def prod.case mem_Collect_eq
list_rel_def
apply (clarsimp)
apply (subst (asm) list.rel_sel)
apply (intro conjI)
apply (rename_tac y, rule_tac b = ‹tl y› in relcompI)
apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def
list.tl_def term_poly_list_rel_def nonzero_coeffs_def split: list.splits)
done

lemma sorted_poly_list_rel_Cons_iff:
‹((ys, n) # p, a) ∈ sorted_poly_list_rel S ⟷ (p, remove1_mset (mset ys, n) a) ∈ sorted_poly_list_rel S ∧
(mset ys, n) ∈# a ∧ (∀x ∈ set p. S ys (fst x)) ∧ sorted_wrt (rel2p var_order_rel) ys ∧
distinct ys ∧ ys ∉ set (map fst p) ∧ n ≠ 0 ∧ nonzero_coeffs a›
apply (rule iffI)
subgoal
by (auto dest!: sorted_poly_list_rel_ConsD)
subgoal
unfolding sorted_poly_list_rel_wrt_def prod.case mem_Collect_eq
list_rel_def
apply (clarsimp)
apply (intro conjI)
apply (rename_tac y; rule_tac b = ‹(mset ys, n) # y› in relcompI)
by (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def
nonzero_coeffs_def
dest!: multi_member_split)
done

lemma sorted_repeat_poly_list_rel_ConsD:
‹((ys, n) # p, a) ∈ sorted_repeat_poly_list_rel S ⟹ (p, remove1_mset (mset ys, n) a) ∈ sorted_repeat_poly_list_rel S ∧
(mset ys, n) ∈# a ∧ (∀x ∈ set p. S ys (fst x)) ∧ sorted_wrt (rel2p var_order_rel) ys ∧
distinct ys ∧ n ≠ 0 ∧ nonzero_coeffs a›
unfolding sorted_repeat_poly_list_rel_wrt_def prod.case mem_Collect_eq
list_rel_def
apply (clarsimp)
apply (subst (asm) list.rel_sel)
apply (intro conjI)
apply (rename_tac y, rule_tac b = ‹tl y› in relcompI)
apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def
list.tl_def term_poly_list_rel_def nonzero_coeffs_def split: list.splits)
done

lemma sorted_repeat_poly_list_rel_Cons_iff:
‹((ys, n) # p, a) ∈ sorted_repeat_poly_list_rel S ⟷ (p, remove1_mset (mset ys, n) a) ∈ sorted_repeat_poly_list_rel S ∧
(mset ys, n) ∈# a ∧ (∀x ∈ set p. S ys (fst x)) ∧ sorted_wrt (rel2p var_order_rel) ys ∧
distinct ys ∧ n ≠ 0 ∧ nonzero_coeffs a›
apply (rule iffI)
subgoal
by (auto dest!: sorted_repeat_poly_list_rel_ConsD)
subgoal
unfolding sorted_repeat_poly_list_rel_wrt_def prod.case mem_Collect_eq
list_rel_def
apply (clarsimp)
apply (intro conjI)
apply (rename_tac y, rule_tac b = ‹(mset ys, n) # y› in relcompI)
by (auto simp: sorted_repeat_poly_list_rel_wrt_def list_mset_rel_def br_def
nonzero_coeffs_def
dest!: multi_member_split)
done

‹n + m = 0 ⟹add_poly_p⇧*⇧* (A, Aa, {#}) ({#}, {#}, r) ⟹
({#}, {#}, r)›
apply (rule converse_rtranclp_into_rtranclp)
apply (rule converse_rtranclp_into_rtranclp)
apply (rule converse_rtranclp_into_rtranclp)
done

‹(aa, ba) ∈ set (add_poly_l' x) ⟹ aa ∈ fst ` set (fst x) ∨ aa ∈ fst ` set (snd x)›
(auto split: if_splits)

‹add_poly_p⇧*⇧* (A, B, r) (A', B', r') ⟹
(A, B, p + r) (A', B', p + r')›
apply (induction rule: rtranclp_induct[of add_poly_p ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
subgoal by auto

‹add_poly_p⇧*⇧* (A, Aa, {#}) ({#}, {#}, r) ⟹
(add_mset (xs, n) A, Aa, {#})
({#}, {#}, add_mset (xs, n) r)›
apply (rule converse_rtranclp_into_rtranclp)
by auto

‹add_poly_p⇧*⇧* (A, Aa, {#}) ({#}, {#}, r) ⟹
({#}, {#}, add_mset (ys, n + m) r)›
apply (rule converse_rtranclp_into_rtranclp)
apply (rule converse_rtranclp_into_rtranclp)
by auto

‹add_poly_p⇧*⇧* (A, Aa, {#}) ({#}, {#}, r) ⟹
(A, add_mset (ys, m) Aa, {#})
({#}, {#}, add_mset (ys, m) r)›
apply (rule converse_rtranclp_into_rtranclp)
by auto

lemma total_on_lexord:
‹Relation.total_on UNIV R ⟹ Relation.total_on UNIV (lexord R)›
apply (auto simp: Relation.total_on_def)
by (meson lexord_linear)

lemma antisym_lexord:
‹antisym R ⟹ irrefl R ⟹ antisym (lexord R)›
by (auto simp: antisym_def lexord_def irrefl_def
elim!: list_match_lel_lel)

lemma less_than_char_linear:
‹(a, b) ∈ less_than_char ∨
a = b ∨ (b, a) ∈ less_than_char›
by (auto simp: less_than_char_def)

lemma total_on_lexord_less_than_char_linear:
‹xs ≠ ys ⟹ (xs, ys) ∉ lexord (lexord less_than_char) ⟷
(ys, xs) ∈ lexord (lexord less_than_char)›
using lexord_linear[of ‹lexord less_than_char› xs ys]
using lexord_linear[of ‹less_than_char›] less_than_char_linear
using lexord_irrefl[OF irrefl_less_than_char]
antisym_lexord[OF antisym_lexord[OF antisym_less_than_char irrefl_less_than_char]]
apply (auto simp: antisym_def Relation.total_on_def)
done

lemma sorted_poly_list_rel_nonzeroD:
‹(p, r) ∈ sorted_poly_list_rel term_order ⟹
nonzero_coeffs (r)›
‹(p, r) ∈ sorted_poly_list_rel (rel2p (lexord (lexord less_than_char))) ⟹
nonzero_coeffs (r)›
by (auto simp: sorted_poly_list_rel_wrt_def nonzero_coeffs_def)

assumes ‹(pq, pq') ∈ sorted_poly_rel ×⇩r sorted_poly_rel›
shows ‹∃r. (add_poly_l' pq, r) ∈ sorted_poly_rel ∧
add_poly_p⇧*⇧* (fst pq', snd pq', {#}) ({#}, {#}, r)›
supply [[goals_limit=1]]
using assms
apply (induction ‹pq› arbitrary: pq' rule: add_poly_l'.induct)
subgoal for p pq'
using add_poly_p_empty_l[of ‹fst pq'› ‹{#}› ‹{#}›]
by (cases pq') (auto intro!: exI[of _ ‹fst pq'›])
subgoal for x p pq'
using add_poly_p_empty_r[of  ‹{#}› ‹snd pq'› ‹{#}›]
by (cases pq')  (auto intro!: exI[of _ ‹snd pq'›])
subgoal premises p for xs n p ys m q pq'
apply (cases pq') ― ‹Isabelle does a completely stupid case distinction here›
apply (cases ‹xs = ys›)
subgoal
apply (cases ‹n + m = 0›)
subgoal
using p(1)[of ‹(remove1_mset (mset xs, n) (fst pq'), remove1_mset (mset ys, m)  (snd pq'))›] p(5-)
apply (auto dest!: sorted_poly_list_rel_ConsD multi_member_split
)
subgoal
using p(2)[of ‹(remove1_mset (mset xs, n) (fst pq'), remove1_mset (mset ys, m)  (snd pq'))›] p(5-)
apply (auto dest!: sorted_poly_list_rel_ConsD multi_member_split)
apply (rule_tac x = ‹add_mset (mset ys, n + m) r› in exI)
apply (fastforce dest!: monoms_add_poly_l'D simp: sorted_poly_list_rel_Cons_iff rel2p_def
sorted_poly_list_rel_nonzeroD var_order_rel_def
done
done
subgoal
apply (cases ‹(xs, ys) ∈ term_order_rel›)
subgoal
using p(3)[of ‹(remove1_mset (mset xs, n) (fst pq'), (snd pq'))›] p(5-)
apply (auto dest!: multi_member_split simp: sorted_poly_list_rel_Cons_iff rel2p_def)
apply (rule_tac x = ‹add_mset (mset xs, n) r› in exI)
apply (rule lexord_trans)
apply assumption
sorted_poly_list_rel_nonzeroD var_order_rel_def)
using total_on_lexord_less_than_char_linear by fastforce

subgoal
using p(4)[of ‹(fst pq', remove1_mset (mset ys, m) (snd pq'))›] p(5-)
apply (auto dest!: multi_member_split simp: sorted_poly_list_rel_Cons_iff rel2p_def
var_order_rel_def)
apply (rule_tac x = ‹add_mset (mset ys, m) r› in exI)
simp: total_on_lexord_less_than_char_linear)
total_on_lexord_less_than_char_linear var_order_rel_def)
apply (rule lexord_trans)
apply assumption
sorted_poly_list_rel_nonzeroD var_order_rel_def)
using total_on_lexord_less_than_char_linear by fastforce
done
done
done

(solves ‹subst RECT_unfold, refine_mono, simp split: list.split›)+

‹(add_poly_l, uncurry (λp q. SPEC(λr. add_poly_p⇧*⇧* (p, q, {#}) ({#}, {#}, r)))) ∈
sorted_poly_rel ×⇩r sorted_poly_rel →⇩f ⟨sorted_poly_rel⟩nres_rel›
apply (intro nres_relI frefI)
apply (auto simp: conc_fun_RES)
done

definition sort_poly_spec :: ‹llist_polynomial ⇒ llist_polynomial nres› where
‹sort_poly_spec p =
SPEC(λp'. mset p = mset p' ∧ sorted_wrt (rel2p (Id ∪ term_order_rel)) (map fst p'))›

lemma sort_poly_spec_id:
assumes ‹(p, p') ∈ unsorted_poly_rel›
shows ‹sort_poly_spec p ≤ ⇓ (sorted_repeat_poly_rel) (RETURN p')›
proof -
obtain y where
py: ‹(p, y) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel› and
p'_y: ‹p' = mset y› and
zero: ‹0 ∉# snd `# p'›
using assms
unfolding sort_poly_spec_def poly_list_rel_def sorted_poly_list_rel_wrt_def
by (auto simp: list_mset_rel_def br_def)
then have [simp]: ‹length y = length p›
by (auto simp: list_rel_def list_all2_conv_all_nth)
have H: ‹(x, p')
∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel O list_mset_rel›
if px: ‹mset p = mset x› and ‹sorted_wrt (rel2p (Id ∪ lexord var_order_rel)) (map fst x)›
for x :: ‹llist_polynomial›
proof -
from px have ‹length x = length p›
by (metis size_mset)
from px have ‹mset x = mset p›
by simp
then obtain f where ‹f permutes {..<length p}› ‹permute_list f p = x›
by (rule mset_eq_permutation)
with ‹length x = length p› have f: ‹bij_betw f {..<length x} {..<length p}›
from ‹f permutes {..<length p}› ‹permute_list f p = x› [symmetric]
have [simp]: ‹⋀i. i < length x ⟹ x ! i = p ! (f i)›
let ?y = ‹map (λi. y ! f i) [0 ..< length x]›
have ‹i < length y ⟹ (p ! f i, y ! f i) ∈ term_poly_list_rel ×⇩r int_rel› for i
using list_all2_nthD[of _ p y
‹f i›, OF py[unfolded list_rel_def mem_Collect_eq prod.case]]
mset_eq_length[OF px] f
by (auto simp: list_rel_def list_all2_conv_all_nth bij_betw_def)
then have ‹(x, ?y) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel› and
xy: ‹length x = length y›
using py list_all2_nthD[of ‹rel2p (term_poly_list_rel ×⇩r int_rel)› p y
‹f i› for i, simplified] mset_eq_length[OF px]
by (auto simp: list_rel_def list_all2_conv_all_nth)
moreover {
have f: ‹mset_set {0..<length x} = f `# mset_set {0..<length x}›
using f mset_eq_length[OF px]
by (auto simp: bij_betw_def lessThan_atLeast0 image_mset_mset_set)
have ‹mset y = {#y ! f x. x ∈# mset_set {0..<length x}#}›
by (subst drop_0[symmetric], subst mset_drop_upto, subst xy[symmetric], subst f)
auto
then have ‹(?y, p') ∈ list_mset_rel›
by (auto simp: list_mset_rel_def br_def p'_y)
}
ultimately show ?thesis
by (auto intro!: relcompI[of _ ?y])
qed
show ?thesis
using zero
unfolding sort_poly_spec_def poly_list_rel_def sorted_repeat_poly_list_rel_wrt_def
by refine_rcg (auto intro: H)
qed

subsection ‹Multiplication›

fun mult_monoms :: ‹term_poly_list ⇒ term_poly_list ⇒ term_poly_list› where
‹mult_monoms p [] = p› |
‹mult_monoms [] p = p› |
‹mult_monoms (x # p) (y # q) =
(if x = y then x # mult_monoms p q
else if (x, y) ∈ var_order_rel then x # mult_monoms p (y # q)
else y # mult_monoms (x # p) q)›

lemma term_poly_list_rel_empty_iff[simp]:
‹([], q') ∈ term_poly_list_rel ⟷ q' = {#}›
by (auto simp: term_poly_list_rel_def)

lemma mset_eqD_set_mset: ‹mset xs = A ⟹ set xs = set_mset A›
by auto

lemma term_poly_list_rel_Cons_iff:
‹(y # p, p') ∈ term_poly_list_rel ⟷
(p, remove1_mset y p') ∈ term_poly_list_rel ∧
y ∈# p' ∧ y ∉ set p ∧ y ∉# remove1_mset y p' ∧
(∀x∈#mset p. (y, x) ∈ var_order_rel)›
by (auto simp: term_poly_list_rel_def rel2p_def dest!: multi_member_split mset_eqD_set_mset)

lemma var_order_rel_antisym[simp]:
‹(y, y) ∉ var_order_rel›
by (simp add: less_than_char_def lexord_irreflexive var_order_rel_def)

lemma term_poly_list_rel_remdups_mset:
‹(p, p') ∈ term_poly_list_rel ⟹
(p, remdups_mset p') ∈ term_poly_list_rel›
by (auto simp: term_poly_list_rel_def distinct_mset_remdups_mset_id simp flip: distinct_mset_mset_distinct)

lemma var_notin_notin_mult_monomsD:
‹y ∈ set (mult_monoms p q) ⟹ y ∈ set p ∨ y ∈ set q›
by (induction p q arbitrary: p' q' rule: mult_monoms.induct) (auto split: if_splits)

lemma term_poly_list_rel_set_mset:
‹(p, q) ∈ term_poly_list_rel ⟹ set p = set_mset q›
by (auto simp: term_poly_list_rel_def)

lemma mult_monoms_spec:
‹(mult_monoms, (λa b. remdups_mset (a + b))) ∈ term_poly_list_rel → term_poly_list_rel → term_poly_list_rel›
proof -
have [dest]: ‹remdups_mset (A + Aa) = add_mset y Ab ⟹ y ∉# A ⟹
y ∉# Aa ⟹
False› for Aa Ab y A
by (metis set_mset_remdups_mset union_iff union_single_eq_member)
show ?thesis
apply (intro fun_relI)
apply (rename_tac p p' q q')
subgoal for p p' q q'
apply (induction p q arbitrary: p' q' rule: mult_monoms.induct)
subgoal by (auto simp: term_poly_list_rel_Cons_iff rel2p_def term_poly_list_rel_remdups_mset)
subgoal for x p p' q'
by (auto simp: term_poly_list_rel_Cons_iff rel2p_def term_poly_list_rel_remdups_mset
dest!: multi_member_split[of _ q'])
subgoal premises p for x p y q p' q'
apply (cases ‹x = y›)
subgoal
using p(1)[of ‹remove1_mset y p'› ‹remove1_mset y q'›] p(4-)
by (auto simp: term_poly_list_rel_Cons_iff rel2p_def
dest!: var_notin_notin_mult_monomsD
dest!: multi_member_split)
apply (cases ‹(x, y) ∈ var_order_rel›)
subgoal
using p(2)[of ‹remove1_mset x p'› ‹q'›] p(4-)
apply (auto simp: term_poly_list_rel_Cons_iff
term_poly_list_rel_set_mset rel2p_def var_order_rel_def
dest!: multi_member_split[of _ p'] multi_member_split[of _ q']
var_notin_notin_mult_monomsD
split: if_splits)
apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear)
apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear)
apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear)
using lexord_trans trans_less_than_char var_order_rel_antisym
unfolding var_order_rel_def apply blast+
done
subgoal
using p(3)[of ‹p'› ‹remove1_mset y q'›] p(4-)
apply (auto simp: term_poly_list_rel_Cons_iff rel2p_def
term_poly_list_rel_set_mset rel2p_def var_order_rel_antisym
dest!: multi_member_split[of _ p'] multi_member_split[of _ q']
var_notin_notin_mult_monomsD
split: if_splits)
using lexord_trans trans_less_than_char var_order_rel_antisym
unfolding var_order_rel_def apply blast
apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear)
by (meson less_than_char_linear lexord_linear lexord_trans trans_less_than_char)
done
done
done
qed

definition mult_monomials :: ‹term_poly_list × int ⇒ term_poly_list × int ⇒ term_poly_list × int› where
‹mult_monomials = (λ(x, a) (y, b). (mult_monoms x y, a * b))›

definition mult_poly_raw :: ‹llist_polynomial ⇒ llist_polynomial ⇒ llist_polynomial› where
‹mult_poly_raw p q = foldl (λb x. map (mult_monomials x) q @ b) [] p›

fun map_append where
‹map_append f b [] = b› |
‹map_append f b (x # xs) = f x # map_append f b xs›

lemma map_append_alt_def:
‹map_append f b xs = map f xs @ b›
by (induction f b xs rule: map_append.induct)
auto

lemma foldl_append_empty:
‹NO_MATCH [] xs ⟹ foldl (λb x. f x @ b) xs p = foldl (λb x. f x @ b) [] p @ xs›
apply (induction p arbitrary: xs)
apply simp
by (metis (mono_tags, lifting) NO_MATCH_def append.assoc append_self_conv foldl_Cons)

lemma poly_list_rel_empty_iff[simp]:
‹([], r) ∈ poly_list_rel R ⟷ r = {#}›
by (auto simp: poly_list_rel_def list_mset_rel_def br_def)

lemma mult_poly_raw_simp[simp]:
‹mult_poly_raw [] q = []›
‹mult_poly_raw (x # p) q = mult_poly_raw p q @ map (mult_monomials x) q›
subgoal by (auto simp: mult_poly_raw_def)
subgoal by (induction p) (auto simp: mult_poly_raw_def foldl_append_empty)
done

lemma sorted_poly_list_relD:
‹(q, q') ∈ sorted_poly_list_rel R ⟹ q' = (λ(a, b). (mset a, b)) `# mset q›
apply (induction q arbitrary: q')
apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def
list_rel_split_right_iff)
apply (subst (asm)(2) term_poly_list_rel_def)
done

lemma list_all2_in_set_ExD:
‹list_all2 R p q ⟹ x ∈ set p ⟹ ∃y ∈ set q. R x y›
by (induction p q rule: list_all2_induct)
auto

inductive_cases mult_poly_p_elim: ‹mult_poly_p q (A, r) (B, r')›

‹(mult_poly_p q')⇧*⇧* (A, r) (B, r') ⟹ (mult_poly_p q')⇧*⇧* (add_mset x A, r) (add_mset x B, r')›
apply (induction rule: rtranclp_induct[of ‹mult_poly_p q'› ‹(_, r)› ‹(p', q'')› for p' q'', split_format(complete)])
subgoal by simp
apply (rule rtranclp.rtrancl_into_rtrancl)
apply assumption
by (auto elim!: mult_poly_p_elim intro: mult_poly_p.intros

lemma mult_poly_raw_mult_poly_p:
assumes ‹(p, p') ∈ sorted_poly_rel› and ‹(q, q') ∈ sorted_poly_rel›
shows ‹∃r. (mult_poly_raw p q, r) ∈ unsorted_poly_rel ∧ (mult_poly_p q')⇧*⇧* (p', {#}) ({#}, r)›
proof -
have H: ‹(q, q') ∈ sorted_poly_list_rel term_order ⟹ n < length q ⟹
distinct aa ⟹ sorted_wrt var_order aa ⟹
(mult_monoms aa (fst (q ! n)),
mset (mult_monoms aa (fst (q ! n))))
∈ term_poly_list_rel› for aa n
using mult_monoms_spec[unfolded fun_rel_def, simplified] apply -
apply (drule bspec[of _ _ ‹(aa, (mset aa))›])
apply (auto simp: term_poly_list_rel_def)[]
unfolding prod.case sorted_poly_list_rel_wrt_def
apply clarsimp
subgoal for y
apply (drule bspec[of _ _ ‹(fst (q ! n), mset (fst (q ! n)))›])
apply (cases ‹q ! n›; cases ‹y ! n›)
using param_nth[of n y n q ‹term_poly_list_rel ×⇩r int_rel›]
by (auto simp: list_rel_imp_same_length term_poly_list_rel_def)
done

have H': ‹(q, q') ∈ sorted_poly_list_rel term_order ⟹
distinct aa ⟹ sorted_wrt var_order aa ⟹
(ab, ba) ∈ set q ⟹
remdups_mset (mset aa + mset ab) = mset (mult_monoms aa ab)› for aa n ab ba
using mult_monoms_spec[unfolded fun_rel_def, simplified] apply -
apply (drule bspec[of _ _ ‹(aa, (mset aa))›])
apply (auto simp: term_poly_list_rel_def)[]
unfolding prod.case sorted_poly_list_rel_wrt_def
apply clarsimp
subgoal for y
apply (drule bspec[of _ _ ‹(ab, mset ab)›])
apply (auto simp: list_rel_imp_same_length term_poly_list_rel_def list_rel_def
dest: list_all2_in_set_ExD)
done
done

have  H: ‹(q, q') ∈ sorted_poly_list_rel term_order ⟹
a = (aa, b) ⟹
(pq, r) ∈ unsorted_poly_rel ⟹
p' = add_mset (mset aa, b) A ⟹
∀x∈set p. term_order aa (fst x) ⟹
sorted_wrt var_order aa ⟹
distinct aa ⟹ b≠ 0 ⟹
(⋀aaa. (aaa, 0) ∉# q') ⟹
(pq @
map (mult_monomials (aa, b)) q,
{#case x of (ys, n) ⇒ (remdups_mset (mset aa + ys), n * b)
. x ∈# q'#} +
r)
∈ unsorted_poly_rel› for a p p' pq aa b r
apply (auto simp: poly_list_rel_def)
apply (rule_tac b = ‹y @ map (λ(a,b). (mset a, b)) (map (mult_monomials (aa, b)) q)› in relcompI)
apply (auto simp: list_rel_def list_all2_append list_all2_lengthD H
list_mset_rel_def br_def mult_monomials_def case_prod_beta intro!: list_all2_all_nthI
simp: sorted_poly_list_relD)
apply (subst sorted_poly_list_relD[of q q' term_order])
apply (auto simp: case_prod_beta H' intro!: image_mset_cong)
done

show ?thesis
using assms
apply (induction p arbitrary: p')
subgoal
by auto
subgoal premises p for a p p'
using p(1)[of ‹remove1_mset (mset (fst a), snd a) p'›] p(2-)
apply (cases a)
apply (auto simp: sorted_poly_list_rel_Cons_iff
dest!: multi_member_split)
apply (rule_tac x = ‹(λ(ys, n). (remdups_mset (mset (fst a) + ys), n * snd a)) `# q' + r› in exI)
apply (auto 5 3 intro: mult_poly_p.intros simp: intro!: H
dest: sorted_poly_list_rel_nonzeroD nonzero_coeffsD)
apply (rule rtranclp_trans)
apply assumption
apply (rule converse_rtranclp_into_rtranclp)
apply (auto intro!: mult_poly_p.intros simp: ac_simps)
done
done
qed

fun merge_coeffs :: ‹llist_polynomial ⇒ llist_polynomial› where
‹merge_coeffs [] = []› |
‹merge_coeffs [(xs, n)] = [(xs, n)]› |
‹merge_coeffs ((xs, n) # (ys, m) # p) =
(if xs = ys
then if n + m ≠ 0 then merge_coeffs ((xs, n + m) # p) else merge_coeffs p
else (xs, n) # merge_coeffs ((ys, m) # p))›

abbreviation  (in -)mononoms :: ‹llist_polynomial ⇒ term_poly_list set› where
‹mononoms p ≡ fst `set p›

lemma fst_normalize_polynomial_subset:
‹mononoms (merge_coeffs p) ⊆ mononoms p›
by (induction p rule: merge_coeffs.induct)  auto

lemma fst_normalize_polynomial_subsetD:
‹(a, b) ∈ set (merge_coeffs p) ⟹ a ∈ mononoms p›
apply (induction p rule: merge_coeffs.induct)
subgoal
by auto
subgoal
by auto
subgoal
by (auto split: if_splits)
done

lemma distinct_merge_coeffs:
assumes ‹sorted_wrt R (map fst xs)› and ‹transp R› ‹antisymp R›
shows ‹distinct (map fst (merge_coeffs xs))›
using assms
by (induction xs rule: merge_coeffs.induct)
(auto 5 4 dest: antisympD dest!: fst_normalize_polynomial_subsetD)

lemma in_set_merge_coeffsD:
‹(a, b) ∈ set (merge_coeffs p) ⟹∃b. (a, b) ∈ set p›
by  (auto dest!: fst_normalize_polynomial_subsetD)

by (induction rule: rtranclp_induct)
(auto dest: normalize_poly_p.keep_coeff[of _ _ x])

lemma nonzero_coeffs_diff:
‹nonzero_coeffs A ⟹ nonzero_coeffs (A - B)›
by (auto simp: nonzero_coeffs_def dest: in_diffD)

lemma merge_coeffs_is_normalize_poly_p:
‹(xs, ys) ∈ sorted_repeat_poly_rel ⟹ ∃r. (merge_coeffs xs, r) ∈ sorted_poly_rel ∧ normalize_poly_p⇧*⇧* ys r›
apply (induction xs arbitrary: ys rule: merge_coeffs.induct)
subgoal by (auto simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def)
subgoal
by (auto simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def)
subgoal premises p for xs n ys m p ysa
apply (cases ‹xs = ys›, cases ‹m+n ≠ 0›)
subgoal
using p(1)[of ‹add_mset (mset ys, m+n) ysa - {#(mset ys, m), (mset ys, n)#}›] p(4-)
apply (auto simp: sorted_poly_list_rel_Cons_iff ac_simps add_mset_commute
apply (rule_tac x = ‹r› in exI)
using normalize_poly_p.merge_dup_coeff[of ‹ysa -  {#(mset ys, m), (mset ys, n)#}› ‹ysa -  {#(mset ys, m), (mset ys, n)#}› ‹mset ys› m n]
by (auto dest!: multi_member_split simp del: normalize_poly_p.merge_dup_coeff
intro: converse_rtranclp_into_rtranclp)
subgoal
using p(2)[of ‹ysa - {#(mset ys, m), (mset ys, n)#}›] p(4-)
apply (auto simp: sorted_poly_list_rel_Cons_iff ac_simps add_mset_commute
apply (rule_tac x = ‹r› in exI)
using normalize_poly_p.rem_0_coeff[of ‹add_mset (mset ys, m +n) ysa -  {#(mset ys, m), (mset ys, n)#}› ‹add_mset (mset ys, m +n) ysa -  {#(mset ys, m), (mset ys, n)#}› ‹mset ys›]
using normalize_poly_p.merge_dup_coeff[of ‹ysa -  {#(mset ys, m), (mset ys, n)#}› ‹ysa -  {#(mset ys, m), (mset ys, n)#}› ‹mset ys› m n]
by (force intro: add_mset_commute[of ‹(mset ys, n)› ‹(mset ys, -n)›]
converse_rtranclp_into_rtranclp
dest!: multi_member_split
simp del: normalize_poly_p.rem_0_coeff
intro: normalize_poly_p.rem_0_coeff)
subgoal
using p(3)[of ‹add_mset (mset ys, m) ysa - {#(mset xs, n), (mset ys, m)#}›] p(4-)
apply (auto simp: sorted_poly_list_rel_Cons_iff ac_simps add_mset_commute
apply (rule_tac x = ‹add_mset (mset xs, n) r› in exI)
apply (auto dest!: in_set_merge_coeffsD)
simp: rel2p_def var_order_rel_def
dest!: multi_member_split
dest: sorted_poly_list_rel_nonzeroD)
using total_on_lexord_less_than_char_linear apply fastforce
using total_on_lexord_less_than_char_linear apply fastforce
done
done
done

subsection ‹Normalisation›

definition normalize_poly where
‹normalize_poly p = do {
p ← sort_poly_spec p;
RETURN (merge_coeffs p)
}›
definition sort_coeff :: ‹string list ⇒ string list nres› where
‹sort_coeff ys = SPEC(λxs. mset xs = mset ys ∧ sorted_wrt (rel2p (Id ∪ var_order_rel)) xs)›

lemma distinct_var_order_Id_var_order:
‹distinct a ⟹ sorted_wrt (rel2p (Id ∪ var_order_rel)) a ⟹
sorted_wrt var_order a›
by (induction a) (auto simp: rel2p_def)

definition sort_all_coeffs :: ‹llist_polynomial ⇒ llist_polynomial nres› where
‹sort_all_coeffs xs = monadic_nfoldli xs (λ_. RETURN True) (λ(a, n) b. do {a ← sort_coeff a; RETURN ((a, n) # b)}) []›

lemma sort_all_coeffs_gen:
assumes ‹(∀xs ∈ mononoms xs'. sorted_wrt (rel2p (var_order_rel)) xs)› and
‹∀x ∈ mononoms (xs @ xs'). distinct x›
shows ‹monadic_nfoldli xs (λ_. RETURN True) (λ(a, n) b. do {a ← sort_coeff a; RETURN ((a, n) # b)}) xs' ≤
⇓Id (SPEC(λys. map (λ(a,b). (mset a, b)) (rev xs @ xs') = map (λ(a,b). (mset a, b)) (ys) ∧
(∀xs ∈ mononoms ys. sorted_wrt (rel2p (var_order_rel)) xs)))›
proof -
have H: ‹
∀x∈set xs'. sorted_wrt var_order (fst x) ⟹
sorted_wrt (rel2p (Id ∪ var_order_rel)) x ⟹
(aaa, ba) ∈ set xs' ⟹
sorted_wrt (rel2p (Id ∪ var_order_rel)) aaa› for xs  xs' ba aa b x aaa
by (metis UnCI fst_eqD rel2p_def sorted_wrt_mono_rel)
show ?thesis
using assms
unfolding sort_all_coeffs_def sort_coeff_def
apply (induction xs arbitrary: xs')
subgoal
using assms
by auto
subgoal premises p for a xs
using p(2-)
intro_spec_refine_iff prod.case)
by (auto 5 3 simp: intro_spec_refine_iff image_Un
dest: same_mset_distinct_iff
intro!: p(1)[THEN order_trans] distinct_var_order_Id_var_order
simp: H)
done
qed

definition shuffle_coefficients where
‹shuffle_coefficients xs = (SPEC(λys. map (λ(a,b). (mset a, b)) (rev xs) = map (λ(a,b). (mset a, b)) ys ∧
(∀xs ∈ mononoms ys. sorted_wrt (rel2p (var_order_rel)) xs)))›

lemma sort_all_coeffs:
‹∀x ∈ mononoms xs. distinct x ⟹
sort_all_coeffs xs ≤ ⇓ Id (shuffle_coefficients xs)›
unfolding sort_all_coeffs_def shuffle_coefficients_def
by (rule sort_all_coeffs_gen[THEN order_trans])
auto

lemma unsorted_term_poly_list_rel_mset:
‹(ys, aa) ∈ unsorted_term_poly_list_rel ⟹ mset ys = aa›
by (auto simp: unsorted_term_poly_list_rel_def)

lemma RETURN_map_alt_def:
‹RETURN o (map f) =
REC⇩T (λg xs.
case xs of
[] ⇒ RETURN []
| x # xs ⇒ do {xs ← g xs; RETURN (f x # xs)})›
unfolding comp_def
apply (subst eq_commute)
apply (intro ext)
apply (induct_tac x)
subgoal
apply (subst RECT_unfold)
apply refine_mono
apply auto
done
subgoal
apply (subst RECT_unfold)
apply refine_mono
apply auto
done
done

lemma fully_unsorted_poly_rel_Cons_iff:
‹((ys, n) # p, a) ∈ fully_unsorted_poly_rel ⟷
(p, remove1_mset (mset ys, n) a) ∈ fully_unsorted_poly_rel ∧
(mset ys, n) ∈# a ∧ distinct ys›
apply (auto simp: poly_list_rel_def list_rel_split_right_iff list_mset_rel_def br_def
unsorted_term_poly_list_rel_def
nonzero_coeffs_def fully_unsorted_poly_list_rel_def dest!: multi_member_split)
apply blast
apply (rule_tac b = ‹(mset ys, n) # y› in relcompI)
apply auto
done

lemma map_mset_unsorted_term_poly_list_rel:
‹(⋀a. a ∈ mononoms s ⟹ distinct a) ⟹ ∀x ∈ mononoms s. distinct x ⟹
(∀xs ∈ mononoms s. sorted_wrt (rel2p (Id ∪ var_order_rel)) xs) ⟹
(s, map (λ(a, y). (mset a, y)) s)
∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel›
by (induction s) (auto simp: term_poly_list_rel_def
distinct_var_order_Id_var_order)

lemma list_rel_unsorted_term_poly_list_relD:
‹(p, y) ∈ ⟨unsorted_term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
mset y = (λ(a, y). (mset a, y)) `# mset p ∧ (∀x ∈ mononoms p. distinct x)›
by (induction p arbitrary: y)
(auto simp: list_rel_split_right_iff
unsorted_term_poly_list_rel_def)

lemma shuffle_terms_distinct_iff:
assumes ‹map (λ(a, y). (mset a, y)) p = map (λ(a, y). (mset a, y)) s›
shows ‹(∀x∈set p. distinct (fst x)) ⟷ (∀x∈set s. distinct (fst x))›
proof -
have  ‹∀x∈set s. distinct (fst x)›
if m:  ‹map (λ(a, y). (mset a, y)) p = map (λ(a, y). (mset a, y)) s› and
dist: ‹∀x∈set p. distinct (fst x)›
for s p
proof standard+
fix x
assume x: ‹x ∈ set s›
obtain v n where [simp]: ‹x = (v, n)› by (cases x)
then have ‹(mset v, n) ∈ set (map (λ(a, y). (mset a, y)) p)›
using x unfolding m by auto
then obtain v' where
‹(v', n) ∈ set p› and
‹mset v' = mset v›
by (auto simp: image_iff)
then show ‹distinct (fst x)›
using dist by (metis ‹x = (v, n)› distinct_mset_mset_distinct fst_conv)
qed
from this[of p s] this[of s p]
show ‹?thesis›
unfolding assms
by blast
qed

lemma
‹(p, y) ∈ ⟨unsorted_term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
(a, b) ∈ set p ⟹  distinct a›
using list_rel_unsorted_term_poly_list_relD by fastforce

lemma sort_all_coeffs_unsorted_poly_rel_with0:
assumes ‹(p, p') ∈ fully_unsorted_poly_rel›
shows ‹sort_all_coeffs p ≤ ⇓ (unsorted_poly_rel_with0) (RETURN p')›
proof -
have H: ‹(map (λ(a, y). (mset a, y)) (rev p)) =
map (λ(a, y). (mset a, y)) s ⟷
(map (λ(a, y). (mset a, y)) p) =
map (λ(a, y). (mset a, y)) (rev s)› for s
by (auto simp flip: rev_map simp: eq_commute[of ‹rev (map _ _)› ‹map _ _›])
have 1: ‹⋀s y. (p, y) ∈ ⟨unsorted_term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
p' = mset y ⟹
map (λ(a, y). (mset a, y)) (rev p) = map (λ(a, y). (mset a, y)) s ⟹
∀x∈set s. sorted_wrt var_order (fst x) ⟹
(s, map (λ(a, y). (mset a, y)) s)
∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel›
by (auto 4 4 simp: rel2p_def
dest!: list_rel_unsorted_term_poly_list_relD
dest: shuffle_terms_distinct_iff["THEN" iffD1]
intro!: map_mset_unsorted_term_poly_list_rel
sorted_wrt_mono_rel[of _ ‹rel2p (var_order_rel)› ‹rel2p (Id ∪ var_order_rel)›])
have 2: ‹⋀s y. (p, y) ∈ ⟨unsorted_term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
p' = mset y ⟹
map (λ(a, y). (mset a, y)) (rev p) = map (λ(a, y). (mset a, y)) s ⟹
∀x∈set s. sorted_wrt var_order (fst x) ⟹
mset y = {#case x of (a, x) ⇒ (mset a, x). x ∈# mset s#}›
by (metis (no_types, lifting) list_rel_unsorted_term_poly_list_relD mset_map mset_rev)
show ?thesis
apply (rule sort_all_coeffs[THEN order_trans])
using assms
by (auto simp: shuffle_coefficients_def poly_list_rel_def
RETURN_def fully_unsorted_poly_list_rel_def list_mset_rel_def
br_def dest: list_rel_unsorted_term_poly_list_relD
intro!: RES_refine relcompI[of _  ‹map (λ(a, y). (mset a, y)) (rev p)›]
1 2)
qed

lemma sort_poly_spec_id':
assumes ‹(p, p') ∈ unsorted_poly_rel_with0›
shows ‹sort_poly_spec p ≤ ⇓ (sorted_repeat_poly_rel_with0) (RETURN p')›
proof -
obtain y where
py: ‹(p, y) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel› and
p'_y: ‹p' = mset y›
using assms
unfolding fully_unsorted_poly_list_rel_def poly_list_rel_def sorted_poly_list_rel_wrt_def
by (auto simp: list_mset_rel_def br_def)
then have [simp]: ‹length y = length p›
by (auto simp: list_rel_def list_all2_conv_all_nth)
have H: ‹(x, p')
∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel O list_mset_rel›
if px: ‹mset p = mset x› and ‹sorted_wrt (rel2p (Id ∪ lexord var_order_rel)) (map fst x)›
for x :: ‹llist_polynomial›
proof -
from px have ‹length x = length p›
by (metis size_mset)
from px have ‹mset x = mset p›
by simp
then obtain f where ‹f permutes {..<length p}› ‹permute_list f p = x›
by (rule mset_eq_permutation)
with ‹length x = length p› have f: ‹bij_betw f {..<length x} {..<length p}›
from ‹f permutes {..<length p}› ‹permute_list f p = x› [symmetric]
have [simp]: ‹⋀i. i < length x ⟹ x ! i = p ! (f i)›
let ?y = ‹map (λi. y ! f i) [0 ..< length x]›
have ‹i < length y ⟹ (p ! f i, y ! f i) ∈ term_poly_list_rel ×⇩r int_rel› for i
using list_all2_nthD[of _ p y
‹f i›, OF py[unfolded list_rel_def mem_Collect_eq prod.case]]
mset_eq_length[OF px] f
by (auto simp: list_rel_def list_all2_conv_all_nth bij_betw_def)
then have ‹(x, ?y) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel› and
xy: ‹length x = length y›
using py list_all2_nthD[of ‹rel2p (term_poly_list_rel ×⇩r int_rel)› p y
‹f i› for i, simplified] mset_eq_length[OF px]
by (auto simp: list_rel_def list_all2_conv_all_nth)
moreover {
have f: ‹mset_set {0..<length x} = f `# mset_set {0..<length x}›
using f mset_eq_length[OF px]
by (auto simp: bij_betw_def lessThan_atLeast0 image_mset_mset_set)
have ‹mset y = {#y ! f x. x ∈# mset_set {0..<length x}#}›
by (subst drop_0[symmetric], subst mset_drop_upto, subst xy[symmetric], subst f)
auto
then have ‹(?y, p') ∈ list_mset_rel›
by (auto simp: list_mset_rel_def br_def p'_y)
}
ultimately show ?thesis
by (auto intro!: relcompI[of _ ?y])
qed
show ?thesis
unfolding sort_poly_spec_def poly_list_rel_def sorted_repeat_poly_list_rel_with0_wrt_def
by refine_rcg (auto intro: H)
qed

fun merge_coeffs0 :: ‹llist_polynomial ⇒ llist_polynomial› where
‹merge_coeffs0 [] = []› |
‹merge_coeffs0 [(xs, n)] = (if n = 0 then [] else [(xs, n)])› |
‹merge_coeffs0 ((xs, n) # (ys, m) # p) =
(if xs = ys
then if n + m ≠ 0 then merge_coeffs0 ((xs, n + m) # p) else merge_coeffs0 p
else if n = 0 then merge_coeffs0 ((ys, m) # p)
else(xs, n) # merge_coeffs0 ((ys, m) # p))›

lemma sorted_repeat_poly_list_rel_with0_wrt_ConsD:
‹((ys, n) # p, a) ∈ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel ⟹
(p, remove1_mset (mset ys, n) a) ∈ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel ∧
(mset ys, n) ∈# a ∧ (∀x ∈ set p. S ys (fst x)) ∧ sorted_wrt (rel2p var_order_rel) ys ∧
distinct ys›
unfolding sorted_repeat_poly_list_rel_with0_wrt_def prod.case mem_Collect_eq
list_rel_def
apply (clarsimp)
apply (subst (asm) list.rel_sel)
apply (intro conjI)
apply (rule_tac b = ‹tl y› in relcompI)
apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def)
apply (case_tac ‹lead_coeff y›; case_tac y)
apply (auto simp: term_poly_list_rel_def)
apply (case_tac ‹lead_coeff y›; case_tac y)
apply (auto simp: term_poly_list_rel_def)
apply (case_tac ‹lead_coeff y›; case_tac y)
apply (auto simp: term_poly_list_rel_def)
apply (case_tac ‹lead_coeff y›; case_tac y)
apply (auto simp: term_poly_list_rel_def)
done

lemma sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff:
‹((ys, n) # p, a) ∈ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel ⟷
(p, remove1_mset (mset ys, n) a) ∈ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel ∧
(mset ys, n) ∈# a ∧ (∀x ∈ set p. S ys (fst x)) ∧ sorted_wrt (rel2p var_order_rel) ys ∧
distinct ys›
apply (rule iffI)
subgoal
by (auto dest!: sorted_repeat_poly_list_rel_with0_wrt_ConsD)
subgoal
unfolding sorted_poly_list_rel_wrt_def prod.case mem_Collect_eq
list_rel_def sorted_repeat_poly_list_rel_with0_wrt_def
apply (clarsimp)
apply (rule_tac b = ‹(mset ys, n) # y› in relcompI)
by (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def
nonzero_coeffs_def
dest!: multi_member_split)
done

lemma fst_normalize0_polynomial_subsetD:
‹(a, b) ∈ set (merge_coeffs0 p) ⟹ a ∈ mononoms p›
apply (induction p rule: merge_coeffs0.induct)
subgoal
by auto
subgoal
by (auto split: if_splits)
subgoal
by (auto split: if_splits)
done

lemma in_set_merge_coeffs0D:
‹(a, b) ∈ set (merge_coeffs0 p) ⟹∃b. (a, b) ∈ set p›
by  (auto dest!: fst_normalize0_polynomial_subsetD)

lemma merge_coeffs0_is_normalize_poly_p:
‹(xs, ys) ∈ sorted_repeat_poly_rel_with0 ⟹ ∃r. (merge_coeffs0 xs, r) ∈ sorted_poly_rel ∧ normalize_poly_p⇧*⇧* ys r›
apply (induction xs arbitrary: ys rule: merge_coeffs0.induct)
subgoal by (auto simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def
sorted_repeat_poly_list_rel_with0_wrt_def list_mset_rel_def br_def)
subgoal for xs n ys
by (force simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def
sorted_repeat_poly_list_rel_with0_wrt_def list_mset_rel_def br_def
list_rel_split_right_iff)
subgoal premises p for xs n ys m p ysa
apply (cases ‹xs = ys›, cases ‹m+n ≠ 0›)
subgoal
using p(1)[of ‹add_mset (mset ys, m+n) ysa - {#(mset ys, m), (mset ys, n)#}›] p(5-)
apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute
converse_rtranclp_into_rtranclp dest!: multi_member_split
simp del: normalize_poly_p.merge_dup_coeff)
apply (rule_tac x = ‹r› in exI)
using normalize_poly_p.merge_dup_coeff[of ‹ysa -  {#(mset ys, m), (mset ys, n)#}› ‹ysa -  {#(mset ys, m), (mset ys, n)#}› ‹mset ys› m n]
by (auto intro: normalize_poly_p.intros
converse_rtranclp_into_rtranclp dest!: multi_member_split
simp: add_mset_commute[of ‹(mset ys, n)› ‹(mset ys, m)›]
simp del: normalize_poly_p.merge_dup_coeff)
subgoal
using p(2)[of ‹ysa - {#(mset ys, m), (mset ys, n)#}›] p(5-)
apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute
apply (rule_tac x = ‹r› in exI)
using normalize_poly_p.rem_0_coeff[of ‹add_mset (mset ys, m +n) ysa -  {#(mset ys, m), (mset ys, n)#}› ‹add_mset (mset ys, m +n) ysa -  {#(mset ys, m), (mset ys, n)#}› ‹mset ys›]
using normalize_poly_p.merge_dup_coeff[of ‹ysa -  {#(mset ys, m), (mset ys, n)#}› ‹ysa -  {#(mset ys, m), (mset ys, n)#}› ‹mset ys› m n]
by (force intro: normalize_poly_p.intros converse_rtranclp_into_rtranclp
dest!: multi_member_split
simp del: normalize_poly_p.rem_0_coeff
simp: add_mset_commute[of ‹(mset ys, n)› ‹(mset ys, m)›])
apply (cases ‹n = 0›)
subgoal
using p(3)[of ‹add_mset (mset ys, m) ysa - {#(mset xs, n), (mset ys, m)#}›] p(4-)
apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute
apply (rule_tac x = ‹r› in exI)
apply (auto dest!: in_set_merge_coeffsD)
simp: rel2p_def var_order_rel_def sorted_poly_list_rel_Cons_iff
dest!: multi_member_split
dest: sorted_poly_list_rel_nonzeroD)
subgoal
using p(4)[of ‹add_mset (mset ys, m) ysa - {#(mset xs, n), (mset ys, m)#}›] p(5-)
apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute
apply (rule_tac x = ‹add_mset (mset xs, n) r› in exI)
apply (auto dest!: in_set_merge_coeffs0D)
simp: rel2p_def var_order_rel_def sorted_poly_list_rel_Cons_iff
dest!: multi_member_split
dest: sorted_poly_list_rel_nonzeroD)
using in_set_merge_coeffs0D total_on_lexord_less_than_char_linear apply fastforce
using in_set_merge_coeffs0D total_on_lexord_less_than_char_linear apply fastforce
done
done
done

definition full_normalize_poly where
‹full_normalize_poly p = do {
p ← sort_all_coeffs p;
p ← sort_poly_spec p;
RETURN (merge_coeffs0 p)
}›

fun sorted_remdups where
‹sorted_remdups (x # y # zs) =
(if x = y then sorted_remdups (y # zs) else x # sorted_remdups (y # zs))› |
‹sorted_remdups zs = zs›

lemma set_sorted_remdups[simp]:
‹set (sorted_remdups xs) = set xs›
by (induction xs rule: sorted_remdups.induct)
auto

lemma distinct_sorted_remdups:
‹sorted_wrt R xs ⟹ antisymp R ⟹ distinct (sorted_remdups xs)›
by (induction xs rule: sorted_remdups.induct)
(auto dest: antisympD)

lemma full_normalize_poly_normalize_poly_p:
assumes ‹(p, p') ∈ fully_unsorted_poly_rel›
shows ‹full_normalize_poly p ≤ ⇓ (sorted_poly_rel) (SPEC (λr. normalize_poly_p⇧*⇧* p' r))›
(is ‹?A ≤ ⇓ ?R ?B›)
proof -
have 1: ‹?B = do {
p' ← RETURN p';
p' ← RETURN p';
SPEC (λr. normalize_poly_p⇧*⇧* p' r)
}›
by auto
have [refine0]: ‹sort_all_coeffs p ≤ SPEC(λp. (p, p') ∈ unsorted_poly_rel_with0)›
by (rule sort_all_coeffs_unsorted_poly_rel_with0[OF assms, THEN order_trans])
(auto simp: conc_fun_RES RETURN_def)
have [refine0]: ‹sort_poly_spec p ≤ SPEC (λc. (c, p') ∈ sorted_repeat_poly_rel_with0)›
if ‹(p, p') ∈ unsorted_poly_rel_with0›
for p p'
by (rule sort_poly_spec_id'[THEN order_trans, OF that])
(auto simp: conc_fun_RES RETURN_def)
show ?thesis
apply (subst 1)
unfolding full_normalize_poly_def
by (refine_rcg)
(auto intro!: RES_refine
dest!: merge_coeffs0_is_normalize_poly_p
simp: RETURN_def)
qed

definition mult_poly_full :: ‹_› where
‹mult_poly_full p q = do {
let pq = mult_poly_raw p q;
normalize_poly pq
}›

lemma normalize_poly_normalize_poly_p:
assumes ‹(p, p') ∈ unsorted_poly_rel›
shows ‹normalize_poly p ≤ ⇓ (sorted_poly_rel) (SPEC (λr. normalize_poly_p⇧*⇧* p' r))›
proof -
have 1: ‹SPEC (λr. normalize_poly_p⇧*⇧* p' r) = do {
p' ← RETURN p';
SPEC (λr. normalize_poly_p⇧*⇧* p' r)
}›
by auto
show ?thesis
unfolding normalize_poly_def
apply (subst 1)
apply (refine_rcg sort_poly_spec_id[OF assms]
merge_coeffs_is_normalize_poly_p)
subgoal
by (drule merge_coeffs_is_normalize_poly_p)
(auto intro!: RES_refine simp: RETURN_def)
done
qed

subsection ‹Multiplication and normalisation›

definition mult_poly_p' :: ‹_› where
‹mult_poly_p' p' q' = do {
pq ← SPEC(λr. (mult_poly_p q')⇧*⇧* (p', {#}) ({#}, r));
SPEC (λr. normalize_poly_p⇧*⇧* pq r)
}›

lemma unsorted_poly_rel_fully_unsorted_poly_rel:
‹unsorted_poly_rel ⊆ fully_unsorted_poly_rel›
proof -
have ‹term_poly_list_rel  ×⇩r int_rel ⊆ unsorted_term_poly_list_rel ×⇩r int_rel›
by (auto simp: unsorted_term_poly_list_rel_def term_poly_list_rel_def)
from list_rel_mono[OF this]
show ?thesis
unfolding poly_list_rel_def fully_unsorted_poly_list_rel_def
by (auto simp:)
qed

lemma mult_poly_full_mult_poly_p':
assumes ‹(p, p') ∈ sorted_poly_rel› ‹(q, q') ∈ sorted_poly_rel›
shows ‹mult_poly_full p q ≤ ⇓ (sorted_poly_rel) (mult_poly_p' p' q')›
unfolding mult_poly_full_def mult_poly_p'_def
apply (refine_rcg full_normalize_poly_normalize_poly_p
normalize_poly_normalize_poly_p)
apply (subst RETURN_RES_refine_iff)
apply (subst Bex_def)
apply (subst mem_Collect_eq)
apply (subst conj_commute)
apply (rule mult_poly_raw_mult_poly_p[OF assms(1,2)])
subgoal
by blast
done

‹add_poly_spec p q = SPEC (λr. p + q - r ∈ ideal polynomial_bool)›

‹add_poly_p' p q = SPEC(λr. add_poly_p⇧*⇧* (p, q, {#}) ({#}, {#}, r))›

assumes ‹(p, p') ∈ sorted_poly_rel› ‹(q, q') ∈ sorted_poly_rel›
apply (refine_rcg add_poly_l_spec[THEN fref_to_Down_curry_right, THEN order_trans, of _ p' q'])
subgoal by auto
subgoal using assms by auto
subgoal
by auto
done

subsection ‹Correctness›

context poly_embed
begin

definition mset_poly_rel where
‹mset_poly_rel = {(a, b). b = polynomial_of_mset a}›

definition var_rel where
‹var_rel = br φ (λ_. True)›

lemma normalize_poly_p_normalize_poly_spec:
‹(p, p') ∈ mset_poly_rel ⟹
SPEC (λr. normalize_poly_p⇧*⇧* p r) ≤ ⇓mset_poly_rel (normalize_poly_spec p')›
by (auto simp: mset_poly_rel_def rtranclp_normalize_poly_p_poly_of_mset ideal.span_zero
normalize_poly_spec_def intro!: RES_refine)

lemma mult_poly_p'_mult_poly_spec:
‹(p, p') ∈ mset_poly_rel ⟹ (q, q') ∈ mset_poly_rel ⟹
mult_poly_p' p q ≤ ⇓mset_poly_rel (mult_poly_spec p' q')›
unfolding mult_poly_p'_def mult_poly_spec_def
apply refine_rcg
apply (auto simp: mset_poly_rel_def dest!: rtranclp_mult_poly_p_mult_ideal_final)
apply (intro RES_refine)
by (fastforce dest!: rtranclp_normalize_poly_p_poly_of_mset intro: ideal.span_add_eq2)

‹(p, p') ∈ mset_poly_rel ⟹ (q, q') ∈ mset_poly_rel ⟹
apply (auto simp: mset_poly_rel_def dest!: rtranclp_add_poly_p_polynomial_of_mset_full)
apply (intro RES_refine)
done

end

definition weak_equality_l :: ‹llist_polynomial ⇒ llist_polynomial ⇒ bool nres› where
‹weak_equality_l p q = RETURN (p = q)›

definition weak_equality :: ‹int mpoly ⇒ int mpoly ⇒ bool nres› where
‹weak_equality p q = SPEC (λr. r ⟶ p = q)›

definition weak_equality_spec :: ‹mset_polynomial ⇒ mset_polynomial ⇒ bool nres› where
‹weak_equality_spec p q = SPEC (λr. r ⟶ p = q)›

lemma term_poly_list_rel_same_rightD:
‹(a, aa) ∈ term_poly_list_rel ⟹ (a, ab) ∈ term_poly_list_rel ⟹ aa = ab›
by (auto simp: term_poly_list_rel_def)

lemma list_rel_term_poly_list_rel_same_rightD:
‹(xa, y) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
(xa, ya) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
y = ya›
by (induction xa arbitrary: y ya)
(auto simp: list_rel_split_right_iff
dest: term_poly_list_rel_same_rightD)

lemma weak_equality_l_weak_equality_spec:
‹(uncurry weak_equality_l, uncurry weak_equality_spec) ∈
sorted_poly_rel ×⇩r sorted_poly_rel →⇩f ⟨bool_rel⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: weak_equality_l_def weak_equality_spec_def
sorted_poly_list_rel_wrt_def list_mset_rel_def br_def
dest: list_rel_term_poly_list_rel_same_rightD)

end
```