Theory PAC_Polynomials_Operations
theory PAC_Polynomials_Operations
imports PAC_Polynomials_Term PAC_Checker_Specification
begin
subsection ‹Addition›
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
‹add_poly_l = REC⇩T
(λadd_poly_l (p, q).
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 {
pq ← add_poly_l (p, q);
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
term_poly_list_rel_def add_mset_eq_add_mset eq_commute[of _ ‹mset _›]
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
term_poly_list_rel_def add_mset_eq_add_mset eq_commute[of _ ‹mset _›]
nonzero_coeffs_def
dest!: multi_member_split)
done
lemma add_poly_p_add_mset_sum_0:
‹n + m = 0 ⟹add_poly_p⇧*⇧* (A, Aa, {#}) ({#}, {#}, r) ⟹
add_poly_p⇧*⇧*
(add_mset (mset ys, n) A, add_mset (mset ys, m) Aa, {#})
({#}, {#}, r)›
apply (rule converse_rtranclp_into_rtranclp)
apply (rule add_poly_p.add_new_coeff_r)
apply (rule converse_rtranclp_into_rtranclp)
apply (rule add_poly_p.add_same_coeff_l)
apply (rule converse_rtranclp_into_rtranclp)
apply (auto intro: add_poly_p.rem_0_coeff)
done
lemma monoms_add_poly_l'D:
‹(aa, ba) ∈ set (add_poly_l' x) ⟹ aa ∈ fst ` set (fst x) ∨ aa ∈ fst ` set (snd x)›
by (induction x rule: add_poly_l'.induct)
(auto split: if_splits)
lemma add_poly_p_add_to_result:
‹add_poly_p⇧*⇧* (A, B, r) (A', B', r') ⟹
add_poly_p⇧*⇧*
(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
by (elim add_poly_pE)
(metis (no_types, lifting) Pair_inject add_poly_p.intros rtranclp.simps union_mset_add_mset_right)+
lemma add_poly_p_add_mset_comb:
‹add_poly_p⇧*⇧* (A, Aa, {#}) ({#}, {#}, r) ⟹
add_poly_p⇧*⇧*
(add_mset (xs, n) A, Aa, {#})
({#}, {#}, add_mset (xs, n) r)›
apply (rule converse_rtranclp_into_rtranclp)
apply (rule add_poly_p.add_new_coeff_l)
using add_poly_p_add_to_result[of A Aa ‹{#}› ‹{#}› ‹{#}› r ‹{#(xs, n)#}›]
by auto
lemma add_poly_p_add_mset_comb2:
‹add_poly_p⇧*⇧* (A, Aa, {#}) ({#}, {#}, r) ⟹
add_poly_p⇧*⇧*
(add_mset (ys, n) A, add_mset (ys, m) Aa, {#})
({#}, {#}, add_mset (ys, n + m) r)›
apply (rule converse_rtranclp_into_rtranclp)
apply (rule add_poly_p.add_new_coeff_r)
apply (rule converse_rtranclp_into_rtranclp)
apply (rule add_poly_p.add_same_coeff_l)
using add_poly_p_add_to_result[of A Aa ‹{#}› ‹{#}› ‹{#}› r ‹{#(ys, n+m)#}›]
by auto
lemma add_poly_p_add_mset_comb3:
‹add_poly_p⇧*⇧* (A, Aa, {#}) ({#}, {#}, r) ⟹
add_poly_p⇧*⇧*
(A, add_mset (ys, m) Aa, {#})
({#}, {#}, add_mset (ys, m) r)›
apply (rule converse_rtranclp_into_rtranclp)
apply (rule add_poly_p.add_new_coeff_r)
using add_poly_p_add_to_result[of A Aa ‹{#}› ‹{#}› ‹{#}› r ‹{#(ys, m)#}›]
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)
lemma add_poly_l'_add_poly_p:
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')
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
)
using add_poly_p_add_mset_sum_0 by blast
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
intro: add_poly_p_add_mset_comb2)
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 (auto dest!: monoms_add_poly_l'D)
apply (auto intro: lexord_trans add_poly_p_add_mset_comb simp: lexord_transI var_order_rel_def)
apply (rule lexord_trans)
apply assumption
apply (auto intro: lexord_trans add_poly_p_add_mset_comb simp: lexord_transI
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)
apply (auto dest!: monoms_add_poly_l'D
simp: total_on_lexord_less_than_char_linear)
apply (auto intro: lexord_trans add_poly_p_add_mset_comb simp: lexord_transI
total_on_lexord_less_than_char_linear var_order_rel_def)
apply (rule lexord_trans)
apply assumption
apply (auto intro: lexord_trans add_poly_p_add_mset_comb3 simp: lexord_transI
sorted_poly_list_rel_nonzeroD var_order_rel_def)
using total_on_lexord_less_than_char_linear by fastforce
done
done
done
lemma add_poly_l_add_poly:
‹add_poly_l x = RETURN (add_poly_l' x)›
unfolding add_poly_l_def
by (induction x rule: add_poly_l'.induct)
(solves ‹subst RECT_unfold, refine_mono, simp split: list.split›)+
lemma add_poly_l_spec:
‹(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›
unfolding add_poly_l_add_poly
apply (intro nres_relI frefI)
apply (drule add_poly_l'_add_poly_p)
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}›
by (simp add: permutes_imp_bij)
from ‹f permutes {..<length p}› ‹permute_list f p = x› [symmetric]
have [simp]: ‹⋀i. i < length x ⟹ x ! i = p ! (f i)›
by (simp add: permute_list_nth)
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)
apply (simp add: relcomp.relcompI)
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')›
lemma mult_poly_p_add_mset_same:
‹(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
intro: rtranclp.rtrancl_into_rtrancl simp: add_mset_commute[of x])
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 (rule mult_poly_p_add_mset_same)
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)
lemma rtranclp_normalize_poly_add_mset:
‹normalize_poly_p⇧*⇧* A r ⟹ normalize_poly_p⇧*⇧* (add_mset x A) (add_mset x r)›
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
remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff)
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
simp: add_mset_commute
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
remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff)
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
simp: add_eq_0_iff2
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
remove1_mset_add_mset_If sorted_repeat_poly_list_rel_Cons_iff)
apply (rule_tac x = ‹add_mset (mset xs, n) r› in exI)
apply (auto dest!: in_set_merge_coeffsD)
apply (auto intro: normalize_poly_p.intros rtranclp_normalize_poly_add_mset
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-)
apply (cases a, simp only: monadic_nfoldli_simp bind_to_let_conv Let_def if_True Refine_Basic.nres_monad3
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}›
by (simp add: permutes_imp_bij)
from ‹f permutes {..<length p}› ‹permute_list f p = x› [symmetric]
have [simp]: ‹⋀i. i < length x ⟹ x ! i = p ! (f i)›
by (simp add: permute_list_nth)
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
term_poly_list_rel_def add_mset_eq_add_mset eq_commute[of _ ‹mset _›]
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
remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff)
apply (auto intro: normalize_poly_p.intros add_mset_commute 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
remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff)
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
remove1_mset_add_mset_If sorted_repeat_poly_list_rel_Cons_iff)
apply (rule_tac x = ‹r› in exI)
apply (auto dest!: in_set_merge_coeffsD)
by (force intro: rtranclp_normalize_poly_add_mset converse_rtranclp_into_rtranclp
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
remove1_mset_add_mset_If sorted_repeat_poly_list_rel_Cons_iff)
apply (rule_tac x = ‹add_mset (mset xs, n) r› in exI)
apply (auto dest!: in_set_merge_coeffs0D)
apply (auto intro: normalize_poly_p.intros rtranclp_normalize_poly_add_mset
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
definition add_poly_spec :: ‹_› where
‹add_poly_spec p q = SPEC (λr. p + q - r ∈ ideal polynomial_bool)›
definition add_poly_p' :: ‹_› where
‹add_poly_p' p q = SPEC(λr. add_poly_p⇧*⇧* (p, q, {#}) ({#}, {#}, r))›
lemma add_poly_l_add_poly_p':
assumes ‹(p, p') ∈ sorted_poly_rel› ‹(q, q') ∈ sorted_poly_rel›
shows ‹add_poly_l (p, q) ≤ ⇓ (sorted_poly_rel) (add_poly_p' p' q')›
unfolding add_poly_p'_def
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)
using ideal.span_add_eq2 ideal.span_zero
by (fastforce dest!: rtranclp_normalize_poly_p_poly_of_mset intro: ideal.span_add_eq2)
lemma add_poly_p'_add_poly_spec:
‹(p, p') ∈ mset_poly_rel ⟹ (q, q') ∈ mset_poly_rel ⟹
add_poly_p' p q ≤ ⇓mset_poly_rel (add_poly_spec p' q')›
unfolding add_poly_p'_def add_poly_spec_def
apply (auto simp: mset_poly_rel_def dest!: rtranclp_add_poly_p_polynomial_of_mset_full)
apply (intro RES_refine)
apply (auto simp: rtranclp_add_poly_p_polynomial_of_mset_full ideal.span_zero)
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