Theory EPAC_Checker_Specification

(* File: PAC_Checker_Specification.thy Author: Mathias Fleury, Daniela Kaufmann, JKU Maintainer: Mathias Fleury, JKU *) theory EPAC_Checker_Specification imports EPAC_Specification Refine_Imperative_HOL.IICF PAC_Checker.Finite_Map_Multiset PAC_Checker.PAC_Checker_Specification 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 ‹Algorithm› datatype ('a, 'b, 'lbls) pac_step = CL (pac_srcs: ‹('a × 'lbls) list›) (new_id: 'lbls) (pac_res: 'a) | Extension (new_id: 'lbls) (new_var: 'b) (pac_res: 'a) | Del (pac_src1: 'lbls) definition check_linear_comb :: ‹(nat, int mpoly) fmap ⇒ nat set ⇒ (int mpoly × nat) list ⇒ nat ⇒ int mpoly ⇒ bool nres› where ‹check_linear_comb 𝒜 𝒱 xs n r = SPEC(λb. b ⟶ (∀i ∈ set xs. snd i ∈# dom_m 𝒜 ∧ vars (fst i) ⊆ 𝒱) ∧ n ∉# dom_m 𝒜 ∧ vars r ⊆ 𝒱 ∧ xs ≠ [] ∧ (∑(p,n) ∈#mset xs. the (fmlookup 𝒜 n) * p) - r ∈ ideal polynomial_bool)› lemma PAC_Format_LC: assumes i: ‹((𝒱, A), 𝒱_B, B) ∈ polys_rel_full› and st: ‹PAC_Format^*^* (𝒱₀, A₀) (𝒱, B)› and vars: ‹∀i∈#x11. snd i ∈# dom_m A ∧ vars (fst i) ⊆ 𝒱› and AV: ‹⋃ (vars ` set_mset (ran_m A)) ⊆ 𝒱› and fin: ‹x11 ≠ {#}› and r: ‹(∑x∈#x11. case x of (p, n) ⇒ the (fmlookup A n) * p) - r ∈ More_Modules.ideal polynomial_bool› ‹vars r ⊆ 𝒱› shows ‹PAC_Format^*^* (𝒱, B) (𝒱, add_mset r B)› proof - have AB: ‹i ∈# dom_m A ⟹ the (fmlookup A i) ∈# B› and BA: ‹B = ran_m A› for i using i by (auto simp: polys_rel_full_def polys_rel_def) have ‹PAC_Format^*^* (𝒱, B) (𝒱, add_mset ((∑x∈#x11. case x of (p, n) ⇒ the (fmlookup A n) * p)) B)› using fin vars proof (induction x11) case empty then show ?case by auto next case (add x F) then have IH: ‹F ≠ {#} ⟹ PAC_Format^*^* (𝒱, B) (𝒱, add_mset (∑(p,n)∈#F. the (fmlookup A n) * p) B)› and x_A: ‹snd x ∈# dom_m A› and x_var: ‹vars (fst x) ⊆ 𝒱› and x_in: ‹the (fmlookup A (snd x)) ∈# B› using AB[of ‹snd x›] by auto have vars_A: ‹vars (the (fmlookup A (snd x))) ⊆ 𝒱› using AV x_A by (auto simp: ran_m_def) let ?B = ‹(add_mset (∑(p,n)∈#F. the (fmlookup A n) * p) B)› let ?p = ‹(∑(p,n)∈#F. the (fmlookup A n) * p)› let ?q = ‹(∑(p,n)∈#{#x#}. the (fmlookup A n) * p)› let ?vars = ‹λA. ⋃ (vars ` set_mset (A)) ⊆ 𝒱› consider (empty) ‹F = {#}› | (nempty) ‹F ≠ {#}› by blast then show ?case proof cases case empty2: empty have ‹PAC_Format (𝒱, B) (𝒱, add_mset ((∑x∈#{#x#}. case x of (p, n) ⇒ the (fmlookup A n) * p)) B)› apply (cases x) apply (rule PAC_Format.intros(2)[OF x_in, of ‹fst x›]) by (use x_var vars_A in ‹auto simp: ideal.span_zero elim!: vars_unE›) then show ?thesis using empty2 by auto next case nempty then have IH: ‹PAC_Format^*^* (𝒱, B) (𝒱, add_mset ?p B)› using IH by auto from rtranclp_PAC_Format_subset_ideal[OF this] have vars2: ‹?vars ?B› using AV unfolding BA[symmetric] by auto have 1: ‹PAC_Format (𝒱, ?B) (𝒱, add_mset (the (fmlookup A (snd x)) * fst x) ?B)› (is ‹PAC_Format _ (_, ?C)›) apply (cases x) apply (rule PAC_Format.intros(2)[of ‹the (fmlookup A (snd x))› _ ‹fst x›]) by (use x_in x_var vars_A in ‹auto simp: ideal.span_zero elim!: vars_unE›) from PAC_Format_subset_ideal[OF this] have ‹?vars (add_mset (the (fmlookup A (snd x)) * fst x) ?B)› using vars2 by auto have 2: ‹PAC_Format (𝒱, ?C) (𝒱, add_mset (∑(p,n)∈#add_mset x F. the (fmlookup A n) * p) ?C)› (is ‹PAC_Format _ (_, ?D)›) apply (cases x) apply (rule PAC_Format.intros(1)[of ‹?p› _ ?q]) by (use insert x_in x_var vars_A vars2 in ‹auto simp: ideal.span_zero elim!: in_vars_addE vars_unE›) then have 3: ‹PAC_Format^*^* (𝒱, ?D) (𝒱, add_mset (∑(p,n)∈# add_mset x F. the (fmlookup A n) * p) B)› using PAC_Format.del[of ?p ?D 𝒱] PAC_Format.del[of ‹the (fmlookup A (snd x)) * fst x› ‹remove1_mset ?p ?D› 𝒱] by (auto 4 7) show ?thesis using IH 1 2 3 by auto qed qed moreover have ‹PAC_Format (𝒱, add_mset (∑(p,n)∈#x11. the (fmlookup A n) * p) B) (𝒱, add_mset r (add_mset (∑(p,n)∈#x11. the (fmlookup A n) * p) B))› (is ‹PAC_Format _ ?E›) by (rule PAC_Format.intros(2)[of ‹(∑(p,n)∈#x11. the (fmlookup A n) * p)› _ 1]) (use r in auto) moreover have ‹PAC_Format ?E (𝒱, add_mset r B)› using PAC_Format.del[of ‹(∑(p,n)∈#x11. the (fmlookup A n) * p)› ‹snd ?E› ‹fst ?E›] by auto ultimately show ?thesis using st by auto qed definition PAC_checker_step_inv where ‹PAC_checker_step_inv spec stat 𝒱 A ⟷ (∀i∈#dom_m A. vars (the (fmlookup A i)) ⊆ 𝒱) ∧ vars spec ⊆ 𝒱› definition check_extension_precalc :: ‹(nat, int mpoly) fmap ⇒ nat set ⇒ nat ⇒ nat ⇒ int mpoly ⇒ (bool) nres› where ‹check_extension_precalc A 𝒱 i v p' = SPEC(λb. b ⟶ (i ∉# dom_m A ∧ (v ∉ 𝒱 ∧ (p')² - (p') ∈ ideal polynomial_bool ∧ vars (p') ⊆ 𝒱)))› 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 CL _ _ _ ⇒ do { ASSERT(PAC_checker_step_inv spec stat 𝒱 A); r ← normalize_poly_spec (pac_res st); eq ← check_linear_comb A 𝒱 (pac_srcs 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 { ASSERT(PAC_checker_step_inv spec stat 𝒱 A); eq ← check_del A (pac_src1 st); if eq then RETURN (stat, (𝒱, fmdrop (pac_src1 st) A)) else RETURN (FAILED, (𝒱, A)) } | Extension _ _ _ ⇒ do { ASSERT(PAC_checker_step_inv spec stat 𝒱 A); r ← normalize_poly_spec (pac_res st); (eq) ← check_extension_precalc A 𝒱 (new_id st) (new_var st) r; if eq then do { r0 ← SPEC(λr0. r0 = (r - Var (new_var st)) ∧ vars r0 = vars (r) ∪ {new_var st}); RETURN (stat, insert (new_var st) 𝒱, fmupd (new_id st) (r0) A)} else RETURN (FAILED, (𝒱, 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₀)› and A₀B: ‹PAC_Format^*^* (𝒱₀, A₀) (𝒱, B)› and spec₀: ‹vars spec ⊆ 𝒱₀› and vars_A₀: ‹⋃ (vars ` set_mset A₀) ⊆ 𝒱₀› shows ‹PAC_checker_step spec (a, (𝒱, A)) st ≤ ⇓ (status_rel ×_r polys_rel_full) (PAC_checker_specification_step2 (𝒱₀, A₀) 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 ⟹ spec - r ∈ 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 [intro]: ‹spec ∈ pac_ideal (set_mset B) ⟹ spec ∈ pac_ideal (set_mset A₀)› and vars_B: ‹⋃ (vars ` set_mset B) ⊆ 𝒱›and vars_B: ‹⋃ (vars ` set_mset (ran_m A)) ⊆ 𝒱› using rtranclp_PAC_Format_subset_ideal[OF A₀B vars_A₀] spec₀ ‹(A, B) ∈ polys_rel›[unfolded polys_rel_def, simplified] by (smt in_mono mem_Collect_eq restricted_ideal_to_def)+ have spec_found: ‹PAC_Format^*^* (𝒱₀, A₀) (V, add_mset r B) ⟹ r - spec ∈ ideal polynomial_bool ⟹ spec ∈ pac_ideal (set_mset A₀)› for V B r using rtranclp_PAC_Format_subset_ideal[of 𝒱₀ A₀ V ‹add_mset r B›] vars_A₀ spec₀ by (smt diff_in_polynomial_bool_pac_idealI2 in_mono mem_Collect_eq restricted_ideal_to_def rtranclp_PAC_Format_subset_ideal union_single_eq_member) 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 pre: ‹PAC_checker_step_inv spec a 𝒱 A› unfolding PAC_checker_step_inv_def using assms by (smt UN_I in_dom_in_ran_m rtranclp_PAC_Format_subset_ideal subset_iff vars_B) have G[intro]: ‹ b² - b ∈ ideal polynomial_bool› if ‹a - b ∈ ideal polynomial_bool› ‹a² - a ∈ ideal polynomial_bool› for a b proof - have ‹(a-b) * (a+b-1) ∈ ideal polynomial_bool› using ideal_mult_right_in that(1) by blast then have ‹-(a-b) * (a+b-1) ∈ ideal polynomial_bool› using ideal.span_neg ideal_mult_right_in that(1) by blast then have ‹-(a-b) * (a+b-1) + (a² - a) ∈ ideal polynomial_bool› using ideal.span_add that(2) by blast then show ‹?thesis› by (auto simp: algebra_simps power2_eq_square) qed 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_extension_precalc_def polys_rel_full_def check_linear_comb_def apply (cases st) apply clarsimp_all subgoal for x11 x12 x13 apply (refine_vcg lhs_step_If) subgoal by (rule pre) subgoal for r eqa st' using assms vars_B PAC_Format_LC[OF assms(1), of 𝒱₀ A₀ ‹mset x11› r] spec_found[of 𝒱 r B] rtranclp_trans[of PAC_Format ‹(𝒱₀, A₀)› ‹(𝒱, B)› ‹(𝒱, add_mset r B)›] apply - apply (rule RETURN_SPEC_refine) apply (rule_tac x = ‹(merge_status a st',𝒱,add_mset r B)› in exI) apply (auto simp: polys_rel_update_remove ran_m_mapsto_upd_notin intro: PAC_Format_add_and_remove dest: rtranclp_PAC_Format_subset_ideal) done subgoal by (rule RETURN_SPEC_refine) (auto simp: Ex_status_iff dest: rtranclp_PAC_Format_subset_ideal) done subgoal for x31 x32 x34 apply (refine_vcg lhs_step_If) subgoal by (rule pre) subgoal for r0 x r using assms vars_B apply - apply (rule RETURN_SPEC_refine) apply (rule_tac x = ‹(a,insert x32 𝒱, add_mset r B)› in exI) apply clarsimp_all apply (intro conjI) by (auto simp: intro!: polys_rel_update_remove PAC_Format_add_and_remove(5-) dest: rtranclp_PAC_Format_subset_ideal) 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 by (rule pre) 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) 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_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 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 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