diff --git a/thys/PAC_Checker/PAC_Checker.thy b/thys/PAC_Checker/PAC_Checker.thy --- a/thys/PAC_Checker/PAC_Checker.thy +++ b/thys/PAC_Checker/PAC_Checker.thy @@ -1,1383 +1,1383 @@ (* File: PAC_Checker.thy Author: Mathias Fleury, Daniela Kaufmann, JKU Maintainer: Mathias Fleury, JKU *) theory PAC_Checker imports PAC_Polynomials_Operations PAC_Checker_Specification PAC_Map_Rel Show.Show Show.Show_Instances PAC_Misc begin 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 \Extended error message\ datatype 'a code_status = is_cfailed: CFAILED (the_error: 'a) | CSUCCESS | is_cfound: CFOUND text \In the following function, we merge errors. We will never merge an error message with an another error message; hence we do not attempt to concatenate error messages. \ fun merge_cstatus where \merge_cstatus (CFAILED a) _ = CFAILED a\ | \merge_cstatus _ (CFAILED a) = CFAILED a\ | \merge_cstatus CFOUND _ = CFOUND\ | \merge_cstatus _ CFOUND = CFOUND\ | \merge_cstatus _ _ = CSUCCESS\ definition code_status_status_rel :: \('a code_status \ status) set\ where \code_status_status_rel = {(CFOUND, FOUND), (CSUCCESS, SUCCESS)} \ {(CFAILED a, FAILED)| a. True}\ lemma in_code_status_status_rel_iff[simp]: \(CFOUND, b) \ code_status_status_rel \ b = FOUND\ \(a, FOUND) \ code_status_status_rel \ a = CFOUND\ \(CSUCCESS, b) \ code_status_status_rel \ b = SUCCESS\ \(a, SUCCESS) \ code_status_status_rel \ a = CSUCCESS\ \(a, FAILED) \ code_status_status_rel \ is_cfailed a\ \(CFAILED C, b) \ code_status_status_rel \ b = FAILED\ by (cases a; cases b; auto simp: code_status_status_rel_def; fail)+ 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 (Add p1 p2 i r) (Add p1' p2' i' r') \ (p1, p1') \ R1 \ (p2, p2') \ R1 \ (i, i') \ R1 \ (r, r') \ R2\ | \pac_step_rel_raw R1 R2 R3 (Mult p1 p2 i r) (Mult p1' p2' i' r') \ (p1, p1') \ R1 \ (p2, p2') \ R2 \ (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 (Add p1 p2 i r) (Add p1' p2' i' r') = R1 p1 p1' * R1 p2 p2' * R1 i i' * R2 r r'\ | \pac_step_rel_assn R1 R2 R3 (Mult p1 p2 i r) (Mult p1' p2' i' r') = R1 p1 p1' * R2 p2 p2' * 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 (Add p1 p2 i r, Add p1' p2' i' r') \ R1 p1 p1' * R1 p2 p2' * R1 i i' * R2 r r' | (Mult p1 p2 i r, Mult p1' p2' i' r') \ R1 p1 p1' * R2 p2 p2' * 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\ definition error_msg where \error_msg i msg = CFAILED (''s CHECKING failed at line '' @ show i @ '' with error '' @ msg)\ definition error_msg_notin_dom_err where \error_msg_notin_dom_err = '' notin domain''\ definition error_msg_notin_dom :: \nat \ string\ where \error_msg_notin_dom i = show i @ error_msg_notin_dom_err\ definition error_msg_reused_dom where \error_msg_reused_dom i = show i @ '' already in domain''\ definition error_msg_not_equal_dom where \error_msg_not_equal_dom p q pq r = show p @ '' + '' @ show q @ '' = '' @ show pq @ '' not equal'' @ show r\ definition check_not_equal_dom_err :: \llist_polynomial \ llist_polynomial \ llist_polynomial \ llist_polynomial \ string nres\ where \check_not_equal_dom_err p q pq r = SPEC (\_. True)\ definition vars_llist :: \llist_polynomial \ string set\ where \vars_llist xs = \(set ` fst ` set xs)\ definition check_addition_l :: \_ \ _ \ string set \ nat \ nat \ nat \ llist_polynomial \ string code_status nres\ where \check_addition_l spec A \ p q i r = do { let b = p \# dom_m A \ q \# dom_m A \ i \# dom_m A \ vars_llist r \ \; if \b then RETURN (error_msg i ((if p \# dom_m A then error_msg_notin_dom p else []) @ (if q \# dom_m A then error_msg_notin_dom p else []) @ (if i \# dom_m A then error_msg_reused_dom p else []))) else do { ASSERT (p \# dom_m A); let p = the (fmlookup A p); ASSERT (q \# dom_m A); let q = the (fmlookup A q); pq \ add_poly_l (p, q); b \ weak_equality_l pq r; b' \ weak_equality_l r spec; if b then (if b' then RETURN CFOUND else RETURN CSUCCESS) else do { c \ check_not_equal_dom_err p q pq r; RETURN (error_msg i c)} } }\ paragraph \Multiplication checking\ definition check_mult_l_dom_err :: \bool \ nat \ bool \ nat \ string nres\ where \check_mult_l_dom_err p_notin p i_already i = SPEC (\_. True)\ definition check_mult_l_mult_err :: \llist_polynomial \ llist_polynomial \ llist_polynomial \ llist_polynomial \ string nres\ where \check_mult_l_mult_err p q pq r = SPEC (\_. True)\ definition check_mult_l :: \_ \ _ \ _ \ nat \llist_polynomial \ nat \ llist_polynomial \ string code_status nres\ where \check_mult_l spec A \ p q i r = do { let b = p \# dom_m A \ i \# dom_m A \ vars_llist q \ \\ vars_llist r \ \; if \b then do { c \ check_mult_l_dom_err (p \# dom_m A) p (i \# dom_m A) i; RETURN (error_msg i c)} else do { ASSERT (p \# dom_m A); let p = the (fmlookup A p); pq \ mult_poly_full p q; b \ weak_equality_l pq r; b' \ weak_equality_l r spec; if b then (if b' then RETURN CFOUND else RETURN CSUCCESS) else do { c \ check_mult_l_mult_err p q pq r; RETURN (error_msg i c) } } }\ paragraph \Deletion checking\ definition check_del_l :: \_ \ _ \ nat \ string code_status nres\ where \check_del_l spec A p = RETURN CSUCCESS\ paragraph \Extension checking\ definition check_extension_l_dom_err :: \nat \ string nres\ where \check_extension_l_dom_err p = SPEC (\_. True)\ definition check_extension_l_no_new_var_err :: \llist_polynomial \ string nres\ where \check_extension_l_no_new_var_err p = SPEC (\_. True)\ definition check_extension_l_new_var_multiple_err :: \string \ llist_polynomial \ string nres\ where \check_extension_l_new_var_multiple_err v p = SPEC (\_. True)\ definition check_extension_l_side_cond_err :: \string \ llist_polynomial \ llist_polynomial \ llist_polynomial \ string nres\ where \check_extension_l_side_cond_err v p p' q = SPEC (\_. True)\ definition check_extension_l :: \_ \ _ \ string set \ nat \ string \ llist_polynomial \ (string code_status) nres\ where \check_extension_l spec A \ i v p = do { let b = i \# dom_m A \ v \ \ \ ([v], -1) \ set p; if \b then do { c \ check_extension_l_dom_err i; RETURN (error_msg i c) } else do { let p' = remove1 ([v], -1) 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 { p2 \ mult_poly_full p' p'; let p' = map (\(a,b). (a, -b)) p'; q \ add_poly_l (p2, p'); eq \ weak_equality_l q []; if eq then do { RETURN (CSUCCESS) } else do { c \ check_extension_l_side_cond_err v p p' q; RETURN (error_msg i c) } } } }\ lemma check_extension_alt_def: \check_extension A \ i v p \ do { b \ SPEC(\b. b \ i \# dom_m A \ v \ \); if \b then RETURN (False) else do { p' \ RETURN (p + Var v); 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\<^sub>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\<^sub>0_def simp flip: monom.abs_eq simp: not_in_vars_coeff0 MPoly_Type.coeff_def Var.abs_eq Var\<^sub>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_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 (* Copy of WB_More_Refinement *) lemma RES_RES_RETURN_RES: \RES A \ (\T. RES (f T)) = RES (\(f ` A))\ by (auto simp: pw_eq_iff refine_pw_simps) lemma check_add_alt_def: \check_add A \ p q i r \ do { b \ SPEC(\b. b \ p \# dom_m A \ q \# dom_m A \ i \# dom_m A \ vars r \ \); if \b then RETURN False else do { ASSERT (p \# dom_m A); let p = the (fmlookup A p); ASSERT (q \# dom_m A); let q = the (fmlookup A q); pq \ add_poly_spec p q; eq \ weak_equality pq r; RETURN eq } }\ (is \_ \ ?A\) proof - have check_add_alt_def: \check_add A \ p q i r = do { b \ SPEC(\b. b \ p \# dom_m A \ q \# dom_m A \ i \# dom_m A \ vars r \ \); if \b then 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) else 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)}\ (is \_ = ?B\) by (auto simp: check_add_def RES_RES_RETURN_RES) have \?A \ \ Id (check_add A \ p q i r)\ apply refine_vcg apply ((auto simp: check_add_alt_def weak_equality_def add_poly_spec_def RES_RES_RETURN_RES summarize_ASSERT_conv cong: if_cong intro!: ideal.span_zero;fail)+) done then show ?thesis unfolding check_add_alt_def[symmetric] by simp qed lemma check_mult_alt_def: \check_mult A \ p q i r \ do { b \ SPEC(\b. b \ p \# dom_m A \ i \# dom_m A \ vars q \ \ \ vars r \ \); if \b then RETURN False else do { ASSERT (p \# dom_m A); let p = the (fmlookup A p); pq \ mult_poly_spec p q; p \ weak_equality pq r; RETURN p } }\ unfolding check_mult_def apply (rule refine_IdD) by refine_vcg (auto simp: check_mult_def weak_equality_def mult_poly_spec_def RES_RES_RETURN_RES intro!: ideal.span_zero exI[of _ \the (fmlookup A p) * q\]) primrec insort_key_rel :: "('b \ 'b \ bool) \ 'b \ 'b list \ 'b list" where "insort_key_rel f x [] = [x]" | "insort_key_rel f x (y#ys) = (if f x y then (x#y#ys) else y#(insort_key_rel f x ys))" lemma set_insort_key_rel[simp]: \set (insort_key_rel R x xs) = insert x (set xs)\ by (induction xs) auto lemma sorted_wrt_insort_key_rel: \total_on R (insert x (set xs)) \ transp R \ reflp R \ sorted_wrt R xs \ sorted_wrt R (insort_key_rel R x xs)\ by (induction xs) (auto dest: transpD reflpD simp: Restricted_Predicates.total_on_def) lemma sorted_wrt_insort_key_rel2: \total_on R (insert x (set xs)) \ transp R \ x \ set xs \ sorted_wrt R xs \ sorted_wrt R (insort_key_rel R x xs)\ by (induction xs) (auto dest: transpD simp: Restricted_Predicates.total_on_def in_mono) paragraph \Step checking\ 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. case st of Add _ _ _ _ \ do { r \ full_normalize_poly (pac_res st); eq \ check_addition_l spec A \ (pac_src1 st) (pac_src2 st) (new_id 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 { 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) } | Mult _ _ _ _ \ do { r \ full_normalize_poly (pac_res st); q \ full_normalize_poly (pac_mult st); eq \ check_mult_l spec A \ (pac_src1 st) q (new_id st) r; let _ = eq; if \is_cfailed eq then RETURN (merge_cstatus st' eq, \, fmupd (new_id st) r A) else RETURN (eq, \, A) } | Extension _ _ _ \ do { r \ full_normalize_poly (([new_var st], -1) # (pac_res st)); (eq) \ check_extension_l spec A \ (new_id st) (new_var st) r; if \is_cfailed eq then do { 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) definition mononoms_equal_up_to_reorder where \mononoms_equal_up_to_reorder xs ys \ map (\(a, b). (mset a, b)) xs = map (\(a, b). (mset a, b)) ys\ definition normalize_poly_l where \normalize_poly_l p = SPEC (\p'. normalize_poly_p\<^sup>*\<^sup>* ((\(a, b). (mset a, b)) `# mset p) ((\(a, b). (mset a, b)) `# mset p') \ 0 \# snd `# mset p' \ sorted_wrt (rel2p (term_order_rel \\<^sub>r int_rel)) p' \ (\ x \ mononoms p'. sorted_wrt (rel2p var_order_rel) x))\ definition remap_polys_l_dom_err :: \string nres\ where \remap_polys_l_dom_err = SPEC (\_. True)\ definition remap_polys_l :: \llist_polynomial \ string set \ (nat, llist_polynomial) fmap \ (_ code_status \ string set \ (nat, llist_polynomial) fmap) nres\ where \remap_polys_l spec = (\\ A. do{ dom \ SPEC(\dom. set_mset (dom_m A) \ dom \ finite dom); failed \ SPEC(\_::bool. True); if failed then do { c \ remap_polys_l_dom_err; RETURN (error_msg (0 :: nat) c, \, fmempty) } else do { (b, \, A) \ FOREACH dom (\i (b, \, A'). if i \# dom_m A then do { p \ full_normalize_poly (the (fmlookup A i)); eq \ weak_equality_l p spec; \ \ RETURN(\ \ vars_llist (the (fmlookup A i))); RETURN(b \ eq, \, fmupd i p A') } else RETURN (b, \, A')) (False, \, fmempty); RETURN (if b then CFOUND else CSUCCESS, \, A) }})\ definition PAC_checker_l where \PAC_checker_l spec A b st = do { (S, _) \ WHILE\<^sub>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 }\ subsection \Correctness\ text \We now enter the locale to reason about polynomials directly.\ context poly_embed begin abbreviation pac_step_rel where \pac_step_rel \ p2rel (\Id, fully_unsorted_poly_rel O mset_poly_rel, var_rel\ pac_step_rel_raw)\ abbreviation fmap_polys_rel where \fmap_polys_rel \ \nat_rel, sorted_poly_rel O mset_poly_rel\fmap_rel\ lemma \normalize_poly_p s0 s \ (s0, p) \ mset_poly_rel \ (s, p) \ mset_poly_rel\ by (auto simp: mset_poly_rel_def normalize_poly_p_poly_of_mset) lemma vars_poly_of_vars: \vars (poly_of_vars a :: int mpoly) \ (\ ` set_mset a)\ by (induction a) (auto simp: vars_mult_Var) lemma vars_polynomial_of_mset: \vars (polynomial_of_mset za) \ \(image \ ` (set_mset o fst) ` set_mset za)\ apply (induction za) using vars_poly_of_vars by (fastforce elim!: in_vars_addE simp: vars_mult_Const split: if_splits)+ lemma fully_unsorted_poly_rel_vars_subset_vars_llist: \(A, B) \ fully_unsorted_poly_rel O mset_poly_rel \ vars B \ \ ` vars_llist A\ by (auto simp: fully_unsorted_poly_list_rel_def mset_poly_rel_def set_rel_def var_rel_def br_def vars_llist_def list_rel_append2 list_rel_append1 list_rel_split_right_iff list_mset_rel_def image_iff unsorted_term_poly_list_rel_def list_rel_split_left_iff dest!: set_rev_mp[OF _ vars_polynomial_of_mset] split_list dest: multi_member_split dest: arg_cong[of \mset _\ \add_mset _ _\ set_mset]) lemma fully_unsorted_poly_rel_extend_vars: \(A, B) \ fully_unsorted_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 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_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\ shows \remap_polys_l spec \ A \ \(code_status_status_rel \\<^sub>r \var_rel\set_rel \\<^sub>r fmap_polys_rel) (remap_polys spec' \' 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 \ SPEC (\eqa. eqa \ pa = spec')\ for p pa using spec by (auto simp: weak_equality_l_def weak_equality_spec_def list_mset_rel_def br_def mset_poly_rel_def dest: list_rel_term_poly_list_rel_same_rightD sorted_poly_list_relD) have emp: \(\, \') \ \var_rel\set_rel \ ((False, \, fmempty), False, \', fmempty) \ bool_rel \\<^sub>r \var_rel\set_rel \\<^sub>r fmap_polys_rel\ for \ \' by auto show ?thesis using assms unfolding remap_polys_l_def remap_polys_l_dom_err_def remap_polys_def prod.case apply (refine_rcg full_normalize_poly fmap_rel_fmupd_fmap_rel) subgoal by auto subgoal by auto subgoal by (auto simp: error_msg_def) apply (rule 1) subgoal by auto apply (rule emp) subgoal using V by auto subgoal by auto subgoal by auto subgoal by (rule H') 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 by (auto intro!: fmap_rel_fmupd_fmap_rel) subgoal by auto subgoal by auto done qed lemma fref_to_Down_curry: \(uncurry f, uncurry g) \ [P]\<^sub>f A \ \B\nres_rel \ (\x x' y y'. P (x', y') \ ((x, y), (x', y')) \ A \ f x y \ \ B (g x' y'))\ unfolding fref_def uncurry_def nres_rel_def by auto lemma weak_equality_spec_weak_equality: \(p, p') \ mset_poly_rel \ (r, r') \ mset_poly_rel \ weak_equality_spec p r \ weak_equality p' r'\ unfolding weak_equality_spec_def weak_equality_def by (auto simp: mset_poly_rel_def) lemma weak_equality_l_weak_equality_l'[refine]: \weak_equality_l p q \ \ bool_rel (weak_equality p' q')\ if \(p, p') \ sorted_poly_rel O mset_poly_rel\ \(q, q') \ sorted_poly_rel O mset_poly_rel\ for p p' q q' using that by (auto intro!: weak_equality_l_weak_equality_spec[THEN fref_to_Down_curry, THEN order_trans] ref_two_step' weak_equality_spec_weak_equality simp flip: conc_fun_chain) lemma error_msg_ne_SUCCES[iff]: \error_msg i m \ CSUCCESS\ \error_msg i m \ CFOUND\ \is_cfailed (error_msg i m)\ \\is_cfound (error_msg i m)\ by (auto simp: error_msg_def) lemma sorted_poly_rel_vars_llist: \(r, r') \ sorted_poly_rel O mset_poly_rel \ vars r' \ \ ` vars_llist r\ apply (auto simp: mset_poly_rel_def set_rel_def var_rel_def br_def vars_llist_def list_rel_append2 list_rel_append1 list_rel_split_right_iff list_mset_rel_def image_iff sorted_poly_list_rel_wrt_def dest!: set_rev_mp[OF _ vars_polynomial_of_mset] dest!: split_list) apply (auto dest!: multi_member_split simp: list_rel_append1 term_poly_list_rel_def eq_commute[of _ \mset _\] list_rel_split_right_iff list_rel_append2 list_rel_split_left_iff dest: arg_cong[of \mset _\ \add_mset _ _\ set_mset]) done lemma check_addition_l_check_add: assumes \(A, B) \ fmap_polys_rel\ and \(r, r') \ sorted_poly_rel O mset_poly_rel\ \(p, p') \ Id\ \(q, q') \ Id\ \(i, i') \ nat_rel\ \(\', \) \ \var_rel\set_rel\ shows \check_addition_l spec A \' p q i r \ \ {(st, b). (\is_cfailed st \ b) \ (is_cfound st \ spec = r)} (check_add B \ p' q' i' r')\ proof - have [refine]: \add_poly_l (p, q) \ \ (sorted_poly_rel O mset_poly_rel) (add_poly_spec p' q')\ if \(p, p') \ sorted_poly_rel O mset_poly_rel\ \(q, q') \ sorted_poly_rel O mset_poly_rel\ for p p' q q' using that by (auto intro!: add_poly_l_add_poly_p'[THEN order_trans] ref_two_step' add_poly_p'_add_poly_spec simp flip: conc_fun_chain) show ?thesis using assms unfolding check_addition_l_def check_not_equal_dom_err_def apply - apply (rule order_trans) defer apply (rule ref_two_step') apply (rule check_add_alt_def) apply refine_rcg subgoal by (drule sorted_poly_rel_vars_llist) (auto simp: set_rel_def var_rel_def br_def) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: weak_equality_l_def bind_RES_RETURN_eq) done qed 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_mult_l_check_mult: assumes \(A, B) \ fmap_polys_rel\ and \(r, r') \ sorted_poly_rel O mset_poly_rel\ and \(q, q') \ sorted_poly_rel O mset_poly_rel\ \(p, p') \ Id\ \(i, i') \ nat_rel\ \(\, \') \ \var_rel\set_rel\ shows \check_mult_l spec A \ p q i r \ \ {(st, b). (\is_cfailed st \ b) \ (is_cfound st \ spec = r)} (check_mult B \' p' q' i' r')\ proof - have [refine]: \mult_poly_full p q \ \ (sorted_poly_rel O mset_poly_rel) (mult_poly_spec p' q')\ if \(p, p') \ sorted_poly_rel O mset_poly_rel\ \(q, q') \ sorted_poly_rel O mset_poly_rel\ for p p' q q' using that by (auto intro!: mult_poly_full_mult_poly_p'[THEN order_trans] ref_two_step' mult_poly_p'_mult_poly_spec simp flip: conc_fun_chain) show ?thesis using assms unfolding check_mult_l_def check_mult_l_mult_err_def check_mult_l_dom_err_def apply - apply (rule order_trans) defer apply (rule ref_two_step') apply (rule check_mult_alt_def) apply refine_rcg subgoal by (drule sorted_poly_rel_vars_llist)+ (fastforce simp: set_rel_def var_rel_def br_def) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: weak_equality_l_def bind_RES_RETURN_eq) done qed lemma normalize_poly_normalize_poly_spec: assumes \(r, t) \ unsorted_poly_rel O mset_poly_rel\ shows \normalize_poly r \ \(sorted_poly_rel O mset_poly_rel) (normalize_poly_spec t)\ proof - obtain s where rs: \(r, s) \ unsorted_poly_rel\ and st: \(s, t) \ mset_poly_rel\ using assms by auto show ?thesis by (rule normalize_poly_normalize_poly_p[THEN order_trans, OF rs]) (use st in \auto dest!: rtranclp_normalize_poly_p_poly_of_mset intro!: ref_two_step' RES_refine exI[of _ t] simp: normalize_poly_spec_def ideal.span_zero mset_poly_rel_def simp flip: conc_fun_chain\) qed lemma remove1_list_rel: \(xs, ys) \ \R\ list_rel \ (a, b) \ R \ IS_RIGHT_UNIQUE R \ IS_LEFT_UNIQUE R \ (remove1 a xs, remove1 b ys) \ \R\list_rel\ by (induction xs ys rule: list_rel_induct) (auto simp: single_valued_def IS_LEFT_UNIQUE_def) lemma remove1_list_rel2: \(xs, ys) \ \R\ list_rel \ (a, b) \ R \ (\c. (a, c) \ R \ c = b) \ (\c. (c, b) \ R \ c = a) \ (remove1 a xs, remove1 b ys) \ \R\list_rel\ apply (induction xs ys rule: list_rel_induct) apply (solves \simp (no_asm)\) - by (smt list_rel_simp(4) remove1.simps(2)) + by (smt (verit) list_rel_simp(4) remove1.simps(2)) lemma remove1_sorted_poly_rel_mset_poly_rel: assumes \(r, r') \ sorted_poly_rel O mset_poly_rel\ and \([a], 1) \ set r\ shows \(remove1 ([a], 1) r, r' - Var (\ a)) \ sorted_poly_rel O mset_poly_rel\ proof - have [simp]: \([a], {#a#}) \ term_poly_list_rel\ \\aa. ([a], aa) \ term_poly_list_rel \ aa = {#a#}\ by (auto simp: term_poly_list_rel_def) have H: \\aa. ([a], aa) \ term_poly_list_rel \ aa = {#a#}\ \\aa. (aa, {#a#}) \ term_poly_list_rel \ aa = [a]\ by (auto simp: single_valued_def IS_LEFT_UNIQUE_def term_poly_list_rel_def) have [simp]: \Const (1 :: int) = (1 :: int mpoly)\ by (simp add: Const.abs_eq Const\<^sub>0_one one_mpoly.abs_eq) have [simp]: \sorted_wrt term_order (map fst r) \ sorted_wrt term_order (map fst (remove1 ([a], 1) r))\ by (induction r) auto have [intro]: \distinct (map fst r) \ distinct (map fst (remove1 x r))\ for x by (induction r) (auto dest: notin_set_remove1) have [simp]: \(r, ya) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel \ polynomial_of_mset (mset ya) - Var (\ a) = polynomial_of_mset (remove1_mset ({#a#}, 1) (mset ya))\ for ya using assms by (auto simp: list_rel_append1 list_rel_split_right_iff dest!: split_list) show ?thesis using assms apply (elim relcompEpair) apply (rename_tac za, rule_tac b = \remove1_mset ({#a#}, 1) za\ in relcompI) apply (auto simp: mset_poly_rel_def sorted_poly_list_rel_wrt_def Collect_eq_comp' intro!: relcompI[of _ \remove1 ({#a#}, 1) ya\ for ya :: \(string multiset \ int) list\] remove1_list_rel2 intro: H simp: list_mset_rel_def br_def dest: in_diffD) done qed lemma remove1_sorted_poly_rel_mset_poly_rel_minus: assumes \(r, r') \ sorted_poly_rel O mset_poly_rel\ and \([a], -1) \ set r\ shows \(remove1 ([a], -1) r, r' + Var (\ a)) \ sorted_poly_rel O mset_poly_rel\ proof - have [simp]: \([a], {#a#}) \ term_poly_list_rel\ \\aa. ([a], aa) \ term_poly_list_rel \ aa = {#a#}\ by (auto simp: term_poly_list_rel_def) have H: \\aa. ([a], aa) \ term_poly_list_rel \ aa = {#a#}\ \\aa. (aa, {#a#}) \ term_poly_list_rel \ aa = [a]\ by (auto simp: single_valued_def IS_LEFT_UNIQUE_def term_poly_list_rel_def) have [simp]: \Const (1 :: int) = (1 :: int mpoly)\ by (simp add: Const.abs_eq Const\<^sub>0_one one_mpoly.abs_eq) have [simp]: \sorted_wrt term_order (map fst r) \ sorted_wrt term_order (map fst (remove1 ([a], -1) r))\ by (induction r) auto have [intro]: \distinct (map fst r) \ distinct (map fst (remove1 x r))\ for x apply (induction r) apply auto by (meson img_fst in_set_remove1D) have [simp]: \(r, ya) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel \ polynomial_of_mset (mset ya) + Var (\ a) = polynomial_of_mset (remove1_mset ({#a#}, -1) (mset ya))\ for ya using assms by (auto simp: list_rel_append1 list_rel_split_right_iff dest!: split_list) show ?thesis using assms apply (elim relcompEpair) apply (rename_tac za, rule_tac b = \remove1_mset ({#a#}, -1) za\ in relcompI) by (auto simp: mset_poly_rel_def sorted_poly_list_rel_wrt_def Collect_eq_comp' dest: in_diffD intro!: relcompI[of _ \remove1 ({#a#}, -1) ya\ for ya :: \(string multiset \ int) list\] remove1_list_rel2 intro: H simp: list_mset_rel_def br_def) qed lemma insert_var_rel_set_rel: \(\, \') \ \var_rel\set_rel \ (yb, x2) \ var_rel \ (insert yb \, insert x2 \') \ \var_rel\set_rel\ by (auto simp: var_rel_def set_rel_def) lemma var_rel_set_rel_iff: \(\, \') \ \var_rel\set_rel \ (yb, x2) \ var_rel \ yb \ \ \ x2 \ \'\ using \_inj inj_eq by (fastforce simp: var_rel_def set_rel_def br_def) lemma check_extension_l_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_l spec A \ i x r \ \{((st), (b)). (\is_cfailed st \ b) \ (is_cfound st \ spec = r)} (check_extension B \' i' x' r')\ proof - have \x' = \ x\ using assms(5) by (auto simp: var_rel_def br_def) have [refine]: \mult_poly_full p q \ \ (sorted_poly_rel O mset_poly_rel) (mult_poly_spec p' q')\ if \(p, p') \ sorted_poly_rel O mset_poly_rel\ \(q, q') \ sorted_poly_rel O mset_poly_rel\ for p p' q q' using that by (auto intro!: mult_poly_full_mult_poly_p'[THEN order_trans] ref_two_step' mult_poly_p'_mult_poly_spec simp flip: conc_fun_chain) have [refine]: \add_poly_l (p, q) \ \ (sorted_poly_rel O mset_poly_rel) (add_poly_spec p' q')\ if \(p, p') \ sorted_poly_rel O mset_poly_rel\ \(q, q') \ sorted_poly_rel O mset_poly_rel\ for p p' q q' using that by (auto intro!: add_poly_l_add_poly_p'[THEN order_trans] ref_two_step' add_poly_p'_add_poly_spec simp flip: conc_fun_chain) have [simp]: \(l, l') \ \term_poly_list_rel \\<^sub>r int_rel\list_rel \ (map (\(a, b). (a, - b)) l, map (\(a, b). (a, - b)) l') \ \term_poly_list_rel \\<^sub>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 \\<^sub>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 \\<^sub>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 ba aa l l', rule_tac b = \(aa, - ba) # 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 intro: ext) 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 _ \{#}\]) show ?thesis unfolding check_extension_l_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 ) 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 (subst \x' = \ x\, rule remove1_sorted_poly_rel_mset_poly_rel_minus) subgoal using assms by auto subgoal using assms by auto 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 by auto subgoal by auto subgoal using assms by auto subgoal using assms by auto apply (rule uminus) subgoal using assms by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms by auto done qed lemma full_normalize_poly_diff_ideal: fixes dom assumes \(p, p') \ fully_unsorted_poly_rel O mset_poly_rel\ shows \full_normalize_poly p \ \ (sorted_poly_rel O mset_poly_rel) (normalize_poly_spec p')\ proof - obtain q where pq: \(p, q) \ fully_unsorted_poly_rel\ and qp':\(q, p') \ mset_poly_rel\ using assms by auto show ?thesis unfolding normalize_poly_spec_def apply (rule full_normalize_poly_normalize_poly_p[THEN order_trans]) apply (rule pq) unfolding conc_fun_chain[symmetric] by (rule ref_two_step', rule RES_refine) (use qp' in \auto dest!: rtranclp_normalize_poly_p_poly_of_mset simp: mset_poly_rel_def ideal.span_zero\) qed lemma insort_key_rel_decomp: \\ys zs. xs = ys @ zs \ insort_key_rel R x xs = ys @ x # zs\ apply (induction xs) subgoal by auto subgoal for a xs by (force intro: exI[of _ \a # _\]) done lemma list_rel_append_same_length: \length xs = length xs' \ (xs @ ys, xs' @ ys') \ \R\list_rel \ (xs, xs') \ \R\list_rel \ (ys, ys') \ \R\list_rel\ by (auto simp: list_rel_def list_all2_append2 dest: list_all2_lengthD) lemma term_poly_list_rel_list_relD: \(ys, cs) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel \ cs = map (\(a, y). (mset a, y)) ys\ by (induction ys arbitrary: cs) (auto simp: term_poly_list_rel_def list_rel_def list_all2_append list_all2_Cons1 list_all2_Cons2) lemma term_poly_list_rel_single: \([x32], {#x32#}) \ term_poly_list_rel\ by (auto simp: term_poly_list_rel_def) lemma unsorted_poly_rel_list_rel_list_rel_uminus: \(map (\(a, b). (a, - b)) r, yc) \ \unsorted_term_poly_list_rel \\<^sub>r int_rel\list_rel \ (r, map (\(a, b). (a, - b)) yc) \ \unsorted_term_poly_list_rel \\<^sub>r int_rel\list_rel\ by (induction r arbitrary: yc) (auto simp: elim!: list_relE3) lemma mset_poly_rel_minus: \({#(a, b)#}, v') \ mset_poly_rel \ (mset yc, r') \ mset_poly_rel \ (r, yc) \ \unsorted_term_poly_list_rel \\<^sub>r int_rel\list_rel \ (add_mset (a, b) (mset yc), v' + r') \ mset_poly_rel\ by (induction r arbitrary: r') (auto simp: mset_poly_rel_def polynomial_of_mset_uminus) lemma fully_unsorted_poly_rel_diff: \([v], v') \ fully_unsorted_poly_rel O mset_poly_rel \ (r, r') \ fully_unsorted_poly_rel O mset_poly_rel \ (v # r, v' + r') \ fully_unsorted_poly_rel O mset_poly_rel\ apply auto apply (rule_tac b = \y + ya\ in relcompI) apply (auto simp: fully_unsorted_poly_list_rel_def list_mset_rel_def br_def) apply (rule_tac b = \yb @ yc\ in relcompI) apply (auto elim!: list_relE3 simp: unsorted_poly_rel_list_rel_list_rel_uminus mset_poly_rel_minus) done lemma PAC_checker_l_step_PAC_checker_step: assumes \(Ast, Bst) \ code_status_status_rel \\<^sub>r \var_rel\set_rel \\<^sub>r fmap_polys_rel\ and \(st, st') \ pac_step_rel\ and spec: \(spec, spec') \ sorted_poly_rel O mset_poly_rel\ shows \PAC_checker_l_step spec Ast st \ \ (code_status_status_rel \\<^sub>r \var_rel\set_rel \\<^sub>r fmap_polys_rel) (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: \(A, B) \ fmap_polys_rel\ \(cst, cst') \ code_status_status_rel\ using assms(1) by (cases Ast; cases Bst; auto) have [refine]: \(r, ra) \ sorted_poly_rel O mset_poly_rel \ (eqa, eqaa) \ {(st, b). (\ is_cfailed st \ b) \ (is_cfound st \ spec = r)} \ 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 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 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_mult_l_check_mult check_addition_l_check_add full_normalize_poly_diff_ideal) subgoal using AB by auto subgoal using AB by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto intro: \) apply assumption+ subgoal by (auto simp: code_status_status_rel_def) subgoal by (auto intro!: fmap_rel_fmupd_fmap_rel fmap_rel_fmdrop_fmap_rel AB) subgoal using AB by auto done subgoal apply (refine_rcg normalize_poly_normalize_poly_spec check_mult_l_check_mult check_addition_l_check_add full_normalize_poly_diff_ideal[unfolded normalize_poly_spec_def[symmetric]]) subgoal using AB by auto subgoal using AB by auto subgoal using AB by auto subgoal by auto subgoal by auto subgoal by auto apply assumption+ subgoal by (auto simp: code_status_status_rel_def) subgoal by (auto intro!: fmap_rel_fmupd_fmap_rel fmap_rel_fmdrop_fmap_rel AB) subgoal using AB by auto done subgoal apply (refine_rcg full_normalize_poly_diff_ideal check_extension_l_check_extension) 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 simp: code_status_status_rel_def) subgoal by (auto simp: AB intro!: fmap_rel_fmupd_fmap_rel insert_var_rel_set_rel) subgoal by (auto simp: code_status_status_rel_def AB 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 AB by auto subgoal using AB by auto subgoal by (auto intro!: fmap_rel_fmupd_fmap_rel fmap_rel_fmdrop_fmap_rel code_status_status_rel_def AB) subgoal by (auto intro!: fmap_rel_fmupd_fmap_rel fmap_rel_fmdrop_fmap_rel AB) done done qed lemma code_status_status_rel_discrim_iff: \(x1a, x1c) \ code_status_status_rel \ is_cfailed x1a \ is_failed x1c\ \(x1a, x1c) \ code_status_status_rel \ is_cfound x1a \ is_found x1c\ by (cases x1a; cases x1c; auto; fail)+ lemma PAC_checker_l_PAC_checker: assumes \(A, B) \ \var_rel\set_rel \\<^sub>r fmap_polys_rel\ and \(st, st') \ \pac_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 \ \ (code_status_status_rel \\<^sub>r \var_rel\set_rel \\<^sub>r fmap_polys_rel) (PAC_checker spec' B b' st')\ proof - have [refine0]: \(((b, A), st), (b', B), st') \ ((code_status_status_rel \\<^sub>r \var_rel\set_rel \\<^sub>r fmap_polys_rel) \\<^sub>r \pac_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 WHILEIT_refine[where R = \((bool_rel \\<^sub>r \var_rel\set_rel \\<^sub>r fmap_polys_rel) \\<^sub>r \pac_step_rel\list_rel)\]) subgoal by (auto simp: code_status_status_rel_discrim_iff) 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 done qed end lemma less_than_char_of_char[code_unfold]: \(x, y) \ less_than_char \ (of_char x :: nat) < of_char y\ by (auto simp: less_than_char_def less_char_def) lemmas [code] = add_poly_l'.simps[unfolded var_order_rel_def] export_code add_poly_l' in SML module_name test definition 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 spec' {} A; if is_cfailed b then RETURN (b, \, A) else do { let \ = \ \ vars_llist spec; PAC_checker_l spec' (\, A) b st } }\ context poly_embed begin term normalize_poly_spec thm full_normalize_poly_diff_ideal[unfolded normalize_poly_spec_def[symmetric]] abbreviation unsorted_fmap_polys_rel where \unsorted_fmap_polys_rel \ \nat_rel, fully_unsorted_poly_rel O mset_poly_rel\fmap_rel\ lemma full_checker_l_full_checker: assumes \(A, B) \ unsorted_fmap_polys_rel\ and \(st, st') \ \pac_step_rel\list_rel\ and \(spec, spec') \ fully_unsorted_poly_rel O mset_poly_rel\ shows \full_checker_l spec A st \ \ (code_status_status_rel \\<^sub>r \var_rel\set_rel \\<^sub>r fmap_polys_rel) (full_checker spec' B st')\ proof - have [refine]: \(spec, spec') \ sorted_poly_rel O mset_poly_rel \ (\, \') \ \var_rel\set_rel \ remap_polys_l spec \ A \ \(code_status_status_rel \\<^sub>r \var_rel\set_rel \\<^sub>r fmap_polys_rel) (remap_polys_change_all spec' \' B)\ for spec spec' \ \' apply (rule remap_polys_l_remap_polys[THEN order_trans, OF assms(1)]) apply assumption+ apply (rule ref_two_step[OF order.refl]) apply(rule remap_polys_spec[THEN order_trans]) by (rule remap_polys_polynomial_bool_remap_polys_change_all) show ?thesis unfolding full_checker_l_def full_checker_def apply (refine_rcg remap_polys_l_remap_polys full_normalize_poly_diff_ideal[unfolded normalize_poly_spec_def[symmetric]] PAC_checker_l_PAC_checker) subgoal using assms(3) . subgoal by auto subgoal by (auto simp: is_cfailed_def is_failed_def) subgoal by auto apply (rule fully_unsorted_poly_rel_extend_vars) subgoal using assms(3) . subgoal by auto subgoal by auto subgoal using assms(2) by (auto simp: p2rel_def) subgoal by auto done qed lemma full_checker_l_full_checker': \(uncurry2 full_checker_l, uncurry2 full_checker) \ ((fully_unsorted_poly_rel O mset_poly_rel) \\<^sub>r unsorted_fmap_polys_rel) \\<^sub>r \pac_step_rel\list_rel \\<^sub>f \(code_status_status_rel \\<^sub>r \var_rel\set_rel \\<^sub>r fmap_polys_rel)\nres_rel\ apply (intro frefI nres_relI) using full_checker_l_full_checker by force end definition remap_polys_l2 :: \llist_polynomial \ string set \ (nat, llist_polynomial) fmap \ _ nres\ where \remap_polys_l2 spec = (\\ A. do{ n \ upper_bound_on_dom A; b \ RETURN (n \ 2^64); if b then do { c \ remap_polys_l_dom_err; RETURN (error_msg (0 ::nat) c, \, fmempty) } else do { (b, \, A) \ nfoldli ([0.._. True) (\i (b, \, A'). if i \# dom_m A then do { ASSERT(fmlookup A i \ None); p \ full_normalize_poly (the (fmlookup A i)); eq \ weak_equality_l p spec; \ \ RETURN (\ \ vars_llist (the (fmlookup A i))); RETURN(b \ eq, \, fmupd i p A') } else RETURN (b, \, A') ) (False, \, fmempty); RETURN (if b then CFOUND else CSUCCESS, \, A) } })\ lemma remap_polys_l2_remap_polys_l: \remap_polys_l2 spec \ A \ \ Id (remap_polys_l spec \ A)\ proof - have [refine]: \(A, A') \ Id \ upper_bound_on_dom A \ \ {(n, dom). dom = set [0..dom. set_mset (dom_m A') \ dom \ finite dom))\ for A A' unfolding upper_bound_on_dom_def apply (rule RES_refine) apply (auto simp: upper_bound_on_dom_def) done have 1: \inj_on id dom\ for dom by auto have 2: \x \# dom_m A \ x' \# dom_m A' \ (x, x') \ nat_rel \ (A, A') \ Id \ full_normalize_poly (the (fmlookup A x)) \ \ Id (full_normalize_poly (the (fmlookup A' x')))\ for A A' x x' by (auto) have 3: \(n, dom) \ {(n, dom). dom = set [0.. ([0.. \nat_rel\list_set_rel\ for n dom by (auto simp: list_set_rel_def br_def) have 4: \(p,q) \ Id \ weak_equality_l p spec \ \Id (weak_equality_l q spec)\ for p q spec by auto have 6: \a = b \ (a, b) \ Id\ for a b by auto show ?thesis unfolding remap_polys_l2_def remap_polys_l_def apply (refine_rcg LFO_refine[where R= \Id \\<^sub>r \Id\set_rel \\<^sub>r Id\]) subgoal by auto subgoal by auto subgoal by auto apply (rule 3) subgoal by auto subgoal by (simp add: in_dom_m_lookup_iff) subgoal by (simp add: in_dom_m_lookup_iff) apply (rule 2) subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (rule 4; assumption) apply (rule 6) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed end diff --git a/thys/PAC_Checker/PAC_Checker_Init.thy b/thys/PAC_Checker/PAC_Checker_Init.thy --- a/thys/PAC_Checker/PAC_Checker_Init.thy +++ b/thys/PAC_Checker/PAC_Checker_Init.thy @@ -1,892 +1,892 @@ (* File: PAC_Checker_Init.thy Author: Mathias Fleury, Daniela Kaufmann, JKU Maintainer: Mathias Fleury, JKU *) theory PAC_Checker_Init imports PAC_Checker WB_Sort PAC_Checker_Relation begin section \Initial Normalisation of Polynomials\ subsection \Sorting\ text \Adapted from the theory \<^text>\HOL-ex.MergeSort\ by Tobias Nipkow. We did not change much, but we refine it to executable code and try to improve efficiency. \ fun merge :: "_ \ 'a list \ 'a list \ 'a list" where "merge f (x#xs) (y#ys) = (if f x y then x # merge f xs (y#ys) else y # merge f (x#xs) ys)" | "merge f xs [] = xs" | "merge f [] ys = ys" lemma mset_merge [simp]: "mset (merge f xs ys) = mset xs + mset ys" by (induct f xs ys rule: merge.induct) (simp_all add: ac_simps) lemma set_merge [simp]: "set (merge f xs ys) = set xs \ set ys" by (induct f xs ys rule: merge.induct) auto lemma sorted_merge: "transp f \ (\x y. f x y \ f y x) \ sorted_wrt f (merge f xs ys) \ sorted_wrt f xs \ sorted_wrt f ys" apply (induct f xs ys rule: merge.induct) apply (auto simp add: ball_Un not_le less_le dest: transpD) apply blast apply (blast dest: transpD) done fun msort :: "_ \ 'a list \ 'a list" where "msort f [] = []" | "msort f [x] = [x]" | "msort f xs = merge f (msort f (take (size xs div 2) xs)) (msort f (drop (size xs div 2) xs))" fun swap_ternary :: \_\nat\nat\ ('a \ 'a \ 'a) \ ('a \ 'a \ 'a)\ where \swap_ternary f m n = (if (m = 0 \ n = 1) then (\(a, b, c). if f a b then (a, b, c) else (b,a,c)) else if (m = 0 \ n = 2) then (\(a, b, c). if f a c then (a, b, c) else (c,b,a)) else if (m = 1 \ n = 2) then (\(a, b, c). if f b c then (a, b, c) else (a,c,b)) else (\(a, b, c). (a,b,c)))\ fun msort2 :: "_ \ 'a list \ 'a list" where "msort2 f [] = []" | "msort2 f [x] = [x]" | "msort2 f [x,y] = (if f x y then [x,y] else [y,x])" | "msort2 f xs = merge f (msort f (take (size xs div 2) xs)) (msort f (drop (size xs div 2) xs))" lemmas [code del] = msort2.simps declare msort2.simps[simp del] lemmas [code] = msort2.simps[unfolded swap_ternary.simps, simplified] declare msort2.simps[simp] lemma msort_msort2: fixes xs :: \'a :: linorder list\ shows \msort (\) xs = msort2 (\) xs\ apply (induction \(\) :: 'a \ 'a \ bool\ xs rule: msort2.induct) apply (auto dest: transpD) done lemma sorted_msort: "transp f \ (\x y. f x y \ f y x) \ sorted_wrt f (msort f xs)" by (induct f xs rule: msort.induct) (simp_all add: sorted_merge) lemma mset_msort[simp]: "mset (msort f xs) = mset xs" by (induction f xs rule: msort.induct) (simp_all add: union_code) subsection \Sorting applied to monomials\ lemma merge_coeffs_alt_def: \(RETURN o merge_coeffs) p = REC\<^sub>T(\f p. (case p of [] \ RETURN [] | [_] => RETURN p | ((xs, n) # (ys, m) # p) \ (if xs = ys then if n + m \ 0 then f ((xs, n + m) # p) else f p else do {p \ f ((ys, m) # p); RETURN ((xs, n) # p)}))) p\ apply (induction p rule: merge_coeffs.induct) subgoal by (subst RECT_unfold, refine_mono) auto subgoal by (subst RECT_unfold, refine_mono) auto subgoal for x p y q by (subst RECT_unfold, refine_mono) (smt case_prod_conv list.simps(5) merge_coeffs.simps(3) nres_monad1 push_in_let_conv(2)) done lemma hn_invalid_recover: \is_pure R \ hn_invalid R = (\x y. R x y * true)\ \is_pure R \ invalid_assn R = (\x y. R x y * true)\ by (auto simp: is_pure_conv invalid_pure_recover hn_ctxt_def intro!: ext) lemma safe_poly_vars: shows [safe_constraint_rules]: "is_pure (poly_assn)" and [safe_constraint_rules]: "is_pure (monom_assn)" and [safe_constraint_rules]: "is_pure (monomial_assn)" and [safe_constraint_rules]: "is_pure string_assn" by (auto intro!: pure_prod list_assn_pure simp: prod_assn_pure_conv) lemma invalid_assn_distrib: \invalid_assn monom_assn \\<^sub>a invalid_assn int_assn = invalid_assn (monom_assn \\<^sub>a int_assn)\ apply (simp add: invalid_pure_recover hn_invalid_recover safe_constraint_rules) apply (subst hn_invalid_recover) apply (rule safe_poly_vars(2)) apply (subst hn_invalid_recover) apply (rule safe_poly_vars) apply (auto intro!: ext) done lemma WTF_RF_recover: \hn_ctxt (invalid_assn monom_assn \\<^sub>a invalid_assn int_assn) xb x'a \\<^sub>A hn_ctxt monomial_assn xb x'a \\<^sub>t hn_ctxt (monomial_assn) xb x'a\ by (smt assn_aci(5) hn_ctxt_def invalid_assn_distrib invalid_pure_recover is_pure_conv merge_thms(4) merge_true_star reorder_enttI safe_poly_vars(3) star_aci(2) star_aci(3)) lemma WTF_RF: \hn_ctxt (invalid_assn monom_assn \\<^sub>a invalid_assn int_assn) xb x'a * (hn_invalid poly_assn la l'a * hn_invalid int_assn a2' a2 * hn_invalid monom_assn a1' a1 * hn_invalid poly_assn l l' * hn_invalid monomial_assn xa x' * hn_invalid poly_assn ax px) \\<^sub>t hn_ctxt (monomial_assn) xb x'a * hn_ctxt poly_assn la l'a * hn_ctxt poly_assn l l' * (hn_invalid int_assn a2' a2 * hn_invalid monom_assn a1' a1 * hn_invalid monomial_assn xa x' * hn_invalid poly_assn ax px)\ \hn_ctxt (invalid_assn monom_assn \\<^sub>a invalid_assn int_assn) xa x' * (hn_ctxt poly_assn l l' * hn_invalid poly_assn ax px) \\<^sub>t hn_ctxt (monomial_assn) xa x' * hn_ctxt poly_assn l l' * hn_ctxt poly_assn ax px * emp\ by sepref_dbg_trans_step+ text \The refinement frameword is completely lost here when synthesizing the constants -- it does not understant what is pure (actually everything) and what must be destroyed.\ sepref_definition merge_coeffs_impl is \RETURN o merge_coeffs\ :: \poly_assn\<^sup>d \\<^sub>a poly_assn\ supply [[goals_limit=1]] unfolding merge_coeffs_alt_def HOL_list.fold_custom_empty poly_assn_alt_def apply (rewrite in \_\ annotate_assn[where A=\poly_assn\]) apply sepref_dbg_preproc apply sepref_dbg_cons_init apply sepref_dbg_id apply sepref_dbg_monadify apply sepref_dbg_opt_init apply (rule WTF_RF | sepref_dbg_trans_step)+ apply sepref_dbg_opt apply sepref_dbg_cons_solve apply sepref_dbg_cons_solve apply sepref_dbg_constraints done definition full_quicksort_poly where \full_quicksort_poly = full_quicksort_ref (\x y. x = y \ (x, y) \ term_order_rel) fst\ lemma down_eq_id_list_rel: \\(\Id\list_rel) x = x\ by auto definition quicksort_poly:: \nat \ nat \ llist_polynomial \ (llist_polynomial) nres\ where \quicksort_poly x y z = quicksort_ref (\) fst (x, y, z)\ term partition_between_ref definition partition_between_poly :: \nat \ nat \ llist_polynomial \ (llist_polynomial \ nat) nres\ where \partition_between_poly = partition_between_ref (\) fst\ definition partition_main_poly :: \nat \ nat \ llist_polynomial \ (llist_polynomial \ nat) nres\ where \partition_main_poly = partition_main (\) fst\ lemma string_list_trans: \(xa ::char list list, ya) \ lexord (lexord {(x, y). x < y}) \ (ya, z) \ lexord (lexord {(x, y). x < y}) \ (xa, z) \ lexord (lexord {(x, y). x < y})\ - by (smt less_char_def char.less_trans less_than_char_def lexord_partial_trans p2rel_def) + by (smt (verit) less_char_def char.less_trans less_than_char_def lexord_partial_trans p2rel_def) lemma full_quicksort_sort_poly_spec: \(full_quicksort_poly, sort_poly_spec) \ \Id\list_rel \\<^sub>f \\Id\list_rel\nres_rel\ proof - have xs: \(xs, xs) \ \Id\list_rel\ and \\(\Id\list_rel) x = x\ for x xs by auto show ?thesis apply (intro frefI nres_relI) unfolding full_quicksort_poly_def apply (rule full_quicksort_ref_full_quicksort[THEN fref_to_Down_curry, THEN order_trans]) subgoal by (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def dest: string_list_trans) subgoal using total_on_lexord_less_than_char_linear[unfolded var_order_rel_def] apply (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def less_char_def) done subgoal by fast apply (rule xs) apply (subst down_eq_id_list_rel) unfolding sorted_wrt_map sort_poly_spec_def apply (rule full_quicksort_correct_sorted[where R = \(\x y. x = y \ (x, y) \ term_order_rel)\ and h = \fst\, THEN order_trans]) subgoal by (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def dest: string_list_trans) subgoal for x y using total_on_lexord_less_than_char_linear[unfolded var_order_rel_def] apply (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def less_char_def) done subgoal by (auto simp: rel2p_def p2rel_def) done qed subsection \Lifting to polynomials\ definition merge_sort_poly :: \_\ where \merge_sort_poly = msort (\a b. fst a \ fst b)\ definition merge_monoms_poly :: \_\ where \merge_monoms_poly = msort (\)\ definition merge_poly :: \_\ where \merge_poly = merge (\a b. fst a \ fst b)\ definition merge_monoms :: \_\ where \merge_monoms = merge (\)\ definition msort_poly_impl :: \(String.literal list \ int) list \ _\ where \msort_poly_impl = msort (\a b. fst a \ fst b)\ definition msort_monoms_impl :: \(String.literal list) \ _\ where \msort_monoms_impl = msort (\)\ lemma msort_poly_impl_alt_def: \msort_poly_impl xs = (case xs of [] \ [] | [a] \ [a] | [a,b] \ if fst a \ fst b then [a,b]else [b,a] | xs \ merge_poly (msort_poly_impl (take ((length xs) div 2) xs)) (msort_poly_impl (drop ((length xs) div 2) xs)))\ unfolding msort_poly_impl_def apply (auto split: list.splits simp: merge_poly_def) done lemma le_term_order_rel': \(\) = (\x y. x = y \ term_order_rel' x y)\ apply (intro ext) apply (auto simp add: less_list_def less_eq_list_def lexordp_eq_conv_lexord lexordp_def) using term_order_rel'_alt_def_lexord term_order_rel'_def apply blast using term_order_rel'_alt_def_lexord term_order_rel'_def apply blast done fun lexord_eq where \lexord_eq [] _ = True\ | \lexord_eq (x # xs) (y # ys) = (x < y \ (x = y \ lexord_eq xs ys))\ | \lexord_eq _ _ = False\ lemma [simp]: \lexord_eq [] [] = True\ \lexord_eq (a # b)[] = False\ \lexord_eq [] (a # b) = True\ apply auto done lemma var_order_rel': \(\) = (\x y. x = y \ (x,y) \ var_order_rel)\ by (intro ext) (auto simp add: less_list_def less_eq_list_def lexordp_eq_conv_lexord lexordp_def var_order_rel_def lexordp_conv_lexord p2rel_def) lemma var_order_rel'': \(x,y) \ var_order_rel \ x < y\ by (metis leD less_than_char_linear lexord_linear neq_iff var_order_rel' var_order_rel_antisym var_order_rel_def) lemma lexord_eq_alt_def1: \a \ b = lexord_eq a b\ for a b :: \String.literal list\ unfolding le_term_order_rel' apply (induction a b rule: lexord_eq.induct) apply (auto simp: var_order_rel'' less_eq_list_def) done lemma lexord_eq_alt_def2: \(RETURN oo lexord_eq) xs ys = REC\<^sub>T (\f (xs, ys). case (xs, ys) of ([], _) \ RETURN True | (x # xs, y # ys) \ if x < y then RETURN True else if x = y then f (xs, ys) else RETURN False | _ \ RETURN False) (xs, ys)\ apply (subst eq_commute) apply (induction xs ys rule: lexord_eq.induct) subgoal by (subst RECT_unfold, refine_mono) auto subgoal by (subst RECT_unfold, refine_mono) auto subgoal by (subst RECT_unfold, refine_mono) auto done definition var_order' where [simp]: \var_order' = var_order\ lemma var_order_rel[def_pat_rules]: \(\)$(x,y)$var_order_rel \ var_order'$x$y\ by (auto simp: p2rel_def rel2p_def) lemma var_order_rel_alt_def: \var_order_rel = p2rel char.lexordp\ apply (auto simp: p2rel_def char.lexordp_conv_lexord var_order_rel_def) using char.lexordp_conv_lexord apply auto done lemma var_order_rel_var_order: \(x, y) \ var_order_rel \ var_order x y\ by (auto simp: rel2p_def) lemma var_order_string_le[sepref_import_param]: \((<), var_order') \ string_rel \ string_rel \ bool_rel\ apply (auto intro!: frefI simp: string_rel_def String.less_literal_def rel2p_def linorder.lexordp_conv_lexord[OF char.linorder_axioms, unfolded less_eq_char_def] var_order_rel_def p2rel_def simp flip: PAC_Polynomials_Term.less_char_def) using char.lexordp_conv_lexord apply auto done lemma [sepref_import_param]: \( (\), (\)) \ monom_rel \ monom_rel \bool_rel\ apply (intro fun_relI) using list_rel_list_rel_order_iff by fastforce lemma [sepref_import_param]: \( (<), (<)) \ string_rel \ string_rel \bool_rel\ proof - have [iff]: \ord.lexordp (<) (literal.explode a) (literal.explode aa) \ List.lexordp (<) (literal.explode a) (literal.explode aa)\ for a aa apply (rule iffI) apply (metis PAC_Checker_Relation.less_char_def char.lexordp_conv_lexord less_list_def p2rel_def var_order_rel'' var_order_rel_def) apply (metis PAC_Checker_Relation.less_char_def char.lexordp_conv_lexord less_list_def p2rel_def var_order_rel'' var_order_rel_def) done show ?thesis unfolding string_rel_def less_literal.rep_eq less_than_char_def less_eq_list_def PAC_Polynomials_Term.less_char_def[symmetric] by (intro fun_relI) (auto simp: string_rel_def less_literal.rep_eq less_list_def char.lexordp_conv_lexord lexordp_eq_refl lexordp_eq_conv_lexord) qed lemma lexordp_char_char: \ord_class.lexordp = char.lexordp\ unfolding char.lexordp_def ord_class.lexordp_def by (rule arg_cong[of _ _ lfp]) (auto intro!: ext) lemma [sepref_import_param]: \( (\), (\)) \ string_rel \ string_rel \bool_rel\ unfolding string_rel_def less_eq_literal.rep_eq less_than_char_def less_eq_list_def PAC_Polynomials_Term.less_char_def[symmetric] by (intro fun_relI) (auto simp: string_rel_def less_eq_literal.rep_eq less_than_char_def less_eq_list_def char.lexordp_eq_conv_lexord lexordp_eq_refl lexordp_eq_conv_lexord lexordp_char_char simp flip: less_char_def[abs_def]) sepref_register lexord_eq sepref_definition lexord_eq_term is \uncurry (RETURN oo lexord_eq)\ :: \monom_assn\<^sup>k *\<^sub>a monom_assn\<^sup>k \\<^sub>a bool_assn\ supply[[goals_limit=1]] unfolding lexord_eq_alt_def2 by sepref declare lexord_eq_term.refine[sepref_fr_rules] lemmas [code del] = msort_poly_impl_def msort_monoms_impl_def lemmas [code] = msort_poly_impl_def[unfolded lexord_eq_alt_def1[abs_def]] msort_monoms_impl_def[unfolded msort_msort2] lemma term_order_rel_trans: \(a, aa) \ term_order_rel \ (aa, ab) \ term_order_rel \ (a, ab) \ term_order_rel\ by (metis PAC_Checker_Relation.less_char_def p2rel_def string_list_trans var_order_rel_def) lemma merge_sort_poly_sort_poly_spec: \(RETURN o merge_sort_poly, sort_poly_spec) \ \Id\list_rel \\<^sub>f \\Id\list_rel\nres_rel\ unfolding sort_poly_spec_def merge_sort_poly_def apply (intro frefI nres_relI) using total_on_lexord_less_than_char_linear var_order_rel_def by (auto intro!: sorted_msort simp: sorted_wrt_map rel2p_def le_term_order_rel' transp_def dest: term_order_rel_trans) lemma msort_alt_def: \RETURN o (msort f) = REC\<^sub>T (\g xs. case xs of [] \ RETURN [] | [x] \ RETURN [x] | _ \ do { a \ g (take (size xs div 2) xs); b \ g (drop (size xs div 2) xs); RETURN (merge f a b)})\ apply (intro ext) unfolding comp_def apply (induct_tac f x rule: msort.induct) subgoal by (subst RECT_unfold, refine_mono) auto subgoal by (subst RECT_unfold, refine_mono) auto subgoal by (subst RECT_unfold, refine_mono) - (smt let_to_bind_conv list.simps(5) msort.simps(3)) + (smt (verit) let_to_bind_conv list.simps(5) msort.simps(3)) done lemma monomial_rel_order_map: \(x, a, b) \ monomial_rel \ (y, aa, bb) \ monomial_rel \ fst x \ fst y \ a \ aa\ apply (cases x; cases y) apply auto using list_rel_list_rel_order_iff by fastforce+ lemma step_rewrite_pure: fixes K :: \('olbl \ 'lbl) set\ shows \pure (p2rel (\K, V, R\pac_step_rel_raw)) = pac_step_rel_assn (pure K) (pure V) (pure R)\ \monomial_assn = pure (monom_rel \\<^sub>r int_rel)\ and poly_assn_list: \poly_assn = pure (\monom_rel \\<^sub>r int_rel\list_rel)\ subgoal apply (intro ext) apply (case_tac x; case_tac xa) apply (auto simp: relAPP_def p2rel_def pure_def) done subgoal H apply (intro ext) apply (case_tac x; case_tac xa) by (simp add: list_assn_pure_conv) subgoal unfolding H by (simp add: list_assn_pure_conv relAPP_def) done lemma safe_pac_step_rel_assn[safe_constraint_rules]: "is_pure K \ is_pure V \ is_pure R \ is_pure (pac_step_rel_assn K V R)" by (auto simp: step_rewrite_pure(1)[symmetric] is_pure_conv) lemma merge_poly_merge_poly: \(merge_poly, merge_poly) \ poly_rel \ poly_rel \ poly_rel\ unfolding merge_poly_def apply (intro fun_relI) subgoal for a a' aa a'a apply (induction \(\(a :: String.literal list \ int) (b :: String.literal list \ int). fst a \ fst b)\ a aa arbitrary: a' a'a rule: merge.induct) subgoal by (auto elim!: list_relE3 list_relE4 list_relE list_relE2 simp: monomial_rel_order_map) subgoal by (auto elim!: list_relE3 list_relE) subgoal by (auto elim!: list_relE3 list_relE4 list_relE list_relE2) done done lemmas [fcomp_norm_unfold] = poly_assn_list[symmetric] step_rewrite_pure(1) lemma merge_poly_merge_poly2: \(a, b) \ poly_rel \ (a', b') \ poly_rel \ (merge_poly a a', merge_poly b b') \ poly_rel\ using merge_poly_merge_poly unfolding fun_rel_def by auto lemma list_rel_takeD: \(a, b) \ \R\list_rel \ (n, n')\ Id \ (take n a, take n' b) \ \R\list_rel\ by (simp add: list_rel_eq_listrel listrel_iff_nth relAPP_def) lemma list_rel_dropD: \(a, b) \ \R\list_rel \ (n, n')\ Id \ (drop n a, drop n' b) \ \R\list_rel\ by (simp add: list_rel_eq_listrel listrel_iff_nth relAPP_def) lemma merge_sort_poly[sepref_import_param]: \(msort_poly_impl, merge_sort_poly) \ poly_rel \ poly_rel\ unfolding merge_sort_poly_def msort_poly_impl_def apply (intro fun_relI) subgoal for a a' apply (induction \(\(a :: String.literal list \ int) (b :: String.literal list \ int). fst a \ fst b)\ a arbitrary: a' rule: msort.induct) subgoal by auto subgoal by (auto elim!: list_relE3 list_relE) subgoal premises p using p by (auto elim!: list_relE3 list_relE4 list_relE list_relE2 simp: merge_poly_def[symmetric] intro!: list_rel_takeD list_rel_dropD intro!: merge_poly_merge_poly2 p(1)[simplified] p(2)[simplified], auto simp: list_rel_imp_same_length) done done lemmas [sepref_fr_rules] = merge_sort_poly[FCOMP merge_sort_poly_sort_poly_spec] sepref_definition partition_main_poly_impl is \uncurry2 partition_main_poly\ :: \nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a poly_assn\<^sup>k \\<^sub>a prod_assn poly_assn nat_assn \ unfolding partition_main_poly_def partition_main_def term_order_rel'_def[symmetric] term_order_rel'_alt_def le_term_order_rel' by sepref declare partition_main_poly_impl.refine[sepref_fr_rules] sepref_definition partition_between_poly_impl is \uncurry2 partition_between_poly\ :: \nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a poly_assn\<^sup>k \\<^sub>a prod_assn poly_assn nat_assn \ unfolding partition_between_poly_def partition_between_ref_def partition_main_poly_def[symmetric] unfolding choose_pivot3_def term_order_rel'_def[symmetric] term_order_rel'_alt_def choose_pivot_def lexord_eq_alt_def1 by sepref declare partition_between_poly_impl.refine[sepref_fr_rules] sepref_definition quicksort_poly_impl is \uncurry2 quicksort_poly\ :: \nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a poly_assn\<^sup>k \\<^sub>a poly_assn\ unfolding partition_main_poly_def quicksort_ref_def quicksort_poly_def partition_between_poly_def[symmetric] by sepref lemmas [sepref_fr_rules] = quicksort_poly_impl.refine sepref_register quicksort_poly sepref_definition full_quicksort_poly_impl is \full_quicksort_poly\ :: \poly_assn\<^sup>k \\<^sub>a poly_assn\ unfolding full_quicksort_poly_def full_quicksort_ref_def quicksort_poly_def[symmetric] le_term_order_rel'[symmetric] term_order_rel'_def[symmetric] List.null_def by sepref lemmas sort_poly_spec_hnr = full_quicksort_poly_impl.refine[FCOMP full_quicksort_sort_poly_spec] declare merge_coeffs_impl.refine[sepref_fr_rules] sepref_definition normalize_poly_impl is \normalize_poly\ :: \poly_assn\<^sup>k \\<^sub>a poly_assn\ supply [[goals_limit=1]] unfolding normalize_poly_def by sepref declare normalize_poly_impl.refine[sepref_fr_rules] definition full_quicksort_vars where \full_quicksort_vars = full_quicksort_ref (\x y. x = y \ (x, y) \ var_order_rel) id\ definition quicksort_vars:: \nat \ nat \ string list \ (string list) nres\ where \quicksort_vars x y z = quicksort_ref (\) id (x, y, z)\ definition partition_between_vars :: \nat \ nat \ string list \ (string list \ nat) nres\ where \partition_between_vars = partition_between_ref (\) id\ definition partition_main_vars :: \nat \ nat \ string list \ (string list \ nat) nres\ where \partition_main_vars = partition_main (\) id\ lemma total_on_lexord_less_than_char_linear2: \xs \ ys \ (xs, ys) \ lexord (less_than_char) \ (ys, xs) \ lexord less_than_char\ using lexord_linear[of \less_than_char\ xs ys] using lexord_linear[of \less_than_char\] less_than_char_linear apply (auto simp: Relation.total_on_def) using lexord_irrefl[OF irrefl_less_than_char] antisym_lexord[OF antisym_less_than_char irrefl_less_than_char] apply (auto simp: antisym_def) done lemma string_trans: \(xa, ya) \ lexord {(x::char, y::char). x < y} \ (ya, z) \ lexord {(x::char, y::char). x < y} \ (xa, z) \ lexord {(x::char, y::char). x < y}\ - by (smt less_char_def char.less_trans less_than_char_def lexord_partial_trans p2rel_def) + by (smt (verit) less_char_def char.less_trans less_than_char_def lexord_partial_trans p2rel_def) lemma full_quicksort_sort_vars_spec: \(full_quicksort_vars, sort_coeff) \ \Id\list_rel \\<^sub>f \\Id\list_rel\nres_rel\ proof - have xs: \(xs, xs) \ \Id\list_rel\ and \\(\Id\list_rel) x = x\ for x xs by auto show ?thesis apply (intro frefI nres_relI) unfolding full_quicksort_vars_def apply (rule full_quicksort_ref_full_quicksort[THEN fref_to_Down_curry, THEN order_trans]) subgoal by (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def dest: string_trans) subgoal using total_on_lexord_less_than_char_linear2[unfolded var_order_rel_def] apply (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def less_char_def) done subgoal by fast apply (rule xs) apply (subst down_eq_id_list_rel) unfolding sorted_wrt_map sort_coeff_def apply (rule full_quicksort_correct_sorted[where R = \(\x y. x = y \ (x, y) \ var_order_rel)\ and h = \id\, THEN order_trans]) subgoal by (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def dest: string_trans) subgoal for x y using total_on_lexord_less_than_char_linear2[unfolded var_order_rel_def] by (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def less_char_def) subgoal by (auto simp: rel2p_def p2rel_def rel2p_def[abs_def]) done qed sepref_definition partition_main_vars_impl is \uncurry2 partition_main_vars\ :: \nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a (monom_assn)\<^sup>k \\<^sub>a prod_assn (monom_assn) nat_assn\ unfolding partition_main_vars_def partition_main_def var_order_rel_var_order var_order'_def[symmetric] term_order_rel'_alt_def le_term_order_rel' id_apply by sepref declare partition_main_vars_impl.refine[sepref_fr_rules] sepref_definition partition_between_vars_impl is \uncurry2 partition_between_vars\ :: \nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a monom_assn\<^sup>k \\<^sub>a prod_assn monom_assn nat_assn \ unfolding partition_between_vars_def partition_between_ref_def partition_main_vars_def[symmetric] unfolding choose_pivot3_def term_order_rel'_def[symmetric] term_order_rel'_alt_def choose_pivot_def le_term_order_rel' id_apply by sepref declare partition_between_vars_impl.refine[sepref_fr_rules] sepref_definition quicksort_vars_impl is \uncurry2 quicksort_vars\ :: \nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a monom_assn\<^sup>k \\<^sub>a monom_assn\ unfolding partition_main_vars_def quicksort_ref_def quicksort_vars_def partition_between_vars_def[symmetric] by sepref lemmas [sepref_fr_rules] = quicksort_vars_impl.refine sepref_register quicksort_vars lemma le_var_order_rel: \(\) = (\x y. x = y \ (x, y) \ var_order_rel)\ by (intro ext) (auto simp add: less_list_def less_eq_list_def rel2p_def p2rel_def lexordp_conv_lexord p2rel_def var_order_rel_def lexordp_eq_conv_lexord lexordp_def) sepref_definition full_quicksort_vars_impl is \full_quicksort_vars\ :: \monom_assn\<^sup>k \\<^sub>a monom_assn\ unfolding full_quicksort_vars_def full_quicksort_ref_def quicksort_vars_def[symmetric] le_var_order_rel[symmetric] term_order_rel'_def[symmetric] List.null_def by sepref lemmas sort_vars_spec_hnr = full_quicksort_vars_impl.refine[FCOMP full_quicksort_sort_vars_spec] lemma string_rel_order_map: \(x, a) \ string_rel \ (y, aa) \ string_rel \ x \ y \ a \ aa\ unfolding string_rel_def less_eq_literal.rep_eq less_than_char_def less_eq_list_def PAC_Polynomials_Term.less_char_def[symmetric] by (auto simp: string_rel_def less_eq_literal.rep_eq less_than_char_def less_eq_list_def char.lexordp_eq_conv_lexord lexordp_eq_refl lexordp_char_char lexordp_eq_conv_lexord simp flip: less_char_def[abs_def]) lemma merge_monoms_merge_monoms: \(merge_monoms, merge_monoms) \ monom_rel \ monom_rel \ monom_rel\ unfolding merge_monoms_def apply (intro fun_relI) subgoal for a a' aa a'a apply (induction \(\(a :: String.literal) (b :: String.literal). a \ b)\ a aa arbitrary: a' a'a rule: merge.induct) subgoal by (auto elim!: list_relE3 list_relE4 list_relE list_relE2 simp: string_rel_order_map) subgoal by (auto elim!: list_relE3 list_relE) subgoal by (auto elim!: list_relE3 list_relE4 list_relE list_relE2) done done lemma merge_monoms_merge_monoms2: \(a, b) \ monom_rel \ (a', b') \ monom_rel \ (merge_monoms a a', merge_monoms b b') \ monom_rel\ using merge_monoms_merge_monoms unfolding fun_rel_def merge_monoms_def by auto lemma msort_monoms_impl: \(msort_monoms_impl, merge_monoms_poly) \ monom_rel \ monom_rel\ unfolding msort_monoms_impl_def merge_monoms_poly_def apply (intro fun_relI) subgoal for a a' apply (induction \(\(a :: String.literal) (b :: String.literal). a \ b)\ a arbitrary: a' rule: msort.induct) subgoal by auto subgoal by (auto elim!: list_relE3 list_relE) subgoal premises p using p by (auto elim!: list_relE3 list_relE4 list_relE list_relE2 simp: merge_monoms_def[symmetric] intro!: list_rel_takeD list_rel_dropD intro!: merge_monoms_merge_monoms2 p(1)[simplified] p(2)[simplified]) (simp_all add: list_rel_imp_same_length) done done lemma merge_sort_monoms_sort_monoms_spec: \(RETURN o merge_monoms_poly, sort_coeff) \ \Id\list_rel \\<^sub>f \\Id\list_rel\nres_rel\ unfolding merge_monoms_poly_def sort_coeff_def by (intro frefI nres_relI) (auto intro!: sorted_msort simp: sorted_wrt_map rel2p_def le_term_order_rel' transp_def rel2p_def[abs_def] simp flip: le_var_order_rel) sepref_register sort_coeff lemma [sepref_fr_rules]: \(return o msort_monoms_impl, sort_coeff) \ monom_assn\<^sup>k \\<^sub>a monom_assn\ using msort_monoms_impl[sepref_param, FCOMP merge_sort_monoms_sort_monoms_spec] by auto sepref_definition sort_all_coeffs_impl is \sort_all_coeffs\ :: \poly_assn\<^sup>k \\<^sub>a poly_assn\ unfolding sort_all_coeffs_def HOL_list.fold_custom_empty by sepref declare sort_all_coeffs_impl.refine[sepref_fr_rules] lemma merge_coeffs0_alt_def: \(RETURN o merge_coeffs0) p = REC\<^sub>T(\f p. (case p of [] \ RETURN [] | [p] => if snd p = 0 then RETURN [] else RETURN [p] | ((xs, n) # (ys, m) # p) \ (if xs = ys then if n + m \ 0 then f ((xs, n + m) # p) else f p else if n = 0 then do {p \ f ((ys, m) # p); RETURN p} else do {p \ f ((ys, m) # p); RETURN ((xs, n) # p)}))) p\ apply (subst eq_commute) apply (induction p rule: merge_coeffs0.induct) subgoal by (subst RECT_unfold, refine_mono) auto subgoal by (subst RECT_unfold, refine_mono) auto subgoal by (subst RECT_unfold, refine_mono) (auto simp: let_to_bind_conv) done text \Again, Sepref does not understand what is going here.\ sepref_definition merge_coeffs0_impl is \RETURN o merge_coeffs0\ :: \poly_assn\<^sup>k \\<^sub>a poly_assn\ supply [[goals_limit=1]] unfolding merge_coeffs0_alt_def HOL_list.fold_custom_empty apply sepref_dbg_preproc apply sepref_dbg_cons_init apply sepref_dbg_id apply sepref_dbg_monadify apply sepref_dbg_opt_init apply (rule WTF_RF | sepref_dbg_trans_step)+ apply sepref_dbg_opt apply sepref_dbg_cons_solve apply sepref_dbg_cons_solve apply sepref_dbg_constraints done declare merge_coeffs0_impl.refine[sepref_fr_rules] sepref_definition fully_normalize_poly_impl is \full_normalize_poly\ :: \poly_assn\<^sup>k \\<^sub>a poly_assn\ supply [[goals_limit=1]] unfolding full_normalize_poly_def by sepref declare fully_normalize_poly_impl.refine[sepref_fr_rules] end \ No newline at end of file diff --git a/thys/PAC_Checker/PAC_Checker_Relation.thy b/thys/PAC_Checker/PAC_Checker_Relation.thy --- a/thys/PAC_Checker/PAC_Checker_Relation.thy +++ b/thys/PAC_Checker/PAC_Checker_Relation.thy @@ -1,389 +1,389 @@ (* File: PAC_Checker_Relation.thy Author: Mathias Fleury, Daniela Kaufmann, JKU Maintainer: Mathias Fleury, JKU *) theory PAC_Checker_Relation imports PAC_Checker WB_Sort "Native_Word.Uint64" begin section \Various Refinement Relations\ text \When writing this, it was not possible to share the definition with the IsaSAT version.\ definition uint64_nat_rel :: "(uint64 \ nat) set" where \uint64_nat_rel = br nat_of_uint64 (\_. True)\ abbreviation uint64_nat_assn where \uint64_nat_assn \ pure uint64_nat_rel\ instantiation uint32 :: hashable begin definition hashcode_uint32 :: \uint32 \ uint32\ where \hashcode_uint32 n = n\ definition def_hashmap_size_uint32 :: \uint32 itself \ nat\ where \def_hashmap_size_uint32 = (\_. 16)\ \ \same as @{typ nat}\ instance by standard (simp add: def_hashmap_size_uint32_def) end instantiation uint64 :: hashable begin context includes bit_operations_syntax begin definition hashcode_uint64 :: \uint64 \ uint32\ where \hashcode_uint64 n = (uint32_of_nat (nat_of_uint64 ((n) AND ((2 :: uint64)^32 -1))))\ end definition def_hashmap_size_uint64 :: \uint64 itself \ nat\ where \def_hashmap_size_uint64 = (\_. 16)\ \ \same as @{typ nat}\ instance by standard (simp add: def_hashmap_size_uint64_def) end lemma word_nat_of_uint64_Rep_inject[simp]: \nat_of_uint64 ai = nat_of_uint64 bi \ ai = bi\ by transfer (simp add: word_unat_eq_iff) instance uint64 :: heap by standard (auto simp: inj_def exI[of _ nat_of_uint64]) instance uint64 :: semiring_numeral by standard lemma nat_of_uint64_012[simp]: \nat_of_uint64 0 = 0\ \nat_of_uint64 2 = 2\ \nat_of_uint64 1 = 1\ by (simp_all add: nat_of_uint64.rep_eq zero_uint64.rep_eq one_uint64.rep_eq) definition uint64_of_nat_conv where [simp]: \uint64_of_nat_conv (x :: nat) = x\ lemma less_upper_bintrunc_id: \n < 2 ^b \ n \ 0 \ take_bit b n = n\ for n :: int by (rule take_bit_int_eq_self) lemma nat_of_uint64_uint64_of_nat_id: \n < 2^64 \ nat_of_uint64 (uint64_of_nat n) = n\ by transfer (simp add: take_bit_nat_eq_self unsigned_of_nat) lemma [sepref_fr_rules]: \(return o uint64_of_nat, RETURN o uint64_of_nat_conv) \ [\a. a < 2 ^64]\<^sub>a nat_assn\<^sup>k \ uint64_nat_assn\ by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def nat_of_uint64_uint64_of_nat_id) definition string_rel :: \(String.literal \ string) set\ where \string_rel = {(x, y). y = String.explode x}\ abbreviation string_assn :: \string \ String.literal \ assn\ where \string_assn \ pure string_rel\ lemma eq_string_eq: \((=), (=)) \ string_rel \ string_rel \ bool_rel\ by (auto intro!: frefI simp: string_rel_def String.less_literal_def less_than_char_def rel2p_def literal.explode_inject) lemmas eq_string_eq_hnr = eq_string_eq[sepref_import_param] definition string2_rel :: \(string \ string) set\ where \string2_rel \ \Id\list_rel\ abbreviation string2_assn :: \string \ string \ assn\ where \string2_assn \ pure string2_rel\ abbreviation monom_rel where \monom_rel \ \string_rel\list_rel\ abbreviation monom_assn where \monom_assn \ list_assn string_assn\ abbreviation monomial_rel where \monomial_rel \ monom_rel \\<^sub>r int_rel\ abbreviation monomial_assn where \monomial_assn \ monom_assn \\<^sub>a int_assn\ abbreviation poly_rel where \poly_rel \ \monomial_rel\list_rel\ abbreviation poly_assn where \poly_assn \ list_assn monomial_assn\ lemma poly_assn_alt_def: \poly_assn = pure poly_rel\ by (simp add: list_assn_pure_conv) abbreviation polys_assn where \polys_assn \ hm_fmap_assn uint64_nat_assn poly_assn\ lemma string_rel_string_assn: \(\ ((c, a) \ string_rel)) = string_assn a c\ by (auto simp: pure_app_eq) lemma single_valued_string_rel: \single_valued string_rel\ by (auto simp: single_valued_def string_rel_def) lemma IS_LEFT_UNIQUE_string_rel: \IS_LEFT_UNIQUE string_rel\ by (auto simp: IS_LEFT_UNIQUE_def single_valued_def string_rel_def literal.explode_inject) lemma IS_RIGHT_UNIQUE_string_rel: \IS_RIGHT_UNIQUE string_rel\ by (auto simp: single_valued_def string_rel_def literal.explode_inject) lemma single_valued_monom_rel: \single_valued monom_rel\ by (rule list_rel_sv) (auto intro!: frefI simp: string_rel_def rel2p_def single_valued_def p2rel_def) lemma single_valued_monomial_rel: \single_valued monomial_rel\ using single_valued_monom_rel by (auto intro!: frefI simp: rel2p_def single_valued_def p2rel_def) lemma single_valued_monom_rel': \IS_LEFT_UNIQUE monom_rel\ unfolding IS_LEFT_UNIQUE_def inv_list_rel_eq string2_rel_def by (rule list_rel_sv)+ (auto intro!: frefI simp: string_rel_def rel2p_def single_valued_def p2rel_def literal.explode_inject) lemma single_valued_monomial_rel': \IS_LEFT_UNIQUE monomial_rel\ using single_valued_monom_rel' unfolding IS_LEFT_UNIQUE_def inv_list_rel_eq by (auto intro!: frefI simp: rel2p_def single_valued_def p2rel_def) lemma [safe_constraint_rules]: \Sepref_Constraints.CONSTRAINT single_valued string_rel\ \Sepref_Constraints.CONSTRAINT IS_LEFT_UNIQUE string_rel\ by (auto simp: CONSTRAINT_def single_valued_def string_rel_def IS_LEFT_UNIQUE_def literal.explode_inject) lemma eq_string_monom_hnr[sepref_fr_rules]: \(uncurry (return oo (=)), uncurry (RETURN oo (=))) \ monom_assn\<^sup>k *\<^sub>a monom_assn\<^sup>k \\<^sub>a bool_assn\ using single_valued_monom_rel' single_valued_monom_rel unfolding list_assn_pure_conv by sepref_to_hoare (sep_auto simp: list_assn_pure_conv string_rel_string_assn single_valued_def IS_LEFT_UNIQUE_def dest!: mod_starD simp flip: inv_list_rel_eq) definition term_order_rel' where [simp]: \term_order_rel' x y = ((x, y) \ term_order_rel)\ lemma term_order_rel[def_pat_rules]: \(\)$(x,y)$term_order_rel \ term_order_rel'$x$y\ by auto lemma term_order_rel_alt_def: \term_order_rel = lexord (p2rel char.lexordp)\ by (auto simp: p2rel_def char.lexordp_conv_lexord var_order_rel_def intro!: arg_cong[of _ _ lexord]) instantiation char :: linorder begin definition less_char where [symmetric, simp]: "less_char = PAC_Polynomials_Term.less_char" definition less_eq_char where [symmetric, simp]: "less_eq_char = PAC_Polynomials_Term.less_eq_char" instance apply standard using char.linorder_axioms by (auto simp: class.linorder_def class.order_def class.preorder_def less_eq_char_def less_than_char_def class.order_axioms_def class.linorder_axioms_def p2rel_def less_char_def) end instantiation list :: (linorder) linorder begin definition less_list where "less_list = lexordp (<)" definition less_eq_list where "less_eq_list = lexordp_eq" instance proof standard have [dest]: \\x y :: 'a :: linorder list. (x, y) \ lexord {(x, y). x < y} \ lexordp_eq y x \ False\ by (metis lexordp_antisym lexordp_conv_lexord lexordp_eq_conv_lexord) have [simp]: \\x y :: 'a :: linorder list. lexordp_eq x y \ \ lexordp_eq y x \ (x, y) \ lexord {(x, y). x < y}\ using lexordp_conv_lexord lexordp_conv_lexordp_eq by blast show \(x < y) = Restricted_Predicates.strict (\) x y\ \x \ x\ \x \ y \ y \ z \ x \ z\ \x \ y \ y \ x \ x = y\ \x \ y \ y \ x\ for x y z :: \'a :: linorder list\ by (auto simp: less_list_def less_eq_list_def List.lexordp_def lexordp_conv_lexord lexordp_into_lexordp_eq lexordp_antisym antisym_def lexordp_eq_refl lexordp_eq_linear intro: lexordp_eq_trans dest: lexordp_eq_antisym) qed end lemma term_order_rel'_alt_def_lexord: \term_order_rel' x y = ord_class.lexordp x y\ and term_order_rel'_alt_def: \term_order_rel' x y \ x < y\ proof - show \term_order_rel' x y = ord_class.lexordp x y\ \term_order_rel' x y \ x < y\ unfolding less_than_char_of_char[symmetric, abs_def] by (auto simp: lexordp_conv_lexord less_eq_list_def less_list_def lexordp_def var_order_rel_def rel2p_def term_order_rel_alt_def p2rel_def) qed lemma list_rel_list_rel_order_iff: assumes \(a, b) \ \string_rel\list_rel\ \(a', b') \ \string_rel\list_rel\ shows \a < a' \ b < b'\ proof have H: \(a, b) \ \string_rel\list_rel \ (a, cs) \ \string_rel\list_rel \ b = cs\ for cs using single_valued_monom_rel' IS_RIGHT_UNIQUE_string_rel unfolding string2_rel_def by (subst (asm)list_rel_sv_iff[symmetric]) (auto simp: single_valued_def) assume \a < a'\ then consider u u' where \a' = a @ u # u'\ | u aa v w aaa where \a = u @ aa # v\ \a' = u @ aaa # w\ \aa < aaa\ by (subst (asm) less_list_def) (auto simp: lexord_def List.lexordp_def list_rel_append1 list_rel_split_right_iff) then show \b < b'\ proof cases case 1 then show \b < b'\ using assms by (subst less_list_def) (auto simp: lexord_def List.lexordp_def list_rel_append1 list_rel_split_right_iff dest: H) next case 2 then obtain u' aa' v' w' aaa' where \b = u' @ aa' # v'\ \b' = u' @ aaa' # w'\ \(aa, aa') \ string_rel\ \(aaa, aaa') \ string_rel\ using assms - by (smt list_rel_append1 list_rel_split_right_iff single_valued_def single_valued_monom_rel) + by (smt (verit) list_rel_append1 list_rel_split_right_iff single_valued_def single_valued_monom_rel) with \aa < aaa\ have \aa' < aaa'\ by (auto simp: string_rel_def less_literal.rep_eq less_list_def lexordp_conv_lexord lexordp_def char.lexordp_conv_lexord simp flip: less_char_def PAC_Polynomials_Term.less_char_def) then show \b < b'\ using \b = u' @ aa' # v'\ \b' = u' @ aaa' # w'\ by (subst less_list_def) (fastforce simp: lexord_def List.lexordp_def list_rel_append1 list_rel_split_right_iff) qed next have H: \(a, b) \ \string_rel\list_rel \ (a', b) \ \string_rel\list_rel \ a = a'\ for a a' b using single_valued_monom_rel' by (auto simp: single_valued_def IS_LEFT_UNIQUE_def simp flip: inv_list_rel_eq) assume \b < b'\ then consider u u' where \b' = b @ u # u'\ | u aa v w aaa where \b = u @ aa # v\ \b' = u @ aaa # w\ \aa < aaa\ by (subst (asm) less_list_def) (auto simp: lexord_def List.lexordp_def list_rel_append1 list_rel_split_right_iff) then show \a < a'\ proof cases case 1 then show \a < a'\ using assms by (subst less_list_def) (auto simp: lexord_def List.lexordp_def list_rel_append2 list_rel_split_left_iff dest: H) next case 2 then obtain u' aa' v' w' aaa' where \a = u' @ aa' # v'\ \a' = u' @ aaa' # w'\ \(aa', aa) \ string_rel\ \(aaa', aaa) \ string_rel\ using assms by (auto simp: lexord_def List.lexordp_def list_rel_append2 list_rel_split_left_iff dest: H) with \aa < aaa\ have \aa' < aaa'\ by (auto simp: string_rel_def less_literal.rep_eq less_list_def lexordp_conv_lexord lexordp_def char.lexordp_conv_lexord simp flip: less_char_def PAC_Polynomials_Term.less_char_def) then show \a < a'\ using \a = u' @ aa' # v'\ \a' = u' @ aaa' # w'\ by (subst less_list_def) (fastforce simp: lexord_def List.lexordp_def list_rel_append1 list_rel_split_right_iff) qed qed lemma string_rel_le[sepref_import_param]: shows \((<), (<)) \ \string_rel\list_rel \ \string_rel\list_rel \ bool_rel\ by (auto intro!: fun_relI simp: list_rel_list_rel_order_iff) (* TODO Move *) lemma [sepref_import_param]: assumes \CONSTRAINT IS_LEFT_UNIQUE R\ \CONSTRAINT IS_RIGHT_UNIQUE R\ shows \(remove1, remove1) \ R \ \R\list_rel \ \R\list_rel\ apply (intro fun_relI) subgoal premises p for x y xs ys using p(2) p(1) assms by (induction xs ys rule: list_rel_induct) (auto simp: IS_LEFT_UNIQUE_def single_valued_def) done instantiation pac_step :: (heap, heap, heap) heap begin instance proof standard obtain f :: \'a \ nat\ where f: \inj f\ by blast obtain g :: \nat \ nat \ nat \ nat \ nat \ nat\ where g: \inj g\ by blast obtain h :: \'b \ nat\ where h: \inj h\ by blast obtain i :: \'c \ nat\ where i: \inj i\ by blast have [iff]: \g a = g b \ a = b\\h a'' = h b'' \ a'' = b''\ \f a' = f b' \ a' = b'\ \i a''' = i b''' \ a''' = b'''\ for a b a' b' a'' b'' a''' b''' using f g h i unfolding inj_def by blast+ let ?f = \\x :: ('a, 'b, 'c) pac_step. g (case x of Add a b c d \ (0, i a, i b, i c, f d) | Del a \ (1, i a, 0, 0, 0) | Mult a b c d \ (2, i a, f b, i c, f d) | Extension a b c \ (3, i a, f c, 0, h b))\ have \inj ?f\ apply (auto simp: inj_def) apply (case_tac x; case_tac y) apply auto done then show \\f :: ('a, 'b, 'c) pac_step \ nat. inj f\ by blast qed end end \ No newline at end of file diff --git a/thys/PAC_Checker/PAC_Checker_Specification.thy b/thys/PAC_Checker/PAC_Checker_Specification.thy --- a/thys/PAC_Checker/PAC_Checker_Specification.thy +++ b/thys/PAC_Checker/PAC_Checker_Specification.thy @@ -1,853 +1,853 @@ (* 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\<^sub>I (\(vars ` set_mset A) \ vars spec) B \ restricted_ideal_to\<^sub>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\<^sup>*\<^sup>* (\, A) B) \ (is_found b \ PAC_Format\<^sup>*\<^sup>* (\, 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 = (\(\\<^sub>0, A\<^sub>0) spec (\, A) (b, B). (is_success b \ \(vars ` set_mset A\<^sub>0) \ \\<^sub>0 \ \(vars ` set_mset A) \ \ \ PAC_Format\<^sup>*\<^sup>* (\\<^sub>0, A\<^sub>0) (\, A) \ PAC_Format\<^sup>*\<^sup>* (\, A) B) \ (is_found b \ \(vars ` set_mset A\<^sub>0) \ \\<^sub>0 \ \(vars ` set_mset A) \ \ \ PAC_Format\<^sup>*\<^sup>* (\\<^sub>0, A\<^sub>0) (\, A) \ PAC_Format\<^sup>*\<^sup>* (\, A) B \ spec \ pac_ideal (set_mset A\<^sub>0)))\ abbreviation PAC_checker_specification_step2 :: \pac_state \ int_poly \ pac_state \ (status \ pac_state) nres\ where \PAC_checker_specification_step2 A\<^sub>0 spec A \ SPEC(PAC_checker_specification_step_spec A\<^sub>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)\<^sup>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\<^sup>*\<^sup>* (\, 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\<^sup>*\<^sup>* (\, 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\<^sup>*\<^sup>* (\, 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\<^sup>*\<^sup>* (\, 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\<^sup>*\<^sup>* (\, B) (\, remove1_mset (the (fmlookup A x11)) (add_mset r B))\ \(A, B) \ polys_rel \ x12 \# dom_m A \ PAC_Format\<^sup>*\<^sup>* (\, B) (\, remove1_mset (the (fmlookup A x12)) B)\ \(A, B) \ polys_rel \ (p' + Var x)\<^sup>2 - (p' + Var x) \ ideal polynomial_bool \ x \ \ \ x \ vars(p' + Var x) \ vars(p' + Var x) \ \ \ PAC_Format\<^sup>*\<^sup>* (\, 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),(\\<^sub>B, B)) \ polys_rel_full\ and \\is_failed a\ and [simp,intro]: \a = FOUND \ spec \ pac_ideal (set_mset A\<^sub>0)\ and A\<^sub>0B: \PAC_Format\<^sup>*\<^sup>* (\\<^sub>0, A\<^sub>0) (\, B)\ and spec\<^sub>0: \vars spec \ \\<^sub>0\ and vars_A\<^sub>0: \\ (vars ` set_mset A\<^sub>0) \ \\<^sub>0\ shows \PAC_checker_step spec (a, (\, A)) st \ \ (status_rel \\<^sub>r polys_rel_full) (PAC_checker_specification_step2 (\\<^sub>0, A\<^sub>0) spec (\, B))\ proof - have \\\<^sub>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\<^sub>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\<^sub>0B vars_A\<^sub>0] spec\<^sub>0 \(A, B) \ polys_rel\[unfolded polys_rel_def, simplified] - by (smt in_mono mem_Collect_eq restricted_ideal_to_def)+ + 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\<^sub>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 \\<^sub>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 \\<^sub>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\<^sub>I \ I \ restricted_ideal_to\<^sub>I \' J \ \ \ \ \ restricted_ideal_to\<^sub>I \ I \ restricted_ideal_to\<^sub>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\<^sub>I x1b b \ restricted_ideal_to\<^sub>I x1b (ran_m x2a) \ xa \ restricted_ideal_to\<^sub>I (\ (vars ` set_mset (ran_m A)) \ vars spec) b \ xa \ restricted_ideal_to\<^sub>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\<^sub>I x1b b \ restricted_ideal_to\<^sub>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 \\<^sub>r polys_rel) \\<^sub>r Id \\<^sub>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 diff --git a/thys/PAC_Checker/PAC_More_Poly.thy b/thys/PAC_Checker/PAC_More_Poly.thy --- a/thys/PAC_Checker/PAC_More_Poly.thy +++ b/thys/PAC_Checker/PAC_More_Poly.thy @@ -1,926 +1,926 @@ (* File: PAC_More_Poly.thy Author: Mathias Fleury, Daniela Kaufmann, JKU Maintainer: Mathias Fleury, JKU *) theory PAC_More_Poly imports "HOL-Library.Poly_Mapping" "HOL-Algebra.Polynomials" "Polynomials.MPoly_Type_Class" "HOL-Algebra.Module" "HOL-Library.Countable_Set" begin section \Overview\ text \ One solution to check circuit of multipliers is to use algebraic method, like producing proofs on polynomials. We are here interested in checking PAC proofs on the Boolean ring. The idea is the following: each variable represents an input or the output of a gate and we want to prove the bitwise multiplication of the input bits yields the output, namely the bitwise representation of the multiplication of the input (modulo \<^term>\(2::nat)^n\ where \<^term>\n::nat\ is the number of bits of the circuit). Algebraic proof systems typically reason over polynomials in a ring $\set K[X]$, where the variables $X$ represent Boolean values. The aim of an algebraic proof is to derive whether a polynomial $f$ can be derived from a given set of polynomials $G = \{g_1,\dots,g_l\} \subseteq \set K[X]$ together with the Boolean value constraints $B(X) = \{x^2_i-x_i \mid x_i \in X\}$. In algebraic terms this means to show that the polynomial \<^latex>\\(f \in \langle G \cup B(X)\rangle\)\. In our setting we set $\set K = \set Z$ and we treat the Boolean value constraints implicitly, i.e., we consider proofs in the ring \<^latex>\\(\set Z[X]/\langle B(X)\rangle\)\ to admit shorter proofs The checker takes as input 3 files: \<^enum> an input file containing all polynomials that are initially present; \<^enum> a target (or specification) polynomial ; \<^enum> a ``proof'' file to check that contains the proof in PAC format that shows that the specification is in the ideal generated by the polynomials present initially. Each step of the proof is either an addition of two polynomials previously derived, a multiplication from a previously derived polynomial and an arbitrary polynomial, and the deletion a derived polynomial. One restriction on the proofs compared to generic PAC proofs is that \<^term>\(x::nat)^2 = x\ in the Boolean ring we are considering. The checker can produce two outputs: valid (meaning that each derived polynomial in the proof has been correctly derived and the specification polynomial was also derived at some point [either in the proof or as input]) or invalid (without proven information what went wrong). The development is organised as follows: \<^item> \<^file>\PAC_Specification.thy\ (this file) contains the specification as described above on ideals without any peculiarities on the PAC proof format \<^item> \<^file>\PAC_Checker_Specification.thy\ specialises to the PAC format and enters the nondeterminism monad to prepare the subsequent refinements. \<^item> \<^file>\PAC_Checker.thy\ contains the refined version where polynomials are represented as lists. \<^item> \<^file>\PAC_Checker_Synthesis.thy\ contains the efficient implementation with imperative data structure like a hash set. \<^item> \<^file>\PAC_Checker_MLton.thy\ contains the code generation and the command to compile the file with the ML compiler MLton. Here is an example of a proof and an input file (taken from the appendix of our FMCAD paper~\cite{KaufmannFleuryBiere-FMCAD20}, available at \<^url>\http://fmv.jku.at/pacheck_pasteque\): \<^verbatim>\ 1 x*y; 3 = fz, -z+1; 2 y*z-y-z+1; 4 * 3, y-1, -fz*y+fz-y*z+y+z-1; 5 + 2, 4, -fz*y+fz; 2 d; 4 d; 6 * 1, fz, fz*x*y; -x*z+x; 1 d; 7 * 5, x, -fz*x*y+fz*x; 8 + 6, 7, fz*x; 9 * 3, x, -fz*x-x*z+x; 10 + 8, 9, -x*z+x; \ Each line starts with a number that is used to index the (conclusion) polynomial. In the proof, there are four kind of steps: \<^enum> \<^verbatim>\3 = fz, -z+1;\ is an extension that introduces a new variable (in this case \<^verbatim>\fz\); \<^enum> \<^verbatim>\4 * 3, y-1, -fz*y+fz-y*z+y+z-1;\ is a multiplication of the existing polynomial with index 3 by the arbitrary polynomial \<^verbatim>\y-1\ and generates the new polynomial \<^verbatim>\-fz*y+fz-y*z+y+z-1\ with index 4; \<^enum> \<^verbatim>\5 + 2, 4, -fz*y+fz;\ is an addition of the existing polynomials with index 2 and 4 and generates the new polynomial \<^verbatim>\-fz*y+fz\ with index 5; \<^enum> \<^verbatim>\1 d;\ deletes the polynomial with index 1 and it cannot be reused in subsequent steps. Remark that unlike DRAT checker, we do forward checking and check every derived polynomial. The target polynomial can also be part of the input file. \ section \Libraries\ subsection \More Polynomials\ text \ Here are more theorems on polynomials. Most of these facts are extremely trivial and should probably be generalised and moved to the Isabelle distribution. \ lemma Const\<^sub>0_add: \Const\<^sub>0 (a + b) = Const\<^sub>0 a + Const\<^sub>0 b\ by transfer (simp add: Const\<^sub>0_def single_add) lemma Const_mult: \Const (a * b) = Const a * Const b\ by transfer (simp add: Const\<^sub>0_def times_monomial_monomial) lemma Const\<^sub>0_mult: \Const\<^sub>0 (a * b) = Const\<^sub>0 a * Const\<^sub>0 b\ by transfer (simp add: Const\<^sub>0_def times_monomial_monomial) lemma Const0[simp]: \Const 0 = 0\ by transfer (simp add: Const\<^sub>0_def) lemma (in -) Const_uminus[simp]: \Const (-n) = - Const n\ by transfer (auto simp: Const\<^sub>0_def monomial_uminus) lemma [simp]: \Const\<^sub>0 0 = 0\ \MPoly 0 = 0\ by (auto simp: Const\<^sub>0_def zero_mpoly_def) lemma Const_add: \Const (a + b) = Const a + Const b\ by transfer (simp add: Const\<^sub>0_def single_add) instance mpoly :: (comm_semiring_1) comm_semiring_1 by standard lemma degree_uminus[simp]: \degree (-A) x' = degree A x'\ by (auto simp: degree_def uminus_mpoly.rep_eq) lemma degree_sum_notin: \x' \ vars B \ degree (A + B) x' = degree A x'\ apply (auto simp: degree_def) apply (rule arg_cong[of _ _ Max]) apply standard+ apply (auto simp: plus_mpoly.rep_eq UN_I UnE image_iff in_keys_iff subsetD vars_def lookup_add dest: keys_add intro: in_keys_plusI1 cong: ball_cong_simp) done lemma degree_notin_vars: \x \ (vars B) \ degree (B :: 'a :: {monoid_add} mpoly) x = 0\ using degree_sum_notin[of x B 0] by auto lemma not_in_vars_coeff0: \x \ vars p \ MPoly_Type.coeff p (monomial (Suc 0) x) = 0\ by (subst not_not[symmetric], subst coeff_keys[symmetric]) (auto simp: vars_def) lemma keys_add': "p \ keys (f + g) \ p \ keys f \ keys g" by transfer auto lemma keys_mapping_sum_add: \finite A \ keys (mapping_of (\v \ A. f v)) \ \(keys ` mapping_of ` f ` UNIV)\ by (induction A rule: finite_induct) (auto simp add: zero_mpoly.rep_eq plus_mpoly.rep_eq keys_plus_ninv_comm_monoid_add dest: keys_add') lemma vars_sum_vars_union: fixes f :: \int mpoly \ int mpoly\ assumes \finite {v. f v \ 0}\ shows \vars (\v | f v \ 0. f v * v) \ \(vars ` {v. f v \ 0}) \ \(vars ` f ` {v. f v \ 0})\ (is \?A \ ?B\) proof fix p assume \p \ vars (\v | f v \ 0. f v * v)\ then obtain x where \x \ keys (mapping_of (\v | f v \ 0. f v * v))\ and p: \p \ keys x\ by (auto simp: vars_def times_mpoly.rep_eq simp del: keys_mult) then have \x \ (\x. keys (mapping_of (f x) * mapping_of x))\ using keys_mapping_sum_add[of \{v. f v \ 0}\ \\x. f x * x\] assms by (auto simp: vars_def times_mpoly.rep_eq) then have \x \ (\x. {a+b| a b. a \ keys (mapping_of (f x)) \ b \ keys (mapping_of x)})\ using Union_mono[OF ] keys_mult by fast then show \p \ ?B\ using p by (force simp: vars_def zero_mpoly.rep_eq dest!: keys_add') qed lemma vars_in_right_only: "x \ vars q \ x \ vars p \ x \ vars (p+q)" unfolding vars_def keys_def plus_mpoly.rep_eq lookup_plus_fun apply clarify subgoal for xa by (auto simp: vars_def keys_def plus_mpoly.rep_eq lookup_plus_fun intro!: exI[of _ xa] dest!: spec[of _ xa]) done lemma [simp]: \vars 0 = {}\ by (simp add: vars_def zero_mpoly.rep_eq) lemma vars_Un_nointer: \keys (mapping_of p) \ keys (mapping_of q) = {} \ vars (p + q) = vars p \ vars q\ by (auto simp: vars_def plus_mpoly.rep_eq simp flip: More_MPoly_Type.keys_add dest!: keys_add') lemmas [simp] = zero_mpoly.rep_eq lemma polynomial_sum_monoms: fixes p :: \'a :: {comm_monoid_add,cancel_comm_monoid_add} mpoly\ shows \p = (\x\keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))\ \keys (mapping_of p) \ I \ finite I \ p = (\x\I. MPoly_Type.monom x (MPoly_Type.coeff p x))\ proof - define J where \J \ keys (mapping_of p)\ define a where \a x \ coeff p x\ for x have \finite (keys (mapping_of p))\ by auto have \p = (\x\I. MPoly_Type.monom x (MPoly_Type.coeff p x))\ if \finite I\ and \keys (mapping_of p) \ I\ for I using that unfolding a_def proof (induction I arbitrary: p rule: finite_induct) case empty then have \p = 0\ using empty coeff_all_0 coeff_keys by blast then show ?case using empty by (auto simp: zero_mpoly.rep_eq) next case (insert x F) note fin = this(1) and xF = this(2) and IH = this(3) and incl = this(4) let ?p = \p - MPoly_Type.monom x (MPoly_Type.coeff p x)\ have H: \\xa. x \ F \ xa \ F \ MPoly_Type.monom xa (MPoly_Type.coeff (p - MPoly_Type.monom x (MPoly_Type.coeff p x)) xa) = MPoly_Type.monom xa (MPoly_Type.coeff p xa)\ by (metis (mono_tags, opaque_lifting) add_diff_cancel_right' remove_term_coeff remove_term_sum when_def) have \?p = (\xa\F. MPoly_Type.monom xa (MPoly_Type.coeff ?p xa))\ apply (rule IH) using incl apply - - by standard (smt Diff_iff Diff_insert_absorb add_diff_cancel_right' + by standard (smt (verit) Diff_iff Diff_insert_absorb add_diff_cancel_right' remove_term_keys remove_term_sum subsetD xF) also have \... = (\xa\F. MPoly_Type.monom xa (MPoly_Type.coeff p xa))\ by (use xF in \auto intro!: sum.cong simp: H\) finally show ?case apply (subst (asm) remove_term_sum[of x p, symmetric]) apply (subst remove_term_sum[of x p, symmetric]) using xF fin by (auto simp: ac_simps) qed from this[of I] this[of J] show \p = (\x\keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))\ \keys (mapping_of p) \ I \ finite I \ p = (\x\I. MPoly_Type.monom x (MPoly_Type.coeff p x))\ by (auto simp: J_def) qed lemma vars_mult_monom: fixes p :: \int mpoly\ shows \vars (p * (monom (monomial (Suc 0) x') 1)) = (if p = 0 then {} else insert x' (vars p))\ proof - let ?v = \monom (monomial (Suc 0) x') 1\ have p: \p = (\x\keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))\ (is \_ = (\x \ ?I. ?f x)\) using polynomial_sum_monoms(1)[of p] . have pv: \p * ?v = (\x \ ?I. ?f x * ?v)\ by (subst p) (auto simp: field_simps sum_distrib_left) define I where \I \ ?I\ have in_keysD: \x \ keys (mapping_of (\x\I. MPoly_Type.monom x (h x))) \ x \ I\ if \finite I\ for I and h :: \_ \ int\ and x using that by (induction rule: finite_induct) (force simp: monom.rep_eq empty_iff insert_iff keys_single coeff_monom simp: coeff_keys simp flip: coeff_add simp del: coeff_add)+ have in_keys: \keys (mapping_of (\x\I. MPoly_Type.monom x (h x))) = (\x \ I. (if h x = 0 then {} else {x}))\ if \finite I\ for I and h :: \_ \ int\ and x supply in_keysD[dest] using that by (induction rule: finite_induct) (auto simp: plus_mpoly.rep_eq MPoly_Type_Class.keys_plus_eqI) have H[simp]: \vars ((\x\I. MPoly_Type.monom x (h x))) = (\x\I. (if h x = 0 then {} else keys x))\ if \finite I\ for I and h :: \_ \ int\ using that by (auto simp: vars_def in_keys) have sums: \(\x\I. MPoly_Type.monom (x + a') (c x)) = (\x\ (\x. x + a') ` I. MPoly_Type.monom x (c (x - a')))\ if \finite I\ for I a' c q using that apply (induction rule: finite_induct) subgoal by auto subgoal unfolding image_insert by (subst sum.insert) auto done have non_zero_keysEx: \p \ 0 \ \a. a \ keys (mapping_of p)\ for p :: \int mpoly\ using mapping_of_inject by (fastforce simp add: ex_in_conv) have \finite I\ \keys (mapping_of p) \ I\ unfolding I_def by auto then show \vars (p * (monom (monomial (Suc 0) x') 1)) = (if p = 0 then {} else insert x' (vars p))\ apply (subst pv, subst I_def[symmetric], subst mult_monom) apply (auto simp: mult_monom sums I_def) using Poly_Mapping.keys_add vars_def apply fastforce apply (auto dest!: non_zero_keysEx) apply (rule_tac x= \a + monomial (Suc 0) x'\ in bexI) apply (auto simp: coeff_keys) apply (simp add: in_keys_iff lookup_add) apply (auto simp: vars_def) apply (rule_tac x= \xa + monomial (Suc 0) x'\ in bexI) apply (auto simp: coeff_keys) apply (simp add: in_keys_iff lookup_add) done qed term \(x', u, lookup u x', A)\ lemma in_mapping_mult_single: \x \ (\x. lookup x x') ` keys (A * (Var\<^sub>0 x' :: (nat \\<^sub>0 nat) \\<^sub>0 'b :: {monoid_mult,zero_neq_one,semiring_0})) \ x > 0 \ x - 1 \ (\x. lookup x x') ` keys (A)\ apply (standard+; clarify) subgoal apply (auto elim!: in_keys_timesE simp: lookup_add) apply (auto simp: keys_def lookup_times_monomial_right Var\<^sub>0_def lookup_single image_iff) done subgoal apply (auto elim!: in_keys_timesE simp: lookup_add) apply (auto simp: keys_def lookup_times_monomial_right Var\<^sub>0_def lookup_single image_iff) done subgoal for xa apply (auto elim!: in_keys_timesE simp: lookup_add) apply (auto simp: keys_def lookup_times_monomial_right Var\<^sub>0_def lookup_single image_iff lookup_add intro!: exI[of _ \xa + Poly_Mapping.single x' 1\]) done done lemma Max_Suc_Suc_Max: \finite A \ A \ {} \ Max (insert 0 (Suc ` A)) = Suc (Max (insert 0 A))\ by (induction rule: finite_induct) (auto simp: hom_Max_commute) lemma [simp]: \keys (Var\<^sub>0 x' :: ('a \\<^sub>0 nat) \\<^sub>0 'b :: {zero_neq_one}) = {Poly_Mapping.single x' 1}\ by (auto simp: Var\<^sub>0_def) lemma degree_mult_Var: \degree (A * Var x') x' = (if A = 0 then 0 else Suc (degree A x'))\ for A :: \int mpoly\ proof - have [simp]: \A \ 0 \ Max (insert 0 ((\x. Suc (lookup x x')) ` keys (mapping_of A))) = Max (insert (Suc 0) ((\x. Suc (lookup x x')) ` keys (mapping_of A)))\ unfolding image_image[of Suc \\x. lookup x x'\, symmetric] image_insert[symmetric] by (subst Max_Suc_Suc_Max, use mapping_of_inject in fastforce, use mapping_of_inject in fastforce)+ (simp add: Max.hom_commute) have \A \ 0 \ Max (insert 0 ((\x. lookup x x') ` keys (mapping_of A * mapping_of (Var x')))) = Suc (Max (insert 0 ((\m. lookup m x') ` keys (mapping_of A))))\ by (subst arg_cong[of _ \insert 0 (Suc ` ((\x. lookup x x') ` keys (mapping_of A)))\ Max]) (auto simp: image_image Var.rep_eq lookup_plus_fun in_mapping_mult_single hom_Max_commute Max_Suc_Suc_Max elim!: in_keys_timesE split: if_splits) then show ?thesis by (auto simp: degree_def times_mpoly.rep_eq intro!: arg_cong[of _ \insert 0 (Suc ` ((\x. lookup x x') ` keys (mapping_of A)))\ Max]) qed lemma degree_mult_Var': \degree (Var x' * A) x' = (if A = 0 then 0 else Suc (degree A x'))\ for A :: \int mpoly\ by (simp add: degree_mult_Var semiring_normalization_rules(7)) lemma degree_times_le: \degree (A * B) x \ degree A x + degree B x\ by (auto simp: degree_def times_mpoly.rep_eq max_def lookup_add add_mono dest!: set_rev_mp[OF _ Poly_Mapping.keys_add] elim!: in_keys_timesE) lemma monomial_inj: "monomial c s = monomial (d::'b::zero_neq_one) t \ (c = 0 \ d = 0) \ (c = d \ s = t)" by (fastforce simp add: monomial_inj Poly_Mapping.single_def poly_mapping.Abs_poly_mapping_inject when_def fun_eq_iff cong: if_cong split: if_splits) lemma MPoly_monomial_power': \MPoly (monomial 1 x') ^ (n+1) = MPoly (monomial (1) (((\x. x + x') ^^ n) x'))\ by (induction n) (auto simp: times_mpoly.abs_eq mult_single ac_simps) lemma MPoly_monomial_power: \n > 0 \ MPoly (monomial 1 x') ^ (n) = MPoly (monomial (1) (((\x. x + x') ^^ (n - 1)) x'))\ using MPoly_monomial_power'[of _ \n-1\] by auto lemma vars_uminus[simp]: \vars (-p) = vars p\ by (auto simp: vars_def uminus_mpoly.rep_eq) lemma coeff_uminus[simp]: \MPoly_Type.coeff (-p) x = -MPoly_Type.coeff p x\ by (auto simp: coeff_def uminus_mpoly.rep_eq) definition decrease_key::"'a \ ('a \\<^sub>0 'b::{monoid_add, minus,one}) \ ('a \\<^sub>0 'b)" where "decrease_key k0 f = Abs_poly_mapping (\k. if k = k0 \ lookup f k \ 0 then lookup f k - 1 else lookup f k)" lemma remove_key_lookup: "lookup (decrease_key k0 f) k = (if k = k0 \ lookup f k \ 0 then lookup f k - 1 else lookup f k)" unfolding decrease_key_def using finite_subset apply simp apply (subst lookup_Abs_poly_mapping) apply (auto intro: finite_subset[of _ \{x. lookup f x \ 0}\]) apply (subst lookup_Abs_poly_mapping) apply (auto intro: finite_subset[of _ \{x. lookup f x \ 0}\]) done lemma polynomial_split_on_var: fixes p :: \'a :: {comm_monoid_add,cancel_comm_monoid_add,semiring_0,comm_semiring_1} mpoly\ obtains q r where \p = monom (monomial (Suc 0) x') 1 * q + r\ and \x' \ vars r\ proof - have [simp]: \{x \ keys (mapping_of p). x' \ keys x} \ {x \ keys (mapping_of p). x' \ keys x} = keys (mapping_of p)\ by auto have \p = (\x\keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))\ (is \_ = (\x \ ?I. ?f x)\) using polynomial_sum_monoms(1)[of p] . also have \... = (\x\ {x \ ?I. x' \ keys x}. ?f x) + (\x\ {x \ ?I. x' \ keys x}. ?f x)\ (is \_ = ?pX + ?qX\) by (subst comm_monoid_add_class.sum.union_disjoint[symmetric]) auto finally have 1: \p = ?pX + ?qX\ . have H: \0 < lookup x x' \ (\k. (if x' = k then Suc 0 else 0) + (if k = x' \ 0 < lookup x k then lookup x k - 1 else lookup x k)) = lookup x\ for x x' by auto have [simp]: \finite {x. 0 < (Suc 0 when x' = x)}\ for x' :: nat and x - by (smt bounded_nat_set_is_finite lessI mem_Collect_eq neq0_conv when_cong when_neq_zero) + by (smt (verit) bounded_nat_set_is_finite lessI mem_Collect_eq neq0_conv when_cong when_neq_zero) have H: \x' \ keys x \ monomial (Suc 0) x' + Abs_poly_mapping (\k. if k = x' \ 0 < lookup x k then lookup x k - 1 else lookup x k) = x\ for x and x' :: nat apply (simp only: keys_def single.abs_eq) apply (subst plus_poly_mapping.abs_eq) by (auto simp: eq_onp_def when_def H intro!: finite_subset[of \{xa. (xa = x' \ 0 < lookup x xa \ Suc 0 < lookup x x') \ (xa \ x' \ 0 < lookup x xa)}\ \{xa. 0 < lookup x xa}\]) have [simp]: \x' \ keys x \ MPoly_Type.monom (monomial (Suc 0) x' + decrease_key x' x) n = MPoly_Type.monom x n\ for x n and x' apply (subst mpoly.mapping_of_inject[symmetric], subst poly_mapping.lookup_inject[symmetric]) unfolding mapping_of_monom lookup_single apply (auto intro!: ext simp: decrease_key_def when_def H) done have pX: \?pX = monom (monomial (Suc 0) x') 1 * (\x\ {x \ ?I. x' \ keys x}. MPoly_Type.monom (decrease_key x' x) (MPoly_Type.coeff p x))\ (is \_ = _ * ?pX'\) by (subst sum_distrib_left, subst mult_monom) (auto intro!: sum.cong) have \x' \ vars ?qX\ using vars_setsum[of \{x. x \ keys (mapping_of p) \ x' \ keys x}\ \?f\] by (auto dest!: vars_monom_subset[unfolded subset_eq Ball_def, rule_format]) then show ?thesis using that[of ?pX' ?qX] unfolding pX[symmetric] 1[symmetric] by blast qed lemma polynomial_split_on_var2: fixes p :: \int mpoly\ assumes \x' \ vars s\ obtains q r where \p = (monom (monomial (Suc 0) x') 1 - s) * q + r\ and \x' \ vars r\ proof - have eq[simp]: \monom (monomial (Suc 0) x') 1 = Var x'\ by (simp add: Var.abs_eq Var\<^sub>0_def monom.abs_eq) have \\m \ n. \P::int mpoly. degree P x' < m \ (\A B. P = (Var x' - s) * A + B \ x' \ vars B)\ for n proof (induction n) case 0 then show ?case by auto next case (Suc n) then have IH: \m\n \ MPoly_Type.degree P x' < m \ (\A B. P = (Var x' - s) * A + B \ x' \ vars B)\ for m P by fast show ?case proof (intro allI impI) fix m and P :: \int mpoly\ assume \m \ Suc n\ and deg: \MPoly_Type.degree P x' < m\ consider \m \ n\ | \m = Suc n\ using \m \ Suc n\ by linarith then show \\A B. P = (Var x' - s) * A + B \ x' \ vars B\ proof cases case 1 then show \?thesis\ using Suc deg by blast next case [simp]: 2 obtain A B where P: \P = Var x' * A + B\ and \x' \ vars B\ using polynomial_split_on_var[of P x'] unfolding eq by blast have P': \P = (Var x' - s) * A + (s * A + B)\ by (auto simp: field_simps P) have \A = 0 \ degree (s * A) x' < degree P x'\ using deg \x' \ vars B\ \x' \ vars s\ degree_times_le[of s A x'] deg unfolding P by (auto simp: degree_sum_notin degree_mult_Var' degree_mult_Var degree_notin_vars split: if_splits) then obtain A' B' where sA: \s*A = (Var x' - s) * A' + B'\ and \x' \ vars B'\ using IH[of \m-1\ \s*A\] deg \x' \ vars B\ that[of 0 0] by (cases \0 < n\) (auto dest!: vars_in_right_only) have \P = (Var x' - s) * (A + A') + (B' + B)\ unfolding P' sA by (auto simp: field_simps) moreover have \x' \ vars (B' + B)\ using \x' \ vars B'\ \x' \ vars B\ by (meson UnE subset_iff vars_add) ultimately show ?thesis by fast qed qed qed then show ?thesis using that unfolding eq by blast qed lemma finit_whenI[intro]: \finite {x. (0 :: nat) < (y x)} \ finite {x. 0 < (y x when x \ x')}\ apply (rule finite_subset) defer apply assumption apply (auto simp: when_def) done lemma polynomial_split_on_var_diff_sq2: fixes p :: \int mpoly\ obtains q r s where \p = monom (monomial (Suc 0) x') 1 * q + r + s * (monom (monomial (Suc 0) x') 1^2 - monom (monomial (Suc 0) x') 1)\ and \x' \ vars r\ and \x' \ vars q\ proof - let ?v = \monom (monomial (Suc 0) x') 1 :: int mpoly\ have H: \n < m \ n > 0 \ \q. ?v^n = ?v + q * (?v^2 - ?v)\ for n m :: nat proof (induction m arbitrary: n) case 0 then show ?case by auto next case (Suc m n) note IH = this(1-) consider \n < m\ | \m = n\ \n > 1\ | \n = 1\ using IH by (cases \n < m\; cases n) auto then show ?case proof cases case 1 then show ?thesis using IH by auto next case 2 have eq: \?v^(n) = ((?v :: int mpoly) ^ (n-2)) * (?v^2-?v) + ?v^(n-1)\ using 2 by (auto simp: field_simps power_eq_if ideal.scale_right_diff_distrib) obtain q where q: \?v^(n-1) = ?v + q * (?v^2 - ?v)\ using IH(1)[of \n-1\] 2 by auto show ?thesis using q unfolding eq by (auto intro!: exI[of _ \?v ^ (n - 2) + q\] simp: distrib_right) next case 3 then show \?thesis\ by auto qed qed have H: \n>0 \ \q. ?v^n = ?v + q * (?v^2-?v)\ for n using H[of n \n+1\] by auto obtain qr :: \nat \ int mpoly\ where qr: \n > 0 \ ?v^n = ?v + qr n * (?v^2-?v)\ for n using H by metis have vn: \(if lookup x x' = 0 then 1 else Var x' ^ lookup x x') = (if lookup x x' = 0 then 1 else ?v) + (if lookup x x' = 0 then 0 else 1) * qr (lookup x x') * (?v^2-?v)\ for x by (simp add: qr[symmetric] Var_def Var\<^sub>0_def monom.abs_eq[symmetric] cong: if_cong) have q: \p = (\x\keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))\ by (rule polynomial_sum_monoms(1)[of p]) have [simp]: \lookup x x' = 0 \ Abs_poly_mapping (\k. lookup x k when k \ x') = x\ for x by (cases x, auto simp: poly_mapping.Abs_poly_mapping_inject) (auto intro!: ext simp: when_def) have [simp]: \finite {x. 0 < (a when x' = x)}\ for a :: nat by (metis (no_types, lifting) infinite_nat_iff_unbounded less_not_refl lookup_single lookup_single_not_eq mem_Collect_eq) have [simp]: \((\x. x + monomial (Suc 0) x') ^^ (n)) (monomial (Suc 0) x') = Abs_poly_mapping (\k. (if k = x' then n+1 else 0))\ for n by (induction n) (auto simp: single_def Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def cong:if_cong) have [simp]: \0 < lookup x x' \ Abs_poly_mapping (\k. lookup x k when k \ x') + Abs_poly_mapping (\k. if k = x' then lookup x x' - Suc 0 + 1 else 0) = x\ for x apply (cases x, auto simp: poly_mapping.Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def) apply (subst plus_poly_mapping.abs_eq) apply (auto simp: poly_mapping.Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def) apply (subst Abs_poly_mapping_inject) apply auto done define f where \f x = (MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)) * (if lookup x x' = 0 then 1 else Var x' ^ (lookup x x'))\ for x have f_alt_def: \f x = MPoly_Type.monom x (MPoly_Type.coeff p x)\ for x by (auto simp: f_def monom_def remove_key_def Var_def MPoly_monomial_power Var\<^sub>0_def mpoly.MPoly_inject monomial_inj times_mpoly.abs_eq times_mpoly.abs_eq mult_single) have p: \p = (\x\keys (mapping_of p). MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) * (if lookup x x' = 0 then 1 else ?v)) + (\x\keys (mapping_of p). MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) * (if lookup x x' = 0 then 0 else 1) * qr (lookup x x')) * (?v\<^sup>2 - ?v)\ (is \_ = ?a + ?v2v\) apply (subst q) unfolding f_alt_def[symmetric, abs_def] f_def vn semiring_class.distrib_left comm_semiring_1_class.semiring_normalization_rules(18) semiring_0_class.sum_distrib_right by (simp add: semiring_class.distrib_left sum.distrib) have I: \keys (mapping_of p) = {x \ keys (mapping_of p). lookup x x' = 0} \ {x \ keys (mapping_of p). lookup x x' \ 0}\ by auto have \p = (\x | x \ keys (mapping_of p) \ lookup x x' = 0. MPoly_Type.monom x (MPoly_Type.coeff p x)) + (\x | x \ keys (mapping_of p) \ lookup x x' \ 0. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)) * (MPoly_Type.monom (monomial (Suc 0) x') 1) + (\x | x \ keys (mapping_of p) \ lookup x x' \ 0. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) * qr (lookup x x')) * (?v\<^sup>2 - ?v)\ (is \p = ?A + ?B * _ + ?C * _\) unfolding semiring_0_class.sum_distrib_right[of _ _ \(MPoly_Type.monom (monomial (Suc 0) x') 1)\] apply (subst p) apply (subst (2)I) apply (subst I) apply (subst comm_monoid_add_class.sum.union_disjoint) apply auto[3] apply (subst comm_monoid_add_class.sum.union_disjoint) apply auto[3] apply (subst (4) sum.cong[OF refl, of _ _ \\x. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) * qr (lookup x x')\]) apply (auto; fail) apply (subst (3) sum.cong[OF refl, of _ _ \\x. 0\]) apply (auto; fail) apply (subst (2) sum.cong[OF refl, of _ _ \\x. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) * (MPoly_Type.monom (monomial (Suc 0) x') 1)\]) apply (auto; fail) apply (subst (1) sum.cong[OF refl, of _ _ \\x. MPoly_Type.monom x (MPoly_Type.coeff p x)\]) by (auto simp: f_def simp flip: f_alt_def) moreover have \x' \ vars ?A\ using vars_setsum[of \{x \ keys (mapping_of p). lookup x x' = 0}\ \\x. MPoly_Type.monom x (MPoly_Type.coeff p x)\] apply auto apply (drule set_rev_mp, assumption) apply (auto dest!: lookup_eq_zero_in_keys_contradict) by (meson lookup_eq_zero_in_keys_contradict subsetD vars_monom_subset) moreover have \x' \ vars ?B\ using vars_setsum[of \{x \ keys (mapping_of p). lookup x x' \ 0}\ \\x. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)\] apply auto apply (drule set_rev_mp, assumption) apply (auto dest!: lookup_eq_zero_in_keys_contradict) apply (drule subsetD[OF vars_monom_subset]) apply (auto simp: remove_key_keys[symmetric]) done ultimately show ?thesis apply - apply (rule that[of ?B ?A ?C]) apply (auto simp: ac_simps) done qed lemma polynomial_decomp_alien_var: fixes q A b :: \int mpoly\ assumes q: \q = A * (monom (monomial (Suc 0) x') 1) + b\ and x: \x' \ vars q\ \x' \ vars b\ shows \A = 0\ and \q = b\ proof - let ?A = \A * (monom (monomial (Suc 0) x') 1)\ have \?A = q - b\ using arg_cong[OF q, of \\a. a - b\] by auto moreover have \x' \ vars (q - b)\ using x vars_in_right_only by fastforce ultimately have \x' \ vars (?A)\ by simp then have \?A = 0\ by (auto simp: vars_mult_monom split: if_splits) moreover have \?A = 0 \ A = 0\ by (metis empty_not_insert mult_zero_left vars_mult_monom) ultimately show \A = 0\ by blast then show \q = b\ using q by auto qed lemma polynomial_decomp_alien_var2: fixes q A b :: \int mpoly\ assumes q: \q = A * (monom (monomial (Suc 0) x') 1 + p) + b\ and x: \x' \ vars q\ \x' \ vars b\ \x' \ vars p\ shows \A = 0\ and \q = b\ proof - let ?x = \monom (monomial (Suc 0) x') 1\ have x'[simp]: \?x = Var x'\ by (simp add: Var.abs_eq Var\<^sub>0_def monom.abs_eq) have \\n Ax A'. A = ?x * Ax + A' \ x' \ vars A' \ degree Ax x' = n\ using polynomial_split_on_var[of A x'] by metis from wellorder_class.exists_least_iff[THEN iffD1, OF this] obtain Ax A' n where A: \A = Ax * ?x + A'\ and \x' \ vars A'\ and n: \MPoly_Type.degree Ax x' = n\ and H: \\m Ax A'. m < n \ A \ Ax * MPoly_Type.monom (monomial (Suc 0) x') 1 + A' \ x' \ vars A' \ MPoly_Type.degree Ax x' \ m\ unfolding wellorder_class.exists_least_iff[of \\n. \Ax A'. A = Ax * ?x + A' \ x' \ vars A' \ degree Ax x' = n\] by (auto simp: field_simps) have \q = (A + Ax * p) * monom (monomial (Suc 0) x') 1 + (p * A' + b)\ unfolding q A by (auto simp: field_simps) moreover have \x' \ vars q\ \x' \ vars (p * A' + b)\ using x \x' \ vars A'\ - by (smt UnE add.assoc add.commute calculation subset_iff vars_in_right_only vars_mult)+ + by (smt (verit) UnE add.assoc add.commute calculation subset_iff vars_in_right_only vars_mult)+ ultimately have \A + Ax * p = 0\ \q = p * A' + b\ by (rule polynomial_decomp_alien_var)+ have A': \A' = -Ax * ?x - Ax * p\ using \A + Ax * p = 0\ unfolding A by (metis (no_types, lifting) add_uminus_conv_diff eq_neg_iff_add_eq_0 minus_add_cancel mult_minus_left) have \A = - (Ax * p)\ using A unfolding A' apply auto done obtain Axx Ax' where Ax: \Ax = ?x * Axx + Ax'\ and \x' \ vars Ax'\ using polynomial_split_on_var[of Ax x'] by metis have \A = ?x * (- Axx * p) + (- Ax' * p)\ unfolding \A = - (Ax * p)\ Ax by (auto simp: field_simps) moreover have \x' \ vars (-Ax' * p)\ using \x' \ vars Ax'\ by (metis (no_types, opaque_lifting) UnE add.right_neutral add_minus_cancel assms(4) subsetD vars_in_right_only vars_mult) moreover have \Axx \ 0 \ MPoly_Type.degree (- Axx * p) x' < degree Ax x'\ using degree_times_le[of Axx p x'] x by (auto simp: Ax degree_sum_notin \x' \ vars Ax'\ degree_mult_Var' degree_notin_vars) ultimately have [simp]: \Axx = 0\ using H[of \MPoly_Type.degree (- Axx * p) x'\ \- Axx * p\ \- Ax' * p\] by (auto simp: n) then have [simp]: \Ax' = Ax\ using Ax by auto show \A = 0\ using A \A = - (Ax * p)\ \x' \ vars (- Ax' * p)\ \x' \ vars A'\ polynomial_decomp_alien_var(1) by force then show \q = b\ using q by auto qed lemma vars_unE: \x \ vars (a * b) \ (x \ vars a \ thesis) \ (x \ vars b \ thesis) \ thesis\ using vars_mult[of a b] by auto lemma in_keys_minusI1: assumes "t \ keys p" and "t \ keys q" shows "t \ keys (p - q)" using assms unfolding in_keys_iff lookup_minus by simp lemma in_keys_minusI2: fixes t :: \'a\ and q :: \'a \\<^sub>0 'b :: {cancel_comm_monoid_add,group_add}\ assumes "t \ keys q" and "t \ keys p" shows "t \ keys (p - q)" using assms unfolding in_keys_iff lookup_minus by simp lemma in_vars_addE: \x \ vars (p + q) \ (x \ vars p \ thesis) \ (x \ vars q \ thesis) \ thesis\ by (meson UnE in_mono vars_add) lemma lookup_monomial_If: \lookup (monomial v k) = (\k'. if k = k' then v else 0)\ by (intro ext) (auto simp: lookup_single_not_eq) lemma vars_mult_Var: \vars (Var x * p) = (if p = 0 then {} else insert x (vars p))\ for p :: \int mpoly\ proof - have \p \ 0 \ \xa. (\k. xa = monomial (Suc 0) x + k) \ lookup (mapping_of p) (xa - monomial (Suc 0) x) \ 0 \ 0 < lookup xa x\ by (metis (no_types, opaque_lifting) One_nat_def ab_semigroup_add_class.add.commute add_diff_cancel_right' aux lookup_add lookup_single_eq mapping_of_inject neq0_conv one_neq_zero plus_eq_zero_2 zero_mpoly.rep_eq) then show ?thesis apply (auto simp: vars_def times_mpoly.rep_eq Var.rep_eq elim!: in_keys_timesE dest: keys_add') apply (auto simp: keys_def lookup_times_monomial_left Var.rep_eq Var\<^sub>0_def adds_def lookup_add eq_diff_eq'[symmetric]) done qed lemma keys_mult_monomial: \keys (monomial (n :: int) k * mapping_of a) = (if n = 0 then {} else ((+) k) ` keys (mapping_of a))\ proof - have [simp]: \(\aa. (if k = aa then n else 0) * (\q. lookup (mapping_of a) q when k + xa = aa + q)) = (\aa. (if k = aa then n * (\q. lookup (mapping_of a) q when k + xa = aa + q) else 0))\ for xa - by (smt Sum_any.cong mult_not_zero) + by (smt (verit) 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\<^sub>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 vars_mult_Const: \vars (Const n * a) = (if n = 0 then {} else vars a)\ for a :: \int mpoly\ by (auto simp: vars_def times_mpoly.rep_eq Const.rep_eq keys_mult_monomial Const\<^sub>0_def elim!: in_keys_timesE split: if_splits) lemma coeff_minus: "coeff p m - coeff q m = coeff (p-q) m" by (simp add: coeff_def lookup_minus minus_mpoly.rep_eq) lemma Const_1_eq_1: \Const (1 :: int) = (1 :: int mpoly)\ by (simp add: Const.abs_eq Const\<^sub>0_one one_mpoly.abs_eq) lemma [simp]: \vars (1 :: int mpoly) = {}\ by (auto simp: vars_def one_mpoly.rep_eq Const_1_eq_1) subsection \More Ideals\ lemma fixes A :: \(('x \\<^sub>0 nat) \\<^sub>0 'a::comm_ring_1) set\ assumes \p \ ideal A\ shows \p * q \ ideal A\ by (metis assms ideal.span_scale semiring_normalization_rules(7)) text \The following theorem is very close to @{thm ideal.span_insert}, except that it is more useful if we need to take an element of \<^term>\More_Modules.ideal (insert a S)\.\ lemma ideal_insert': \More_Modules.ideal (insert a S) = {y. \x k. y = x + k * a \ x \ More_Modules.ideal S}\ apply (auto simp: ideal.span_insert intro: exI[of _ \_ - k * a\]) apply (rule_tac x = \x - k * a\ in exI) apply auto apply (rule_tac x = \k\ in exI) apply auto done lemma ideal_mult_right_in: \a \ ideal A \ a * b \ More_Modules.ideal A\ by (metis ideal.span_scale mult.commute) lemma ideal_mult_right_in2: \a \ ideal A \ b * a \ More_Modules.ideal A\ by (metis ideal.span_scale) lemma [simp]: \vars (Var x :: 'a :: {zero_neq_one} mpoly) = {x}\ by (auto simp: vars_def Var.rep_eq Var\<^sub>0_def) lemma vars_minus_Var_subset: \vars (p' - Var x :: 'a :: {ab_group_add,one,zero_neq_one} mpoly) \ \ \ vars p' \ insert x \\ using vars_add[of \p' - Var x\ \Var x\] by auto lemma vars_add_Var_subset: \vars (p' + Var x :: 'a :: {ab_group_add,one,zero_neq_one} mpoly) \ \ \ vars p' \ insert x \\ using vars_add[of \p' + Var x\ \-Var x\] by auto lemma coeff_monomila_in_varsD: \coeff p (monomial (Suc 0) x) \ 0 \ x \ vars (p :: int mpoly)\ by (auto simp: coeff_def vars_def keys_def intro!: exI[of _ \monomial (Suc 0) x\]) lemma coeff_MPoly_monomial[simp]: \(MPoly_Type.coeff (MPoly (monomial a m)) m) = a\ by (metis MPoly_Type.coeff_def lookup_single_eq monom.abs_eq monom.rep_eq) end \ No newline at end of file diff --git a/thys/PAC_Checker/PAC_Specification.thy b/thys/PAC_Checker/PAC_Specification.thy --- a/thys/PAC_Checker/PAC_Specification.thy +++ b/thys/PAC_Checker/PAC_Specification.thy @@ -1,575 +1,575 @@ (* File: PAC_Specification.thy Author: Mathias Fleury, Daniela Kaufmann, JKU Maintainer: Mathias Fleury, JKU *) theory PAC_Specification imports PAC_More_Poly begin section \Specification of the PAC checker\ subsection \Ideals\ type_synonym int_poly = \int mpoly\ definition polynomial_bool :: \int_poly set\ where \polynomial_bool = (\c. Var c ^ 2 - Var c) ` UNIV\ definition pac_ideal where \pac_ideal A \ ideal (A \ polynomial_bool)\ lemma X2_X_in_pac_ideal: \Var c ^ 2 - Var c \ pac_ideal A\ unfolding polynomial_bool_def pac_ideal_def by (auto intro: ideal.span_base) lemma pac_idealI1[intro]: \p \ A \ p \ pac_ideal A\ unfolding pac_ideal_def by (auto intro: ideal.span_base) lemma pac_idealI2[intro]: \p \ ideal A \ p \ pac_ideal A\ using ideal.span_subspace_induct pac_ideal_def by blast lemma pac_idealI3[intro]: \p \ ideal A \ p*q \ pac_ideal A\ by (metis ideal.span_scale mult.commute pac_idealI2) lemma pac_ideal_Xsq2_iff: \Var c ^ 2 \ pac_ideal A \ Var c \ pac_ideal A\ unfolding pac_ideal_def apply (subst (2) ideal.span_add_eq[symmetric, OF X2_X_in_pac_ideal[of c, unfolded pac_ideal_def]]) apply auto done lemma diff_in_polynomial_bool_pac_idealI: assumes a1: "p \ pac_ideal A" assumes a2: "p - p' \ More_Modules.ideal polynomial_bool" shows \p' \ pac_ideal A\ proof - have "insert p polynomial_bool \ pac_ideal A" using a1 unfolding pac_ideal_def by (meson ideal.span_superset insert_subset le_sup_iff) then show ?thesis using a2 unfolding pac_ideal_def by (metis (no_types) ideal.eq_span_insert_eq ideal.span_subset_spanI ideal.span_superset insert_subset subsetD) qed lemma diff_in_polynomial_bool_pac_idealI2: assumes a1: "p \ A" assumes a2: "p - p' \ More_Modules.ideal polynomial_bool" shows \p' \ pac_ideal A\ using diff_in_polynomial_bool_pac_idealI[OF _ assms(2), of A] assms(1) by (auto simp: ideal.span_base) lemma pac_ideal_alt_def: \pac_ideal A = ideal (A \ ideal polynomial_bool)\ unfolding pac_ideal_def by (meson ideal.span_eq ideal.span_mono ideal.span_superset le_sup_iff subset_trans sup_ge2) text \ The equality on ideals is restricted to polynomials whose variable appear in the set of ideals. The function restrict sets: \ definition restricted_ideal_to where \restricted_ideal_to B A = {p \ A. vars p \ B}\ abbreviation restricted_ideal_to\<^sub>I where \restricted_ideal_to\<^sub>I B A \ restricted_ideal_to B (pac_ideal (set_mset A))\ abbreviation restricted_ideal_to\<^sub>V where \restricted_ideal_to\<^sub>V B \ restricted_ideal_to (\(vars ` set_mset B))\ abbreviation restricted_ideal_to\<^sub>V\<^sub>I where \restricted_ideal_to\<^sub>V\<^sub>I B A \ restricted_ideal_to (\(vars ` set_mset B)) (pac_ideal (set_mset A))\ lemma restricted_idealI: \p \ pac_ideal (set_mset A) \ vars p \ C \ p \ restricted_ideal_to\<^sub>I C A\ unfolding restricted_ideal_to_def by auto lemma pac_ideal_insert_already_in: \pq \ pac_ideal (set_mset A) \ pac_ideal (insert pq (set_mset A)) = pac_ideal (set_mset A)\ by (auto simp: pac_ideal_alt_def ideal.span_insert_idI) lemma pac_ideal_add: \p \# A \ q \# A \ p + q \ pac_ideal (set_mset A)\ by (simp add: ideal.span_add ideal.span_base pac_ideal_def) lemma pac_ideal_mult: \p \# A \ p * q \ pac_ideal (set_mset A)\ by (simp add: ideal.span_base pac_idealI3) lemma pac_ideal_mono: \A \ B \ pac_ideal A \ pac_ideal B\ using ideal.span_mono[of \A \ _\ \B \ _\] by (auto simp: pac_ideal_def intro: ideal.span_mono) subsection \PAC Format\ text \The PAC format contains three kind of steps: \<^item> \<^verbatim>\add\ that adds up two polynomials that are known. \<^item> \<^verbatim>\mult\ that multiply a known polynomial with another one. \<^item> \<^verbatim>\del\ that removes a polynomial that cannot be reused anymore. To model the simplification that happens, we add the \<^term>\p - p' \ polynomial_bool\ stating that \<^term>\p\ and \<^term>\p'\ are equivalent. \ type_synonym pac_st = \(nat set \ int_poly multiset)\ inductive PAC_Format :: \pac_st \ pac_st \ bool\ where add: \PAC_Format (\, A) (\, add_mset p' A)\ if \p \# A\ \q \# A\ \p+q - p' \ ideal polynomial_bool\ \vars p' \ \\ | mult: \PAC_Format (\, A) (\, add_mset p' A)\ if \p \# A\ \p*q - p' \ ideal polynomial_bool\ \vars p' \ \\ \vars q \ \\ | del: \p \# A \ PAC_Format (\, A) (\, A - {#p#})\ | extend_pos: \PAC_Format (\, A) (\ \ {x' \ vars (-Var x + p'). x' \ \}, add_mset (-Var x + p') A)\ if \(p')\<^sup>2 - p' \ ideal polynomial_bool\ \vars p' \ \\ \x \ \\ text \ In the PAC format above, we have a technical condition on the normalisation: \<^term>\vars p' \ vars (p + q)\ is here to ensure that we don't normalise \<^term>\0 :: int mpoly\ to \<^term>\Var x^2 - Var x :: int mpoly\ for a new variable \<^term>\x :: nat\. This is completely obvious for the normalisation process we have in mind when we write the specification, but we must add it explicitly because we are too general. \ lemmas PAC_Format_induct_split = PAC_Format.induct[split_format(complete), of V A V' A' for V A V' A'] lemma PAC_Format_induct[consumes 1, case_names add mult del ext]: assumes \PAC_Format (\, A) (\', A')\ and cases: \\p q p' A \. p \# A \ q \# A \ p+q - p' \ ideal polynomial_bool \ vars p' \ \ \ P \ A \ (add_mset p' A)\ \\p q p' A \. p \# A \ p*q - p' \ ideal polynomial_bool \ vars p' \ \ \ vars q \ \ \ P \ A \ (add_mset p' A)\ \\p A \. p \# A \ P \ A \ (A - {#p#})\ \\p' x r. (p')^2 - (p') \ ideal polynomial_bool \ vars p' \ \ \ x \ \ \ P \ A (\ \ {x' \ vars (p' - Var x). x' \ \}) (add_mset (p' -Var x) A)\ shows \P \ A \' A'\ using assms(1) apply - by (induct V\\ A\A \' A' rule: PAC_Format_induct_split) (auto intro: assms(1) cases) text \ The theorem below (based on the proof ideal by Manuel Kauers) is the correctness theorem of extensions. Remark that the assumption \<^term>\vars q \ \\ is only used to show that \<^term>\x' \ vars q\. \ lemma extensions_are_safe: assumes \x' \ vars p\ and x': \x' \ \\ and \\ (vars ` set_mset A) \ \\ and p_x_coeff: \coeff p (monomial (Suc 0) x') = 1\ and vars_q: \vars q \ \\ and q: \q \ More_Modules.ideal (insert p (set_mset A \ polynomial_bool))\ and leading: \x' \ vars (p - Var x')\ and diff: \(Var x' - p)\<^sup>2 - (Var x' - p) \ More_Modules.ideal polynomial_bool\ shows \q \ More_Modules.ideal (set_mset A \ polynomial_bool)\ proof - define p' where \p' \ p - Var x'\ let ?v = \Var x' :: int mpoly\ have p_p': \p = ?v + p'\ by (auto simp: p'_def) define q' where \q' \ Var x' - p\ have q_q': \p = ?v - q'\ by (auto simp: q'_def) have diff: \q'^2 - q' \ More_Modules.ideal polynomial_bool\ using diff unfolding q_q' by auto have [simp]: \vars ((Var c)\<^sup>2 - Var c :: int mpoly) = {c}\ for c apply (auto simp: vars_def Var_def Var\<^sub>0_def mpoly.MPoly_inverse keys_def lookup_minus_fun lookup_times_monomial_right single.rep_eq split: if_splits) apply (auto simp: vars_def Var_def Var\<^sub>0_def mpoly.MPoly_inverse keys_def lookup_minus_fun lookup_times_monomial_right single.rep_eq when_def ac_simps adds_def lookup_plus_fun power2_eq_square times_mpoly.rep_eq minus_mpoly.rep_eq split: if_splits) apply (rule_tac x = \(2 :: nat \\<^sub>0 nat) * monomial (Suc 0) c\ in exI) apply (auto dest: monomial_0D simp: plus_eq_zero_2 lookup_plus_fun mult_2) by (meson Suc_neq_Zero monomial_0D plus_eq_zero_2) have eq: \More_Modules.ideal (insert p (set_mset A \ polynomial_bool)) = More_Modules.ideal (insert p (set_mset A \ (\c. Var c ^ 2 - Var c) ` {c. c \ x'}))\ (is \?A = ?B\ is \_ = More_Modules.ideal ?trimmed\) proof - let ?C = \insert p (set_mset A \ (\c. Var c ^ 2 - Var c) ` {c. c \ x'})\ let ?D = \(\c. Var c ^ 2 - Var c) ` {c. c \ x'}\ have diff: \q'^2 - q' \ More_Modules.ideal ?D\ (is \?q \ _\) proof - obtain r t where q: \?q = (\a\t. r a * a)\ and fin_t: \finite t\ and t: \t \ polynomial_bool\ using diff unfolding ideal.span_explicit by auto show ?thesis proof (cases \?v^2-?v \ t\) case True then show \?thesis\ using q fin_t t unfolding ideal.span_explicit by (auto intro!: exI[of _ \t - {?v^2 -?v}\] exI[of _ r] simp: polynomial_bool_def sum_diff1) next case False define t' where \t' = t - {?v^2 - ?v}\ have t_t': \t = insert (?v^2 - ?v) t'\ and notin: \?v^2 - ?v \ t'\ and \t' \ (\c. Var c ^ 2 - Var c) ` {c. c \ x'}\ using False t unfolding t'_def polynomial_bool_def by auto have mon: \monom (monomial (Suc 0) x') 1 = Var x'\ by (auto simp: coeff_def minus_mpoly.rep_eq Var_def Var\<^sub>0_def monom_def times_mpoly.rep_eq lookup_minus lookup_times_monomial_right mpoly.MPoly_inverse) then have \\a. \g h. r a = ?v * g + h \ x' \ vars h\ using polynomial_split_on_var[of \r _\ x'] by metis then obtain g h where r: \r a = ?v * g a + h a\ and x'_h: \x' \ vars (h a)\ for a using polynomial_split_on_var[of \r a\ x'] by metis have \?q = ((\a\t'. g a * a) + r (?v^2-?v) * (?v - 1)) * ?v + (\a\t'. h a * a)\ using fin_t notin unfolding t_t' q r by (auto simp: field_simps comm_monoid_add_class.sum.distrib power2_eq_square ideal.scale_left_commute sum_distrib_left) moreover have \x' \ vars ?q\ by (metis (no_types, opaque_lifting) Groups.add_ac(2) Un_iff add_diff_cancel_left' diff_minus_eq_add in_mono leading q'_def semiring_normalization_rules(29) vars_in_right_only vars_mult) moreover { have \x' \ (\m\t' - {?v^2-?v}. vars (h m * m))\ using fin_t x'_h vars_mult[of \h _\] \t \ polynomial_bool\ by (auto simp: polynomial_bool_def t_t' elim!: vars_unE) then have \x' \ vars (\a\t'. h a * a)\ using vars_setsum[of \t'\ \\a. h a * a\] fin_t x'_h t notin by (auto simp: t_t') } ultimately have \?q = (\a\t'. h a * a)\ unfolding mon[symmetric] by (rule polynomial_decomp_alien_var(2)[unfolded]) then show ?thesis using t fin_t \t' \ (\c. Var c ^ 2 - Var c) ` {c. c \ x'}\ unfolding ideal.span_explicit t_t' by auto qed qed have eq1: \More_Modules.ideal (insert p (set_mset A \ polynomial_bool)) = More_Modules.ideal (insert (?v^2 - ?v) ?C)\ (is \More_Modules.ideal _ = More_Modules.ideal (insert _ ?C)\) by (rule arg_cong[of _ _ More_Modules.ideal]) (auto simp: polynomial_bool_def) moreover have \?v^2 - ?v \ More_Modules.ideal ?C\ proof - have \?v - q' \ More_Modules.ideal ?C\ by (auto simp: q_q' ideal.span_base) from ideal.span_scale[OF this, of \?v + q' - 1\] have \(?v - q') * (?v + q' - 1) \ More_Modules.ideal ?C\ by (auto simp: field_simps) moreover have \q'^2 - q' \ More_Modules.ideal ?C\ - using diff by (smt Un_insert_right ideal.span_mono insert_subset subsetD sup_ge2) + using diff by (smt (verit) Un_insert_right ideal.span_mono insert_subset subsetD sup_ge2) ultimately have \(?v - q') * (?v + q' - 1) + (q'^2 - q') \ More_Modules.ideal ?C\ by (rule ideal.span_add) moreover have \?v^2 - ?v = (?v - q') * (?v + q' - 1) + (q'^2 - q')\ by (auto simp: p'_def q_q' field_simps power2_eq_square) ultimately show ?thesis by simp qed ultimately show ?thesis using ideal.span_insert_idI by blast qed have \n < m \ n > 0 \ \q. ?v^n = ?v + q * (?v^2 - ?v)\ for n m :: nat proof (induction m arbitrary: n) case 0 then show ?case by auto next case (Suc m n) note IH = this(1-) consider \n < m\ | \m = n\ \n > 1\ | \n = 1\ using IH by (cases \n < m\; cases n) auto then show ?case proof cases case 1 then show ?thesis using IH by auto next case 2 have eq: \?v^(n) = ((?v :: int mpoly) ^ (n-2)) * (?v^2-?v) + ?v^(n-1)\ using 2 by (auto simp: field_simps power_eq_if ideal.scale_right_diff_distrib) obtain q where q: \?v^(n-1) = ?v + q * (?v^2 - ?v)\ using IH(1)[of \n-1\] 2 by auto show ?thesis using q unfolding eq by (auto intro!: exI[of _ \Var x' ^ (n - 2) + q\] simp: distrib_right) next case 3 then show \?thesis\ by auto qed qed obtain r t where q: \q = (\a\t. r a * a)\ and fin_t: \finite t\ and t: \t \ ?trimmed\ using q unfolding eq unfolding ideal.span_explicit by auto define t' where \t' \ t - {p}\ have t': \t = (if p \ t then insert p t' else t')\ and t''[simp]: \p \ t'\ unfolding t'_def by auto show ?thesis proof (cases \r p = 0 \ p \ t\) case True have q: \q = (\a\t'. r a * a)\ and fin_t: \finite t'\ and t: \t' \ set_mset A \ polynomial_bool\ using q fin_t t True t'' apply (subst (asm) t') apply (auto intro: sum.cong simp: sum.insert_remove t'_def) using q fin_t t True t'' apply (auto intro: sum.cong simp: sum.insert_remove t'_def polynomial_bool_def) done then show ?thesis by (auto simp: ideal.span_explicit) next case False then have \r p \ 0\ and \p \ t\ by auto then have t: \t = insert p t'\ by (auto simp: t'_def) have \x' \ vars (- p')\ using leading p'_def vars_in_right_only by fastforce have mon: \monom (monomial (Suc 0) x') 1 = Var x'\ by (auto simp:coeff_def minus_mpoly.rep_eq Var_def Var\<^sub>0_def monom_def times_mpoly.rep_eq lookup_minus lookup_times_monomial_right mpoly.MPoly_inverse) then have \\a. \g h. r a = (?v + p') * g + h \ x' \ vars h\ using polynomial_split_on_var2[of x' \-p'\ \r _\] \x' \ vars (- p')\ by (metis diff_minus_eq_add) then obtain g h where r: \r a = p * g a + h a\ and x'_h: \x' \ vars (h a)\ for a using polynomial_split_on_var2[of x' p' \r a\] unfolding p_p'[symmetric] by metis have ISABLLE_come_on: \a * (p * g a) = p * (a * g a)\ for a by auto have q1: \q = p * (\a\t'. g a * a) + (\a\t'. h a * a) + p * r p\ (is \_ = _ + ?NOx' + _\) using fin_t t'' unfolding q t ISABLLE_come_on r apply (subst semiring_class.distrib_right)+ apply (auto simp: comm_monoid_add_class.sum.distrib semigroup_mult_class.mult.assoc ISABLLE_come_on simp flip: semiring_0_class.sum_distrib_right semiring_0_class.sum_distrib_left) by (auto simp: field_simps) also have \... = ((\a\t'. g a * a) + r p) * p + (\a\t'. h a * a)\ by (auto simp: field_simps) finally have q_decomp: \q = ((\a\t'. g a * a) + r p) * p + (\a\t'. h a * a)\ (is \q = ?X * p + ?NOx'\). have [iff]: \monomial (Suc 0) c = 0 - monomial (Suc 0) c = False\ for c by (metis One_nat_def diff_is_0_eq' le_eq_less_or_eq less_Suc_eq_le monomial_0_iff single_diff zero_neq_one) have \x \ t' \ x' \ vars x \ False\ for x using \t \ ?trimmed\ t assms(2,3) apply (auto simp: polynomial_bool_def dest!: multi_member_split) apply (frule set_rev_mp) apply assumption apply (auto dest!: multi_member_split) done then have \x' \ (\m\t'. vars (h m * m))\ using fin_t x'_h vars_mult[of \h _\] by (auto simp: t elim!: vars_unE) then have \x' \ vars ?NOx'\ using vars_setsum[of \t'\ \\a. h a * a\] fin_t x'_h by (auto simp: t) moreover { have \x' \ vars p'\ using assms(7) unfolding p'_def by auto then have \x' \ vars (h p * p')\ using vars_mult[of \h p\ p'] x'_h by auto } ultimately have \x' \ vars q\ \x' \ vars ?NOx'\ \x' \ vars p'\ using x' vars_q vars_add[of \h p * p'\ \\a\t'. h a * a\] x'_h leading p'_def by auto then have \?X = 0\ and q_decomp: \q = ?NOx'\ unfolding mon[symmetric] p_p' using polynomial_decomp_alien_var2[OF q_decomp[unfolded p_p' mon[symmetric]]] by auto then have \r p = (\a\t'. (- g a) * a)\ (is \_ = ?CL\) unfolding add.assoc add_eq_0_iff equation_minus_iff by (auto simp: sum_negf ac_simps) then have q2: \q = (\a\t'. a * (r a - p * g a))\ using fin_t unfolding q apply (auto simp: t r q comm_monoid_add_class.sum.distrib[symmetric] sum_distrib_left sum_distrib_right left_diff_distrib intro!: sum.cong) apply (auto simp: field_simps) done then show \?thesis\ using t fin_t \t \ ?trimmed\ unfolding ideal.span_explicit by (auto intro!: exI[of _ t'] exI[of _ \\a. r a - p * g a\] simp: field_simps polynomial_bool_def) qed qed lemma extensions_are_safe_uminus: assumes \x' \ vars p\ and x': \x' \ \\ and \\ (vars ` set_mset A) \ \\ and p_x_coeff: \coeff p (monomial (Suc 0) x') = -1\ and vars_q: \vars q \ \\ and q: \q \ More_Modules.ideal (insert p (set_mset A \ polynomial_bool))\ and leading: \x' \ vars (p + Var x')\ and diff: \(Var x' + p)^2 - (Var x' + p) \ More_Modules.ideal polynomial_bool\ shows \q \ More_Modules.ideal (set_mset A \ polynomial_bool)\ proof - have \q \ More_Modules.ideal (insert (- p) (set_mset A \ polynomial_bool))\ by (metis ideal.span_breakdown_eq minus_mult_minus q) then show ?thesis using extensions_are_safe[of x' \-p\ \ A q] assms using vars_in_right_only by force qed text \This is the correctness theorem of a PAC step: no polynomials are added to the ideal.\ lemma vars_subst_in_left_only: \x \ vars p \ x \ vars (p - Var x)\ for p :: \int mpoly\ by (metis One_nat_def Var.abs_eq Var\<^sub>0_def group_eq_aux monom.abs_eq mult_numeral_1 polynomial_decomp_alien_var(1) zero_neq_numeral) lemma vars_subst_in_left_only_diff_iff: fixes p :: \int mpoly\ assumes \x \ vars p\ shows \vars (p - Var x) = insert x (vars p)\ proof - have \\xa. x \ vars p \ xa \ vars (p - Var x) \ xa \ vars p \ xa = x\ by (metis (no_types, opaque_lifting) diff_0_right diff_minus_eq_add empty_iff in_vars_addE insert_iff keys_single minus_diff_eq monom_one mult.right_neutral one_neq_zero single_zero vars_monom_keys vars_mult_Var vars_uminus) moreover have \\xa. x \ vars p \ xa \ vars p \ xa \ vars (p - Var x)\ by (metis add.inverse_inverse diff_minus_eq_add empty_iff insert_iff keys_single minus_diff_eq monom_one mult.right_neutral one_neq_zero single_zero vars_in_right_only vars_monom_keys vars_mult_Var vars_uminus) ultimately show ?thesis using assms by (auto simp: vars_subst_in_left_only) qed lemma vars_subst_in_left_only_iff: \x \ vars p \ vars (p + Var x) = insert x (vars p)\ for p :: \int mpoly\ using vars_subst_in_left_only_diff_iff[of x \-p\] by (metis diff_0 diff_diff_add vars_uminus) lemma coeff_add_right_notin: \x \ vars p \ MPoly_Type.coeff (Var x - p) (monomial (Suc 0) x) = 1\ apply (auto simp flip: coeff_minus simp: not_in_vars_coeff0) by (simp add: MPoly_Type.coeff_def Var.rep_eq Var\<^sub>0_def) lemma coeff_add_left_notin: \x \ vars p \ MPoly_Type.coeff (p - Var x) (monomial (Suc 0) x) = -1\ for p :: \int mpoly\ apply (auto simp flip: coeff_minus simp: not_in_vars_coeff0) by (simp add: MPoly_Type.coeff_def Var.rep_eq Var\<^sub>0_def) lemma ideal_insert_polynomial_bool_swap: \r - s \ ideal polynomial_bool \ More_Modules.ideal (insert r (A \ polynomial_bool)) = More_Modules.ideal (insert s (A \ polynomial_bool))\ apply auto using ideal.eq_span_insert_eq ideal.span_mono sup_ge2 apply blast+ done lemma PAC_Format_subset_ideal: \PAC_Format (\, A) (\', B) \ \(vars ` set_mset A) \ \ \ restricted_ideal_to\<^sub>I \ B \ restricted_ideal_to\<^sub>I \ A \ \ \ \' \ \(vars ` set_mset B) \ \'\ unfolding restricted_ideal_to_def apply (induction rule:PAC_Format_induct) subgoal for p q pq A \ using vars_add by (force simp: ideal.span_add_eq ideal.span_base pac_ideal_insert_already_in[OF diff_in_polynomial_bool_pac_idealI[of \p + q\ \_\ pq]] pac_ideal_add intro!: diff_in_polynomial_bool_pac_idealI[of \p + q\ \_\ pq]) subgoal for p q pq using vars_mult[of p q] by (force simp: ideal.span_add_eq ideal.span_base pac_ideal_mult pac_ideal_insert_already_in[OF diff_in_polynomial_bool_pac_idealI[of \p*q\ \_\ pq]]) subgoal for p A using pac_ideal_mono[of \set_mset (A - {#p#})\ \set_mset A\] by (auto dest: in_diffD) subgoal for p x' r' apply (subgoal_tac \x' \ vars p\) using extensions_are_safe_uminus[of x' \-Var x' + p\ \ A] unfolding pac_ideal_def apply (auto simp: vars_subst_in_left_only coeff_add_left_notin) done done text \ In general, if deletions are disallowed, then the stronger \<^term>\B = pac_ideal A\ holds. \ lemma restricted_ideal_to_restricted_ideal_to\<^sub>ID: \restricted_ideal_to \ (set_mset A) \ restricted_ideal_to\<^sub>I \ A\ by (auto simp add: Collect_disj_eq pac_idealI1 restricted_ideal_to_def) lemma rtranclp_PAC_Format_subset_ideal: \rtranclp PAC_Format (\, A) (\', B) \ \(vars ` set_mset A) \ \ \ restricted_ideal_to\<^sub>I \ B \ restricted_ideal_to\<^sub>I \ A \ \ \ \' \ \(vars ` set_mset B) \ \'\ apply (induction rule:rtranclp_induct[of PAC_Format \(_, _)\ \(_, _)\, split_format(complete)]) subgoal by (simp add: restricted_ideal_to_restricted_ideal_to\<^sub>ID) subgoal by (drule PAC_Format_subset_ideal) (auto simp: restricted_ideal_to_def Collect_mono_iff) done end \ No newline at end of file diff --git a/thys/PAC_Checker/WB_Sort.thy b/thys/PAC_Checker/WB_Sort.thy --- a/thys/PAC_Checker/WB_Sort.thy +++ b/thys/PAC_Checker/WB_Sort.thy @@ -1,1688 +1,1688 @@ (* File: WB_Sort.thy Author: Mathias Fleury, Daniela Kaufmann, JKU Author: Maximilian Wuttke, Saarland University Maintainer: Mathias Fleury, JKU Correctness proof contributed by Maximilian Wuttke *) theory WB_Sort imports Refine_Imperative_HOL.IICF "HOL-Library.Rewrite" Nested_Multisets_Ordinals.Duplicate_Free_Multiset begin text \This a complete copy-paste of the IsaFoL version because sharing is too hard.\ text \Every element between \<^term>\lo\ and \<^term>\hi\ can be chosen as pivot element.\ definition choose_pivot :: \('b \ 'b \ bool) \ ('a \ 'b) \ 'a list \ nat \ nat \ nat nres\ where \choose_pivot _ _ _ lo hi = SPEC(\k. k \ lo \ k \ hi)\ text \The element at index \p\ partitions the subarray \lo..hi\. This means that every element \ definition isPartition_wrt :: \('b \ 'b \ bool) \ 'b list \ nat \ nat \ nat \ bool\ where \isPartition_wrt R xs lo hi p \ (\ i. i \ lo \ i < p \ R (xs!i) (xs!p)) \ (\ j. j > p \ j \ hi \ R (xs!p) (xs!j))\ lemma isPartition_wrtI: \(\ i. \i \ lo; i < p\ \ R (xs!i) (xs!p)) \ (\ j. \j > p; j \ hi\ \ R (xs!p) (xs!j)) \ isPartition_wrt R xs lo hi p\ by (simp add: isPartition_wrt_def) definition isPartition :: \'a :: order list \ nat \ nat \ nat \ bool\ where \isPartition xs lo hi p \ isPartition_wrt (\) xs lo hi p\ abbreviation isPartition_map :: \('b \ 'b \ bool) \ ('a \ 'b) \ 'a list \ nat \ nat \ nat \ bool\ where \isPartition_map R h xs i j k \ isPartition_wrt (\a b. R (h a) (h b)) xs i j k\ lemma isPartition_map_def': \lo \ p \ p \ hi \ hi < length xs \ isPartition_map R h xs lo hi p = isPartition_wrt R (map h xs) lo hi p\ by (auto simp add: isPartition_wrt_def conjI) text \Example: 6 is the pivot element (with index 4); \<^term>\7\ is equal to the \<^term>\length xs - 1\.\ lemma \isPartition [0,5,3,4,6,9,8,10::nat] 0 7 4\ by (auto simp add: isPartition_def isPartition_wrt_def nth_Cons') definition sublist :: \'a list \ nat \ nat \ 'a list\ where \sublist xs i j \ take (Suc j - i) (drop i xs)\ (*take from HashMap *) lemma take_Suc0: "l\[] \ take (Suc 0) l = [l!0]" "0 < length l \ take (Suc 0) l = [l!0]" "Suc n \ length l \ take (Suc 0) l = [l!0]" by (cases l, auto)+ lemma sublist_single: \i < length xs \ sublist xs i i = [xs!i]\ by (cases xs) (auto simp add: sublist_def take_Suc0) lemma insert_eq: \insert a b = b \ {a}\ by auto lemma sublist_nth: \\lo \ hi; hi < length xs; k+lo \ hi\ \ (sublist xs lo hi)!k = xs!(lo+k)\ by (simp add: sublist_def) lemma sublist_length: \\i \ j; j < length xs\ \ length (sublist xs i j) = 1 + j - i\ by (simp add: sublist_def) lemma sublist_not_empty: \\i \ j; j < length xs; xs \ []\ \ sublist xs i j \ []\ apply simp apply (rewrite List.length_greater_0_conv[symmetric]) apply (rewrite sublist_length) by auto lemma sublist_app: \\i1 \ i2; i2 \ i3\ \ sublist xs i1 i2 @ sublist xs (Suc i2) i3 = sublist xs i1 i3\ unfolding sublist_def - by (smt Suc_eq_plus1_left Suc_le_mono append.assoc le_SucI le_add_diff_inverse le_trans same_append_eq take_add) + by (smt (verit) Suc_eq_plus1_left Suc_le_mono append.assoc le_SucI le_add_diff_inverse le_trans same_append_eq take_add) definition sorted_sublist_wrt :: \('b \ 'b \ bool) \ 'b list \ nat \ nat \ bool\ where \sorted_sublist_wrt R xs lo hi = sorted_wrt R (sublist xs lo hi)\ definition sorted_sublist :: \'a :: linorder list \ nat \ nat \ bool\ where \sorted_sublist xs lo hi = sorted_sublist_wrt (\) xs lo hi\ abbreviation sorted_sublist_map :: \('b \ 'b \ bool) \ ('a \ 'b) \ 'a list \ nat \ nat \ bool\ where \sorted_sublist_map R h xs lo hi \ sorted_sublist_wrt (\a b. R (h a) (h b)) xs lo hi\ lemma sorted_sublist_map_def': \lo < length xs \ sorted_sublist_map R h xs lo hi \ sorted_sublist_wrt R (map h xs) lo hi\ apply (simp add: sorted_sublist_wrt_def) by (simp add: drop_map sorted_wrt_map sublist_def take_map) lemma sorted_sublist_wrt_refl: \i < length xs \ sorted_sublist_wrt R xs i i\ by (auto simp add: sorted_sublist_wrt_def sublist_single) lemma sorted_sublist_refl: \i < length xs \ sorted_sublist xs i i\ by (auto simp add: sorted_sublist_def sorted_sublist_wrt_refl) lemma sublist_map: \sublist (map f xs) i j = map f (sublist xs i j)\ apply (auto simp add: sublist_def) by (simp add: drop_map take_map) lemma take_set: \j \ length xs \ x \ set (take j xs) \ (\ k. k < j \ xs!k = x)\ by (rule eq_reflection) (auto simp add: take_set) lemma drop_set: \j \ length xs \ x \ set (drop j xs) \ (\k. j\k\k xs!k=x)\ - by (smt Misc.in_set_drop_conv_nth) (* lemma found by sledgehammer *) + by (smt (verit) Misc.in_set_drop_conv_nth) (* lemma found by sledgehammer *) lemma sublist_el: \i \ j \ j < length xs \ x \ set (sublist xs i j) \ (\ k. k < Suc j-i \ xs!(i+k)=x)\ by (auto simp add: take_set sublist_def) lemma sublist_el': \i \ j \ j < length xs \ x \ set (sublist xs i j) \ (\ k. i\k\k\j \ xs!k=x)\ apply (subst sublist_el, assumption, assumption) - by (smt Groups.add_ac(2) le_add1 le_add_diff_inverse less_Suc_eq less_diff_conv nat_less_le order_refl) + by (smt (verit) Groups.add_ac(2) le_add1 le_add_diff_inverse less_Suc_eq less_diff_conv nat_less_le order_refl) lemma sublist_lt: \hi < lo \ sublist xs lo hi = []\ by (auto simp add: sublist_def) lemma nat_le_eq_or_lt: \(a :: nat) \ b = (a = b \ a < b)\ by linarith lemma sorted_sublist_wrt_le: \hi \ lo \ hi < length xs \ sorted_sublist_wrt R xs lo hi\ apply (auto simp add: nat_le_eq_or_lt) unfolding sorted_sublist_wrt_def subgoal apply (rewrite sublist_single) by auto subgoal by (auto simp add: sublist_lt) done text \Elements in a sorted sublists are actually sorted\ lemma sorted_sublist_wrt_nth_le: assumes \sorted_sublist_wrt R xs lo hi\ and \lo \ hi\ and \hi < length xs\ and \lo \ i\ and \i < j\ and \j \ hi\ shows \R (xs!i) (xs!j)\ proof - have A: \lo < length xs\ using assms(2) assms(3) by linarith obtain i' where I: \i = lo + i'\ using assms(4) le_Suc_ex by auto obtain j' where J: \j = lo + j'\ by (meson assms(4) assms(5) dual_order.trans le_iff_add less_imp_le_nat) show ?thesis using assms(1) apply (simp add: sorted_sublist_wrt_def I J) apply (rewrite sublist_nth[symmetric, where k=i', where lo=lo, where hi=hi]) using assms apply auto subgoal using I by linarith apply (rewrite sublist_nth[symmetric, where k=j', where lo=lo, where hi=hi]) using assms apply auto subgoal using J by linarith apply (rule sorted_wrt_nth_less) apply auto subgoal using I J nat_add_left_cancel_less by blast subgoal apply (simp add: sublist_length) using J by linarith done qed text \We can make the assumption \<^term>\i < j\ weaker if we have a reflexivie relation.\ lemma sorted_sublist_wrt_nth_le': assumes ref: \\ x. R x x\ and \sorted_sublist_wrt R xs lo hi\ and \lo \ hi\ and \hi < length xs\ and \lo \ i\ and \i \ j\ and \j \ hi\ shows \R (xs!i) (xs!j)\ proof - have \i < j \ i = j\ using \i \ j\ by linarith then consider (a) \i < j\ | (b) \i = j\ by blast then show ?thesis proof cases case a then show ?thesis using assms(2-5,7) sorted_sublist_wrt_nth_le by blast next case b then show ?thesis by (simp add: ref) qed qed (* lemma sorted_sublist_map_nth_le: assumes \sorted_sublist_map R h xs lo hi\ and \lo \ hi\ and \hi < length xs\ and \lo \ i\ and \i < j\ and \j \ hi\ shows \R (h (xs!i)) (h (xs!j))\ proof - show ?thesis using assms by (rule sorted_sublist_wrt_nth_le) qed *) lemma sorted_sublist_le: \hi \ lo \ hi < length xs \ sorted_sublist xs lo hi\ by (auto simp add: sorted_sublist_def sorted_sublist_wrt_le) lemma sorted_sublist_map_le: \hi \ lo \ hi < length xs \ sorted_sublist_map R h xs lo hi\ by (auto simp add: sorted_sublist_wrt_le) lemma sublist_cons: \lo < hi \ hi < length xs \ sublist xs lo hi = xs!lo # sublist xs (Suc lo) hi\ by (metis Cons_eq_appendI append_self_conv2 less_imp_le_nat less_or_eq_imp_le less_trans sublist_app sublist_single) lemma sorted_sublist_wrt_cons': \sorted_sublist_wrt R xs (lo+1) hi \ lo \ hi \ hi < length xs \ (\j. loj\hi \ R (xs!lo) (xs!j)) \ sorted_sublist_wrt R xs lo hi\ apply (auto simp add: nat_le_eq_or_lt sorted_sublist_wrt_def) apply (auto 5 4 simp add: sublist_cons sublist_el less_diff_conv add.commute[of _ lo] dest: Suc_lessI sublist_single) done lemma sorted_sublist_wrt_cons: assumes trans: \(\ x y z. \R x y; R y z\ \ R x z)\ and \sorted_sublist_wrt R xs (lo+1) hi\ and \lo \ hi\ and \hi < length xs \ and \R (xs!lo) (xs!(lo+1))\ shows \sorted_sublist_wrt R xs lo hi\ proof - show ?thesis apply (rule sorted_sublist_wrt_cons') using assms apply auto subgoal premises assms' for j proof - have A: \j=lo+1 \ j>lo+1\ using assms'(5) by linarith show ?thesis using A proof assume A: \j=lo+1\ show ?thesis by (simp add: A assms') next assume A: \j>lo+1\ show ?thesis apply (rule trans) apply (rule assms(5)) apply (rule sorted_sublist_wrt_nth_le[OF assms(2), where i=\lo+1\, where j=j]) subgoal using A assms'(6) by linarith subgoal using assms'(3) less_imp_diff_less by blast subgoal using assms'(5) by auto subgoal using A by linarith subgoal by (simp add: assms'(6)) done qed qed done qed lemma sorted_sublist_map_cons: \(\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)) \ sorted_sublist_map R h xs (lo+1) hi \ lo \ hi \ hi < length xs \ R (h (xs!lo)) (h (xs!(lo+1))) \ sorted_sublist_map R h xs lo hi\ by (blast intro: sorted_sublist_wrt_cons) lemma sublist_snoc: \lo < hi \ hi < length xs \ sublist xs lo hi = sublist xs lo (hi-1) @ [xs!hi]\ apply (simp add: sublist_def) proof - assume a1: "lo < hi" assume "hi < length xs" then have "take lo xs @ take (Suc hi - lo) (drop lo xs) = (take lo xs @ take (hi - lo) (drop lo xs)) @ [xs ! hi]" using a1 by (metis (no_types) Suc_diff_le add_Suc_right hd_drop_conv_nth le_add_diff_inverse less_imp_le_nat take_add take_hd_drop) then show "take (Suc hi - lo) (drop lo xs) = take (hi - lo) (drop lo xs) @ [xs ! hi]" by simp qed lemma sorted_sublist_wrt_snoc': \sorted_sublist_wrt R xs lo (hi-1) \ lo \ hi \ hi < length xs \ (\j. lo\j\j R (xs!j) (xs!hi)) \ sorted_sublist_wrt R xs lo hi\ apply (simp add: sorted_sublist_wrt_def) apply (auto simp add: nat_le_eq_or_lt) subgoal by (simp add: sublist_single) by (auto simp add: sublist_snoc sublist_el sorted_wrt_append add.commute[of lo] less_diff_conv simp: leI simp flip:nat_le_eq_or_lt) lemma sorted_sublist_wrt_snoc: assumes trans: \(\ x y z. \R x y; R y z\ \ R x z)\ and \sorted_sublist_wrt R xs lo (hi-1)\ and \lo \ hi\ and \hi < length xs\ and \(R (xs!(hi-1)) (xs!hi))\ shows \sorted_sublist_wrt R xs lo hi\ proof - show ?thesis apply (rule sorted_sublist_wrt_snoc') using assms apply auto subgoal premises assms' for j proof - have A: \j=hi-1 \ j using assms'(6) by linarith show ?thesis using A proof assume A: \j=hi-1\ show ?thesis by (simp add: A assms') next assume A: \j show ?thesis apply (rule trans) apply (rule sorted_sublist_wrt_nth_le[OF assms(2), where i=j, where j=\hi-1\]) prefer 6 apply (rule assms(5)) apply auto subgoal using A assms'(5) by linarith subgoal using assms'(3) less_imp_diff_less by blast subgoal using assms'(5) by auto subgoal using A by linarith done qed qed done qed lemma sublist_split: \lo \ hi \ lo < p \ p < hi \ hi < length xs \ sublist xs lo p @ sublist xs (p+1) hi = sublist xs lo hi\ by (simp add: sublist_app) lemma sublist_split_part: \lo \ hi \ lo < p \ p < hi \ hi < length xs \ sublist xs lo (p-1) @ xs!p # sublist xs (p+1) hi = sublist xs lo hi\ by (auto simp add: sublist_split[symmetric] sublist_snoc[where xs=xs,where lo=lo,where hi=p]) text \A property for partitions (we always assume that \<^term>\R\ is transitive.\ lemma isPartition_wrt_trans: \(\ x y z. \R x y; R y z\ \ R x z) \ isPartition_wrt R xs lo hi p \ (\i j. lo \ i \ i < p \ p < j \ j \ hi \ R (xs!i) (xs!j))\ by (auto simp add: isPartition_wrt_def) lemma isPartition_map_trans: \(\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)) \ hi < length xs \ isPartition_map R h xs lo hi p \ (\i j. lo \ i \ i < p \ p < j \ j \ hi \ R (h (xs!i)) (h (xs!j)))\ by (auto simp add: isPartition_wrt_def) lemma merge_sorted_wrt_partitions_between': \lo \ hi \ lo < p \ p < hi \ hi < length xs \ isPartition_wrt R xs lo hi p \ sorted_sublist_wrt R xs lo (p-1) \ sorted_sublist_wrt R xs (p+1) hi \ (\i j. lo \ i \ i < p \ p < j \ j \ hi \ R (xs!i) (xs!j)) \ sorted_sublist_wrt R xs lo hi\ apply (auto simp add: isPartition_def isPartition_wrt_def sorted_sublist_def sorted_sublist_wrt_def sublist_map) apply (simp add: sublist_split_part[symmetric]) apply (auto simp add: List.sorted_wrt_append) subgoal by (auto simp add: sublist_el) subgoal by (auto simp add: sublist_el) subgoal by (auto simp add: sublist_el') done lemma merge_sorted_wrt_partitions_between: \(\ x y z. \R x y; R y z\ \ R x z) \ isPartition_wrt R xs lo hi p \ sorted_sublist_wrt R xs lo (p-1) \ sorted_sublist_wrt R xs (p+1) hi \ lo \ hi \ hi < length xs \ lo < p \ p < hi \ hi < length xs \ sorted_sublist_wrt R xs lo hi\ by (simp add: merge_sorted_wrt_partitions_between' isPartition_wrt_trans) (* lemma merge_sorted_map_partitions_between: \(\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)) \ isPartition_map R h xs lo hi p \ sorted_sublist_map R h xs lo (p-1) \ sorted_sublist_map R h xs (p+1) hi \ lo \ hi \ hi < length xs \ lo < p \ p < hi \ hi < length xs \ sorted_sublist_map R h xs lo hi\ by (simp add: merge_sorted_wrt_partitions_between' isPartition_map_trans) *) text \The main theorem to merge sorted lists\ lemma merge_sorted_wrt_partitions: \isPartition_wrt R xs lo hi p \ sorted_sublist_wrt R xs lo (p - Suc 0) \ sorted_sublist_wrt R xs (Suc p) hi \ lo \ hi \ lo \ p \ p \ hi \ hi < length xs \ (\i j. lo \ i \ i < p \ p < j \ j \ hi \ R (xs!i) (xs!j)) \ sorted_sublist_wrt R xs lo hi\ subgoal premises assms proof - have C: \lo=p\p=hi \ lo=p\p lop=hi \ lop using assms by linarith show ?thesis using C apply auto subgoal \ \lo=p=hi\ apply (rule sorted_sublist_wrt_refl) using assms by auto subgoal \ \lo=p using assms by (simp add: isPartition_def isPartition_wrt_def sorted_sublist_wrt_cons') subgoal \ \lo using assms by (simp add: isPartition_def isPartition_wrt_def sorted_sublist_wrt_snoc') subgoal \ \lo using assms apply (rewrite merge_sorted_wrt_partitions_between'[where p=p]) by auto done qed done theorem merge_sorted_map_partitions: \(\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)) \ isPartition_map R h xs lo hi p \ sorted_sublist_map R h xs lo (p - Suc 0) \ sorted_sublist_map R h xs (Suc p) hi \ lo \ hi \ lo \ p \ p \ hi \ hi < length xs \ sorted_sublist_map R h xs lo hi\ apply (rule merge_sorted_wrt_partitions) apply auto by (simp add: merge_sorted_wrt_partitions isPartition_map_trans) lemma partition_wrt_extend: \isPartition_wrt R xs lo' hi' p \ hi < length xs \ lo \ lo' \ lo' \ hi \ hi' \ hi \ lo' \ p \ p \ hi' \ (\ i. lo\i \ i R (xs!i) (xs!p)) \ (\ j. hi' j\hi \ R (xs!p) (xs!j)) \ isPartition_wrt R xs lo hi p\ unfolding isPartition_wrt_def apply (intro conjI) subgoal by (force simp: not_le) subgoal using leI by blast done lemma partition_map_extend: \isPartition_map R h xs lo' hi' p \ hi < length xs \ lo \ lo' \ lo' \ hi \ hi' \ hi \ lo' \ p \ p \ hi' \ (\ i. lo\i \ i R (h (xs!i)) (h (xs!p))) \ (\ j. hi' j\hi \ R (h (xs!p)) (h (xs!j))) \ isPartition_map R h xs lo hi p\ by (auto simp add: partition_wrt_extend) lemma isPartition_empty: \(\ j. \lo < j; j \ hi\ \ R (xs ! lo) (xs ! j)) \ isPartition_wrt R xs lo hi lo\ by (auto simp add: isPartition_wrt_def) lemma take_ext: \(\i k < length xs \ k < length xs' \ take k xs' = take k xs\ by (simp add: nth_take_lemma) lemma drop_ext': \(\i. i\k \ i xs'!i=xs!i) \ 0 xs\[] \ \ \These corner cases will be dealt with in the next lemma\ length xs'=length xs \ drop k xs' = drop k xs\ apply (rewrite in \drop _ \ = _\ List.rev_rev_ident[symmetric]) apply (rewrite in \_ = drop _ \\ List.rev_rev_ident[symmetric]) apply (rewrite in \\ = _\ List.drop_rev) apply (rewrite in \_ = \\ List.drop_rev) apply simp apply (rule take_ext) by (auto simp add: rev_nth) lemma drop_ext: \(\i. i\k \ i xs'!i=xs!i) \ length xs'=length xs \ drop k xs' = drop k xs\ apply (cases xs) apply auto apply (cases k) subgoal by (simp add: nth_equalityI) subgoal apply (rule drop_ext') by auto done lemma sublist_ext': \(\i. lo\i\i\hi \ xs'!i=xs!i) \ length xs' = length xs \ lo \ hi \ Suc hi < length xs \ sublist xs' lo hi = sublist xs lo hi\ apply (simp add: sublist_def) apply (rule take_ext) by auto lemma lt_Suc: \(a < b) = (Suc a = b \ Suc a < b)\ by auto lemma sublist_until_end_eq_drop: \Suc hi = length xs \ sublist xs lo hi = drop lo xs\ by (simp add: sublist_def) lemma sublist_ext: \(\i. lo\i\i\hi \ xs'!i=xs!i) \ length xs' = length xs \ lo \ hi \ hi < length xs \ sublist xs' lo hi = sublist xs lo hi\ apply (auto simp add: lt_Suc[where a=hi]) subgoal by (auto simp add: sublist_until_end_eq_drop drop_ext) subgoal by (auto simp add: sublist_ext') done lemma sorted_wrt_lower_sublist_still_sorted: assumes \sorted_sublist_wrt R xs lo (lo' - Suc 0)\ and \lo \ lo'\ and \lo' < length xs\ and \(\ i. lo\i\i xs'!i=xs!i)\ and \length xs' = length xs\ shows \sorted_sublist_wrt R xs' lo (lo' - Suc 0)\ proof - have l: \lo < lo' - 1 \ lo \ lo'-1\ by linarith show ?thesis using l apply auto subgoal \ \lo < lo' - 1\ apply (auto simp add: sorted_sublist_wrt_def) apply (rewrite sublist_ext[where xs=xs]) using assms by (auto simp add: sorted_sublist_wrt_def) subgoal \ \lo >= lo' - 1\ using assms by (auto simp add: sorted_sublist_wrt_le) done qed lemma sorted_map_lower_sublist_still_sorted: assumes \sorted_sublist_map R h xs lo (lo' - Suc 0)\ and \lo \ lo'\ and \lo' < length xs\ and \(\ i. lo\i\i xs'!i=xs!i)\ and \length xs' = length xs\ shows \sorted_sublist_map R h xs' lo (lo' - Suc 0)\ using assms by (rule sorted_wrt_lower_sublist_still_sorted) lemma sorted_wrt_upper_sublist_still_sorted: assumes \sorted_sublist_wrt R xs (hi'+1) hi\ and \lo \ lo'\ and \hi < length xs\ and \\ j. hi'j\hi \ xs'!j=xs!j\ and \length xs' = length xs\ shows \sorted_sublist_wrt R xs' (hi'+1) hi\ proof - have l: \hi' + 1 < hi \ hi' + 1 \ hi\ by linarith show ?thesis using l apply auto subgoal \ \hi' + 1 < h\ apply (auto simp add: sorted_sublist_wrt_def) apply (rewrite sublist_ext[where xs=xs]) using assms by (auto simp add: sorted_sublist_wrt_def) subgoal \ \\<^term>\hi' + 1 \ hi\\ using assms by (auto simp add: sorted_sublist_wrt_le) done qed lemma sorted_map_upper_sublist_still_sorted: assumes \sorted_sublist_map R h xs (hi'+1) hi\ and \lo \ lo'\ and \hi < length xs\ and \\ j. hi'j\hi \ xs'!j=xs!j\ and \length xs' = length xs\ shows \sorted_sublist_map R h xs' (hi'+1) hi\ using assms by (rule sorted_wrt_upper_sublist_still_sorted) text \The specification of the partition function\ definition partition_spec :: \('b \ 'b \ bool) \ ('a \ 'b) \ 'a list \ nat \ nat \ 'a list \ nat \ bool\ where \partition_spec R h xs lo hi xs' p \ mset xs' = mset xs \ \ \The list is a permutation\ isPartition_map R h xs' lo hi p \ \ \We have a valid partition on the resulting list\ lo \ p \ p \ hi \ \ \The partition index is in bounds\ (\ i. i xs'!i=xs!i) \ (\ i. hii xs'!i=xs!i)\ \ \Everything else is unchanged.\ lemma in_set_take_conv_nth: \x \ set (take n xs) \ (\m by (metis in_set_conv_nth length_take min.commute min.strict_boundedE nth_take) lemma mset_drop_upto: \mset (drop a N) = {#N!i. i \# mset_set {a.. proof (induction N arbitrary: a) case Nil then show ?case by simp next case (Cons c N) have upt: \{0.. by auto then have H: \mset_set {0.. unfolding upt by auto have mset_case_Suc: \{#case x of 0 \ c | Suc x \ N ! x . x \# mset_set {Suc a..# mset_set {Suc a.. for a b by (rule image_mset_cong) (auto split: nat.splits) have Suc_Suc: \{Suc a.. for a b by auto then have mset_set_Suc_Suc: \mset_set {Suc a..# mset_set {a.. for a b unfolding Suc_Suc by (subst image_mset_mset_set[symmetric]) auto have *: \{#N ! (x-Suc 0) . x \# mset_set {Suc a..# mset_set {a.. for a b by (auto simp add: mset_set_Suc_Suc multiset.map_comp comp_def) show ?case apply (cases a) using Cons[of 0] Cons by (auto simp: nth_Cons drop_Cons H mset_case_Suc *) qed (* Actually, I only need that \set (sublist xs' lo hi) = set (sublist xs lo hi)\ *) lemma mathias: assumes Perm: \mset xs' = mset xs\ and I: \lo\i\ \i\hi\ \xs'!i=x\ and Bounds: \hi < length xs\ and Fix: \\ i. i xs'!i = xs!i\ \\ j. \hi \ xs'!j = xs!j\ shows \\j. lo\j\j\hi \ xs!j = x\ proof - define xs1 xs2 xs3 xs1' xs2' xs3' where \xs1 = take lo xs\ and \xs2 = take (Suc hi - lo) (drop lo xs)\ and \xs3 = drop (Suc hi) xs\ and \xs1' = take lo xs'\ and \xs2' = take (Suc hi - lo) (drop lo xs')\ and \xs3' = drop (Suc hi) xs'\ have [simp]: \length xs' = length xs\ using Perm by (auto dest: mset_eq_length) have [simp]: \mset xs1 = mset xs1'\ using Fix(1) unfolding xs1_def xs1'_def by (metis Perm le_cases mset_eq_length nth_take_lemma take_all) have [simp]: \mset xs3 = mset xs3'\ using Fix(2) unfolding xs3_def xs3'_def mset_drop_upto by (auto intro: image_mset_cong) have \xs = xs1 @ xs2 @ xs3\ \xs' = xs1' @ xs2' @ xs3'\ using I unfolding xs1_def xs2_def xs3_def xs1'_def xs2'_def xs3'_def by (metis append.assoc append_take_drop_id le_SucI le_add_diff_inverse order_trans take_add)+ moreover have \xs ! i = xs2 ! (i - lo)\ \i \ length xs1\ using I Bounds unfolding xs2_def xs1_def by (auto simp: nth_take min_def) moreover have \x \ set xs2'\ using I Bounds unfolding xs2'_def by (auto simp: in_set_take_conv_nth intro!: exI[of _ \i - lo\]) ultimately have \x \ set xs2\ using Perm I by (auto dest: mset_eq_setD) then obtain j where \xs ! (lo + j) = x\ \j \ hi - lo\ unfolding in_set_conv_nth xs2_def by auto then show ?thesis using Bounds I by (auto intro: exI[of _ \lo+j\]) qed text \If we fix the left and right rest of two permutated lists, then the sublists are also permutations.\ text \But we only need that the sets are equal.\ lemma mset_sublist_incl: assumes Perm: \mset xs' = mset xs\ and Fix: \\ i. i xs'!i = xs!i\ \\ j. \hi \ xs'!j = xs!j\ and bounds: \lo \ hi\ \hi < length xs\ shows \set (sublist xs' lo hi) \ set (sublist xs lo hi)\ proof fix x assume \x \ set (sublist xs' lo hi)\ then have \\i. lo\i\i\hi \ xs'!i=x\ by (metis assms(1) bounds(1) bounds(2) size_mset sublist_el') then obtain i where I: \lo\i\ \i\hi\ \xs'!i=x\ by blast have \\j. lo\j\j\hi \ xs!j=x\ using Perm I bounds(2) Fix by (rule mathias, auto) then show \x \ set (sublist xs lo hi)\ by (simp add: bounds(1) bounds(2) sublist_el') qed lemma mset_sublist_eq: assumes \mset xs' = mset xs\ and \\ i. i xs'!i = xs!i\ and \\ j. \hi \ xs'!j = xs!j\ and bounds: \lo \ hi\ \hi < length xs\ shows \set (sublist xs' lo hi) = set (sublist xs lo hi)\ proof show \set (sublist xs' lo hi) \ set (sublist xs lo hi)\ apply (rule mset_sublist_incl) using assms by auto show \set (sublist xs lo hi) \ set (sublist xs' lo hi)\ by (rule mset_sublist_incl) (metis assms size_mset)+ qed text \Our abstract recursive quicksort procedure. We abstract over a partition procedure.\ definition quicksort :: \('b \ 'b \ bool) \ ('a \ 'b) \ nat \ nat \ 'a list \ 'a list nres\ where \quicksort R h = (\(lo,hi,xs0). do { RECT (\f (lo,hi,xs). do { ASSERT(lo \ hi \ hi < length xs \ mset xs = mset xs0); \ \Premise for a partition function\ (xs, p) \ SPEC(uncurry (partition_spec R h xs lo hi)); \ \Abstract partition function\ ASSERT(mset xs = mset xs0); xs \ (if p-1\lo then RETURN xs else f (lo, p-1, xs)); ASSERT(mset xs = mset xs0); if hi\p+1 then RETURN xs else f (p+1, hi, xs) }) (lo,hi,xs0) })\ text \As premise for quicksor, we only need that the indices are ok.\ definition quicksort_pre :: \('b \ 'b \ bool) \ ('a \ 'b) \ 'a list \ nat \ nat \ 'a list \ bool\ where \quicksort_pre R h xs0 lo hi xs \ lo \ hi \ hi < length xs \ mset xs = mset xs0\ definition quicksort_post :: \('b \ 'b \ bool) \ ('a \ 'b) \ nat \ nat \ 'a list \ 'a list \ bool\ where \quicksort_post R h lo hi xs xs' \ mset xs' = mset xs \ sorted_sublist_map R h xs' lo hi \ (\ i. i xs'!i = xs!i) \ (\ j. hij xs'!j = xs!j)\ text \Convert Pure to HOL\ lemma quicksort_postI: \\mset xs' = mset xs; sorted_sublist_map R h xs' lo hi; (\ i. \i \ xs'!i = xs!i); (\ j. \hi \ xs'!j = xs!j)\ \ quicksort_post R h lo hi xs xs'\ by (auto simp add: quicksort_post_def) text \The first case for the correctness proof of (abstract) quicksort: We assume that we called the partition function, and we have \<^term>\p-1\lo\ and \<^term>\hi\p+1\.\ lemma quicksort_correct_case1: assumes trans: \\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and lin: \\x y. x \ y \ R (h x) (h y) \ R (h y) (h x)\ and pre: \quicksort_pre R h xs0 lo hi xs\ and part: \partition_spec R h xs lo hi xs' p\ and ifs: \p-1 \ lo\ \hi \ p+1\ shows \quicksort_post R h lo hi xs xs'\ proof - text \First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\ have pre: \lo \ hi\ \hi < length xs\ using pre by (auto simp add: quicksort_pre_def) (* have part_perm: \set (sublist xs' lo hi) = set (sublist xs lo hi)\ using part partition_spec_set_sublist pre(1) pre(2) by blast *) have part: \mset xs' = mset xs\ True \isPartition_map R h xs' lo hi p\ \lo \ p\ \p \ hi\ \\ i. i xs'!i=xs!i\ \\ i. \hi \ xs'!i=xs!i\ using part by (auto simp add: partition_spec_def) have sorted_lower: \sorted_sublist_map R h xs' lo (p - Suc 0)\ proof - show ?thesis apply (rule sorted_sublist_wrt_le) subgoal using ifs(1) by auto subgoal using ifs(1) mset_eq_length part(1) pre(1) pre(2) by fastforce done qed have sorted_upper: \sorted_sublist_map R h xs' (Suc p) hi\ proof - show ?thesis apply (rule sorted_sublist_wrt_le) subgoal using ifs(2) by auto subgoal using ifs(1) mset_eq_length part(1) pre(1) pre(2) by fastforce done qed have sorted_middle: \sorted_sublist_map R h xs' lo hi\ proof - show ?thesis apply (rule merge_sorted_map_partitions[where p=p]) subgoal by (rule trans) subgoal by (rule part) subgoal by (rule sorted_lower) subgoal by (rule sorted_upper) subgoal using pre(1) by auto subgoal by (simp add: part(4)) subgoal by (simp add: part(5)) subgoal by (metis part(1) pre(2) size_mset) done qed show ?thesis proof (intro quicksort_postI) show \mset xs' = mset xs\ by (simp add: part(1)) next show \sorted_sublist_map R h xs' lo hi\ by (rule sorted_middle) next show \\i. i < lo \ xs' ! i = xs ! i\ using part(6) by blast next show \\j. \hi < j; j < length xs\ \ xs' ! j = xs ! j\ by (metis part(1) part(7) size_mset) qed qed text \In the second case, we have to show that the precondition still holds for (p+1, hi, x') after the partition.\ lemma quicksort_correct_case2: assumes pre: \quicksort_pre R h xs0 lo hi xs\ and part: \partition_spec R h xs lo hi xs' p\ and ifs: \\ hi \ p + 1\ shows \quicksort_pre R h xs0 (Suc p) hi xs'\ proof - text \First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\ have pre: \lo \ hi\ \hi < length xs\ \mset xs = mset xs0\ using pre by (auto simp add: quicksort_pre_def) have part: \mset xs' = mset xs\ True \isPartition_map R h xs' lo hi p\ \lo \ p\ \p \ hi\ \\ i. i xs'!i=xs!i\ \\ i. \hi \ xs'!i=xs!i\ using part by (auto simp add: partition_spec_def) show ?thesis unfolding quicksort_pre_def proof (intro conjI) show \Suc p \ hi\ using ifs by linarith show \hi < length xs'\ by (metis part(1) pre(2) size_mset) show \mset xs' = mset xs0\ using pre(3) part(1) by (auto dest: mset_eq_setD) qed qed lemma quicksort_post_set: assumes \quicksort_post R h lo hi xs xs'\ and bounds: \lo \ hi\ \hi < length xs\ shows \set (sublist xs' lo hi) = set (sublist xs lo hi)\ proof - have \mset xs' = mset xs\ \\ i. i xs'!i = xs!i\ \\ j. \hi \ xs'!j = xs!j\ using assms by (auto simp add: quicksort_post_def) then show ?thesis using bounds by (rule mset_sublist_eq, auto) qed text \In the third case, we have run quicksort recursively on (p+1, hi, xs') after the partition, with hi<=p+1 and p-1<=lo.\ lemma quicksort_correct_case3: assumes trans: \\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and lin: \\x y. x \ y \ R (h x) (h y) \ R (h y) (h x)\ and pre: \quicksort_pre R h xs0 lo hi xs\ and part: \partition_spec R h xs lo hi xs' p\ and ifs: \p - Suc 0 \ lo\ \\ hi \ Suc p\ and IH1': \quicksort_post R h (Suc p) hi xs' xs''\ shows \quicksort_post R h lo hi xs xs''\ proof - text \First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\ have pre: \lo \ hi\ \hi < length xs\ \mset xs = mset xs0\ using pre by (auto simp add: quicksort_pre_def) have part: \mset xs' = mset xs\ True \isPartition_map R h xs' lo hi p\ \lo \ p\ \p \ hi\ \\ i. i xs'!i=xs!i\ \\ i. \hi \ xs'!i=xs!i\ using part by (auto simp add: partition_spec_def) have IH1: \mset xs'' = mset xs'\ \sorted_sublist_map R h xs'' (Suc p) hi\ \\ i. i xs'' ! i = xs' ! i\ \\ j. \hi < j; j < length xs'\ \ xs'' ! j = xs' ! j\ using IH1' by (auto simp add: quicksort_post_def) note IH1_perm = quicksort_post_set[OF IH1'] have still_partition: \isPartition_map R h xs'' lo hi p\ proof(intro isPartition_wrtI) fix i assume \lo \ i\ \i < p\ show \R (h (xs'' ! i)) (h (xs'' ! p))\ text \This holds because this part hasn't changed\ using IH1(3) \i < p\ \lo \ i\ isPartition_wrt_def part(3) by fastforce next fix j assume \p < j\ \j \ hi\ text \Obtain the position \<^term>\posJ\ where \<^term>\xs''!j\ was stored in \<^term>\xs'\.\ have \xs''!j \ set (sublist xs'' (Suc p) hi)\ by (metis IH1(1) Suc_leI \j \ hi\ \p < j\ less_le_trans mset_eq_length part(1) pre(2) sublist_el') then have \xs''!j \ set (sublist xs' (Suc p) hi)\ by (metis IH1_perm ifs(2) nat_le_linear part(1) pre(2) size_mset) then have \\ posJ. Suc p\posJ\posJ\hi \ xs''!j = xs'!posJ\ by (metis Suc_leI \j \ hi\ \p < j\ less_le_trans part(1) pre(2) size_mset sublist_el') then obtain posJ :: nat where PosJ: \Suc p\posJ\ \posJ\hi\ \xs''!j = xs'!posJ\ by blast then show \R (h (xs'' ! p)) (h (xs'' ! j))\ by (metis IH1(3) Suc_le_lessD isPartition_wrt_def lessI part(3)) qed have sorted_lower: \sorted_sublist_map R h xs'' lo (p - Suc 0)\ proof - show ?thesis apply (rule sorted_sublist_wrt_le) subgoal by (simp add: ifs(1)) subgoal using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce done qed note sorted_upper = IH1(2) have sorted_middle: \sorted_sublist_map R h xs'' lo hi\ proof - show ?thesis apply (rule merge_sorted_map_partitions[where p=p]) subgoal by (rule trans) subgoal by (rule still_partition) subgoal by (rule sorted_lower) subgoal by (rule sorted_upper) subgoal using pre(1) by auto subgoal by (simp add: part(4)) subgoal by (simp add: part(5)) subgoal by (metis IH1(1) part(1) pre(2) size_mset) done qed show ?thesis proof (intro quicksort_postI) show \mset xs'' = mset xs\ using part(1) IH1(1) by auto \ \I was faster than sledgehammer :-)\ next show \sorted_sublist_map R h xs'' lo hi\ by (rule sorted_middle) next show \\i. i < lo \ xs'' ! i = xs ! i\ using IH1(3) le_SucI part(4) part(6) by auto next show \\j. hi < j \ j < length xs \ xs'' ! j = xs ! j\ by (metis IH1(4) part(1) part(7) size_mset) qed qed text \In the 4th case, we have to show that the premise holds for \<^term>\(lo,p-1,xs')\, in case \<^term>\\p-1\lo\\ text \Analogous to case 2.\ lemma quicksort_correct_case4: assumes pre: \quicksort_pre R h xs0 lo hi xs\ and part: \partition_spec R h xs lo hi xs' p\ and ifs: \\ p - Suc 0 \ lo \ shows \quicksort_pre R h xs0 lo (p-Suc 0) xs'\ proof - text \First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\ have pre: \lo \ hi\ \hi < length xs\ \mset xs0 = mset xs\ using pre by (auto simp add: quicksort_pre_def) have part: \mset xs' = mset xs\ True \isPartition_map R h xs' lo hi p\ \lo \ p\ \p \ hi\ \\ i. i xs'!i=xs!i\ \\ i. \hi \ xs'!i=xs!i\ using part by (auto simp add: partition_spec_def) show ?thesis unfolding quicksort_pre_def proof (intro conjI) show \lo \ p - Suc 0\ using ifs by linarith show \p - Suc 0 < length xs'\ using mset_eq_length part(1) part(5) pre(2) by fastforce show \mset xs' = mset xs0\ using pre(3) part(1) by (auto dest: mset_eq_setD) qed qed text \In the 5th case, we have run quicksort recursively on (lo, p-1, xs').\ lemma quicksort_correct_case5: assumes trans: \\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and lin: \\x y. x \ y \ R (h x) (h y) \ R (h y) (h x)\ and pre: \quicksort_pre R h xs0 lo hi xs\ and part: \partition_spec R h xs lo hi xs' p\ and ifs: \\ p - Suc 0 \ lo\ \hi \ Suc p\ and IH1': \quicksort_post R h lo (p - Suc 0) xs' xs''\ shows \quicksort_post R h lo hi xs xs''\ proof - text \First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\ have pre: \lo \ hi\ \hi < length xs\ using pre by (auto simp add: quicksort_pre_def) have part: \mset xs' = mset xs\ True \isPartition_map R h xs' lo hi p\ \lo \ p\ \p \ hi\ \\ i. i xs'!i=xs!i\ \\ i. \hi \ xs'!i=xs!i\ using part by (auto simp add: partition_spec_def) have IH1: \mset xs'' = mset xs'\ \sorted_sublist_map R h xs'' lo (p - Suc 0)\ \\ i. i xs''!i = xs'!i\ \\ j. \p-Suc 0 \ xs''!j = xs'!j\ using IH1' by (auto simp add: quicksort_post_def) note IH1_perm = quicksort_post_set[OF IH1'] have still_partition: \isPartition_map R h xs'' lo hi p\ proof(intro isPartition_wrtI) fix i assume \lo \ i\ \i < p\ text \Obtain the position \<^term>\posI\ where \<^term>\xs''!i\ was stored in \<^term>\xs'\.\ have \xs''!i \ set (sublist xs'' lo (p-Suc 0))\ by (metis (no_types, lifting) IH1(1) Suc_leI Suc_pred \i < p\ \lo \ i\ le_less_trans less_imp_diff_less mset_eq_length not_le not_less_zero part(1) part(5) pre(2) sublist_el') then have \xs''!i \ set (sublist xs' lo (p-Suc 0))\ by (metis IH1_perm ifs(1) le_less_trans less_imp_diff_less mset_eq_length nat_le_linear part(1) part(5) pre(2)) then have \\ posI. lo\posI\posI\p-Suc 0 \ xs''!i = xs'!posI\ proof - \ \sledgehammer\ have "p - Suc 0 < length xs" by (meson diff_le_self le_less_trans part(5) pre(2)) then show ?thesis by (metis (no_types) \xs'' ! i \ set (sublist xs' lo (p - Suc 0))\ ifs(1) mset_eq_length nat_le_linear part(1) sublist_el') qed then obtain posI :: nat where PosI: \lo\posI\ \posI\p-Suc 0\ \xs''!i = xs'!posI\ by blast then show \R (h (xs'' ! i)) (h (xs'' ! p))\ by (metis (no_types, lifting) IH1(4) \i < p\ diff_Suc_less isPartition_wrt_def le_less_trans mset_eq_length not_le not_less_eq part(1) part(3) part(5) pre(2) zero_less_Suc) next fix j assume \p < j\ \j \ hi\ then show \R (h (xs'' ! p)) (h (xs'' ! j))\ text \This holds because this part hasn't changed\ - by (smt IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2)) + by (smt (verit) IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2)) qed note sorted_lower = IH1(2) have sorted_upper: \sorted_sublist_map R h xs'' (Suc p) hi\ proof - show ?thesis apply (rule sorted_sublist_wrt_le) subgoal by (simp add: ifs(2)) subgoal using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce done qed have sorted_middle: \sorted_sublist_map R h xs'' lo hi\ proof - show ?thesis apply (rule merge_sorted_map_partitions[where p=p]) subgoal by (rule trans) subgoal by (rule still_partition) subgoal by (rule sorted_lower) subgoal by (rule sorted_upper) subgoal using pre(1) by auto subgoal by (simp add: part(4)) subgoal by (simp add: part(5)) subgoal by (metis IH1(1) part(1) pre(2) size_mset) done qed show ?thesis proof (intro quicksort_postI) show \mset xs'' = mset xs\ by (simp add: IH1(1) part(1)) next show \sorted_sublist_map R h xs'' lo hi\ by (rule sorted_middle) next show \\i. i < lo \ xs'' ! i = xs ! i\ by (simp add: IH1(3) part(6)) next show \\j. hi < j \ j < length xs \ xs'' ! j = xs ! j\ by (metis IH1(4) diff_le_self dual_order.strict_trans2 mset_eq_length part(1) part(5) part(7)) qed qed text \In the 6th case, we have run quicksort recursively on (lo, p-1, xs'). We show the precondition on the second call on (p+1, hi, xs'')\ lemma quicksort_correct_case6: assumes pre: \quicksort_pre R h xs0 lo hi xs\ and part: \partition_spec R h xs lo hi xs' p\ and ifs: \\ p - Suc 0 \ lo\ \\ hi \ Suc p\ and IH1: \quicksort_post R h lo (p - Suc 0) xs' xs''\ shows \quicksort_pre R h xs0 (Suc p) hi xs''\ proof - text \First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\ have pre: \lo \ hi\ \hi < length xs\ \mset xs0 = mset xs\ using pre by (auto simp add: quicksort_pre_def) have part: \mset xs' = mset xs\ True \isPartition_map R h xs' lo hi p\ \lo \ p\ \p \ hi\ \\ i. i xs'!i=xs!i\ \\ i. \hi \ xs'!i=xs!i\ using part by (auto simp add: partition_spec_def) have IH1: \mset xs'' = mset xs'\ \sorted_sublist_map R h xs'' lo (p - Suc 0)\ \\ i. i xs''!i = xs'!i\ \\ j. \p-Suc 0 \ xs''!j = xs'!j\ using IH1 by (auto simp add: quicksort_post_def) show ?thesis unfolding quicksort_pre_def proof (intro conjI) show \Suc p \ hi\ using ifs(2) by linarith show \hi < length xs''\ using IH1(1) mset_eq_length part(1) pre(2) by fastforce show \mset xs'' = mset xs0\ using pre(3) part(1) IH1(1) by (auto dest: mset_eq_setD) qed qed text \In the 7th (and last) case, we have run quicksort recursively on (lo, p-1, xs'). We show the postcondition on the second call on (p+1, hi, xs'')\ lemma quicksort_correct_case7: assumes trans: \\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and lin: \\x y. x \ y \ R (h x) (h y) \ R (h y) (h x)\ and pre: \quicksort_pre R h xs0 lo hi xs\ and part: \partition_spec R h xs lo hi xs' p\ and ifs: \\ p - Suc 0 \ lo\ \\ hi \ Suc p\ and IH1': \quicksort_post R h lo (p - Suc 0) xs' xs''\ and IH2': \quicksort_post R h (Suc p) hi xs'' xs'''\ shows \quicksort_post R h lo hi xs xs'''\ proof - text \First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\ have pre: \lo \ hi\ \hi < length xs\ using pre by (auto simp add: quicksort_pre_def) have part: \mset xs' = mset xs\ True \isPartition_map R h xs' lo hi p\ \lo \ p\ \p \ hi\ \\ i. i xs'!i=xs!i\ \\ i. \hi \ xs'!i=xs!i\ using part by (auto simp add: partition_spec_def) have IH1: \mset xs'' = mset xs'\ \sorted_sublist_map R h xs'' lo (p - Suc 0)\ \\ i. i xs''!i = xs'!i\ \\ j. \p-Suc 0 \ xs''!j = xs'!j\ using IH1' by (auto simp add: quicksort_post_def) note IH1_perm = quicksort_post_set[OF IH1'] have IH2: \mset xs''' = mset xs''\ \sorted_sublist_map R h xs''' (Suc p) hi\ \\ i. i xs'''!i = xs''!i\ \\ j. \hi \ xs'''!j = xs''!j\ using IH2' by (auto simp add: quicksort_post_def) note IH2_perm = quicksort_post_set[OF IH2'] text \We still have a partition after the first call (same as in case 5)\ have still_partition1: \isPartition_map R h xs'' lo hi p\ proof(intro isPartition_wrtI) fix i assume \lo \ i\ \i < p\ text \Obtain the position \<^term>\posI\ where \<^term>\xs''!i\ was stored in \<^term>\xs'\.\ have \xs''!i \ set (sublist xs'' lo (p-Suc 0))\ by (metis (no_types, lifting) IH1(1) Suc_leI Suc_pred \i < p\ \lo \ i\ le_less_trans less_imp_diff_less mset_eq_length not_le not_less_zero part(1) part(5) pre(2) sublist_el') then have \xs''!i \ set (sublist xs' lo (p-Suc 0))\ by (metis IH1_perm ifs(1) le_less_trans less_imp_diff_less mset_eq_length nat_le_linear part(1) part(5) pre(2)) then have \\ posI. lo\posI\posI\p-Suc 0 \ xs''!i = xs'!posI\ proof - \ \sledgehammer\ have "p - Suc 0 < length xs" by (meson diff_le_self le_less_trans part(5) pre(2)) then show ?thesis by (metis (no_types) \xs'' ! i \ set (sublist xs' lo (p - Suc 0))\ ifs(1) mset_eq_length nat_le_linear part(1) sublist_el') qed then obtain posI :: nat where PosI: \lo\posI\ \posI\p-Suc 0\ \xs''!i = xs'!posI\ by blast then show \R (h (xs'' ! i)) (h (xs'' ! p))\ by (metis (no_types, lifting) IH1(4) \i < p\ diff_Suc_less isPartition_wrt_def le_less_trans mset_eq_length not_le not_less_eq part(1) part(3) part(5) pre(2) zero_less_Suc) next fix j assume \p < j\ \j \ hi\ then show \R (h (xs'' ! p)) (h (xs'' ! j))\ text \This holds because this part hasn't changed\ - by (smt IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2)) + by (smt (verit) IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2)) qed text \We still have a partition after the second call (similar as in case 3)\ have still_partition2: \isPartition_map R h xs''' lo hi p\ proof(intro isPartition_wrtI) fix i assume \lo \ i\ \i < p\ show \R (h (xs''' ! i)) (h (xs''' ! p))\ text \This holds because this part hasn't changed\ using IH2(3) \i < p\ \lo \ i\ isPartition_wrt_def still_partition1 by fastforce next fix j assume \p < j\ \j \ hi\ text \Obtain the position \<^term>\posJ\ where \<^term>\xs'''!j\ was stored in \<^term>\xs'''\.\ have \xs'''!j \ set (sublist xs''' (Suc p) hi)\ by (metis IH1(1) IH2(1) Suc_leI \j \ hi\ \p < j\ ifs(2) nat_le_linear part(1) pre(2) size_mset sublist_el') then have \xs'''!j \ set (sublist xs'' (Suc p) hi)\ by (metis IH1(1) IH2_perm ifs(2) mset_eq_length nat_le_linear part(1) pre(2)) then have \\ posJ. Suc p\posJ\posJ\hi \ xs'''!j = xs''!posJ\ by (metis IH1(1) ifs(2) mset_eq_length nat_le_linear part(1) pre(2) sublist_el') then obtain posJ :: nat where PosJ: \Suc p\posJ\ \posJ\hi\ \xs'''!j = xs''!posJ\ by blast then show \R (h (xs''' ! p)) (h (xs''' ! j))\ proof - \ \sledgehammer\ have "\n na as p. (p (as ! na::'a) (as ! posJ) \ posJ \ na) \ \ isPartition_wrt p as n hi na" by (metis (no_types) PosJ(2) isPartition_wrt_def not_less) then show ?thesis by (metis IH2(3) PosJ(1) PosJ(3) lessI not_less_eq_eq still_partition1) qed qed text \We have that the lower part is sorted after the first recursive call\ note sorted_lower1 = IH1(2) text \We show that it is still sorted after the second call.\ have sorted_lower2: \sorted_sublist_map R h xs''' lo (p-Suc 0)\ proof - show ?thesis using sorted_lower1 apply (rule sorted_wrt_lower_sublist_still_sorted) subgoal by (rule part) subgoal using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce subgoal by (simp add: IH2(3)) subgoal by (metis IH2(1) size_mset) done qed text \The second IH gives us the the upper list is sorted after the second recursive call\ note sorted_upper2 = IH2(2) text \Finally, we have to show that the entire list is sorted after the second recursive call.\ have sorted_middle: \sorted_sublist_map R h xs''' lo hi\ proof - show ?thesis apply (rule merge_sorted_map_partitions[where p=p]) subgoal by (rule trans) subgoal by (rule still_partition2) subgoal by (rule sorted_lower2) subgoal by (rule sorted_upper2) subgoal using pre(1) by auto subgoal by (simp add: part(4)) subgoal by (simp add: part(5)) subgoal by (metis IH1(1) IH2(1) part(1) pre(2) size_mset) done qed show ?thesis proof (intro quicksort_postI) show \mset xs''' = mset xs\ by (simp add: IH1(1) IH2(1) part(1)) next show \sorted_sublist_map R h xs''' lo hi\ by (rule sorted_middle) next show \\i. i < lo \ xs''' ! i = xs ! i\ using IH1(3) IH2(3) part(4) part(6) by auto next show \\j. hi < j \ j < length xs \ xs''' ! j = xs ! j\ by (metis IH1(1) IH1(4) IH2(4) diff_le_self ifs(2) le_SucI less_le_trans nat_le_eq_or_lt not_less part(1) part(7) size_mset) qed qed text \We can now show the correctness of the abstract quicksort procedure, using the refinement framework and the above case lemmas.\ lemma quicksort_correct: assumes trans: \\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and lin: \\x y. x \ y \ R (h x) (h y) \ R (h y) (h x)\ and Pre: \lo0 \ hi0\ \hi0 < length xs0\ shows \quicksort R h (lo0,hi0,xs0) \ \ Id (SPEC(\xs. quicksort_post R h lo0 hi0 xs0 xs))\ proof - have wf: \wf (measure (\(lo, hi, xs). Suc hi - lo))\ by auto define pre where \pre = (\(lo,hi,xs). quicksort_pre R h xs0 lo hi xs)\ define post where \post = (\(lo,hi,xs). quicksort_post R h lo hi xs)\ have pre: \pre (lo0,hi0,xs0)\ unfolding quicksort_pre_def pre_def by (simp add: Pre) text \We first generalize the goal a over all states.\ have \WB_Sort.quicksort R h (lo0,hi0,xs0) \ \ Id (SPEC (post (lo0,hi0,xs0)))\ unfolding quicksort_def prod.case apply (rule RECT_rule) apply (refine_mono) apply (rule wf) apply (rule pre) subgoal premises IH for f x apply (refine_vcg ASSERT_leI) unfolding pre_def post_def subgoal \ \First premise (assertion) for partition\ using IH(2) by (simp add: quicksort_pre_def pre_def) subgoal \ \Second premise (assertion) for partition\ using IH(2) by (simp add: quicksort_pre_def pre_def) subgoal using IH(2) by (auto simp add: quicksort_pre_def pre_def dest: mset_eq_setD) text \Termination case: \<^term>\(p-1 \ lo')\ and \<^term>\(hi' \ p+1)\; directly show postcondition\ subgoal unfolding partition_spec_def by (auto dest: mset_eq_setD) subgoal \ \Postcondition (after partition)\ apply - using IH(2) unfolding pre_def apply (simp, elim conjE, split prod.splits) using trans lin apply (rule quicksort_correct_case1) by auto text \Case \<^term>\(p-1 \ lo')\ and \<^term>\(hi' < p+1)\ (Only second recursive call)\ subgoal apply (rule IH(1)[THEN order_trans]) text \Show that the invariant holds for the second recursive call\ subgoal using IH(2) unfolding pre_def apply (simp, elim conjE, split prod.splits) apply (rule quicksort_correct_case2) by auto text \Wellfoundness (easy)\ subgoal by (auto simp add: quicksort_pre_def partition_spec_def) text \Show that the postcondition holds\ subgoal apply (simp add: Misc.subset_Collect_conv post_def, intro allI impI, elim conjE) using trans lin apply (rule quicksort_correct_case3) using IH(2) unfolding pre_def by auto done text \Case: At least the first recursive call\ subgoal apply (rule IH(1)[THEN order_trans]) text \Show that the precondition holds for the first recursive call\ subgoal using IH(2) unfolding pre_def post_def apply (simp, elim conjE, split prod.splits) apply auto apply (rule quicksort_correct_case4) by auto text \Wellfoundness for first recursive call (easy)\ subgoal by (auto simp add: quicksort_pre_def partition_spec_def) text \Simplify some refinement suff...\ apply (simp add: Misc.subset_Collect_conv ASSERT_leI, intro allI impI conjI, elim conjE) apply (rule ASSERT_leI) apply (simp_all add: Misc.subset_Collect_conv ASSERT_leI) subgoal unfolding quicksort_post_def pre_def post_def by (auto dest: mset_eq_setD) text \Only the first recursive call: show postcondition\ subgoal using trans lin apply (rule quicksort_correct_case5) using IH(2) unfolding pre_def post_def by auto apply (rule ASSERT_leI) subgoal unfolding quicksort_post_def pre_def post_def by (auto dest: mset_eq_setD) text \Both recursive calls.\ subgoal apply (rule IH(1)[THEN order_trans]) text \Show precondition for second recursive call (after the first call)\ subgoal unfolding pre_def post_def apply auto apply (rule quicksort_correct_case6) using IH(2) unfolding pre_def post_def by auto text \Wellfoundedness for second recursive call (easy)\ subgoal by (auto simp add: quicksort_pre_def partition_spec_def) text \Show that the postcondition holds (after both recursive calls)\ subgoal apply (simp add: Misc.subset_Collect_conv, intro allI impI, elim conjE) using trans lin apply (rule quicksort_correct_case7) using IH(2) unfolding pre_def post_def by auto done done done done text \Finally, apply the generalized lemma to show the thesis.\ then show ?thesis unfolding post_def by auto qed (* TODO: Show that our (abstract) partition satisifies the specification *) definition partition_main_inv :: \('b \ 'b \ bool) \ ('a \ 'b) \ nat \ nat \ 'a list \ (nat\nat\'a list) \ bool\ where \partition_main_inv R h lo hi xs0 p \ case p of (i,j,xs) \ j < length xs \ j \ hi \ i < length xs \ lo \ i \ i \ j \ mset xs = mset xs0 \ (\k. k \ lo \ k < i \ R (h (xs!k)) (h (xs!hi))) \ \ \All elements from \<^term>\lo\ to \<^term>\i-1\ are smaller than the pivot\ (\k. k \ i \ k < j \ R (h (xs!hi)) (h (xs!k))) \ \ \All elements from \<^term>\i\ to \<^term>\j-1\ are greater than the pivot\ (\k. k < lo \ xs!k = xs0!k) \ \ \Everything below \<^term>\lo\ is unchanged\ (\k. k \ j \ k < length xs \ xs!k = xs0!k) \ \All elements from \<^term>\j\ are unchanged (including everyting above \<^term>\hi\)\ \ text \The main part of the partition function. The pivot is assumed to be the last element. This is exactly the "Lomuto partition scheme" partition function from Wikipedia.\ definition partition_main :: \('b \ 'b \ bool) \ ('a \ 'b) \ nat \ nat \ 'a list \ ('a list \ nat) nres\ where \partition_main R h lo hi xs0 = do { ASSERT(hi < length xs0); pivot \ RETURN (h (xs0 ! hi)); (i,j,xs) \ WHILE\<^sub>T\<^bsup>partition_main_inv R h lo hi xs0\<^esup> \ \We loop from \<^term>\j=lo\ to \<^term>\j=hi-1\.\ (\(i,j,xs). j < hi) (\(i,j,xs). do { ASSERT(i < length xs \ j < length xs); if R (h (xs!j)) pivot then RETURN (i+1, j+1, swap xs i j) else RETURN (i, j+1, xs) }) (lo, lo, xs0); \ \i and j are both initialized to lo\ ASSERT(i < length xs \ j = hi \ lo \ i \ hi < length xs \ mset xs = mset xs0); RETURN (swap xs i hi, i) }\ (* definition partition_spec :: \('b \ 'b \ bool) \ ('a \ 'b) \ 'a list \ nat \ nat \ 'a list \ nat \ bool\ where \partition_spec R h xs lo hi xs' p \ mset xs' = mset xs \ \ \The list is a permutation\ isPartition_map R h xs' lo hi p \ \ \We have a valid partition on the resulting list\ lo \ p \ p \ hi \ \ \The partition index is in bounds\ (\ i. i xs'!i=xs!i) \ (\ i. hii xs'!i=xs!i)\ \ \Everything else is unchanged.\ *) lemma partition_main_correct: assumes bounds: \hi < length xs\ \lo \ hi\ and trans: \\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and lin: \\x y. R (h x) (h y) \ R (h y) (h x)\ shows \partition_main R h lo hi xs \ SPEC(\(xs', p). mset xs = mset xs' \ lo \ p \ p \ hi \ isPartition_map R h xs' lo hi p \ (\ i. i xs'!i=xs!i) \ (\ i. hii xs'!i=xs!i))\ proof - have K: \b \ hi - Suc n \ n > 0 \ Suc n \ hi \ Suc b \ hi - n\ for b hi n by auto have L: \~ R (h x) (h y) \ R (h y) (h x)\ for x y \ \Corollary of linearity\ using assms by blast have M: \a < Suc b \ a = b \ a < b\ for a b by linarith have N: \(a::nat) \ b \ a = b \ a < b\ for a b by arith show ?thesis unfolding partition_main_def choose_pivot_def apply (refine_vcg WHILEIT_rule[where R = \measure(\(i,j,xs). hi-j)\]) subgoal using assms by blast \ \We feed our assumption to the assertion\ subgoal by auto \ \WF\ subgoal \ \Invariant holds before the first iteration\ unfolding partition_main_inv_def using assms apply simp by linarith subgoal unfolding partition_main_inv_def by simp subgoal unfolding partition_main_inv_def by simp subgoal unfolding partition_main_inv_def apply (auto dest: mset_eq_length) done subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length) subgoal unfolding partition_main_inv_def apply (auto dest: mset_eq_length) by (metis L M mset_eq_length nat_le_eq_or_lt) subgoal unfolding partition_main_inv_def by simp \ \assertions, etc\ subgoal unfolding partition_main_inv_def by simp subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length) subgoal unfolding partition_main_inv_def by simp subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length) subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length) subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length) subgoal unfolding partition_main_inv_def by simp subgoal unfolding partition_main_inv_def by simp subgoal \ \After the last iteration, we have a partitioning! :-)\ unfolding partition_main_inv_def by (auto simp add: isPartition_wrt_def) subgoal \ \And the lower out-of-bounds parts of the list haven't been changed\ unfolding partition_main_inv_def by auto subgoal \ \And the upper out-of-bounds parts of the list haven't been changed\ unfolding partition_main_inv_def by auto done qed definition partition_between :: \('b \ 'b \ bool) \ ('a \ 'b) \ nat \ nat \ 'a list \ ('a list \ nat) nres\ where \partition_between R h lo hi xs0 = do { ASSERT(hi < length xs0 \ lo \ hi); k \ choose_pivot R h xs0 lo hi; \ \choice of pivot\ ASSERT(k < length xs0); xs \ RETURN (swap xs0 k hi); \ \move the pivot to the last position, before we start the actual loop\ ASSERT(length xs = length xs0); partition_main R h lo hi xs }\ lemma partition_between_correct: assumes \hi < length xs\ and \lo \ hi\ and \\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and \\x y. R (h x) (h y) \ R (h y) (h x)\ shows \partition_between R h lo hi xs \ SPEC(uncurry (partition_spec R h xs lo hi))\ proof - have K: \b \ hi - Suc n \ n > 0 \ Suc n \ hi \ Suc b \ hi - n\ for b hi n by auto show ?thesis unfolding partition_between_def choose_pivot_def apply (refine_vcg partition_main_correct) using assms apply (auto dest: mset_eq_length simp add: partition_spec_def) by (metis dual_order.strict_trans2 less_imp_not_eq2 mset_eq_length swap_nth) qed text \We use the median of the first, the middle, and the last element.\ definition choose_pivot3 where \choose_pivot3 R h xs lo (hi::nat) = do { ASSERT(lo < length xs); ASSERT(hi < length xs); let k' = (hi - lo) div 2; let k = lo + k'; ASSERT(k < length xs); let start = h (xs ! lo); let mid = h (xs ! k); let end = h (xs ! hi); if (R start mid \ R mid end) \ (R end mid \ R mid start) then RETURN k else if (R start end \ R end mid) \ (R mid end \ R end start) then RETURN hi else RETURN lo }\ \ \We only have to show that this procedure yields a valid index between \lo\ and \hi\.\ lemma choose_pivot3_choose_pivot: assumes \lo < length xs\ \hi < length xs\ \hi \ lo\ shows \choose_pivot3 R h xs lo hi \ \ Id (choose_pivot R h xs lo hi)\ unfolding choose_pivot3_def choose_pivot_def using assms by (auto intro!: ASSERT_leI simp: Let_def) text \The refined partion function: We use the above pivot function and fold instead of non-deterministic iteration.\ definition partition_between_ref :: \('b \ 'b \ bool) \ ('a \ 'b) \ nat \ nat \ 'a list \ ('a list \ nat) nres\ where \partition_between_ref R h lo hi xs0 = do { ASSERT(hi < length xs0 \ hi < length xs0 \ lo \ hi); k \ choose_pivot3 R h xs0 lo hi; \ \choice of pivot\ ASSERT(k < length xs0); xs \ RETURN (swap xs0 k hi); \ \move the pivot to the last position, before we start the actual loop\ ASSERT(length xs = length xs0); partition_main R h lo hi xs }\ lemma partition_main_ref': \partition_main R h lo hi xs \ \ ((\ a b c d. Id) a b c d) (partition_main R h lo hi xs)\ by auto (*TODO already exists somewhere*) lemma Down_id_eq: \\Id x = x\ by auto lemma partition_between_ref_partition_between: \partition_between_ref R h lo hi xs \ (partition_between R h lo hi xs)\ proof - have swap: \(swap xs k hi, swap xs ka hi) \ Id\ if \k = ka\ for k ka using that by auto have [refine0]: \(h (xsa ! hi), h (xsaa ! hi)) \ Id\ if \(xsa, xsaa) \ Id\ for xsa xsaa using that by auto show ?thesis apply (subst (2) Down_id_eq[symmetric]) unfolding partition_between_ref_def partition_between_def OP_def apply (refine_vcg choose_pivot3_choose_pivot swap partition_main_correct) 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 by (auto intro: Refine_Basic.Id_refine dest: mset_eq_length) qed text \Technical lemma for sepref\ lemma partition_between_ref_partition_between': \(uncurry2 (partition_between_ref R h), uncurry2 (partition_between R h)) \ (nat_rel \\<^sub>r nat_rel) \\<^sub>r \Id\list_rel \\<^sub>f \\Id\list_rel \\<^sub>r nat_rel\nres_rel\ by (intro frefI nres_relI) (auto intro: partition_between_ref_partition_between) text \Example instantiation for pivot\ definition choose_pivot3_impl where \choose_pivot3_impl = choose_pivot3 (\) id\ lemma partition_between_ref_correct: assumes trans: \\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and lin: \\x y. R (h x) (h y) \ R (h y) (h x)\ and bounds: \hi < length xs\ \lo \ hi\ shows \partition_between_ref R h lo hi xs \ SPEC (uncurry (partition_spec R h xs lo hi))\ proof - show ?thesis apply (rule partition_between_ref_partition_between[THEN order_trans]) using bounds apply (rule partition_between_correct[where h=h]) subgoal by (rule trans) subgoal by (rule lin) done qed text \Refined quicksort algorithm: We use the refined partition function.\ definition quicksort_ref :: \_ \ _ \ nat \ nat \ 'a list \ 'a list nres\ where \quicksort_ref R h = (\(lo,hi,xs0). do { RECT (\f (lo,hi,xs). do { ASSERT(lo \ hi \ hi < length xs0 \ mset xs = mset xs0); (xs, p) \ partition_between_ref R h lo hi xs; \ \This is the refined partition function. Note that we need the premises (trans,lin,bounds) here.\ ASSERT(mset xs = mset xs0 \ p \ lo \ p < length xs0); xs \ (if p-1\lo then RETURN xs else f (lo, p-1, xs)); ASSERT(mset xs = mset xs0); if hi\p+1 then RETURN xs else f (p+1, hi, xs) }) (lo,hi,xs0) })\ (*TODO share*) lemma fref_to_Down_curry2: \(uncurry2 f, uncurry2 g) \ [P]\<^sub>f A \ \B\nres_rel \ (\x x' y y' z z'. P ((x', y'), z') \ (((x, y), z), ((x', y'), z')) \ A\ f x y z \ \ B (g x' y' z'))\ unfolding fref_def uncurry_def nres_rel_def by auto lemma fref_to_Down_curry: \(f, g) \ [P]\<^sub>f A \ \B\nres_rel \ (\x x' . P x' \ (x, x') \ A\ f x \ \ B (g x'))\ unfolding fref_def uncurry_def nres_rel_def by auto lemma quicksort_ref_quicksort: assumes bounds: \hi < length xs\ \lo \ hi\ and trans: \\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and lin: \\x y. R (h x) (h y) \ R (h y) (h x)\ shows \quicksort_ref R h x0 \ \ Id (quicksort R h x0)\ proof - have wf: \wf (measure (\(lo, hi, xs). Suc hi - lo))\ by auto have pre: \x0 = x0' \ (x0, x0') \ Id \\<^sub>r Id \\<^sub>r \Id\list_rel\ for x0 x0' :: \nat \ nat \ 'b list\ by auto have [refine0]: \(x1e = x1d) \ (x1e,x1d) \ Id\ for x1e x1d :: \'b list\ by auto show ?thesis unfolding quicksort_def quicksort_ref_def apply (refine_vcg pre partition_between_ref_partition_between'[THEN fref_to_Down_curry2]) text \First assertion (premise for partition)\ subgoal by auto text \First assertion (premise for partition)\ subgoal by auto subgoal by (auto dest: mset_eq_length) subgoal by (auto dest: mset_eq_length mset_eq_setD) text \Correctness of the concrete partition function\ subgoal apply (simp, rule partition_between_ref_correct) subgoal by (rule trans) subgoal by (rule lin) subgoal by auto \ \first premise\ subgoal by auto \ \second premise\ done subgoal by (auto dest: mset_eq_length mset_eq_setD) subgoal by (auto simp: partition_spec_def isPartition_wrt_def) subgoal by (auto simp: partition_spec_def isPartition_wrt_def dest: mset_eq_length) subgoal by (auto dest: mset_eq_length mset_eq_setD) subgoal by (auto dest: mset_eq_length mset_eq_setD) subgoal by (auto dest: mset_eq_length mset_eq_setD) subgoal by (auto dest: mset_eq_length mset_eq_setD) by simp+ qed \ \Sort the entire list\ definition full_quicksort where \full_quicksort R h xs \ if xs = [] then RETURN xs else quicksort R h (0, length xs - 1, xs)\ definition full_quicksort_ref where \full_quicksort_ref R h xs \ if List.null xs then RETURN xs else quicksort_ref R h (0, length xs - 1, xs)\ definition full_quicksort_impl :: \nat list \ nat list nres\ where \full_quicksort_impl xs = full_quicksort_ref (\) id xs\ lemma full_quicksort_ref_full_quicksort: assumes trans: \\ x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and lin: \\x y. R (h x) (h y) \ R (h y) (h x)\ shows \(full_quicksort_ref R h, full_quicksort R h) \ \Id\list_rel \\<^sub>f \ \Id\list_rel\nres_rel\ proof - show ?thesis unfolding full_quicksort_ref_def full_quicksort_def apply (intro frefI nres_relI) apply (auto intro!: quicksort_ref_quicksort[unfolded Down_id_eq] simp: List.null_def) subgoal by (rule trans) subgoal using lin by blast done qed lemma sublist_entire: \sublist xs 0 (length xs - 1) = xs\ by (simp add: sublist_def) lemma sorted_sublist_wrt_entire: assumes \sorted_sublist_wrt R xs 0 (length xs - 1)\ shows \sorted_wrt R xs\ proof - have \sorted_wrt R (sublist xs 0 (length xs - 1))\ using assms by (simp add: sorted_sublist_wrt_def ) then show ?thesis by (metis sublist_entire) qed lemma sorted_sublist_map_entire: assumes \sorted_sublist_map R h xs 0 (length xs - 1)\ shows \sorted_wrt (\ x y. R (h x) (h y)) xs\ proof - show ?thesis using assms by (rule sorted_sublist_wrt_entire) qed text \Final correctness lemma\ theorem full_quicksort_correct_sorted: assumes trans: \\x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and lin: \\x y. x \ y \ R (h x) (h y) \ R (h y) (h x)\ shows \full_quicksort R h xs \ \ Id (SPEC(\xs'. mset xs' = mset xs \ sorted_wrt (\ x y. R (h x) (h y)) xs'))\ proof - show ?thesis unfolding full_quicksort_def apply (refine_vcg) subgoal by simp \ \case xs=[]\ subgoal by simp \ \case xs=[]\ apply (rule quicksort_correct[THEN order_trans]) subgoal by (rule trans) subgoal by (rule lin) subgoal by linarith subgoal by simp apply (simp add: Misc.subset_Collect_conv, intro allI impI conjI) subgoal by (auto simp add: quicksort_post_def) subgoal apply (rule sorted_sublist_map_entire) by (auto simp add: quicksort_post_def dest: mset_eq_length) done qed lemma full_quicksort_correct: assumes trans: \\x y z. \R (h x) (h y); R (h y) (h z)\ \ R (h x) (h z)\ and lin: \\x y. R (h x) (h y) \ R (h y) (h x)\ shows \full_quicksort R h xs \ \ Id (SPEC(\xs'. mset xs' = mset xs))\ by (rule order_trans[OF full_quicksort_correct_sorted]) (use assms in auto) end