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
      add_mset_eq_add_mset removeAll_notin
    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)

lemma PAC_Format_add_and_remove:
  ‹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)
    apply (auto simp: polys_rel_def ran_m_def add_mset_eq_add_mset dest!: multi_member_split)
    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›
  by (simp add: fmap_ext in_dom_m_lookup_iff)

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
       ideal.span_base pac_idealI3 set_image_mset set_mset_add_mset_insert union_single_eq_member)+
  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›
      ideal.span_add[OF ideal.span_add[OF ideal.span_neg ideal.span_neg,
         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
       set_mset_add_mset_insert union_single_eq_member)
   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›
      ideal.span_add[OF ideal.span_add[OF ideal.span_neg ideal.span_neg,
         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
       ideal.span_base pac_idealI3 set_image_mset set_mset_add_mset_insert union_single_eq_member)

  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›
      ideal.span_add[OF ideal.span_add[OF ideal.span_neg ideal.span_neg,
         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
      normalize_poly_spec_alt_def check_mult_def check_add_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
          intro: PAC_Format_add_and_remove H2 dest: rtranclp_PAC_Format_subset_ideal)
      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)
          apply (auto simp: polys_rel_update_remove PAC_Format_add_and_remove
               is_failed_def is_success_def is_found_def
            dest!: eq_successI
            split: if_splits
            dest: rtranclp_PAC_Format_subset_ideal
            intro: PAC_Format_add_and_remove H3)
          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
            intro: PAC_Format_add_and_remove)
          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)"
      using a2 a1 by (metis (no_types, lifting) Un_upper1 Un_upper2 add_diff_cancel_left' diff_add_cancel
        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
    add_mset_eq_add_mset
    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 using ideal.span_add 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