# Theory PAC_Checker_Specification

```(*
File:         PAC_Checker_Specification.thy
Author:       Mathias Fleury, Daniela Kaufmann, JKU
Maintainer:   Mathias Fleury, JKU
*)
theory PAC_Checker_Specification
imports PAC_Specification
Refine_Imperative_HOL.IICF
Finite_Map_Multiset
begin

section ‹Checker Algorithm›

text ‹

In this level of refinement, we define the first level of the
implementation of the checker, both with the specification as
on ideals and the first version of the loop.

›

subsection ‹Specification›

datatype status =
is_failed: FAILED |
is_success: SUCCESS |
is_found: FOUND

lemma is_success_alt_def:
‹is_success a ⟷ a = SUCCESS›
by (cases a) auto

datatype ('a, 'b, 'lbls) pac_step =
Add (pac_src1: 'lbls) (pac_src2: 'lbls) (new_id: 'lbls) (pac_res: 'a) |
Mult (pac_src1: 'lbls) (pac_mult: 'a) (new_id: 'lbls) (pac_res: 'a) |
Extension (new_id: 'lbls) (new_var: 'b) (pac_res: 'a) |
Del (pac_src1: 'lbls)

type_synonym  pac_state = ‹(nat set × int_poly multiset)›

definition PAC_checker_specification
:: ‹int_poly ⇒ int_poly multiset ⇒ (status × nat set × int_poly multiset) nres›
where
‹PAC_checker_specification spec A = SPEC(λ(b, 𝒱, B).
(¬is_failed b ⟶ restricted_ideal_to⇩I (⋃(vars ` set_mset A) ∪ vars spec) B ⊆ restricted_ideal_to⇩I (⋃(vars ` set_mset A) ∪ vars spec) A) ∧
(is_found b ⟶ spec ∈ pac_ideal (set_mset A)))›

definition PAC_checker_specification_spec
::  ‹int_poly ⇒ pac_state ⇒ (status × pac_state) ⇒ bool›
where
‹PAC_checker_specification_spec spec = (λ(𝒱, A) (b, B). (¬is_failed b ⟶ ⋃(vars ` set_mset A) ⊆ 𝒱) ∧
(is_success b ⟶ PAC_Format⇧*⇧* (𝒱, A) B) ∧
(is_found b ⟶ PAC_Format⇧*⇧* (𝒱, A) B ∧ spec ∈ pac_ideal (set_mset A)))›

abbreviation PAC_checker_specification2
::  ‹int_poly ⇒ (nat set × int_poly multiset) ⇒ (status × (nat set × int_poly multiset)) nres›
where
‹PAC_checker_specification2 spec A ≡ SPEC(PAC_checker_specification_spec spec A)›

definition PAC_checker_specification_step_spec
::  ‹pac_state ⇒ int_poly ⇒ pac_state ⇒ (status × pac_state) ⇒ bool›
where
‹PAC_checker_specification_step_spec = (λ(𝒱⇩0, A⇩0) spec (𝒱, A) (b, B).
(is_success b ⟶
⋃(vars ` set_mset A⇩0) ⊆ 𝒱⇩0 ∧
⋃(vars ` set_mset A) ⊆ 𝒱 ∧ PAC_Format⇧*⇧* (𝒱⇩0, A⇩0) (𝒱, A) ∧ PAC_Format⇧*⇧* (𝒱, A) B) ∧
(is_found b ⟶
⋃(vars ` set_mset A⇩0) ⊆ 𝒱⇩0 ∧
⋃(vars ` set_mset A) ⊆ 𝒱 ∧ PAC_Format⇧*⇧* (𝒱⇩0, A⇩0) (𝒱, A) ∧ PAC_Format⇧*⇧* (𝒱, A) B ∧
spec ∈ pac_ideal (set_mset A⇩0)))›

abbreviation PAC_checker_specification_step2
::  ‹pac_state ⇒ int_poly ⇒ pac_state ⇒ (status × pac_state) nres›
where
‹PAC_checker_specification_step2 A⇩0 spec A ≡ SPEC(PAC_checker_specification_step_spec A⇩0  spec A)›

definition normalize_poly_spec :: ‹_› where
‹normalize_poly_spec p = SPEC (λr. p - r ∈ ideal polynomial_bool ∧ vars r ⊆ vars p)›

lemma normalize_poly_spec_alt_def:
‹normalize_poly_spec p = SPEC (λr. r - p ∈ ideal polynomial_bool ∧ vars r ⊆ vars p)›
unfolding normalize_poly_spec_def
by (auto dest: ideal.span_neg)

definition mult_poly_spec :: ‹int mpoly ⇒ int mpoly ⇒ int mpoly nres› where
‹mult_poly_spec p q = SPEC (λr. p * q - r ∈ ideal polynomial_bool)›

definition check_add :: ‹(nat, int mpoly) fmap ⇒ nat set ⇒ nat ⇒ nat ⇒ nat ⇒ int mpoly ⇒ bool nres› where
‹check_add A 𝒱 p q i r =
SPEC(λb. b ⟶ p ∈# dom_m A ∧ q ∈# dom_m A ∧ i ∉# dom_m A ∧ vars r ⊆ 𝒱 ∧
the (fmlookup A p) + the (fmlookup A q) - r ∈  ideal polynomial_bool)›

definition check_mult :: ‹(nat, int mpoly) fmap ⇒ nat set ⇒ nat ⇒ int mpoly ⇒ nat ⇒ int mpoly ⇒ bool nres› where
‹check_mult A 𝒱 p q i r =
SPEC(λb. b ⟶ p ∈# dom_m A ∧i ∉# dom_m A ∧ vars q ⊆ 𝒱 ∧ vars r ⊆ 𝒱 ∧
the (fmlookup A p) * q - r ∈  ideal polynomial_bool)›

definition check_extension :: ‹(nat, int mpoly) fmap ⇒ nat set ⇒ nat ⇒ nat ⇒ int mpoly ⇒ (bool) nres› where
‹check_extension A 𝒱 i v p =
SPEC(λb. b ⟶ (i ∉# dom_m A ∧
(v ∉ 𝒱 ∧
(p+Var v)⇧2 - (p+Var v) ∈ ideal polynomial_bool ∧
vars (p+Var v) ⊆ 𝒱)))›

fun merge_status where
‹merge_status (FAILED) _ = FAILED› |
‹merge_status _ (FAILED) = FAILED› |
‹merge_status FOUND _ = FOUND› |
‹merge_status _ FOUND = FOUND› |
‹merge_status _ _ = SUCCESS›

type_synonym fpac_step = ‹nat set × (nat, int_poly) fmap›

definition check_del :: ‹(nat, int mpoly) fmap ⇒ nat ⇒ bool nres› where
‹check_del A p =
SPEC(λb. b ⟶ True)›

subsection ‹Algorithm›

definition PAC_checker_step
::  ‹int_poly ⇒ (status × fpac_step) ⇒ (int_poly, nat, nat) pac_step ⇒
(status × fpac_step) nres›
where
‹PAC_checker_step = (λspec (stat, (𝒱, A)) st. case st of
Add _ _ _ _ ⇒
do {
r ← normalize_poly_spec (pac_res st);
eq ← check_add A 𝒱 (pac_src1 st) (pac_src2 st) (new_id st) r;
st' ← SPEC(λst'. (¬is_failed st' ∧ is_found st' ⟶ r - spec ∈ ideal polynomial_bool));
if eq
then RETURN (merge_status stat st',
𝒱, fmupd (new_id st) r A)
else RETURN (FAILED, (𝒱, A))
}
| Del _ ⇒
do {
eq ← check_del A (pac_src1 st);
if eq
then RETURN (stat, (𝒱, fmdrop (pac_src1 st) A))
else RETURN (FAILED, (𝒱, A))
}
| Mult _ _ _ _ ⇒
do {
r ← normalize_poly_spec (pac_res st);
q ← normalize_poly_spec (pac_mult st);
eq ← check_mult A 𝒱 (pac_src1 st) q (new_id st) r;
st' ← SPEC(λst'. (¬is_failed st' ∧ is_found st' ⟶ r - spec ∈ ideal polynomial_bool));
if eq
then RETURN (merge_status stat st',
𝒱, fmupd (new_id st) r A)
else RETURN (FAILED, (𝒱, A))
}
| Extension _ _ _ ⇒
do {
r ← normalize_poly_spec (pac_res st - Var (new_var st));
(eq) ← check_extension A 𝒱 (new_id st) (new_var st) r;
if eq
then do {
RETURN (stat,
insert (new_var st) 𝒱, fmupd (new_id st) (r) A)}
else RETURN (FAILED, (𝒱, A))
}
)›

definition polys_rel :: ‹((nat, int mpoly)fmap × _) set› where
‹polys_rel = {(A, B). B = (ran_m A)}›

definition polys_rel_full :: ‹((nat set × (nat, int mpoly)fmap) × _) set› where
‹polys_rel_full = {((𝒱, A), (𝒱' , B)). (A, B) ∈ polys_rel ∧ 𝒱 = 𝒱'}›

lemma polys_rel_update_remove:
‹x13 ∉#dom_m A ⟹ x11 ∈# dom_m A ⟹ x12 ∈# dom_m A ⟹ x11 ≠ x12 ⟹ (A,B) ∈ polys_rel ⟹
(fmupd x13 r (fmdrop x11 (fmdrop x12 A)),
add_mset r B - {#the (fmlookup A x11), the (fmlookup A x12)#})
∈ polys_rel›
‹x13 ∉#dom_m A ⟹ x11 ∈# dom_m A ⟹ (A,B) ∈ polys_rel ⟹
(fmupd x13 r (fmdrop x11 A),add_mset r B - {#the (fmlookup A x11)#})
∈ polys_rel›
‹x13 ∉#dom_m A ⟹ (A,B) ∈ polys_rel ⟹
(fmupd x13 r A, add_mset r B) ∈ polys_rel›
‹x13 ∈#dom_m A ⟹ (A,B) ∈ polys_rel ⟹
(fmdrop x13 A, remove1_mset (the (fmlookup A x13)) B) ∈ polys_rel›
using distinct_mset_dom[of A]
apply (auto simp: polys_rel_def ran_m_mapsto_upd ran_m_mapsto_upd_notin
ran_m_fmdrop)
apply (subst ran_m_mapsto_upd_notin)
apply (auto dest: in_diffD dest!: multi_member_split simp: ran_m_fmdrop ran_m_fmdrop_If distinct_mset_remove1_All ran_m_def
split: if_splits intro!: image_mset_cong)
done

lemma polys_rel_in_dom_inD:
‹(A, B) ∈ polys_rel ⟹
x12 ∈# dom_m A ⟹
the (fmlookup A x12) ∈# B›
by (auto simp: polys_rel_def)

‹r - x14 ∈ More_Modules.ideal polynomial_bool ⟹
(A, B) ∈ polys_rel ⟹
x12 ∈# dom_m A ⟹
x13 ∉# dom_m A ⟹
vars r ⊆ 𝒱 ⟹
2 * the (fmlookup A x12) - r ∈ More_Modules.ideal polynomial_bool ⟹
PAC_Format⇧*⇧* (𝒱, B) (𝒱, remove1_mset (the (fmlookup A x12)) (add_mset r B))›
‹r - x14 ∈ More_Modules.ideal polynomial_bool ⟹
(A, B) ∈ polys_rel ⟹
the (fmlookup A x11) + the (fmlookup A x12) - r ∈ More_Modules.ideal polynomial_bool ⟹
x11 ∈# dom_m A ⟹
x12 ∈# dom_m A ⟹
vars r ⊆ 𝒱 ⟹
PAC_Format⇧*⇧* (𝒱, B) (𝒱, add_mset r B)›
‹r - x14 ∈ More_Modules.ideal polynomial_bool ⟹
(A, B) ∈ polys_rel ⟹
x11 ∈# dom_m A ⟹
x12 ∈# dom_m A ⟹
the (fmlookup A x11) + the (fmlookup A x12) - r ∈ More_Modules.ideal polynomial_bool ⟹
vars r ⊆ 𝒱 ⟹
x11 ≠ x12 ⟹
PAC_Format⇧*⇧* (𝒱, B)
(𝒱, add_mset r B - {#the (fmlookup A x11), the (fmlookup A x12)#})›
‹(A, B) ∈ polys_rel ⟹
r - x34 ∈ More_Modules.ideal polynomial_bool ⟹
x11 ∈# dom_m A ⟹
the (fmlookup A x11) * x32 - r ∈ More_Modules.ideal polynomial_bool ⟹
vars x32 ⊆ 𝒱 ⟹
vars r ⊆ 𝒱 ⟹
PAC_Format⇧*⇧* (𝒱, B) (𝒱, add_mset r B)›
‹(A, B) ∈ polys_rel ⟹
r - x34 ∈ More_Modules.ideal polynomial_bool ⟹
x11 ∈# dom_m A ⟹
the (fmlookup A x11) * x32 - r ∈ More_Modules.ideal polynomial_bool ⟹
vars x32 ⊆ 𝒱 ⟹
vars r ⊆ 𝒱 ⟹
PAC_Format⇧*⇧* (𝒱, B) (𝒱, remove1_mset (the (fmlookup A x11)) (add_mset r B))›
‹(A, B) ∈ polys_rel ⟹
x12 ∈# dom_m A ⟹
PAC_Format⇧*⇧* (𝒱, B) (𝒱, remove1_mset (the (fmlookup A x12)) B)›
‹(A, B) ∈ polys_rel ⟹
(p' + Var x)⇧2 - (p' + Var x) ∈ ideal polynomial_bool ⟹
x ∉ 𝒱 ⟹
x ∉ vars(p' + Var x) ⟹
vars(p' + Var x) ⊆ 𝒱 ⟹
PAC_Format⇧*⇧* (𝒱, B)
(insert x 𝒱, add_mset p' B)›
subgoal
apply (rule converse_rtranclp_into_rtranclp)
apply (rule PAC_Format.add[of ‹the (fmlookup A x12)› B ‹the (fmlookup A x12)›])
apply (auto dest: polys_rel_in_dom_inD)
apply (rule converse_rtranclp_into_rtranclp)
apply (rule PAC_Format.del[of ‹the (fmlookup A x12)›])
apply (auto dest: polys_rel_in_dom_inD)
done
subgoal H2
apply (rule converse_rtranclp_into_rtranclp)
apply (rule PAC_Format.add[of ‹the (fmlookup A x11)› B ‹the (fmlookup A x12)›])
apply (auto dest: polys_rel_in_dom_inD)
done
subgoal
apply (rule rtranclp_trans)
apply (rule H2; assumption)
apply (rule converse_rtranclp_into_rtranclp)
apply (rule PAC_Format.del[of ‹the (fmlookup A x12)›])
apply (auto dest: polys_rel_in_dom_inD)
apply (rule converse_rtranclp_into_rtranclp)
apply (rule PAC_Format.del[of ‹the (fmlookup A x11)›])
apply (auto dest: polys_rel_in_dom_inD)
done
subgoal H2
apply (rule converse_rtranclp_into_rtranclp)
apply (rule PAC_Format.mult[of ‹the (fmlookup A x11)› B ‹x32› r])
apply (auto dest: polys_rel_in_dom_inD)
done
subgoal
apply (rule rtranclp_trans)
apply (rule H2; assumption)
apply (rule converse_rtranclp_into_rtranclp)
apply (rule PAC_Format.del[of ‹the (fmlookup A x11)›])
apply (auto dest: polys_rel_in_dom_inD)
done
subgoal
apply (rule converse_rtranclp_into_rtranclp)
apply (rule PAC_Format.del[of ‹the (fmlookup A x12)› B])
apply (auto dest: polys_rel_in_dom_inD)
done
subgoal
apply (rule converse_rtranclp_into_rtranclp)
apply (rule PAC_Format.extend_pos[of ‹p' + Var x› _ x])
using coeff_monomila_in_varsD[of ‹p' - Var x› x]
apply (auto dest: polys_rel_in_dom_inD simp: vars_in_right_only vars_subst_in_left_only)
apply (subgoal_tac ‹𝒱 ∪ {x' ∈ vars (p'). x' ∉ 𝒱} = insert x 𝒱›)
apply simp
using coeff_monomila_in_varsD[of p' x]
apply (auto dest: vars_add_Var_subset vars_minus_Var_subset polys_rel_in_dom_inD simp: vars_subst_in_left_only_iff)
using vars_in_right_only vars_subst_in_left_only by force
done

abbreviation status_rel :: ‹(status × status) set› where
‹status_rel ≡ Id›

lemma is_merge_status[simp]:
‹is_failed (merge_status a st') ⟷ is_failed a ∨ is_failed st'›
‹is_found (merge_status a st') ⟷ ¬is_failed a ∧ ¬is_failed st' ∧ (is_found a ∨ is_found st')›
‹is_success (merge_status a st') ⟷ (is_success a ∧ is_success st')›
by (cases a; cases st'; auto; fail)+

lemma status_rel_merge_status:
‹(merge_status a b, SUCCESS) ∉ status_rel ⟷
(a = FAILED) ∨ (b = FAILED) ∨
a = FOUND ∨ (b = FOUND)›
by (cases a; cases b; auto)

lemma Ex_status_iff:
‹(∃a. P a) ⟷ P SUCCESS ∨ P FOUND ∨ (P (FAILED))›
apply auto
apply (case_tac a; auto)
done

lemma is_failed_alt_def:
‹is_failed st' ⟷ ¬is_success st' ∧ ¬is_found st'›
by (cases st') auto

lemma merge_status_eq_iff[simp]:
‹merge_status a SUCCESS = SUCCESS ⟷ a = SUCCESS›
‹merge_status a SUCCESS = FOUND ⟷ a = FOUND›
‹merge_status SUCCESS a = SUCCESS ⟷ a = SUCCESS›
‹merge_status SUCCESS a = FOUND ⟷ a = FOUND›
‹merge_status SUCCESS a = FAILED ⟷ a = FAILED›
‹merge_status a SUCCESS = FAILED ⟷ a = FAILED›
‹merge_status FOUND a = FAILED ⟷ a = FAILED›
‹merge_status a FOUND = FAILED ⟷ a = FAILED›
‹merge_status a FOUND = SUCCESS ⟷ False›
‹merge_status a b = FOUND ⟷ (a = FOUND ∨ b = FOUND) ∧ (a ≠ FAILED ∧ b ≠ FAILED)›
apply (cases a; auto; fail)+
apply (cases a; cases b; auto; fail)+
done

lemma fmdrop_irrelevant: ‹x11 ∉# dom_m A ⟹ fmdrop x11 A = A›

lemma PAC_checker_step_PAC_checker_specification2:
fixes a :: ‹status›
assumes AB: ‹((𝒱, A),(𝒱⇩B, B)) ∈ polys_rel_full› and
‹¬is_failed a› and
[simp,intro]: ‹a = FOUND ⟹ spec ∈ pac_ideal (set_mset A⇩0)› and
A⇩0B: ‹PAC_Format⇧*⇧* (𝒱⇩0, A⇩0) (𝒱, B)› and
spec⇩0: ‹vars spec ⊆ 𝒱⇩0›  and
vars_A⇩0: ‹⋃ (vars ` set_mset A⇩0) ⊆ 𝒱⇩0›
shows ‹PAC_checker_step spec (a, (𝒱, A)) st ≤ ⇓ (status_rel ×⇩r polys_rel_full) (PAC_checker_specification_step2 (𝒱⇩0, A⇩0) spec (𝒱, B))›
proof -
have
‹𝒱⇩B = 𝒱›and
[simp, intro]:‹(A, B) ∈ polys_rel›
using AB
by (auto simp: polys_rel_full_def)
have H0: ‹2 * the (fmlookup A x12) - r ∈ More_Modules.ideal polynomial_bool ⟹
r ∈ pac_ideal
(insert (the (fmlookup A x12))
((λx. the (fmlookup A x)) ` set_mset Aa))› for x12 r Aa
by (metis (no_types, lifting) ab_semigroup_mult_class.mult.commute
diff_in_polynomial_bool_pac_idealI
then have H0': ‹⋀Aa. 2 * the (fmlookup A x12) - r ∈ More_Modules.ideal polynomial_bool ⟹
r - spec ∈ More_Modules.ideal polynomial_bool ⟹
spec ∈ pac_ideal (insert (the (fmlookup A x12)) ((λx. the (fmlookup A x)) ` set_mset Aa))›
for r x12
by (metis (no_types, lifting) diff_in_polynomial_bool_pac_idealI)

have H1: ‹ x12 ∈# dom_m A ⟹
2 * the (fmlookup A x12) - r ∈ More_Modules.ideal polynomial_bool ⟹
r - spec ∈ More_Modules.ideal polynomial_bool ⟹
vars spec ⊆ vars r ⟹
spec ∈ pac_ideal (set_mset B)› for x12 r
using ‹(A,B) ∈ polys_rel›
of ‹the (fmlookup A x12)› _  ‹the (fmlookup A x12)›],
of ‹set_mset B ∪ polynomial_bool› ‹2 * the (fmlookup A x12) - r›]
unfolding polys_rel_def
by (auto dest!: multi_member_split simp: ran_m_def
intro: H0')
have H2': ‹the (fmlookup A x11) + the (fmlookup A x12) - r ∈ More_Modules.ideal polynomial_bool ⟹
B = add_mset (the (fmlookup A x11)) {#the (fmlookup A x). x ∈# Aa#} ⟹
(the (fmlookup A x11) + the (fmlookup A x12) - r
∈ More_Modules.ideal
(insert (the (fmlookup A x11))
((λx. the (fmlookup A x)) ` set_mset Aa ∪ polynomial_bool)) ⟹
- r
∈ More_Modules.ideal
(insert (the (fmlookup A x11))
((λx. the (fmlookup A x)) ` set_mset Aa ∪ polynomial_bool))) ⟹
r ∈ pac_ideal (insert (the (fmlookup A x11)) ((λx. the (fmlookup A x)) ` set_mset Aa))›
for r x12 x11 A Aa
by (metis (mono_tags, lifting) Un_insert_left diff_diff_eq2 diff_in_polynomial_bool_pac_idealI diff_zero
ideal.span_diff ideal.span_neg minus_diff_eq pac_idealI1 pac_ideal_def set_image_mset
have H2: ‹x11 ∈# dom_m A ⟹
x12 ∈# dom_m A ⟹
the (fmlookup A x11) + the (fmlookup A x12) - r
∈ More_Modules.ideal polynomial_bool ⟹
r - spec ∈ More_Modules.ideal polynomial_bool ⟹
spec ∈ pac_ideal (set_mset B)›  for x12 r x11
using ‹(A,B) ∈ polys_rel›
of ‹the (fmlookup A x11)› _  ‹the (fmlookup A x12)›],
of ‹set_mset B ∪ polynomial_bool› ‹the (fmlookup A x11) + the (fmlookup A x12) - r›]
unfolding polys_rel_def
by (subgoal_tac ‹r ∈ pac_ideal (set_mset B)›)
(auto dest!: multi_member_split simp: ran_m_def ideal.span_base
intro: diff_in_polynomial_bool_pac_idealI simp: H2')

have H3': ‹the (fmlookup A x12) * q - r ∈ More_Modules.ideal polynomial_bool ⟹
r - spec ∈ More_Modules.ideal polynomial_bool ⟹
r ∈ pac_ideal (insert (the (fmlookup A x12)) ((λx. the (fmlookup A x)) ` set_mset Aa))›
for Aa x12 r q
by (metis (no_types, lifting) ab_semigroup_mult_class.mult.commute diff_in_polynomial_bool_pac_idealI

have H3: ‹x12 ∈# dom_m A ⟹
the (fmlookup A x12) * q - r ∈ More_Modules.ideal polynomial_bool ⟹
r - spec ∈ More_Modules.ideal polynomial_bool ⟹
spec ∈ pac_ideal (set_mset B)› for x12 r q
using ‹(A,B) ∈ polys_rel›
of ‹the (fmlookup A x12)› _  ‹the (fmlookup A x12)›],
of ‹set_mset B ∪ polynomial_bool› ‹2 * the (fmlookup A x12) - r›]
unfolding polys_rel_def
by (subgoal_tac ‹r ∈ pac_ideal (set_mset B)›)
(auto dest!: multi_member_split simp: ran_m_def H3'
intro: diff_in_polynomial_bool_pac_idealI)

have [intro]: ‹spec ∈ pac_ideal (set_mset B) ⟹ spec ∈ pac_ideal (set_mset A⇩0)› and
vars_B: ‹⋃ (vars ` set_mset B) ⊆ 𝒱›and
vars_B: ‹⋃ (vars ` set_mset (ran_m A)) ⊆ 𝒱›
using rtranclp_PAC_Format_subset_ideal[OF A⇩0B  vars_A⇩0] spec⇩0 ‹(A, B) ∈ polys_rel›[unfolded polys_rel_def, simplified]
by (smt (verit) in_mono mem_Collect_eq restricted_ideal_to_def)+

have eq_successI: ‹st' ≠ FAILED ⟹
st' ≠ FOUND ⟹ st' = SUCCESS› for st'
by (cases st') auto
have vars_diff_inv: ‹vars (Var x2 - r) = vars (r - Var x2 :: int mpoly)› for x2 r
using vars_uminus[of ‹Var x2 - r›]
by (auto simp del: vars_uminus)
have vars_add_inv: ‹vars (Var x2 + r) = vars (r + Var x2 :: int mpoly)› for x2 r
unfolding add.commute[of ‹Var x2› r] ..

have [iff]: ‹a ≠ FAILED› and
[intro]: ‹a ≠ SUCCESS ⟹ a = FOUND› and
[simp]: ‹merge_status a FOUND = FOUND›
using assms(2) by (cases a; auto)+
note [[goals_limit=1]]
show ?thesis
unfolding PAC_checker_step_def PAC_checker_specification_step_spec_def
check_extension_def polys_rel_full_def
apply (cases st)
apply clarsimp_all
subgoal for x11 x12 x13 x14
apply (refine_vcg lhs_step_If)
subgoal for r eqa st'
using assms vars_B apply -
apply (rule RETURN_SPEC_refine)
apply (rule_tac x = ‹(merge_status a st',𝒱,add_mset r B)› in exI)
by (auto simp: polys_rel_update_remove ran_m_mapsto_upd_notin
subgoal
by (rule RETURN_SPEC_refine)
(auto simp: Ex_status_iff dest: rtranclp_PAC_Format_subset_ideal)
done
subgoal for x11 x12 x13 x14
apply (refine_vcg lhs_step_If)
subgoal for r q eqa st'
using assms vars_B apply -
apply (rule RETURN_SPEC_refine)
apply (rule_tac x = ‹(merge_status a st',𝒱,add_mset r B)› in exI)
by (auto intro: polys_rel_update_remove intro: PAC_Format_add_and_remove(3-) H3
dest: rtranclp_PAC_Format_subset_ideal)
subgoal
by (rule RETURN_SPEC_refine)
(auto simp: Ex_status_iff)
done
subgoal for x31 x32 x34
apply (refine_vcg lhs_step_If)
subgoal for r x
using assms vars_B apply -
apply (rule RETURN_SPEC_refine)
apply (rule_tac x = ‹(a,insert x32 𝒱, add_mset r B)› in exI)
apply (auto simp: intro!: polys_rel_update_remove PAC_Format_add_and_remove(5-)
dest: rtranclp_PAC_Format_subset_ideal)
done
subgoal
by (rule RETURN_SPEC_refine)
(auto simp: Ex_status_iff)
done
subgoal for x11
unfolding check_del_def
apply (refine_vcg lhs_step_If)
subgoal for eq
using assms vars_B apply -
apply (rule RETURN_SPEC_refine)
apply (cases ‹x11 ∈# dom_m A›)
subgoal
apply (rule_tac x = ‹(a,𝒱, remove1_mset (the (fmlookup A x11)) B)› in exI)
is_failed_def is_success_def is_found_def
dest!: eq_successI
split: if_splits
dest: rtranclp_PAC_Format_subset_ideal
done
subgoal
apply (rule_tac x = ‹(a,𝒱, B)› in exI)
apply (auto simp: fmdrop_irrelevant
is_failed_def is_success_def is_found_def
dest!: eq_successI
split: if_splits
dest: rtranclp_PAC_Format_subset_ideal
done
done
subgoal
by (rule RETURN_SPEC_refine)
(auto simp: Ex_status_iff)
done
done
qed

definition PAC_checker
:: ‹int_poly ⇒ fpac_step ⇒ status ⇒ (int_poly, nat, nat) pac_step list ⇒
(status × fpac_step) nres›
where
‹PAC_checker spec A b st = do {
(S, _) ← WHILE⇩T
(λ((b :: status, A :: fpac_step), st). ¬is_failed b ∧ st ≠ [])
(λ((bA), st). do {
ASSERT(st ≠ []);
S ← PAC_checker_step spec (bA) (hd st);
RETURN (S, tl st)
})
((b, A), st);
RETURN S
}›

lemma PAC_checker_specification_spec_trans:
‹PAC_checker_specification_spec spec A (st, x2) ⟹
PAC_checker_specification_step_spec A spec x2 (st', x1a) ⟹
PAC_checker_specification_spec spec A (st', x1a)›
unfolding PAC_checker_specification_spec_def
PAC_checker_specification_step_spec_def
apply auto
using is_failed_alt_def apply blast+
done

lemma RES_SPEC_eq:
‹RES Φ = SPEC(λP. P ∈ Φ)›
by auto

lemma is_failed_is_success_completeD:
‹¬ is_failed x ⟹ ¬is_success x ⟹ is_found x›
by (cases x) auto

lemma PAC_checker_PAC_checker_specification2:
‹(A, B) ∈  polys_rel_full ⟹
¬is_failed a ⟹
(a = FOUND ⟹ spec ∈ pac_ideal (set_mset (snd B))) ⟹
⋃(vars ` set_mset (ran_m (snd A))) ⊆ fst B ⟹
vars spec ⊆ fst B ⟹
PAC_checker spec A a st ≤ ⇓ (status_rel ×⇩r polys_rel_full) (PAC_checker_specification2 spec B)›
unfolding PAC_checker_def conc_fun_RES
apply (subst RES_SPEC_eq)
apply (refine_vcg WHILET_rule[where
I = ‹λ((bB), st). bB ∈ (status_rel ×⇩r polys_rel_full)¯ ``
Collect (PAC_checker_specification_spec spec B)›
and R = ‹measure (λ(_, st).  Suc (length st))›])
subgoal by auto
subgoal apply (auto simp: PAC_checker_specification_spec_def)
apply (cases B; cases A)
apply (auto simp:polys_rel_def polys_rel_full_def Image_iff)
done
subgoal by auto
subgoal
apply auto
apply (rule
PAC_checker_step_PAC_checker_specification2[of _ _ _ _ _ _ _ ‹fst B›, THEN order_trans])
apply assumption
apply assumption
apply (auto intro: PAC_checker_specification_spec_trans simp: conc_fun_RES)
apply (auto simp: PAC_checker_specification_spec_def polys_rel_full_def polys_rel_def
dest: PAC_Format_subset_ideal
dest: is_failed_is_success_completeD; fail)+
by (auto simp: Image_iff intro: PAC_checker_specification_spec_trans
simp: polys_rel_def polys_rel_full_def)
subgoal
by auto
done

definition remap_polys_polynomial_bool :: ‹int mpoly ⇒ nat set ⇒ (nat, int_poly) fmap ⇒ (status × fpac_step) nres› where
‹remap_polys_polynomial_bool spec = (λ𝒱 A.
SPEC(λ(st, 𝒱', A'). (¬is_failed st ⟶
dom_m A = dom_m A' ∧
(∀i ∈# dom_m A. the (fmlookup A i) - the (fmlookup A' i) ∈ ideal polynomial_bool) ∧
⋃(vars ` set_mset (ran_m A)) ⊆ 𝒱' ∧
⋃(vars ` set_mset (ran_m A')) ⊆ 𝒱') ∧
(st = FOUND ⟶ spec ∈# ran_m A')))›

definition remap_polys_change_all :: ‹int mpoly ⇒ nat set ⇒ (nat, int_poly) fmap ⇒ (status × fpac_step) nres› where
‹remap_polys_change_all spec = (λ𝒱 A. SPEC (λ(st, 𝒱', A').
(¬is_failed st ⟶
pac_ideal (set_mset (ran_m A)) = pac_ideal (set_mset (ran_m A')) ∧
⋃(vars ` set_mset (ran_m A)) ⊆ 𝒱' ∧
⋃(vars ` set_mset (ran_m A')) ⊆ 𝒱') ∧
(st = FOUND ⟶ spec ∈# ran_m A')))›

lemma fmap_eq_dom_iff:
‹A = A' ⟷ dom_m A = dom_m A' ∧ (∀i ∈# dom_m A. the (fmlookup A i) = the (fmlookup A' i))›
by (metis fmap_ext in_dom_m_lookup_iff option.expand)

lemma ideal_remap_incl:
‹finite A' ⟹ (∀a'∈A'. ∃a∈A. a-a' ∈ B) ⟹ ideal (A' ∪ B) ⊆ ideal (A ∪ B)›
apply (induction A' rule: finite_induct)
apply (auto intro: ideal.span_mono)
using ideal.span_mono sup_ge2 apply blast
proof -
fix x :: 'a and F :: "'a set" and xa :: 'a and a :: 'a
assume a1: "a ∈ A"
assume a2: "a - x ∈ B"
assume a3: "xa ∈ More_Modules.ideal (insert x (F ∪ B))"
assume a4: "More_Modules.ideal (F ∪ B) ⊆ More_Modules.ideal (A ∪ B)"
have "x ∈ More_Modules.ideal (A ∪ B)"
ideal.module_axioms ideal.span_diff in_mono module.span_superset)
then show "xa ∈ More_Modules.ideal (A ∪ B)"
using a4 a3 ideal.span_insert_subset by blast
qed

lemma pac_ideal_remap_eq:
‹dom_m b = dom_m ba ⟹
∀i∈#dom_m ba.
the (fmlookup b i) - the (fmlookup ba i)
∈ More_Modules.ideal polynomial_bool ⟹
pac_ideal ((λx. the (fmlookup b x)) ` set_mset (dom_m ba)) = pac_ideal ((λx. the (fmlookup ba x)) ` set_mset (dom_m ba))›
unfolding pac_ideal_alt_def
apply standard
subgoal
apply (rule ideal_remap_incl)
apply (auto dest!: multi_member_split
dest: ideal.span_neg)
apply (drule ideal.span_neg)
apply auto
done
subgoal
by (rule ideal_remap_incl)
(auto dest!: multi_member_split)
done

lemma remap_polys_polynomial_bool_remap_polys_change_all:
‹remap_polys_polynomial_bool spec 𝒱 A ≤ remap_polys_change_all spec 𝒱 A›
unfolding remap_polys_polynomial_bool_def remap_polys_change_all_def
apply (simp add: ideal.span_zero fmap_eq_dom_iff ideal.span_eq)
apply (auto dest: multi_member_split simp: ran_m_def ideal.span_base pac_ideal_remap_eq
eq_commute[of ‹add_mset _ _› ‹dom_m (A :: (nat, int mpoly)fmap)› for A])
done

definition remap_polys :: ‹int mpoly ⇒ nat set ⇒ (nat, int_poly) fmap ⇒ (status × fpac_step) nres› where
‹remap_polys spec = (λ𝒱 A. do{
dom ← SPEC(λdom. set_mset (dom_m A) ⊆ dom ∧ finite dom);

failed ← SPEC(λ_::bool. True);
if failed
then do {
RETURN (FAILED, 𝒱, fmempty)
}
else do {
(b, N) ← FOREACH dom
(λi (b, 𝒱, A').
if i ∈# dom_m A
then do {
p ← SPEC(λp. the (fmlookup A i) - p ∈ ideal polynomial_bool ∧ vars p ⊆ vars (the (fmlookup A i)));
eq ← SPEC(λeq. eq ⟶ p = spec);
𝒱 ← SPEC(λ𝒱'. 𝒱 ∪ vars (the (fmlookup A i)) ⊆ 𝒱');
RETURN(b ∨ eq, 𝒱, fmupd i p A')
} else RETURN (b, 𝒱, A'))
(False, 𝒱, fmempty);
RETURN (if b then FOUND else SUCCESS, N)
}
})›

lemma remap_polys_spec:
‹remap_polys spec 𝒱 A ≤ remap_polys_polynomial_bool spec 𝒱 A›
unfolding remap_polys_def remap_polys_polynomial_bool_def
apply (refine_vcg FOREACH_rule[where
I = ‹λdom (b, 𝒱, A').
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')) ⊆ 𝒱 ∧
(b ⟶ spec ∈# ran_m A')›])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal
by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by clarsimp auto
subgoal
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: ran_m_mapsto_upd_notin)
subgoal
by auto
subgoal
by auto
subgoal
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)
subgoal
by auto
subgoal
by (auto simp: distinct_set_mset_eq_iff[symmetric] distinct_mset_dom)
subgoal
by (auto simp: distinct_set_mset_eq_iff[symmetric] distinct_mset_dom)
subgoal
by (auto simp add: ran_m_mapsto_upd_notin dom_m_fmrestrict_set' subset_eq
fmlookup_restrict_set_id')
subgoal
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')
done

subsection ‹Full Checker›

definition full_checker
:: ‹int_poly ⇒ (nat, int_poly) fmap ⇒ (int_poly, nat,nat) pac_step list ⇒ (status × _) nres›
where
‹full_checker spec0 A pac = do {
spec ← normalize_poly_spec spec0;
(st, 𝒱, A) ← remap_polys_change_all spec {} A;
if is_failed st then
RETURN (st, 𝒱, A)
else do {
𝒱 ← SPEC(λ𝒱'. 𝒱 ∪ vars spec0 ⊆ 𝒱');
PAC_checker spec (𝒱, A) st pac
}
}›

lemma restricted_ideal_to_mono:
‹restricted_ideal_to⇩I 𝒱 I ⊆ restricted_ideal_to⇩I 𝒱' J ⟹
𝒰 ⊆ 𝒱 ⟹
restricted_ideal_to⇩I 𝒰 I ⊆ restricted_ideal_to⇩I 𝒰  J›
by (auto simp: restricted_ideal_to_def)

lemma pac_ideal_idemp: ‹pac_ideal (pac_ideal A) = pac_ideal A›
by (metis dual_order.antisym ideal.span_subset_spanI ideal.span_superset le_sup_iff pac_ideal_def)

lemma full_checker_spec:
assumes ‹(A, A') ∈ polys_rel›
shows
‹full_checker spec A pac ≤ ⇓{((st, G), (st', G')). (st, st') ∈ status_rel ∧
(st ≠ FAILED ⟶ (G, G') ∈ polys_rel_full)}
(PAC_checker_specification spec (A'))›
proof -
have H: ‹set_mset b ⊆ pac_ideal (set_mset (ran_m A)) ⟹
x ∈ pac_ideal (set_mset b) ⟹ x ∈ pac_ideal (set_mset A')› for b x
using assms apply -
by (drule pac_ideal_mono) (auto simp: polys_rel_def pac_ideal_idemp)
have 1: ‹x ∈ {(st, 𝒱', A').
( ¬ is_failed st ⟶ pac_ideal (set_mset (ran_m x2)) =
pac_ideal (set_mset (ran_m A')) ∧
⋃ (vars ` set_mset (ran_m ABC)) ⊆ 𝒱' ∧
⋃ (vars ` set_mset (ran_m A')) ⊆ 𝒱') ∧
(st = FOUND ⟶ speca ∈# ran_m A')} ⟹
x = (st, x') ⟹ x' = (𝒱, Aa) ⟹((𝒱', Aa), 𝒱', ran_m Aa) ∈ polys_rel_full› for Aa speca x2 st x 𝒱' 𝒱 x' ABC
by (auto simp: polys_rel_def polys_rel_full_def)
have H1: ‹⋀a aa b xa x x1a x1 x2 speca.
vars spec ⊆ x1b ⟹
⋃ (vars ` set_mset (ran_m A)) ⊆ x1b ⟹
⋃ (vars ` set_mset (ran_m x2a)) ⊆ x1b ⟹
restricted_ideal_to⇩I x1b b ⊆ restricted_ideal_to⇩I x1b (ran_m x2a) ⟹
xa ∈ restricted_ideal_to⇩I (⋃ (vars ` set_mset (ran_m A)) ∪ vars spec) b ⟹
xa ∈ restricted_ideal_to⇩I (⋃ (vars ` set_mset (ran_m A)) ∪ vars spec) (ran_m x2a)›
for x1b b xa x2a
by (drule restricted_ideal_to_mono[of _ _ _ _ ‹⋃ (vars ` set_mset (ran_m A)) ∪ vars spec›])
auto
have H2: ‹⋀a aa b speca x2 x1a x1b x2a.
spec - speca ∈ More_Modules.ideal polynomial_bool ⟹
vars spec ⊆ x1b ⟹
⋃ (vars ` set_mset (ran_m A)) ⊆ x1b ⟹
⋃ (vars ` set_mset (ran_m x2a)) ⊆ x1b ⟹
speca ∈ pac_ideal (set_mset (ran_m x2a)) ⟹
restricted_ideal_to⇩I x1b b ⊆ restricted_ideal_to⇩I x1b (ran_m x2a) ⟹
spec ∈ pac_ideal (set_mset (ran_m x2a))›
by (metis (no_types, lifting) group_eq_aux ideal.span_add ideal.span_base in_mono
pac_ideal_alt_def sup.cobounded2)

show ?thesis
supply[[goals_limit=1]]
unfolding full_checker_def normalize_poly_spec_def
PAC_checker_specification_def remap_polys_change_all_def
apply (refine_vcg PAC_checker_PAC_checker_specification2[THEN order_trans, of _ _]
lhs_step_If)
subgoal by (auto simp: is_failed_def RETURN_RES_refine_iff)
apply (rule 1; assumption)
subgoal
using fmap_ext assms by (auto simp: polys_rel_def ran_m_def)
subgoal
by auto
subgoal
by auto
subgoal for speca x1 x2 x x1a x2a x1b
apply (rule ref_two_step[OF conc_fun_R_mono])
apply auto[]
using assms
by (auto simp add: PAC_checker_specification_spec_def conc_fun_RES polys_rel_def H1 H2
polys_rel_full_def
dest!: rtranclp_PAC_Format_subset_ideal dest: is_failed_is_success_completeD)
done
qed

lemma full_checker_spec':
shows
‹(uncurry2 full_checker, uncurry2 (λspec A _. PAC_checker_specification spec A)) ∈
(Id ×⇩r polys_rel) ×⇩r Id →⇩f ⟨{((st, G), (st', G')). (st, st') ∈ status_rel ∧
(st ≠ FAILED ⟶ (G, G') ∈ polys_rel_full)}⟩nres_rel›
using full_checker_spec
by (auto intro!: frefI nres_relI)

end

```