Theory EPAC_Checker
theory EPAC_Checker
imports
EPAC_Checker_Specification
PAC_Checker.PAC_Map_Rel
PAC_Checker.PAC_Polynomials_Operations
PAC_Checker.PAC_Checker
Show.Show
Show.Show_Instances
begin
hide_const (open) PAC_Checker_Specification.PAC_checker_step
PAC_Checker.PAC_checker_l PAC_Checker_Specification.PAC_checker
hide_fact (open) PAC_Checker_Specification.PAC_checker_step_def
PAC_Checker.PAC_checker_l_def PAC_Checker_Specification.PAC_checker_def
lemma vars_llist[simp]:
‹vars_llist [] = {}›
‹vars_llist (xs @ ys) = vars_llist xs ∪ vars_llist ys›
‹vars_llist (x # ys) = set (fst x) ∪ vars_llist ys›
by (auto simp: vars_llist_def)
section ‹Executable Checker›
text ‹In this layer we finally refine the checker to executable code.›
subsection ‹Definitions›
text ‹Compared to the previous layer, we add an error message when an error is discovered. We do not
attempt to prove anything on the error message (neither that there really is an error, nor that the
error message is correct).
›
paragraph ‹Refinement relation›
fun pac_step_rel_raw :: ‹('olbl × 'lbl) set ⇒ ('a × 'b) set ⇒ ('c × 'd) set ⇒ ('a, 'c, 'olbl) pac_step ⇒ ('b, 'd, 'lbl) pac_step ⇒ bool› where
‹pac_step_rel_raw R1 R2 R3 (CL p i r) (CL p' i' r') ⟷
(p, p') ∈ ⟨R2 ×⇩r R1⟩list_rel ∧ (i, i') ∈ R1 ∧
(r, r') ∈ R2› |
‹pac_step_rel_raw R1 R2 R3 (Del p1) (Del p1') ⟷
(p1, p1') ∈ R1› |
‹pac_step_rel_raw R1 R2 R3 (Extension i x p1) (Extension j x' p1') ⟷
(i, j) ∈ R1 ∧ (x, x') ∈ R3 ∧ (p1, p1') ∈ R2› |
‹pac_step_rel_raw R1 R2 R3 _ _ ⟷ False›
fun pac_step_rel_assn :: ‹('olbl ⇒ 'lbl ⇒ assn) ⇒ ('a ⇒ 'b ⇒ assn) ⇒ ('c ⇒ 'd ⇒ assn) ⇒ ('a, 'c, 'olbl) pac_step ⇒ ('b, 'd, 'lbl) pac_step ⇒ assn› where
‹pac_step_rel_assn R1 R2 R3 (CL p i r) (CL p' i' r') =
list_assn (R2 ×⇩a R1) p p' * R1 i i' * R2 r r'› |
‹pac_step_rel_assn R1 R2 R3 (Del p1) (Del p1') =
R1 p1 p1'› |
‹pac_step_rel_assn R1 R2 R3 (Extension i x p1) (Extension i' x' p1') =
R1 i i' * R3 x x' * R2 p1 p1'› |
‹pac_step_rel_assn R1 R2 _ _ _ = false›
lemma pac_step_rel_assn_alt_def:
‹pac_step_rel_assn R1 R2 R3 x y = (
case (x, y) of
(CL p i r, CL p' i' r') ⇒
list_assn (R2 ×⇩a R1) p p' * R1 i i' * R2 r r'
| (Del p1, Del p1') ⇒ R1 p1 p1'
| (Extension i x p1, Extension i' x' p1') ⇒ R1 i i' * R3 x x' * R2 p1 p1'
| _ ⇒ false)›
by (auto split: pac_step.splits)
paragraph ‹Addition checking›
paragraph ‹Linear Combination›
definition check_linear_combi_l_pre_err :: ‹nat ⇒ bool ⇒ bool ⇒ bool ⇒ string nres› where
‹check_linear_combi_l_pre_err r _ _ _ = SPEC (λ_. True)›
definition check_linear_combi_l_dom_err :: ‹llist_polynomial ⇒ nat ⇒ string nres› where
‹check_linear_combi_l_dom_err p r = SPEC (λ_. True)›
definition check_linear_combi_l_mult_err :: ‹llist_polynomial ⇒ llist_polynomial ⇒ string nres› where
‹check_linear_combi_l_mult_err pq r = SPEC (λ_. True)›
definition linear_combi_l_pre where
‹linear_combi_l_pre i A 𝒱 xs ⟷
(∀i∈#dom_m A. vars_llist (the (fmlookup A i)) ⊆ 𝒱)›
definition linear_combi_l where
‹linear_combi_l i A 𝒱 xs = do {
ASSERT(linear_combi_l_pre i A 𝒱 xs);
WHILE⇩T
(λ(p, xs, err). xs ≠ [] ∧ ¬is_cfailed err)
(λ(p, xs, _). do {
ASSERT(xs ≠ []);
ASSERT(vars_llist p ⊆ 𝒱);
let (q⇩0 :: llist_polynomial, i) = hd xs;
if (i ∉# dom_m A ∨ ¬(vars_llist q⇩0 ⊆ 𝒱))
then do {
err ← check_linear_combi_l_dom_err q⇩0 i;
RETURN (p, xs, error_msg i err)
} else do {
ASSERT(fmlookup A i ≠ None);
let r = the (fmlookup A i);
ASSERT(vars_llist r ⊆ 𝒱);
if q⇩0 = [([], 1)]
then do {
pq ← add_poly_l (p, r);
RETURN (pq, tl xs, CSUCCESS)
}
else do {
q ← full_normalize_poly (q⇩0);
ASSERT(vars_llist q ⊆ 𝒱);
pq ← mult_poly_full q r;
ASSERT(vars_llist pq ⊆ 𝒱);
pq ← add_poly_l (p, pq);
RETURN (pq, tl xs, CSUCCESS)
}
}
})
([], xs, CSUCCESS)
}›
definition check_linear_combi_l where
‹check_linear_combi_l spec A 𝒱 i xs r = do{
b← RES(UNIV::bool set);
if b ∨ i ∈# dom_m A ∨ xs = [] ∨ ¬(vars_llist r ⊆ 𝒱)
then do {
err ← check_linear_combi_l_pre_err i (i ∈# dom_m A) (xs = []) (¬(vars_llist r ⊆ 𝒱));
RETURN (error_msg i err)
}
else do {
(p, _, err) ← linear_combi_l i A 𝒱 xs;
if (is_cfailed err)
then do {
RETURN err
}
else do {
b ← weak_equality_l p r;
b' ← weak_equality_l r spec;
if b then (if b' then RETURN CFOUND else RETURN CSUCCESS) else do {
c ← check_linear_combi_l_mult_err p r;
RETURN (error_msg i c)
}
}
}}›
paragraph ‹Deletion checking›
definition check_extension_l_side_cond_err
:: ‹string ⇒ llist_polynomial ⇒ llist_polynomial ⇒ string nres›
where
‹check_extension_l_side_cond_err v p' q = SPEC (λ_. True)›
definition (in -)check_extension_l2
:: ‹_ ⇒ _ ⇒ string set ⇒ nat ⇒ string ⇒ llist_polynomial ⇒ (string code_status) nres›
where
‹check_extension_l2 spec A 𝒱 i v p' = do {
b ← SPEC(λb. b ⟶ i ∉# dom_m A ∧ v ∉ 𝒱);
if ¬b
then do {
c ← check_extension_l_dom_err i;
RETURN (error_msg i c)
} else do {
let p' = p';
let b = vars_llist p' ⊆ 𝒱;
if ¬b
then do {
c ← check_extension_l_new_var_multiple_err v p';
RETURN (error_msg i c)
}
else do {
ASSERT(vars_llist p' ⊆ 𝒱);
p2 ← mult_poly_full p' p';
ASSERT(vars_llist p2 ⊆ 𝒱);
let p' = map (λ(a,b). (a, -b)) p';
ASSERT(vars_llist p' ⊆ 𝒱);
q ← add_poly_l (p2, p');
ASSERT(vars_llist q ⊆ 𝒱);
eq ← weak_equality_l q [];
if eq then do {
RETURN (CSUCCESS)
} else do {
c ← check_extension_l_side_cond_err v p' q;
RETURN (error_msg i c)
}
}
}
}›
paragraph ‹Extension checking›
paragraph ‹Step checking›
definition PAC_checker_l_step_inv where
‹PAC_checker_l_step_inv spec st' 𝒱 A ⟷
(∀i∈#dom_m A. vars_llist (the (fmlookup A i)) ⊆ 𝒱)›
definition PAC_checker_l_step :: ‹_ ⇒ string code_status × string set × _ ⇒ (llist_polynomial, string, nat) pac_step ⇒ _› where
‹PAC_checker_l_step = (λspec (st', 𝒱, A) st. do {
ASSERT(¬is_cfailed st');
ASSERT(PAC_checker_l_step_inv spec st' 𝒱 A);
case st of
CL _ _ _ ⇒
do {
ASSERT (PAC_checker_l_step_inv spec st' 𝒱 A);
r ← full_normalize_poly (pac_res st);
eq ← check_linear_combi_l spec A 𝒱 (new_id st) (pac_srcs st) r;
let _ = eq;
if ¬is_cfailed eq
then RETURN (merge_cstatus st' eq,
𝒱, fmupd (new_id st) r A)
else RETURN (eq, 𝒱, A)
}
| Del _ ⇒
do {
ASSERT (PAC_checker_l_step_inv spec st' 𝒱 A);
eq ← check_del_l spec A (pac_src1 st);
let _ = eq;
if ¬is_cfailed eq
then RETURN (merge_cstatus st' eq, 𝒱, fmdrop (pac_src1 st) A)
else RETURN (eq, 𝒱, A)
}
| Extension _ _ _ ⇒
do {
ASSERT (PAC_checker_l_step_inv spec st' 𝒱 A);
r ← full_normalize_poly (pac_res st);
eq ← check_extension_l2 spec A 𝒱 (new_id st) (new_var st) r;
if ¬is_cfailed eq
then do {
ASSERT(new_var st ∉ vars_llist r ∧ vars_llist r ⊆ 𝒱);
r' ← add_poly_l ([([new_var st], -1)], r);
RETURN (st',
insert (new_var st) 𝒱, fmupd (new_id st) r' A)}
else RETURN (eq, 𝒱, A)
}}
)›
lemma pac_step_rel_raw_def:
‹⟨K, V, R⟩ pac_step_rel_raw = pac_step_rel_raw K V R›
by (auto intro!: ext simp: relAPP_def)
subsection ‹Correctness›
text ‹We now enter the locale to reason about polynomials directly.›
context poly_embed
begin
lemma (in -) vars_llist_merge_coeffsD:
‹x ∈ vars_llist (merge_coeffs pa) ⟹ x ∈ vars_llist pa›
apply (induction pa rule:merge_coeffs.induct)
apply (auto split: if_splits)
done
lemma (in -) add_nset_list_rel_add_mset_iff:
‹(pa, add_mset (aa) (ys)) ∈ ⟨R⟩list_rel O {(c, a). a = mset c} ⟷
(∃pa⇩1 pa⇩2 x. pa = pa⇩1 @ x # pa⇩2 ∧ (pa⇩1 @ pa⇩2, ys) ∈ ⟨R⟩list_rel O {(c, a). a = mset c} ∧
(x, aa) ∈ R)›
apply (rule iffI)
subgoal
apply clarify
apply (subgoal_tac ‹aa ∈ set y›)
apply (auto dest!: split_list simp: list_rel_split_right_iff list_rel_append1 list_rel_split_left_iff
list_rel_append2)
apply (rule_tac x=cs in exI)
apply (rule_tac x=xs in exI)
apply (rule_tac x=x in exI)
apply simp
apply (rule_tac b = ‹ysa@zs› in relcompI)
apply (auto dest!: split_list simp: list_rel_split_right_iff list_rel_append1 list_rel_split_left_iff
list_rel_append2)
by (metis add_mset_remove_trivial mset_remove1 multi_self_add_other_not_self remove1_idem)
subgoal
apply (auto dest!: split_list simp: list_rel_split_right_iff list_rel_append1 list_rel_split_left_iff
list_rel_append2)
apply (rule_tac b = ‹cs@aa#ds› in relcompI)
apply (auto dest!: split_list simp: list_rel_split_right_iff list_rel_append1 list_rel_split_left_iff
list_rel_append2)
done
done
lemma (in -) sorted_poly_rel_vars_llist2:
‹(pa, r) ∈ sorted_poly_rel ⟹ (vars_llist pa) = ⋃ (set_mset ` fst ` set_mset r)›
apply (auto split: if_splits simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def list_rel_append1
list_rel_append2 list_rel_split_right_iff term_poly_list_rel_set_mset vars_llist_def image_Un
term_poly_list_rel_def
add_nset_list_rel_add_mset_iff dest!: split_list)
apply (auto simp: list_rel_split_left_iff)
done
lemma (in -)normalize_poly_p_vars: ‹normalize_poly_p p q ⟹ ⋃ (set_mset ` fst ` set_mset q) ⊆ ⋃ (set_mset ` fst ` set_mset p)›
by (induction rule: normalize_poly_p.induct)
auto
lemma (in -)rtranclp_normalize_poly_p_vars: ‹normalize_poly_p⇧*⇧* p q ⟹ ⋃ (set_mset ` fst ` set_mset q) ⊆ ⋃ (set_mset ` fst ` set_mset p)›
by (induction rule: rtranclp_induct)
(force dest!: normalize_poly_p_vars)+
lemma normalize_poly_normalize_poly_p2:
assumes ‹(p, p') ∈ unsorted_poly_rel›
shows ‹normalize_poly p ≤ ⇓{(xs,ys). (xs,ys)∈sorted_poly_rel ∧ vars_llist xs ⊆ vars_llist p} (SPEC (λr. normalize_poly_p⇧*⇧* p' r))›
proof -
have 1: ‹sort_poly_spec p ≤ SPEC (λp'. vars_llist p' = vars_llist p)›
unfolding sort_poly_spec_def vars_llist_def
by (auto dest: mset_eq_setD)
have [refine]: ‹sort_poly_spec p ≤ ⇓{(xs,ys). (xs,ys)∈sorted_repeat_poly_list_rel (rel2p (Id ∪ term_order_rel)) ∧
vars_llist xs ⊆ vars_llist p} (RETURN p')›
using sort_poly_spec_id[OF assms] apply -
apply (rule order_trans)
apply (rule SPEC_rule_conjI[OF 1])
unfolding RETURN_def
apply (subst (asm) conc_fun_RES)
apply (subst (asm) RES_SPEC_eq)
apply assumption
apply (auto simp: conc_fun_RES)
done
have 1: ‹SPEC (λr. normalize_poly_p⇧*⇧* p' r) = do {
p'' ← RETURN p';
ASSERT(p'' = p');
SPEC (λr. normalize_poly_p⇧*⇧* p'' r)
}›
by auto
show ?thesis
unfolding normalize_poly_def
apply (subst 1)
apply (refine_rcg)
subgoal for pa p'
by (force intro!: RES_refine simp: RETURN_def dest: vars_llist_merge_coeffsD sorted_poly_rel_vars_llist2
merge_coeffs_is_normalize_poly_p
subsetD vars_llist_merge_coeffsD)
done
qed
lemma (in -)vars_llist_mult_poly_raw: ‹vars_llist (mult_poly_raw p q) ⊆ vars_llist p ∪ vars_llist q›
proof -
have [simp]: ‹foldl (λb x. map (mult_monomials x) qs @ b) b ps = foldl (λb x. map (mult_monomials x) qs @ b) [] ps @ b›
if ‹NO_MATCH [] b› for qs ps b
by (induction ps arbitrary: b)
(simp, metis (no_types, lifting) append_assoc foldl_Cons self_append_conv)
have [simp]: ‹x ∈ set (mult_monoms a aa) ⟷ x ∈ set a ∨ x ∈ set aa› for x a aa
by (induction a aa rule: mult_monoms.induct)
(auto split: if_splits)
have 0: ‹vars_llist (map (mult_monomials (a, ba)) q) ⊆ vars_llist q ∪ set a› for a ba q
unfolding mult_monomials_def
by (induction q) auto
have ‹vars_llist (foldl (λb x. map (mult_monomials x) q @ b) [] p) ⊆ vars_llist p ∪ vars_llist q ∪ vars_llist b› for b
by (induction p) (use 0 in force)+
then show ?thesis
unfolding mult_poly_raw_def
by auto
qed
lemma mult_poly_full_mult_poly_p'2:
assumes ‹(p, p') ∈ sorted_poly_rel› ‹(q, q') ∈ sorted_poly_rel›
shows ‹mult_poly_full p q ≤ ⇓ {(xs,ys). (xs,ys)∈sorted_poly_rel ∧ vars_llist xs ⊆ vars_llist p ∪ vars_llist q} (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_p2[THEN order_trans])
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)])
apply assumption
subgoal
using vars_llist_mult_poly_raw[of p q]
unfolding conc_fun_RES
by auto
done
lemma mult_poly_full_spec2:
assumes
‹(p, p'') ∈ sorted_poly_rel O mset_poly_rel› and
‹(q, q'') ∈ sorted_poly_rel O mset_poly_rel›
shows
‹mult_poly_full p q ≤ ⇓{(xs,ys). (xs,ys)∈sorted_poly_rel O mset_poly_rel ∧ vars_llist xs ⊆ vars_llist p ∪ vars_llist q}
(SPEC (λs. s - p'' * q'' ∈ ideal polynomial_bool))›
proof -
have 1: ‹{(xs, ys). (xs, ys) ∈ sorted_poly_rel O mset_poly_rel ∧ vars_llist xs ⊆ vars_llist p ∪ vars_llist q} =
{(xs, ys). (xs, ys) ∈ sorted_poly_rel ∧ vars_llist xs ⊆ vars_llist p ∪ vars_llist q} O{(xs, ys). (xs, ys) ∈ mset_poly_rel}›
by blast
obtain p' q' where
pq: ‹(p, p') ∈ sorted_poly_rel›
‹(p', p'') ∈ mset_poly_rel›
‹(q, q') ∈ sorted_poly_rel›
‹(q', q'') ∈ mset_poly_rel›
using assms by auto
show ?thesis
apply (rule mult_poly_full_mult_poly_p'2[THEN order_trans, OF pq(1,3)])
apply (subst 1)
apply (subst conc_fun_chain[symmetric])
apply (rule ref_two_step')
unfolding mult_poly_p'_def
apply refine_vcg
by (use pq assms in ‹auto simp: mult_poly_p'_def mset_poly_rel_def
dest!: rtranclp_normalize_poly_p_poly_of_mset rtranclp_mult_poly_p_mult_ideal_final
intro!: RES_refine›)
qed
lemma mult_poly_full_mult_poly_spec:
assumes ‹(p, p') ∈ sorted_poly_rel O mset_poly_rel› ‹(q, q') ∈ sorted_poly_rel O mset_poly_rel›
shows ‹mult_poly_full p q ≤ ⇓ {(xs,ys). (xs,ys)∈sorted_poly_rel O mset_poly_rel ∧ vars_llist xs ⊆ vars_llist p ∪ vars_llist q} (mult_poly_spec p' q')›
apply (rule mult_poly_full_spec2[OF assms, THEN order_trans])
apply (rule ref_two_step')
by (auto simp: mult_poly_spec_def dest: ideal.span_neg)
lemma vars_llist_merge_coeff0: ‹vars_llist (merge_coeffs0 paa) ⊆ vars_llist paa›
by (induction paa rule: merge_coeffs0.induct)
auto
lemma sort_poly_spec_id'2:
assumes ‹(p, p') ∈ unsorted_poly_rel_with0›
shows ‹sort_poly_spec p ≤ ⇓ {(xs, ys). (xs, ys) ∈ sorted_repeat_poly_rel_with0 ∧
vars_llist xs ⊆ vars_llist p} (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 -
obtain f where
f: ‹bij_betw f {..<length x} {..<length p}› and
[simp]: ‹⋀i. i<length x ⟹ x ! i = p ! (f i)›
using px apply - apply (subst (asm)(2) eq_commute) unfolding mset_eq_perm
by (auto dest!: permutation_Ex_bij)
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 simp: vars_llist_def dest: mset_eq_setD)
qed
lemma sort_all_coeffs_unsorted_poly_rel_with02:
assumes ‹(p, p') ∈ fully_unsorted_poly_rel›
shows ‹sort_all_coeffs p ≤ ⇓ {(xs, ys). (xs, ys) ∈ unsorted_poly_rel_with0 ∧ vars_llist xs ⊆ vars_llist p} (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)
have vars_llits_alt_def:
‹x ∈ vars_llist p ⟷ x ∈ ⋃(set_mset ` fst ` set (map (λ(a, y). (mset a, y)) (rev p)))› for p x
by (force simp: vars_llist_def)
have [intro]: ‹map (λ(a, y). (mset a, y)) (rev p) = map (λ(a, y). (mset a, y)) s ⟹
x ∈ vars_llist s ⟹ x ∈ vars_llist p› for s x
unfolding vars_llits_alt_def
by (auto simp: vars_llist_def image_image dest!: split_list)
show ?thesis
by (rule sort_all_coeffs[THEN order_trans])
(use assms in ‹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 1 2
intro!: relcompI[of _ ‹map (λ(a, y). (mset a, y)) (rev p)›]›)
qed
lemma full_normalize_poly_normalize_poly_p2:
assumes ‹(p, p') ∈ fully_unsorted_poly_rel›
shows ‹full_normalize_poly p ≤ ⇓ {(xs, ys). (xs, ys) ∈ sorted_poly_rel ∧ vars_llist xs ⊆ vars_llist p}
(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(λq. (q, p') ∈ {(xs, ys). (xs, ys) ∈ unsorted_poly_rel_with0∧ vars_llist xs ⊆ vars_llist p})›
by (rule sort_all_coeffs_unsorted_poly_rel_with02[OF assms, THEN order_trans])
(auto simp: conc_fun_RES RETURN_def)
have [refine0]: ‹sort_poly_spec p ≤ SPEC (λc. (c, p') ∈
{(xs, ys). (xs, ys) ∈ sorted_repeat_poly_rel_with0 ∧ vars_llist xs ⊆ vars_llist p})›
if ‹(p, p') ∈ unsorted_poly_rel_with0›
for p p'
by (rule sort_poly_spec_id'2[THEN order_trans, OF that])
(auto simp: conc_fun_RES RETURN_def)
show ?thesis
apply (subst 1)
unfolding full_normalize_poly_def
apply (refine_rcg)
by (use in ‹auto intro!: RES_refine
dest!: merge_coeffs0_is_normalize_poly_p
dest!: set_mp[OF vars_llist_merge_coeff0]
simp: RETURN_def›)
qed
lemma add_poly_full_spec:
assumes
‹(p, p'') ∈ sorted_poly_rel O mset_poly_rel› and
‹(q, q'') ∈ sorted_poly_rel O mset_poly_rel›
shows
‹add_poly_l (p, q) ≤ ⇓(sorted_poly_rel O mset_poly_rel)
(SPEC (λs. s - (p'' + q'' )∈ ideal polynomial_bool))›
proof -
obtain p' q' where
pq: ‹(p, p') ∈ sorted_poly_rel›
‹(p', p'') ∈ mset_poly_rel›
‹(q, q') ∈ sorted_poly_rel›
‹(q', q'') ∈ mset_poly_rel›
using assms by auto
show ?thesis
apply (rule add_poly_l_add_poly_p'[THEN order_trans, OF pq(1,3)])
apply (subst conc_fun_chain[symmetric])
apply (rule ref_two_step')
by (use pq assms in ‹clarsimp simp: add_poly_p'_def mset_poly_rel_def ideal.span_zero
dest!: rtranclp_add_poly_p_polynomial_of_mset_full
intro!: RES_refine›)
qed
lemma (in -)add_poly_l_simps:
‹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)
}))›
apply (subst add_poly_l_def)
apply (subst RECT_unfold, refine_mono)
apply (subst add_poly_l_def[symmetric, abs_def])+
apply auto
done
lemma nat_less_induct_useful:
assumes ‹P 0›‹(⋀m. (∀n < Suc m. P n) ⟹ P (Suc m))›
shows ‹P m›
using assms
apply(induction m rule: nat_less_induct)
apply (case_tac n)
apply auto
done
lemma add_poly_l_vars: ‹add_poly_l (p, q) ≤ SPEC(λxa. vars_llist xa ⊆ vars_llist p ∪ vars_llist q)›
apply (induction "length p + length q" arbitrary: p q rule: nat_less_induct_useful)
subgoal
apply (subst add_poly_l_simps)
apply (auto split: list.splits)
done
subgoal premises p for n p q
using p(1)[rule_format, of n ‹tl p› q]
using p(1) [rule_format, of n p ‹tl q›] p(1)[rule_format, of ‹n-1› ‹tl p› ‹tl q›]
using p(2-)
apply (subst add_poly_l_simps)
apply (case_tac p)
subgoal by (auto split: list.splits)
subgoal
apply (simp split: prod.splits list.splits if_splits)
apply (intro conjI impI allI)
apply (auto intro: order_trans intro!: Refine_Basic.bind_rule)
apply (rule order_trans, assumption, auto)+
done
done
done
lemma pw_le_SPEC_merge: ‹f ≤ ⇓R g ⟹ f ≤ RES Φ ⟹ f ≤⇓{(x,y). (x,y)∈R ∧ x ∈ Φ} g›
by (simp add: pw_conc_inres pw_conc_nofail pw_le_iff)
lemma add_poly_l_add_poly_p'2:
assumes ‹(p, p') ∈ sorted_poly_rel› ‹(q, q') ∈ sorted_poly_rel›
shows ‹add_poly_l (p, q) ≤ ⇓ {(xs,ys). (xs,ys) ∈ sorted_poly_rel ∧ vars_llist xs ⊆ vars_llist p ∪ vars_llist q} (add_poly_p' p' q')›
unfolding add_poly_p'_def
apply (rule pw_le_SPEC_merge[THEN order_trans])
apply (rule add_poly_l_spec[THEN fref_to_Down_curry_right, of _ p' q'])
using assms apply auto[2]
apply (rule add_poly_l_vars)
apply (auto simp: conc_fun_RES)
done
lemma add_poly_full_spec2:
assumes
‹(p, p'') ∈ sorted_poly_rel O mset_poly_rel› and
‹(q, q'') ∈ sorted_poly_rel O mset_poly_rel›
shows
‹add_poly_l (p, q) ≤ ⇓ {(xs,ys). (xs,ys) ∈ sorted_poly_rel O mset_poly_rel ∧ vars_llist xs ⊆ vars_llist p ∪ vars_llist q}
(SPEC (λs. s - (p'' + q'' )∈ ideal polynomial_bool))›
proof -
obtain p' q' where
pq: ‹(p, p') ∈ sorted_poly_rel›
‹(p', p'') ∈ mset_poly_rel›
‹(q, q') ∈ sorted_poly_rel›
‹(q', q'') ∈ mset_poly_rel›
using assms by auto
have 1: ‹{(xs, ys). (xs, ys) ∈ sorted_poly_rel O mset_poly_rel ∧ vars_llist xs ⊆ vars_llist p ∪ vars_llist q} =
{(xs, ys). (xs, ys) ∈ sorted_poly_rel ∧ vars_llist xs ⊆ vars_llist p ∪ vars_llist q} O mset_poly_rel›
by blast
show ?thesis
apply (rule add_poly_l_add_poly_p'2[THEN order_trans, OF pq(1,3)])
apply (subst 1, subst conc_fun_chain[symmetric])
apply (rule ref_two_step')
by (use pq assms in ‹clarsimp simp: add_poly_p'_def mset_poly_rel_def ideal.span_zero
dest!: rtranclp_add_poly_p_polynomial_of_mset_full
intro!: RES_refine›)
qed
lemma add_poly_full_spec3:
assumes
‹(p, p'') ∈ sorted_poly_rel O mset_poly_rel› and
‹(q, q'') ∈ sorted_poly_rel O mset_poly_rel›
shows
‹add_poly_l (p, q) ≤ ⇓ {(xs,ys). (xs,ys) ∈ sorted_poly_rel O mset_poly_rel ∧ vars_llist xs ⊆ vars_llist p ∪ vars_llist q}
(add_poly_spec p'' q'')›
apply (rule add_poly_full_spec2[OF assms, THEN order_trans])
apply (rule ref_two_step')
apply (auto simp: add_poly_spec_def dest: ideal.span_neg)
done
lemma full_normalize_poly_full_spec2:
assumes
‹(p, p'') ∈ fully_unsorted_poly_rel O mset_poly_rel›
shows
‹full_normalize_poly p ≤ ⇓{(xs, ys). (xs, ys) ∈ sorted_poly_rel O mset_poly_rel ∧ vars_llist xs ⊆ vars_llist p}
(SPEC (λs. s - (p'')∈ ideal polynomial_bool ∧ vars s ⊆ vars p''))›
proof -
obtain p' where
pq: ‹(p, p') ∈ fully_unsorted_poly_rel›
‹(p', p'') ∈ mset_poly_rel›
using assms by auto
have 1: ‹⇓ {(xs, ys). (xs, ys) ∈ sorted_poly_rel O mset_poly_rel ∧ vars_llist xs ⊆ vars_llist p} =
⇓ ({(xs, ys). (xs, ys) ∈ sorted_poly_rel ∧ vars_llist xs ⊆ vars_llist p} O mset_poly_rel)›
by (rule cong[of ‹λu. ⇓u›]) auto
show ?thesis
apply (rule full_normalize_poly_normalize_poly_p2[THEN order_trans, OF pq(1)])
apply (subst 1)
apply (subst conc_fun_chain[symmetric])
apply (rule ref_two_step')
by (use pq assms in ‹clarsimp simp: add_poly_p'_def mset_poly_rel_def ideal.span_zero
ideal.span_zero rtranclp_normalize_poly_p_poly_of_mset
dest!: rtranclp_add_poly_p_polynomial_of_mset_full
intro!: RES_refine›)
qed
lemma (in -) add_poly_l_simps_empty[simp]: ‹add_poly_l ([], a) = RETURN a›
by (subst add_poly_l_simps, cases a) auto
definition term_rel :: ‹_› where
‹term_rel = sorted_poly_rel O mset_poly_rel›
definition raw_term_rel where
‹raw_term_rel = fully_unsorted_poly_rel O mset_poly_rel›
fun (in -)insort_wrt :: ‹('a ⇒ 'b) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ 'a ⇒ 'a list ⇒ 'a list› where
‹insort_wrt _ _ a [] = [a]› |
‹insort_wrt f P a (x # xs) =
(if P (f a) (f x) then a # x # xs else x # insort_wrt f P a xs)›
lemma (in -)set_insort_wrt [simp]: ‹set (insort_wrt P f a xs) = insert a (set xs)›
by (induction P f a xs rule: insort_wrt.induct) auto
lemma (in -)sorted_insort_wrt:
‹transp P ⟹ total (p2rel P) ⟹ sorted_wrt (λa b. P (f a) (f b)) xs ⟹ reflp_on P (f ` set (a # xs)) ⟹
sorted_wrt (λa b. P (f a) (f b)) (insort_wrt f P a xs)›
apply (induction f P a xs rule: insort_wrt.induct)
subgoal by auto
subgoal for f P a x xs
apply (cases ‹x=a›)
apply (auto simp: Relation.total_on_def p2rel_def reflp_on_def dest: transpD sympD reflpD elim: reflpE)+
apply (force simp: Relation.total_on_def p2rel_def reflp_on_def dest: transpD sympD reflpD elim: reflpE)+
done
done
lemma (in -)sorted_insort_wrt3:
‹transp P ⟹ total (p2rel P) ⟹ sorted_wrt (λa b. P (f a) (f b)) xs ⟹ f a∉f ` set xs ⟹
sorted_wrt (λa b. P (f a) (f b)) (insort_wrt f P a xs)›
apply (induction f P a xs rule: insort_wrt.induct)
subgoal by auto
subgoal for f P a x xs
apply (cases ‹x=a›)
apply (auto simp: Relation.total_on_def p2rel_def reflp_on_def dest: transpD sympD reflpD elim: reflpE)
done
done
lemma (in -)sorted_insort_wrt4:
‹transp P ⟹ total (p2rel P) ⟹ f a∉f ` set xs ⟹ sorted_wrt (λa b. P (f a) (f b)) xs ⟹ f'=(λa b. P (f a) (f b)) ⟹
sorted_wrt f' (insort_wrt f P a xs)›
using sorted_insort_wrt3[of P f xs a] by auto
text ‹When \<^term>‹a› is empty, constants are added up.›
lemma add_poly_p_insort:
‹fst a ≠ [] ⟹ vars_llist [a] ∩ vars_llist b = {} ⟹ add_poly_l ([a],b) = RETURN (insort_wrt fst term_order a b)›
apply (induction b)
subgoal
by (subst add_poly_l_simps) auto
subgoal for y ys
apply (cases a, cases y)
apply (subst add_poly_l_simps)
apply (auto simp: rel2p_def Int_Un_distrib)
done
done
lemma (in -) map_insort_wrt: ‹map f (insort_wrt f P x xs) = insort_wrt id P (f x) (map f xs)›
by (induction xs)
auto
lemma (in-) distinct_insort_wrt[simp]: ‹distinct (insort_wrt f P x xs) ⟷ distinct (x # xs)›
by (induction xs) auto
lemma (in -) mset_insort_wrt[simp]: ‹mset (insort_wrt f P x xs) = add_mset x (mset xs)›
by (induction xs)
auto
lemma (in -) transp_term_order_rel: ‹transp (λx y. (fst x, fst y) ∈ term_order_rel)›
apply (auto simp: transp_def)
by (smt lexord_partial_trans lexord_trans trans_less_than_char var_order_rel_def)
lemma (in -) transp_term_order: ‹transp term_order›
using transp_term_order_rel
by (auto simp: transp_def rel2p_def)
lemma total_term_order_rel: ‹total (term_order_rel)›
apply standard
using total_on_lexord_less_than_char_linear[unfolded var_order_rel_def[symmetric]] by (auto simp: p2rel_def intro!: )
lemma monomom_rel_mapI: ‹sorted_wrt (λx y. (fst x, fst y) ∈ term_order_rel) r ⟹
distinct (map fst r) ⟹
(∀x∈set r. distinct (fst x) ∧ sorted_wrt var_order (fst x)) ⟹
(r, map (λ(a, y). (mset a, y)) r) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel›
apply (induction r)
subgoal
by auto
subgoal for x xs
apply (cases x)
apply (auto simp: term_poly_list_rel_def rel2p_def)
done
done
lemma add_poly_l_single_new_var:
assumes ‹(r, ra) ∈ sorted_poly_rel O mset_poly_rel› and
‹v ∉ vars_llist r› and
v: ‹(v, v') ∈ var_rel›
shows
‹add_poly_l ([([v], -1)], r)
≤ ⇓ {(a,b). (a,b)∈sorted_poly_rel O mset_poly_rel ∧ vars_llist a ⊆ insert v (vars_llist r)}
(SPEC
(λr0. r0 = ra - Var v' ∧
vars r0 = vars ra ∪ {v'}))›
proof -
have [simp]: ‹([], ra) ∈ term_rel ⟹ ([([v], - 1)], ra - Var v') ∈ term_rel› for ra
using v
apply (auto intro!: RETURN_RES_refine relcompI[of _ ‹mset [(mset [v], -1)]›]
simp: mset_poly_rel_def var_rel_def br_def Const_1_eq_1 term_rel_def)
apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def
term_poly_list_rel_def
intro!: relcompI[of _ ‹[(mset [v], -1)]›])
done
have [iff]: ‹v' ∉ vars ra›
proof (rule ccontr)
assume H: ‹¬?thesis›
then have ‹φ v ∈ φ ` vars_llist r›
using assms sorted_poly_rel_vars_llist[OF assms(1)]
by (auto simp: var_rel_def br_def)
then have ‹v ∈ vars_llist r›
using φ_inj by (auto simp: image_iff inj_def)
then show ‹False›
using assms(2) by fast
qed
have [simp]: ‹([], ra) ∈ term_rel ⟹ vars (ra - Var v') = vars (ra) ∪ {v'}› for ra
by (auto simp: term_rel_def mset_poly_rel_def)
have [simp]: ‹v' ∉ vars ra ⟹ vars (ra - Var v') = vars ra ∪ {v'}›
by (auto simp add: vars_subst_in_left_only_diff_iff)
have [iff]: ‹([v], b) ∉ set r › for b
using assms
by (auto simp: vars_llist_def)
have
‹add_poly_l ([([v], -1)], r)
≤ ⇓ (sorted_poly_rel O mset_poly_rel)
(SPEC
(λr0. r0 = ra - Var v' ∧
vars r0 = vars ra ∪ {v'}))›
using v sorted_poly_rel_vars_llist[OF assms(1)]
apply -
apply (subst add_poly_p_insort)
apply (use assms in auto)
apply (rule RETURN_RES_refine)
apply auto
apply (rule_tac b=‹add_mset ({#v#}, -1) (y)› in relcompI)
apply (auto simp: rel2p_def mset_poly_rel_def Const_1_eq_1 var_rel_def br_def)
apply (auto simp: sorted_poly_list_rel_wrt_def sorted_wrt_map)
apply (rule_tac b = ‹map (λ(a,b). (mset a, b)) ((insort_wrt fst term_order ([v], - 1) r))› in relcompI)
apply (auto simp: list_mset_rel_def br_def map_insort_wrt)
prefer 2
apply (auto dest!: term_poly_list_rel_list_relD)[]
prefer 2
apply (auto intro!: sorted_insort_wrt4 monomom_rel_mapI simp: rel2p_def transp_term_order total_term_order_rel
transp_term_order_rel map_insort_wrt)
apply (auto dest!: split_list simp: list_rel_append1 list_rel_split_right_iff
term_poly_list_rel_def)
done
then show ?thesis
using add_poly_l_vars[of ‹[([v], - 1)]› r]
unfolding conc_fun_RES
apply (subst (asm) RES_SPEC_eq)
apply (rule order_trans)
apply (rule SPEC_rule_conjI)
apply assumption
apply auto
done
qed
lemma empty_sorted_poly_rel[simp,intro]: ‹ ([], 0) ∈ sorted_poly_rel O mset_poly_rel›
by (auto intro!: relcompI[of ‹[]›] simp: mset_poly_rel_def)
abbreviation epac_step_rel where
‹epac_step_rel ≡ p2rel (⟨Id, fully_unsorted_poly_rel O mset_poly_rel, var_rel⟩ pac_step_rel_raw)›
lemma single_valued_monomials: ‹single_valued (⟨term_poly_list_rel ×⇩r int_rel⟩list_rel)›
by (intro single_valued_relcomp list_rel_sv)
(auto simp: mset_poly_rel_def sorted_poly_list_rel_wrt_def list_mset_rel_def br_def
single_valued_def term_poly_list_rel_def)
lemma single_valued_term: ‹single_valued (sorted_poly_rel O mset_poly_rel) ›
using single_valued_monomials apply -
by (rule single_valued_relcomp)
(auto simp: mset_poly_rel_def sorted_poly_list_rel_wrt_def list_mset_rel_def br_def
single_valued_def )
lemma single_valued_poly:
‹(ysa, cs) ∈ ⟨sorted_poly_rel O mset_poly_rel ×⇩r nat_rel⟩list_rel ⟹
(ysa, csa) ∈ ⟨sorted_poly_rel O mset_poly_rel ×⇩r nat_rel⟩list_rel ⟹
cs = csa›
using list_rel_sv[of ‹sorted_poly_rel O mset_poly_rel ×⇩r nat_rel›, OF prod_rel_sv[OF single_valued_term]]
by (auto simp: single_valued_def)
lemma check_linear_combi_l_check_linear_comb:
assumes ‹(A, B) ∈ fmap_polys_rel› and ‹(r, r') ∈ sorted_poly_rel O mset_poly_rel›
‹(i, i') ∈ nat_rel›
‹(𝒱', 𝒱) ∈ ⟨var_rel⟩set_rel› and
xs: ‹(xs, xs') ∈ ⟨(fully_unsorted_poly_rel O mset_poly_rel) ×⇩r nat_rel⟩list_rel› and
A: ‹⋀i. i ∈# dom_m A ⟹ vars_llist (the (fmlookup A i)) ⊆ 𝒱'›
shows
‹check_linear_combi_l spec A 𝒱' i xs r ≤ ⇓ {(st, b). (¬is_cfailed st ⟷ b) ∧
(is_cfound st ⟶ spec = r) ∧ (b ⟶ vars_llist r ⊆ 𝒱' ∧ i ∉# dom_m A)} (check_linear_comb B 𝒱 xs' i' r')›
proof -
have 𝒱: ‹𝒱 = φ`𝒱'›
using assms(4) unfolding set_rel_def var_rel_def
by (auto simp: br_def)
define f where
‹f = (λys::((char list list × int) list × nat) list.
(∀x ∈ set (take (length ys) xs'). snd x ∈# dom_m B ∧ vars (fst x) ⊆ 𝒱))›
let ?I = ‹λ(p, xs'', err). ¬is_cfailed err ⟶
(∃r ys. (p, r) ∈ sorted_poly_rel O mset_poly_rel ∧ f ys ∧ vars_llist p ⊆ 𝒱' ∧
(∑(p,n) ∈# mset (take (length ys) xs'). the (fmlookup B n) * p) - r ∈ ideal polynomial_bool ∧ xs = ys @ xs'' ∧
(xs'', drop (length ys) xs') ∈ ⟨(fully_unsorted_poly_rel O mset_poly_rel) ×⇩r nat_rel⟩list_rel)›
have [simp]: ‹length xs = length xs'›
using xs by (auto simp: list_rel_imp_same_length)
have [simp]: ‹drop (length ysa) xs' = cs @ (b) # ysb ⟹ length ysa < length xs'› for ysa cs b ysb
by (rule ccontr) auto
have Hf2: ‹(∑(p, n)←cs. the (fmlookup B n) * p) + the (fmlookup B bb) * ad - xf ∈ More_Modules.ideal polynomial_bool›
if 1: ‹(∑(p, n)←cs. the (fmlookup B n) * p) - r ∈ More_Modules.ideal polynomial_bool› and
2: ‹xd - xb * the (fmlookup B bb) ∈ More_Modules.ideal polynomial_bool› and
3: ‹xb - ad ∈ More_Modules.ideal polynomial_bool› and
4: ‹xf - (r + xd) ∈ More_Modules.ideal polynomial_bool›
for a ba bb r ys cs ysa ad ysc x y xa xb xc xd xe xf
proof -
have 2: ‹xd - ad * the (fmlookup B bb) ∈ More_Modules.ideal polynomial_bool›
using 2 3
by (smt diff_add_eq group_eq_aux ideal.scale_left_diff_distrib ideal.span_add_eq
ideal_mult_right_in)
note two = ideal.span_neg[OF 2]
note 4 = ideal.span_neg[OF 4]
note 5 = ideal.span_add[OF 1 two, simplified]
note 6 = ideal.span_add[OF 4 5]
show ?thesis
using 6 by (auto simp: algebra_simps)
qed
have Hf2': ‹(∑(p, n)←cs. the (fmlookup B n) * p) + the (fmlookup B bb) - xf ∈ More_Modules.ideal polynomial_bool›
if 1: ‹(∑(p, n)←cs. the (fmlookup B n) * p) - r ∈ More_Modules.ideal polynomial_bool› and
2: ‹xd - the (fmlookup B bb) ∈ More_Modules.ideal polynomial_bool› and
4: ‹xf - (r + xd) ∈ More_Modules.ideal polynomial_bool›
for a ba bb r ys cs ysa ad ysc x y xa xb xc xd xe xf
using Hf2[of cs r xd 1 bb 1 xf] that by (auto simp: ideal.span_zero)
have [dest!]: ‹([([], 1)], ad) ∈ raw_term_rel ⟹ ad = 1› for ad
by (auto simp: raw_term_rel_def fully_unsorted_poly_list_rel_def list_mset_rel_def Const_1_eq_1
br_def list_rel_split_right_iff unsorted_term_poly_list_rel_def mset_poly_rel_def)
have H[simp]: ‹length ys < length xs ⟹
i < length xs' - length ys ⟷ (i < length xs' - Suc (length ys) ∨ i = length xs' - length ys - 1)› for ys i
by auto
have lin: ‹linear_combi_l i' A 𝒱' xs ≤ ⇓ {((p, xs, err), (b, p')). (¬b ⟶ is_cfailed err) ∧
(b ⟶(p, p') ∈ sorted_poly_rel O mset_poly_rel)}
(SPEC(λ(b, r). b ⟶ ((∀i ∈ set xs'. snd i ∈# dom_m B ∧ vars (fst i) ⊆ 𝒱) ∧
(∑(p,n) ∈# mset xs'. the (fmlookup B n) * p) - r ∈ ideal polynomial_bool)))›
using assms(1) xs
unfolding linear_combi_l_def conc_fun_RES check_linear_combi_l_dom_err_def term_rel_def[symmetric]
raw_term_rel_def[symmetric] error_msg_def in_dom_m_lookup_iff[symmetric] apply -
apply (rule ASSERT_leI)
subgoal using assms unfolding linear_combi_l_pre_def by blast
apply (subst (2) RES_SPEC_eq)
apply (rule WHILET_rule[where R = ‹measure (λ(_, xs, p). if is_cfailed p then 0 else Suc (length xs))›
and I = ‹?I›])
subgoal by auto
subgoal using xs by (auto 5 5 intro!: exI[of _ 0] intro: exI[of _xs] exI[of _ ‹[]›] ideal.span_zero simp: f_def)
subgoal for s
unfolding term_rel_def[symmetric]
apply (refine_vcg full_normalize_poly_full_spec2[THEN order_trans, unfolded term_rel_def[symmetric]
raw_term_rel_def[symmetric]])
subgoal
by clarsimp
subgoal using xs by auto
subgoal
by (clarsimp simp: list_rel_split_right_iff list_rel_append1 neq_Nil_conv list_rel_imp_same_length)
subgoal
by (clarsimp simp: list_rel_split_right_iff list_rel_append1 neq_Nil_conv list_rel_imp_same_length)
apply ((use assms(6) in ‹solves auto›)+)[2]
subgoal for a b aa ba ab bb
apply (cases aa; cases b)
apply (simp only: prod.simps; clarify)
apply (simp only: prod.simps; clarify)
subgoal for ac bc list aaa baa r ys
using param_nth[of ‹length ys› xs' ‹length ys› xs ‹raw_term_rel ×⇩r nat_rel›]
apply (cases ‹xs' ! length ys›)
apply (auto intro!: add_poly_full_spec2[THEN order_trans, unfolded term_rel_def[symmetric]
raw_term_rel_def[symmetric]] simp: conc_fun_RES)
apply (rule_tac x=ysa in exI)
apply auto
apply (auto simp: f_def take_Suc_conv_app_nth list_rel_imp_same_length[symmetric] single_valued_poly)
apply (auto dest!: sorted_poly_rel_vars_llist[unfolded term_rel_def[symmetric]]
fully_unsorted_poly_rel_vars_subset_vars_llist[unfolded raw_term_rel_def[symmetric]]
simp: 𝒱 ideal.span_zero list_rel_append1 list_rel_split_right_iff
list_rel_imp_same_length
intro!: Hf2')
done
done
apply (clarsimp simp: list_rel_split_right_iff list_rel_append1 neq_Nil_conv list_rel_imp_same_length)
apply (rule_tac P = ‹(x, fst (hd (drop (length xs' - length (fst (snd s))) xs'))) ∈ raw_term_rel› in TrueE)
apply (auto simp: list_rel_imp_same_length)[2]
apply (clarsimp simp: list_rel_split_right_iff list_rel_append1 neq_Nil_conv list_rel_imp_same_length)
apply (auto simp: conc_fun_RES)
apply refine_vcg
subgoal for a ba bb r ys cs ysa ad ysc x y xa xb
by auto
apply (rule mult_poly_full_spec2[THEN order_trans, unfolded term_rel_def[symmetric]])
apply assumption
apply auto
unfolding conc_fun_RES
apply auto
apply refine_vcg
subgoal using A by simp blast
apply (rule add_poly_full_spec2[THEN order_trans, unfolded term_rel_def[symmetric]])
apply assumption
apply (auto simp: )
apply (subst conc_fun_RES)
apply clarsimp_all
apply (auto simp: f_def take_Suc_conv_app_nth list_rel_imp_same_length single_valued_poly)
apply (rule_tac x=yse in exI)
apply (auto simp: f_def take_Suc_conv_app_nth list_rel_imp_same_length[symmetric] single_valued_poly)
apply (auto dest!: sorted_poly_rel_vars_llist[unfolded term_rel_def[symmetric]]
fully_unsorted_poly_rel_vars_subset_vars_llist[unfolded raw_term_rel_def[symmetric]]
simp: 𝒱 intro: Hf2)[]
apply (auto intro: Hf2)
apply force
done
subgoal for s
unfolding term_rel_def[symmetric] f_def
apply simp
apply (case_tac ‹is_cfailed (snd (snd s))›; cases s)
apply simp_all
apply (rule_tac x=False in exI)
apply clarsimp_all
apply (rule_tac x=True in exI)
apply clarsimp_all
apply auto
done
done
have [iff]: ‹ xs = [] ⟷ xs' = []›
using list_rel_imp_same_length[OF assms(5)]
by (metis length_0_conv)
show ?thesis
using sorted_poly_rel_vars_llist[OF assms(2)] list_rel_imp_same_length[OF assms(5)]
fmap_rel_nat_rel_dom_m[OF assms(1)] assms(3) assms(2)
unfolding check_linear_combi_l_def check_linear_comb_def check_linear_combi_l_mult_err_def
weak_equality_l_def conc_fun_RES term_rel_def[symmetric] check_linear_combi_l_pre_err_def
error_msg_def apply -
apply simp
apply (refine_vcg lin[THEN order_trans, unfolded term_rel_def[symmetric]])
apply (clarsimp simp add: conc_fun_RES bind_RES_RETURN_eq split: if_splits)
apply (clarsimp simp add: conc_fun_RES bind_RES_RETURN_eq split: if_splits)
apply (clarsimp simp add: conc_fun_RES bind_RES_RETURN_eq split: if_splits)
apply (auto split: if_splits simp: bind_RES_RETURN_eq)
apply (rule lin[THEN order_trans, unfolded term_rel_def[symmetric]])
apply (clarsimp simp add: conc_fun_RES bind_RES_RETURN_eq split: if_splits)
apply (auto 5 3 split: if_splits simp: bind_RES_RETURN_eq 𝒱)
apply (frule single_valuedD[OF single_valued_term[unfolded term_rel_def[symmetric]]])
apply assumption
apply (auto simp: conc_fun_RES)
apply (drule single_valuedD[OF single_valued_term[unfolded term_rel_def[symmetric]]])
apply assumption
apply (auto simp: conc_fun_RES)
apply (rule lin[THEN order_trans, unfolded term_rel_def[symmetric]])
apply (clarsimp simp add: conc_fun_RES bind_RES_RETURN_eq split: if_splits)
apply (auto 5 3 split: if_splits simp: bind_RES_RETURN_eq 𝒱)
apply (drule single_valuedD[OF single_valued_term[unfolded term_rel_def[symmetric]]])
apply assumption
apply (auto simp: conc_fun_RES bind_RES_RETURN_eq)
done
qed
definition remap_polys_with_err :: ‹int mpoly ⇒ int mpoly ⇒ nat set ⇒ (nat, int_poly) fmap ⇒ (status × fpac_step) nres› where
‹remap_polys_with_err spec spec0 = (λ𝒱 A. do{
dom ← SPEC(λdom. set_mset (dom_m A) ⊆ dom ∧ finite dom);
𝒱 ← SPEC(λ𝒱'. 𝒱 ∪ vars spec0 ⊆ 𝒱');
failed ← SPEC(λ_::bool. True);
if failed
then do {
SPEC (λ(mem, _, _). mem = FAILED)
}
else do {
(b, N) ← FOREACH⇩C dom (λ(b, 𝒱, A'). ¬is_failed b)
(λi (b, 𝒱, A').
if i ∈# dom_m A
then do {
ASSERT(¬is_failed b);
err ← RES {FAILED,SUCCESS};
if is_failed err then SPEC(λ(err', 𝒱, A'). err = err')
else do {
p ← SPEC(λp. the (fmlookup A i) - p ∈ ideal polynomial_bool ∧ vars p ⊆ vars (the (fmlookup A i)));
eq ← SPEC(λeq. eq ≠ FAILED ∧ (eq = FOUND ⟶ p = spec));
𝒱 ← SPEC(λ𝒱'. 𝒱 ∪ vars (the (fmlookup A i)) ⊆ 𝒱');
RETURN(merge_status eq err, 𝒱, fmupd i p A')
}
}
else RETURN (b, 𝒱, A'))
(SUCCESS, 𝒱, fmempty);
RETURN (b, N)
}
})›
lemma remap_polys_with_err_spec:
‹remap_polys_with_err spec spec0 𝒱 A ≤ ⇓{(a,(err, 𝒱', A)). a = (err, 𝒱', A) ∧ (¬is_failed err ⟶ vars spec0 ⊆ 𝒱')} (remap_polys_polynomial_bool spec 𝒱 A)›
proof -
have [dest]: ‹set_mset (dom_m x2a) = set_mset (dom_m A) ⟹ dom_m A = dom_m x2a› for x2a
by (simp add: distinct_mset_dom distinct_set_mset_eq_iff)
define I where
[simp]: ‹I = (λdom (b, 𝒱', A'). ¬is_failed b ⟶
(set_mset (dom_m A') = set_mset (dom_m A) - dom ∧
(∀i ∈ set_mset (dom_m A) - dom. the (fmlookup A i) - the (fmlookup A' i) ∈ ideal polynomial_bool) ∧
⋃(vars ` set_mset (ran_m (fmrestrict_set (set_mset (dom_m A')) A))) ⊆ 𝒱' ∧
⋃(vars ` set_mset (ran_m A')) ⊆ 𝒱') ∧
𝒱 ∪ vars spec0 ⊆ 𝒱' ∧
(b = FOUND ⟶ spec ∈# ran_m A'))›
show ?thesis
unfolding remap_polys_with_err_def remap_polys_polynomial_bool_def conc_fun_RES
apply (rewrite at ‹_ ≤ ⌑› RES_SPEC_eq)
apply (refine_vcg FOREACHc_rule[where I = I])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for x xa xb it σ a b aa ba xc xd xe xf
supply[[goals_limit=1]]
by (auto simp add: ran_m_mapsto_upd_notin dom_m_fmrestrict_set' subset_eq)
subgoal
supply[[goals_limit=1]]
by (auto simp add: ran_m_mapsto_upd_notin dom_m_fmrestrict_set' subset_eq)
subgoal
by (auto simp add: ran_m_mapsto_upd_notin dom_m_fmrestrict_set' subset_eq
fmlookup_restrict_set_id')
subgoal for x xa xb it σ a b
by (cases a)
(auto simp add: ran_m_mapsto_upd_notin dom_m_fmrestrict_set' subset_eq
fmlookup_restrict_set_id')
done
qed
definition (in -) remap_polys_l_with_err_pre
:: ‹llist_polynomial ⇒ llist_polynomial ⇒ string set ⇒ (nat, llist_polynomial) fmap ⇒ bool›
where
‹remap_polys_l_with_err_pre spec spec0 𝒱 A ⟷ vars_llist spec ⊆ vars_llist spec0›
definition (in -) remap_polys_l_with_err :: ‹llist_polynomial ⇒ llist_polynomial ⇒ string set ⇒ (nat, llist_polynomial) fmap ⇒
(_ code_status × string set × (nat, llist_polynomial) fmap) nres› where
‹remap_polys_l_with_err spec spec0 = (λ𝒱 A. do{
ASSERT(remap_polys_l_with_err_pre spec spec0 𝒱 A);
dom ← SPEC(λdom. set_mset (dom_m A) ⊆ dom ∧ finite dom);
𝒱 ← RETURN(𝒱 ∪ vars_llist spec0);
failed ← SPEC(λ_::bool. True);
if failed
then do {
c ← remap_polys_l_dom_err;
SPEC (λ(mem, _, _). mem = error_msg (0 :: nat) c)
}
else do {
(err, 𝒱, A) ← FOREACH⇩C dom (λ(err, 𝒱, A'). ¬is_cfailed err)
(λi (err, 𝒱, A').
if i ∈# dom_m A
then do {
err' ← SPEC(λerr. err ≠ CFOUND);
if is_cfailed err' then RETURN((err', 𝒱, A'))
else do {
p ← full_normalize_poly (the (fmlookup A i));
eq ← weak_equality_l p spec;
𝒱 ← RETURN(𝒱 ∪ vars_llist (the (fmlookup A i)));
RETURN((if eq then CFOUND else CSUCCESS), 𝒱, fmupd i p A')
}
} else RETURN (err, 𝒱, A'))
(CSUCCESS, 𝒱, fmempty);
RETURN (err, 𝒱, A)
}})›
lemma sorted_poly_rel_extend_vars:
‹(A, B) ∈ sorted_poly_rel O mset_poly_rel ⟹
(x1c, x1a) ∈ ⟨var_rel⟩set_rel ⟹
RETURN (x1c ∪ vars_llist A)
≤ ⇓ (⟨var_rel⟩set_rel)
(SPEC ((⊆) (x1a ∪ vars (B))))›
using sorted_poly_rel_vars_llist[of A B]
apply (subst RETURN_RES_refine_iff)
apply clarsimp
apply (rule exI[of _ ‹x1a ∪ φ ` vars_llist A›])
apply (auto simp: set_rel_def var_rel_def br_def
dest: fully_unsorted_poly_rel_vars_subset_vars_llist)
done
lemma remap_polys_l_remap_polys:
assumes
AB: ‹(A, B) ∈ ⟨nat_rel, fully_unsorted_poly_rel O mset_poly_rel⟩fmap_rel› and
spec: ‹(spec, spec') ∈ sorted_poly_rel O mset_poly_rel› and
V: ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel› and
‹(spec0, spec0') ∈ fully_unsorted_poly_rel O mset_poly_rel›
‹remap_polys_l_with_err_pre spec spec0 𝒱 A›
shows ‹remap_polys_l_with_err spec spec0 𝒱 A ≤
⇓{(a,b). ¬is_cfailed (fst a) ⟶ (a,b)∈ code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel}
(remap_polys_with_err spec' spec0' 𝒱' B)›
(is ‹_ ≤ ⇓ ?R _›)
proof -
have 1: ‹inj_on id (dom :: nat set)› for dom
by auto
have H: ‹x ∈# dom_m A ⟹
(⋀p. (the (fmlookup A x), p) ∈ fully_unsorted_poly_rel ⟹
(p, the (fmlookup B x)) ∈ mset_poly_rel ⟹ thesis) ⟹
thesis› for x thesis
using fmap_rel_nat_the_fmlookup[OF AB, of x x] fmap_rel_nat_rel_dom_m[OF AB] by auto
have full_normalize_poly: ‹full_normalize_poly (the (fmlookup A x))
≤ ⇓ (sorted_poly_rel O mset_poly_rel)
(SPEC
(λp. the (fmlookup B x') - p ∈ More_Modules.ideal polynomial_bool ∧
vars p ⊆ vars (the (fmlookup B x'))))›
if x_dom: ‹x ∈# dom_m A› and ‹(x, x') ∈ Id› for x x'
apply (rule H[OF x_dom])
subgoal for p
apply (rule full_normalize_poly_normalize_poly_p[THEN order_trans])
apply assumption
subgoal
using that(2) apply -
unfolding conc_fun_chain[symmetric]
by (rule ref_two_step', rule RES_refine)
(auto simp: rtranclp_normalize_poly_p_poly_of_mset
mset_poly_rel_def ideal.span_zero)
done
done
have H': ‹(p, pa) ∈ sorted_poly_rel O mset_poly_rel ⟹
weak_equality_l p spec ≤ ⇓{(b,enn). b = (enn=FOUND)}
(SPEC (λeqa. eqa ≠ FAILED ∧ (eqa = FOUND ⟶ pa = spec')))› for p pa
using spec by (auto simp: weak_equality_l_def weak_equality_spec_def RETURN_def
list_mset_rel_def br_def mset_poly_rel_def intro!: RES_refine
dest: list_rel_term_poly_list_rel_same_rightD sorted_poly_list_relD)
have [refine]: ‹SPEC (λerr. err ≠ CFOUND) ≤ ⇓code_status_status_rel (RES {FAILED, SUCCESS})›
by (auto simp: code_status_status_rel_def intro!: RES_refine)
(case_tac s, auto)
have [intro!]: ‹∃a. (aa, a) ∈ ⟨var_rel⟩set_rel› for aa
by (auto simp: set_rel_def var_rel_def br_def)
have emp: ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel ⟹
((CSUCCESS, 𝒱, fmempty), SUCCESS, 𝒱', fmempty) ∈ code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel› for 𝒱 𝒱'
by auto
show ?thesis
using assms
unfolding remap_polys_l_with_err_def remap_polys_l_dom_err_def
remap_polys_with_err_def prod.case
apply (refine_rcg full_normalize_poly fmap_rel_fmupd_fmap_rel)
subgoal
by auto
apply (rule fully_unsorted_poly_rel_extend_vars)
subgoal
using assms by auto
subgoal
by auto
subgoal
by auto
subgoal
by (auto simp: error_msg_def intro!: RES_refine)
apply (rule 1)
subgoal by auto
apply (rule emp)
subgoal
using V by auto
subgoal by (auto simp: code_status_status_rel_def)
subgoal by auto
subgoal by auto
subgoal by (auto simp: code_status_status_rel_def RETURN_def intro!: RES_refine)
subgoal by auto
apply (rule H')
subgoal by auto
apply (rule fully_unsorted_poly_rel_extend_vars)
subgoal by (auto intro!: fmap_rel_nat_the_fmlookup)
subgoal by (auto intro!: fmap_rel_fmupd_fmap_rel)
subgoal for dom doma failed faileda x it σ x' it' σ' x1 x2 x1a x2a x1b x2b x1c x2c p pa err' err _ _ eqa eqaa 𝒱'' 𝒱'''
by (cases eqaa)
(auto intro!: fmap_rel_fmupd_fmap_rel)
subgoal by (auto simp: code_status_status_rel_def is_cfailed_def)
subgoal by (auto simp: code_status_status_rel_def)
done
qed
end
export_code add_poly_l' in SML module_name test
definition PAC_checker_l where
‹PAC_checker_l spec A b st = do {
(S, _) ← WHILE⇩T
(λ((b, A), n). ¬is_cfailed b ∧ n ≠ [])
(λ((bA), n). do {
ASSERT(n ≠ []);
S ← PAC_checker_l_step spec bA (hd n);
RETURN (S, tl n)
})
((b, A), st);
RETURN S
}›
lemma (in -) keys_mult_monomial2:
‹keys (monomial (n::int) (k::'a ⇒⇩0 nat) * a) = (if n = 0 then {} else ((+) k) ` keys (a))›
proof -
have [simp]: ‹(∑aa. (if k = aa then n else 0) *
(∑q. lookup (a) q when k + xa = aa + q)) =
(∑aa. (if k = aa then n * (∑q. lookup (a) q when k + xa = aa + q) else 0))›
for xa
by (smt Sum_any.cong mult_not_zero)
show ?thesis
apply (auto simp: vars_def times_mpoly.rep_eq Const.rep_eq times_poly_mapping.rep_eq
Const⇩0_def elim!: in_keys_timesE split: if_splits)
apply (auto simp: lookup_monomial_If prod_fun_def
keys_def times_poly_mapping.rep_eq)
done
qed
lemma keys_Const⇩0_mult_left:
‹keys (Const⇩0 (b::int) * aa) = (if b = 0 then {} else keys aa)› for aa :: ‹('a :: {cancel_semigroup_add,monoid_add} ⇒⇩0 nat) ⇒⇩0 _›
by (auto elim!: in_keys_timesE simp: keys_mult_monomial keys_single Const⇩0_def keys_mult_monomial2)
hide_fact (open) poly_embed.PAC_checker_l_PAC_checker
context poly_embed
begin
definition fmap_polys_rel2 where
‹fmap_polys_rel2 err 𝒱 ≡ {(xs, ys). ¬ is_cfailed err ⟶ ((xs, ys) ∈ fmap_polys_rel ∧ (∀i∈#dom_m xs. vars_llist (the (fmlookup xs i)) ⊆ 𝒱))}›
lemma check_del_l_check_del:
‹(A, B) ∈ fmap_polys_rel ⟹ (x3, x3a) ∈ Id ⟹ check_del_l spec A (pac_src1 (Del x3))
≤ ⇓ {(st, b). (¬is_cfailed st ⟷ b) ∧ (b ⟶ st = CSUCCESS)} (check_del B (pac_src1 (Del x3a)))›
unfolding check_del_l_def check_del_def
by (refine_vcg lhs_step_If RETURN_SPEC_refine)
(auto simp: fmap_rel_nat_rel_dom_m bind_RES_RETURN_eq)
lemma check_extension_alt_def:
‹check_extension_precalc A 𝒱 i v p ≥ do {
b ← SPEC(λb. b ⟶ i ∉# dom_m A ∧ v ∉ 𝒱);
if ¬b
then RETURN (False)
else do {
p' ← RETURN (p);
b ← SPEC(λb. b ⟶ vars p' ⊆ 𝒱);
if ¬b
then RETURN (False)
else do {
pq ← mult_poly_spec p' p';
let p' = - p';
p ← add_poly_spec pq p';
eq ← weak_equality p 0;
if eq then RETURN(True)
else RETURN (False)
}
}
}›
proof -
have [intro]: ‹ab ∉ 𝒱 ⟹
vars ba ⊆ 𝒱 ⟹
MPoly_Type.coeff (ba + Var ab) (monomial (Suc 0) ab) = 1› for ab ba
by (subst coeff_add[symmetric], subst not_in_vars_coeff0)
(auto simp flip: coeff_add monom.abs_eq
simp: not_in_vars_coeff0 MPoly_Type.coeff_def
Var.abs_eq Var⇩0_def lookup_single_eq monom.rep_eq)
have [simp]: ‹MPoly_Type.coeff p (monomial (Suc 0) ab) = -1›
if ‹vars (p + Var ab) ⊆ 𝒱›
‹ab ∉ 𝒱›
for ab
proof -
define q where ‹q ≡ p + Var ab›
then have p: ‹p = q - Var ab›
by auto
show ?thesis
unfolding p
apply (subst coeff_minus[symmetric], subst not_in_vars_coeff0)
using that unfolding q_def[symmetric]
by (auto simp flip: coeff_minus simp: not_in_vars_coeff0
Var.abs_eq Var⇩0_def simp flip: monom.abs_eq
simp: not_in_vars_coeff0 MPoly_Type.coeff_def
Var.abs_eq Var⇩0_def lookup_single_eq monom.rep_eq)
qed
have [simp]: ‹vars (p - Var ab) = vars (Var ab - p)› for ab
using vars_uminus[of ‹p - Var ab›]
by simp
show ?thesis
unfolding check_extension_def
apply (auto 5 5 simp: check_extension_precalc_def weak_equality_def
mult_poly_spec_def field_simps
add_poly_spec_def power2_eq_square cong: if_cong
intro!: intro_spec_refine[where R=Id, simplified]
split: option.splits dest: ideal.span_add)
done
qed
lemma check_extension_l2_check_extension:
assumes ‹(A, B) ∈ fmap_polys_rel› and ‹(r, r') ∈ sorted_poly_rel O mset_poly_rel› and
‹(i, i') ∈ nat_rel› ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel› ‹(x, x') ∈ var_rel›
shows
‹check_extension_l2 spec A 𝒱 i x r ≤
⇓{((st), (b)).
(¬is_cfailed st ⟷ b) ∧
(is_cfound st ⟶ spec = r) ∧
(b ⟶ vars_llist r ⊆ 𝒱 ∧ x ∉ 𝒱)} (check_extension_precalc B 𝒱' i' x' r')›
proof -
have ‹x' = φ x›
using assms(5) by (auto simp: var_rel_def br_def)
have [simp]: ‹(l, l') ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
(map (λ(a, b). (a, - b)) l, map (λ(a, b). (a, - b)) l')
∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel› for l l'
by (induction l l' rule: list_rel_induct)
(auto simp: list_mset_rel_def br_def)
have [intro!]:
‹(x2c, za) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel O list_mset_rel ⟹
(map (λ(a, b). (a, - b)) x2c,
{#case x of (a, b) ⇒ (a, - b). x ∈# za#})
∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel O list_mset_rel› for x2c za
apply (auto)
subgoal for y
apply (induction x2c y rule: list_rel_induct)
apply (auto simp: list_mset_rel_def br_def)
apply (rename_tac a b aa l l', rule_tac b = ‹(aa, - b) # map (λ(a, b). (a, - b)) l'› in relcompI)
by auto
done
have [simp]: ‹(λx. fst (case x of (a, b) ⇒ (a, - b))) = fst›
by auto
have uminus: ‹(x2c, x2a) ∈ sorted_poly_rel O mset_poly_rel ⟹
(map (λ(a, b). (a, - b)) x2c,
- x2a)
∈ sorted_poly_rel O mset_poly_rel› for x2c x2a x1c x1a
apply (clarsimp simp: sorted_poly_list_rel_wrt_def
mset_poly_rel_def)
apply (rule_tac b = ‹(λ(a, b). (a, - b)) `# za› in relcompI)
by (auto simp: sorted_poly_list_rel_wrt_def
mset_poly_rel_def comp_def polynomial_of_mset_uminus)
have [simp]: ‹([], 0) ∈ sorted_poly_rel O mset_poly_rel›
by (auto simp: sorted_poly_list_rel_wrt_def
mset_poly_rel_def list_mset_rel_def br_def
intro!: relcompI[of _ ‹{#}›])
have [simp]: ‹vars_llist (map (λ(a, b). (a, - b)) xs) = vars_llist xs› for xs
by (auto simp: vars_llist_def)
show ?thesis
unfolding check_extension_l2_def
check_extension_l_dom_err_def
check_extension_l_no_new_var_err_def
check_extension_l_new_var_multiple_err_def
check_extension_l_side_cond_err_def
apply (rule order_trans)
defer
apply (rule ref_two_step')
apply (rule check_extension_alt_def)
apply (refine_vcg add_poly_full_spec3 mult_poly_full_mult_poly_spec)
subgoal using assms(1,3,4,5)
by (auto simp: var_rel_set_rel_iff)
subgoal using assms(1,3,4,5)
by (auto simp: var_rel_set_rel_iff)
subgoal by auto
subgoal by auto
apply (rule assms)
subgoal using sorted_poly_rel_vars_llist[of ‹r› ‹r'›] assms
by (force simp: set_rel_def var_rel_def br_def
dest!: sorted_poly_rel_vars_llist)
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply (rule uminus)
subgoal using assms by auto
subgoal by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by (auto simp: in_set_conv_decomp_first[of _ r] remove1_append)
subgoal using assms by auto
done
qed
lemma PAC_checker_l_step_PAC_checker_step:
assumes
‹(Ast, Bst) ∈{((err, 𝒱, A), (err', 𝒱', A')). ((err, 𝒱, A), (err', 𝒱', A')) ∈ (code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel2 err 𝒱)}› and
‹(st, st') ∈ epac_step_rel› and
spec: ‹(spec, spec') ∈ sorted_poly_rel O mset_poly_rel› and
fail: ‹¬is_cfailed (fst Ast)›
shows
‹PAC_checker_l_step spec Ast st ≤
⇓{((err, 𝒱, A), (err', 𝒱', A')). ((err, 𝒱, A), (err', 𝒱', A')) ∈ (code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel2 err 𝒱)}
(PAC_checker_step spec' Bst st')›
proof -
obtain A 𝒱 cst B 𝒱' cst' where
Ast: ‹Ast = (cst, 𝒱, A)› and
Bst: ‹Bst = (cst', 𝒱', B)› and
𝒱[intro]: ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel› and
AB: ‹¬is_cfailed cst ⟹ (A, B) ∈ fmap_polys_rel›
‹(cst, cst') ∈ code_status_status_rel›
using assms(1) unfolding fmap_polys_rel2_def
by (cases Ast; cases Bst; auto)
have [intro]: ‹xc ∈ 𝒱 ⟹ φ xc ∈ 𝒱'› for xc
using 𝒱 by (auto simp: set_rel_def var_rel_def br_def)
have 𝒱': ‹𝒱' = φ ` 𝒱›
using 𝒱
by (auto simp: set_rel_def var_rel_def br_def)
have [refine]: ‹(r, ra) ∈ sorted_poly_rel O mset_poly_rel ⟹
(eqa, eqaa)
∈ {(st, b). (¬ is_cfailed st ⟷ b) ∧ (is_cfound st ⟶ spec = r) ∧ (b ⟶ vars_llist r ⊆ 𝒱 ∧ new_id step ∉# dom_m A)} ⟹
RETURN eqa
≤ ⇓ code_status_status_rel
(SPEC
(λst'. (¬ is_failed st' ∧
is_found st' ⟶
ra - spec' ∈ More_Modules.ideal polynomial_bool)))›
for r ra eqa eqaa step
using spec
by (cases eqa)
(auto intro!: RETURN_RES_refine dest!: sorted_poly_list_relD
simp: mset_poly_rel_def ideal.span_zero)
have [simp]: ‹(eqa, st'a) ∈ code_status_status_rel ⟹
(merge_cstatus cst eqa, merge_status cst' st'a)
∈ code_status_status_rel› for eqa st'a
using AB
by (cases eqa; cases st'a)
(auto simp: code_status_status_rel_def)
have [simp]: ‹(merge_cstatus cst CSUCCESS, cst') ∈ code_status_status_rel›
using AB
by (cases st)
(auto simp: code_status_status_rel_def)
have [simp]: ‹(x32, x32a) ∈ var_rel ⟹
([([x32], -1::int)], -Var x32a) ∈ fully_unsorted_poly_rel O mset_poly_rel› for x32 x32a
by (auto simp: mset_poly_rel_def fully_unsorted_poly_list_rel_def list_mset_rel_def br_def
unsorted_term_poly_list_rel_def var_rel_def Const_1_eq_1
intro!: relcompI[of _ ‹{#({#x32#}, -1 :: int)#}›]
relcompI[of _ ‹[({#x32#}, -1)]›])
have H3: ‹p - Var a = (-Var a) + p› for p :: ‹int mpoly› and a
by auto
have [iff]: ‹x3a ∈# remove1_mset x3a (dom_m B) ⟷ False› for x3a B
using distinct_mset_dom[of B]
by (cases ‹x3a ∈# dom_m B›) (auto dest!: multi_member_split)
show ?thesis
using assms(2)
unfolding PAC_checker_l_step_def PAC_checker_step_def Ast Bst prod.case
apply (cases st; cases st'; simp only: p2rel_def pac_step.case
pac_step_rel_raw_def mem_Collect_eq prod.case pac_step_rel_raw.simps)
subgoal
apply (refine_rcg normalize_poly_normalize_poly_spec check_linear_combi_l_check_linear_comb
full_normalize_poly_diff_ideal)
subgoal using fail unfolding Ast by auto
subgoal using assms(1) fail 𝒱'
unfolding PAC_checker_l_step_inv_def by (auto simp: fmap_polys_rel2_def Ast Bst
dest!: multi_member_split)
subgoal using AB by auto
subgoal using AB by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using AB unfolding PAC_checker_step_inv_def fmap_rel_alt_def PAC_checker_l_step_inv_def
by (auto simp: all_conj_distrib dest!: multi_member_split sorted_poly_rel_vars_llist2)
apply assumption+
subgoal
by (auto simp: code_status_status_rel_def)
subgoal
using AB
by (auto intro!: fmap_rel_fmupd_fmap_rel fmap_rel_fmdrop_fmap_rel AB simp: fmap_polys_rel2_def PAC_checker_l_step_inv_def subset_iff)
subgoal using AB
by (auto intro!: fmap_rel_fmupd_fmap_rel fmap_rel_fmdrop_fmap_rel AB simp: fmap_polys_rel2_def PAC_checker_l_step_inv_def subset_iff)
done
subgoal
apply (refine_rcg full_normalize_poly_diff_ideal add_poly_l_single_new_var
check_extension_l2_check_extension)
subgoal using fail unfolding Ast by auto
subgoal using assms(1) fail 𝒱'
unfolding PAC_checker_l_step_inv_def by (auto simp: fmap_polys_rel2_def Ast Bst
dest!: multi_member_split)
subgoal using AB by (auto intro!: fully_unsorted_poly_rel_diff[of _ ‹-Var _ :: int mpoly›, unfolded H3[symmetric]] simp: comp_def case_prod_beta)
subgoal using AB by (auto intro!: fully_unsorted_poly_rel_diff[of _ ‹-Var _ :: int mpoly›, unfolded H3[symmetric]] simp: comp_def case_prod_beta)
subgoal using AB by auto
subgoal using AB by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by simp
subgoal by simp
subgoal by simp
subgoal using AB 𝒱
by (auto simp: fmap_polys_rel2_def PAC_checker_l_step_inv_def
intro!: fmap_rel_fmupd_fmap_rel insert_var_rel_set_rel dest!: in_diffD)
subgoal
by (auto simp: code_status_status_rel_def AB fmap_polys_rel2_def
code_status.is_cfailed_def)
done
subgoal
apply (refine_rcg normalize_poly_normalize_poly_spec
check_del_l_check_del check_addition_l_check_add
full_normalize_poly_diff_ideal[unfolded normalize_poly_spec_def[symmetric]])
subgoal using fail unfolding Ast by auto
subgoal using assms(1) fail 𝒱'
unfolding PAC_checker_l_step_inv_def by (auto simp: fmap_polys_rel2_def Ast Bst
dest!: multi_member_split)
subgoal using AB by auto
subgoal using AB by auto
subgoal using AB
by (auto intro!: fmap_rel_fmupd_fmap_rel
fmap_rel_fmdrop_fmap_rel code_status_status_rel_def
simp: fmap_polys_rel2_def PAC_checker_l_step_inv_def
dest: in_diffD)
subgoal
using AB
by (auto intro!: fmap_rel_fmupd_fmap_rel
fmap_rel_fmdrop_fmap_rel simp: fmap_polys_rel2_def)
done
done
qed
lemma PAC_checker_l_PAC_checker:
assumes
‹(A, B) ∈{((𝒱, A), (𝒱', A')). ((𝒱, A), (𝒱', A')) ∈ (⟨var_rel⟩set_rel ×⇩r fmap_polys_rel2 b 𝒱)}›
(is ‹_ ∈ ?A›) and
‹(st, st') ∈ ⟨epac_step_rel⟩list_rel› and
‹(spec, spec') ∈ sorted_poly_rel O mset_poly_rel› and
‹(b, b') ∈ code_status_status_rel›
shows
‹PAC_checker_l spec A b st ≤
⇓ {((err, 𝒱, A), (err', 𝒱', A')). ((err, 𝒱, A), (err', 𝒱', A')) ∈ (code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel2 err 𝒱)} (PAC_checker spec' B b' st')›
proof -
have [refine0]: ‹(((b, A), st), (b', B), st') ∈
({((err, 𝒱, A), (err', 𝒱', A')). ((err, 𝒱, A), (err', 𝒱', A')) ∈ (code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel2 err 𝒱)} ×⇩r
⟨epac_step_rel⟩list_rel)›
using assms by (auto simp: code_status_status_rel_def)
show ?thesis
using assms
unfolding PAC_checker_l_def PAC_checker_def
apply (refine_rcg PAC_checker_l_step_PAC_checker_step)
subgoal by (auto simp: code_status_status_rel_discrim_iff
WHILEIT_refine[where R = ‹(?A ×⇩r ⟨pac_step_rel⟩list_rel)›])
subgoal by auto
subgoal by (auto simp: neq_Nil_conv)
subgoal by (auto simp: neq_Nil_conv intro!: param_nth)
subgoal by (auto simp: neq_Nil_conv)
subgoal by (auto simp: neq_Nil_conv fmap_polys_rel2_def)
subgoal by (auto simp: neq_Nil_conv fmap_polys_rel2_def)
done
qed
lemma sorted_poly_rel_extend_vars2:
‹(A, B) ∈ sorted_poly_rel O mset_poly_rel ⟹
(x1c, x1a) ∈ ⟨var_rel⟩set_rel ⟹
RETURN (x1c ∪ vars_llist A)
≤ ⇓ {(a,b). (a,b) ∈ ⟨var_rel⟩set_rel ∧ a = x1c ∪ vars_llist A}
(SPEC ((⊆) (x1a ∪ vars (B))))›
using sorted_poly_rel_vars_llist[of A B]
apply (subst RETURN_RES_refine_iff)
apply clarsimp
apply (rule exI[of _ ‹x1a ∪ φ ` vars_llist A›])
apply (auto simp: set_rel_def var_rel_def br_def
dest: fully_unsorted_poly_rel_vars_subset_vars_llist)
done
lemma fully_unsorted_poly_rel_extend_vars2:
‹(A, B) ∈ fully_unsorted_poly_rel O mset_poly_rel ⟹
(x1c, x1a) ∈ ⟨var_rel⟩set_rel ⟹
RETURN (x1c ∪ vars_llist A)
≤ ⇓ {(a,b). (a,b) ∈ ⟨var_rel⟩set_rel ∧ a = x1c ∪ vars_llist A}
(SPEC ((⊆) (x1a ∪ vars (B))))›
using fully_unsorted_poly_rel_vars_subset_vars_llist[of A B]
apply (subst RETURN_RES_refine_iff)
apply clarsimp
apply (rule exI[of _ ‹x1a ∪ φ ` vars_llist A›])
apply (auto simp: set_rel_def var_rel_def br_def
dest: fully_unsorted_poly_rel_vars_subset_vars_llist)
done
lemma remap_polys_l_with_err_remap_polys_with_err:
assumes
AB: ‹(A, B) ∈ ⟨nat_rel, fully_unsorted_poly_rel O mset_poly_rel⟩fmap_rel› and
spec: ‹(spec, spec') ∈ sorted_poly_rel O mset_poly_rel› and
V: ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel› and
spec0: ‹(spec0, spec0') ∈ fully_unsorted_poly_rel O mset_poly_rel› and
pre: ‹remap_polys_l_with_err_pre spec spec0 𝒱 A›
shows ‹remap_polys_l_with_err spec spec0 𝒱 A ≤
⇓{((err, 𝒱, A), (err', 𝒱', A')). (err, err') ∈ code_status_status_rel ∧
(¬is_cfailed err ⟶ ((err, 𝒱, A), (err', 𝒱', A')) ∈ (code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel2 err 𝒱))}
(remap_polys_with_err spec' spec0' 𝒱' B)›
(is ‹_ ≤ ⇓ ?R _›)
proof -
have 1: ‹inj_on id (dom :: nat set)› for dom
by auto
have H: ‹x ∈# dom_m A ⟹
(⋀p. (the (fmlookup A x), p) ∈ fully_unsorted_poly_rel ⟹
(p, the (fmlookup B x)) ∈ mset_poly_rel ⟹ thesis) ⟹
thesis› for x thesis
using fmap_rel_nat_the_fmlookup[OF AB, of x x] fmap_rel_nat_rel_dom_m[OF AB] by auto
have full_normalize_poly: ‹full_normalize_poly (the (fmlookup A x))
≤ ⇓ {(xs, ys). (xs, ys) ∈ sorted_poly_rel O mset_poly_rel ∧ vars_llist xs ⊆ vars_llist (the (fmlookup A x))}
(SPEC
(λp. the (fmlookup B x') - p ∈ More_Modules.ideal polynomial_bool ∧
vars p ⊆ vars (the (fmlookup B x'))))› (is ‹_ ≤ ⇓?A _›)
if x_dom: ‹x ∈# dom_m A› and ‹(x, x') ∈ Id› for x x'
apply (rule H[OF x_dom])
subgoal for p
apply (rule full_normalize_poly_normalize_poly_p2[THEN order_trans])
apply assumption
subgoal
using that(2) apply -
unfolding conc_fun_chain[symmetric]
by
(auto simp: rtranclp_normalize_poly_p_poly_of_mset conc_fun_RES
mset_poly_rel_def ideal.span_zero
intro!: exI[of _ ‹polynomial_of_mset _›])
done
done
have H': ‹(p, pa) ∈ sorted_poly_rel O mset_poly_rel ⟹
weak_equality_l p spec ≤ ⇓{(b,enn). b = (enn=FOUND)}
(SPEC (λeqa. eqa ≠ FAILED ∧ (eqa = FOUND ⟶ pa = spec')))› for p pa
using spec by (auto simp: weak_equality_l_def weak_equality_spec_def RETURN_def
list_mset_rel_def br_def mset_poly_rel_def intro!: RES_refine
dest: list_rel_term_poly_list_rel_same_rightD sorted_poly_list_relD)
have [refine]: ‹SPEC (λerr. err ≠ CFOUND) ≤ ⇓code_status_status_rel (RES {FAILED, SUCCESS})›
by (auto simp: code_status_status_rel_def intro!: RES_refine)
(case_tac s, auto)
have [intro!]: ‹∃a. (aa, a) ∈ ⟨var_rel⟩set_rel› for aa
by (auto simp: set_rel_def var_rel_def br_def)
have emp: ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel ⟹
((CSUCCESS, 𝒱, fmempty), SUCCESS, 𝒱', fmempty) ∈
{((err, 𝒱, A), (f', 𝒱', A')). ((err, 𝒱, A), (f', 𝒱', A')) ∈
(code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel2 err 𝒱)}›
for 𝒱 𝒱'
by (auto simp: fmap_polys_rel2_def)
have XXX: ‹(𝒱'', 𝒱''') ∈ ⟨var_rel⟩set_rel ⟹ x ∈ 𝒱'' ⟹ φ x ∈ 𝒱'''› for x 𝒱'' 𝒱'''
by (auto simp: br_def set_rel_def var_rel_def)
show ?thesis
using assms
unfolding remap_polys_l_with_err_def remap_polys_l_dom_err_def
remap_polys_with_err_def prod.case term_rel_def[symmetric]
apply (refine_rcg full_normalize_poly fmap_rel_fmupd_fmap_rel)
subgoal
by auto
apply (rule fully_unsorted_poly_rel_extend_vars2[unfolded term_rel_def[symmetric]])
subgoal using spec0 by auto
subgoal by auto
subgoal by auto
subgoal
by (auto simp: error_msg_def fmap_polys_rel2_def intro!: RES_refine)
apply (rule 1)
subgoal by auto
apply (rule emp)
subgoal
using V by auto
subgoal by (auto simp: code_status_status_rel_def)
subgoal by auto
subgoal by auto
subgoal by (auto simp: code_status_status_rel_def RETURN_def fmap_polys_rel2_def intro!: RES_refine)
subgoal by auto
apply (rule H')
subgoal by auto
apply (rule fully_unsorted_poly_rel_extend_vars2[unfolded term_rel_def[symmetric]])
subgoal by (auto intro!: fmap_rel_nat_the_fmlookup)
subgoal by (auto intro!: fmap_rel_fmupd_fmap_rel)
subgoal for dom doma failed faileda x it σ x' it' σ' x1 x2 x1a x2a x1b x2b x1c x2c p pa err' err _ _ eqa eqaa 𝒱'' 𝒱'''
unfolding term_rel_def[symmetric]
by (cases eqaa)
(auto simp: fmap_rel_fmupd_fmap_rel[where R = ‹sorted_poly_rel O mset_poly_rel›, unfolded term_rel_def[symmetric]]
simp: fmap_polys_rel2_def code_status_status_rel_def term_rel_def[symmetric]
dest: in_diffD)
subgoal by (auto simp: code_status_status_rel_def is_cfailed_def)
subgoal by (auto simp: code_status_status_rel_def)
done
qed
definition (in -) full_checker_l
:: ‹llist_polynomial ⇒ (nat, llist_polynomial) fmap ⇒ (_, string, nat) pac_step list ⇒
(string code_status × _) nres›
where
‹full_checker_l spec A st = do {
spec' ← full_normalize_poly spec;
(b, 𝒱, A) ← remap_polys_l_with_err spec' spec {} A;
if is_cfailed b
then RETURN (b, 𝒱, A)
else do {
let 𝒱 = 𝒱;
PAC_checker_l spec' (𝒱, A) b st
}
}›
lemma (in -)RES_RES_RETURN_RES3: ‹RES A ⤜ (λ(a,b,c). RES (f a b c)) = RES (⋃((λ(a,b,c). f a b c) ` A))› for A f
by (auto simp: pw_eq_iff refine_pw_simps)
definition vars_rel2 :: ‹_› where
‹vars_rel2 err = {(A,B). ¬is_cfailed err ⟶ (A,B)∈ ⟨var_rel⟩set_rel} ›
lemma full_normalize_poly_normalize_poly_spec_vars2: ‹(p3, p1) ∈ fully_unsorted_poly_rel O mset_poly_rel ⟹
full_normalize_poly p3
≤ ⇓ ({(xs, ys). (xs, ys) ∈ sorted_poly_rel ∧ vars_llist xs ⊆ vars_llist p3} O
mset_poly_rel)
(normalize_poly_spec p1)
›
using full_normalize_poly_normalize_poly_p2[unfolded normalize_poly_spec_alt_def[symmetric],
THEN ref_two_step[OF _ normalize_poly_p_normalize_poly_spec], unfolded conc_fun_chain]
by auto
lemma full_checker_l_full_checker:
assumes
‹(A, B) ∈ unsorted_fmap_polys_rel› and
st: ‹(st, st') ∈ ⟨epac_step_rel⟩list_rel› and
spec: ‹(spec, spec') ∈ fully_unsorted_poly_rel O mset_poly_rel›
shows
‹full_checker_l spec A st ≤ ⇓ {((err, 𝒱, A), err', 𝒱', A').
((err, 𝒱, A), err', 𝒱', A') ∈ code_status_status_rel ×⇩r vars_rel2 err ×⇩r fmap_polys_rel2 err 𝒱} (full_checker spec' B st')›
proof -
have aa: ‹{((err, 𝒱, A), err', 𝒱', A'). (err,err') ∈ code_status_status_rel ∧
(¬ is_cfailed err ⟶
((err, 𝒱, A), err', 𝒱', A') ∈ code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel2 err 𝒱) ∧
(¬is_failed err' ⟶ vars spec' ⊆ 𝒱')} =
{((err, 𝒱, A), err', 𝒱', A'). (err,err') ∈ code_status_status_rel ∧ (¬ is_cfailed err ⟶
((err, 𝒱, A), err', 𝒱', A') ∈ code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel2 err 𝒱)} O
{((err, 𝒱, A), err', 𝒱', A'). ((err, 𝒱, A), err', 𝒱', A') ∈ Id ∧ (¬is_failed err' ⟶ vars spec' ⊆ 𝒱')}› for spec'
by auto
have [refine]:
‹(spec, spec') ∈ sorted_poly_rel O mset_poly_rel ⟹
(spec0, spec0') ∈ fully_unsorted_poly_rel O mset_poly_rel ⟹
(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel ⟹ remap_polys_l_with_err_pre spec spec0 𝒱 A ⟹
remap_polys_l_with_err spec spec0 𝒱 A ≤ ⇓ {((err, 𝒱, A), err', 𝒱', A'). (err,err') ∈ code_status_status_rel ∧ (¬ is_cfailed err ⟶
((err, 𝒱, A), err', 𝒱', A') ∈ code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel2 err 𝒱) ∧
(¬is_failed err' ⟶ vars spec0' ⊆ 𝒱')}
(remap_polys_change_all spec' 𝒱' B)› (is ‹_ ⟹ _ ⟹ _ ⟹ _ ⟹ _ ≤ ⇓ ?A _›)
for spec spec' 𝒱 𝒱' spec0 spec0'
apply (rule remap_polys_l_with_err_remap_polys_with_err[THEN order_trans, OF assms(1)])
apply assumption+
apply (subst aa, subst conc_fun_chain[symmetric])
apply (rule ref_two_step[OF order.refl])
apply (rule remap_polys_with_err_spec[THEN order_trans])
apply (rule conc_fun_R_mono[THEN order_trans, of _ ‹{((err, 𝒱, A), err', 𝒱', A').
((err, 𝒱, A), err', 𝒱', A') ∈ Id ∧ (¬ is_failed err' ⟶ vars spec0' ⊆ 𝒱')}›])
apply (solves auto)
apply (subst ref_two_step')
apply (rule remap_polys_polynomial_bool_remap_polys_change_all)
apply (solves ‹rule TrueI›)
done
have unfold_code_status: ‹(∃(a). P a) ⟷ (∃a. P (CFAILED a)) ∨ P CFOUND ∨ P CSUCCESS› for P
by (auto, case_tac a, auto)
have unfold_status: ‹(∃(a). P a) ⟷ ( P (FAILED)) ∨ P FOUND ∨ P SUCCESS› for P
by (auto, case_tac a, auto)
have var_rel_set_rel_alt_def: ‹(A, B) ∈ ⟨var_rel⟩set_rel ⟷ B = φ ` A› for A B
by (auto simp: var_rel_def set_rel_def br_def)
have [refine]: ‹(x1c, x1a) ∈ ⟨var_rel⟩set_rel ⟹
SPEC (λ(err, 𝒱'). (err = CSUCCESS ∨ is_cfailed err) ∧ (err = CSUCCESS ⟶ 𝒱' = x1c ∪ vars_llist spec))
≤ ⇓ (code_status_status_rel ×⇩r ⟨var_rel⟩set_rel)
(SPEC (λ(err, 𝒱'). (err = SUCCESS ∨ is_failed err) ∧ (err = SUCCESS ⟶ x1a ∪ vars spec' ⊆ 𝒱')))› for x1c x1a
using fully_unsorted_poly_rel_vars_subset_vars_llist[OF spec]
by (force simp: code_status_status_rel_def is_failed_def unfold_code_status unfold_status is_cfailed_def
var_rel_set_rel_alt_def
intro!: RES_refine
intro: )
have [refine]: ‹(b,b') ∈ {((𝒱, A), 𝒱', A'). ((𝒱, A), 𝒱', A') ∈ ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel2 c 𝒱} ⟹
(spec, spec') ∈ sorted_poly_rel O mset_poly_rel ⟹
(c, c') ∈ code_status_status_rel ⟹
PAC_checker_l spec b c st
≤ ⇓ {((err, 𝒱, A), err', 𝒱', A').
((err, 𝒱, A), err', 𝒱', A') ∈ code_status_status_rel ×⇩r vars_rel2 err ×⇩r fmap_polys_rel2 err 𝒱}
(PAC_checker spec' b' c' st')› for spec b c spec' b' c'
using assms apply -
apply (rule order_trans)
apply (rule ref_two_step[OF PAC_checker_l_PAC_checker])
apply assumption+
apply (rule order_refl)
apply (rule conc_fun_R_mono)
apply (auto simp: vars_rel2_def)
done
have still_in: ‹(spec'a, spec) ∈ {(xs, ys). (xs, ys) ∈ sorted_poly_rel ∧ vars_llist xs ⊆ spec0} O mset_poly_rel ⟹
(x, x') ∈ ?A spec' ⟹
x2 = (x1a, x2a) ⟹
x' = (x1, x2) ⟹
x2b = (x1c, x2c) ⟹
x = (x1b, x2b) ⟹
¬ is_cfailed x1b ⟹
¬ is_failed x1 ⟹
RETURN x1c
≤ ⇓ (⟨var_rel⟩set_rel) (SPEC ((⊆) (x1a ∪ vars spec')))›
for spec'a spec x x' x1 x2 x1a x2a x1b x2b x1c x2c spec0
apply (auto intro!: RETURN_RES_refine exI[of _ x1a])
done
show ?thesis
unfolding full_checker_def full_checker_l_def
apply (refine_rcg remap_polys_l_remap_polys full_normalize_poly_normalize_poly_spec_vars2
assms)
subgoal by auto
subgoal by auto
subgoal unfolding remap_polys_l_with_err_pre_def by auto
subgoal by (auto simp: is_cfailed_def is_failed_def)
subgoal by (auto simp: vars_rel2_def fmap_polys_rel2_def)
apply (rule still_in; assumption)
subgoal by auto
subgoal by auto
subgoal by (auto simp: fmap_polys_rel2_def vars_rel2_def)
done
qed
lemma full_checker_l_full_checker':
‹(uncurry2 full_checker_l, uncurry2 full_checker) ∈
((fully_unsorted_poly_rel O mset_poly_rel) ×⇩r unsorted_fmap_polys_rel) ×⇩r ⟨epac_step_rel⟩list_rel →⇩f
⟨{((err, 𝒱, A), err', 𝒱', A').
((err, 𝒱, A), err', 𝒱', A')
∈ code_status_status_rel ×⇩r vars_rel2 err ×⇩r {(xs, ys).
(¬ is_cfailed err ⟶ (xs, ys) ∈ ⟨nat_rel, sorted_poly_rel O mset_poly_rel⟩fmap_rel ∧
(∀i∈#dom_m xs. vars_llist (the (fmlookup xs i)) ⊆ 𝒱))}}⟩nres_rel›
apply (intro frefI nres_relI)
using full_checker_l_full_checker unfolding fmap_polys_rel2_def by force
end
end