diff --git a/thys/Functional_Ordered_Resolution_Prover/Executable_Subsumption.thy b/thys/Functional_Ordered_Resolution_Prover/Executable_Subsumption.thy --- a/thys/Functional_Ordered_Resolution_Prover/Executable_Subsumption.thy +++ b/thys/Functional_Ordered_Resolution_Prover/Executable_Subsumption.thy @@ -1,365 +1,365 @@ (* Title: An Executable Algorithm for Clause Subsumption Author: Dmitriy Traytel , 2017 Maintainer: Anders Schlichtkrull *) section \An Executable Algorithm for Clause Subsumption\ text \ This theory provides an executable functional implementation of clause subsumption, building on the \textsf{IsaFoR} library. \ theory Executable_Subsumption imports IsaFoR_Term First_Order_Terms.Matching begin subsection \Naive Implementation of Clause Subsumption\ fun subsumes_list where "subsumes_list [] Ks \ = True" | "subsumes_list (L # Ls) Ks \ = (\K \ set Ks. is_pos K = is_pos L \ (case match_term_list [(atm_of L, atm_of K)] \ of None \ False | Some \ \ subsumes_list Ls (remove1 K Ks) \))" lemma atm_of_map_literal[simp]: "atm_of (map_literal f l) = f (atm_of l)" by (cases l; simp) definition "extends_subst \ \ = (\x \ dom \. \ x = \ x)" lemma extends_subst_refl[simp]: "extends_subst \ \" unfolding extends_subst_def by auto lemma extends_subst_trans: "extends_subst \ \ \ extends_subst \ \ \ extends_subst \ \" unfolding extends_subst_def dom_def by (metis mem_Collect_eq) lemma extends_subst_dom: "extends_subst \ \ \ dom \ \ dom \" unfolding extends_subst_def dom_def by auto lemma extends_subst_extends: "extends_subst \ \ \ x \ dom \ \ \ x = \ x" unfolding extends_subst_def dom_def by auto lemma extends_subst_fun_upd_new: "\ x = None \ extends_subst (\(x \ t)) \ \ extends_subst \ \ \ \ x = Some t" unfolding extends_subst_def dom_fun_upd subst_of_map_def by (force simp add: dom_def split: option.splits) lemma extends_subst_fun_upd_matching: "\ x = Some t \ extends_subst (\(x \ t)) \ \ extends_subst \ \" unfolding extends_subst_def dom_fun_upd subst_of_map_def by (auto simp add: dom_def split: option.splits) lemma extends_subst_empty[simp]: "extends_subst Map.empty \" unfolding extends_subst_def by auto lemma extends_subst_cong_term: "extends_subst \ \ \ vars_term t \ dom \ \ t \ subst_of_map Var \ = t \ subst_of_map Var \" by (force simp: extends_subst_def subst_of_map_def split: option.splits intro!: term_subst_eq) lemma extends_subst_cong_lit: "extends_subst \ \ \ vars_lit L \ dom \ \ L \lit subst_of_map Var \ = L \lit subst_of_map Var \" by (cases L) (auto simp: extends_subst_cong_term) definition "subsumes_modulo C D \ = (\\. dom \ = vars_clause C \ dom \ \ extends_subst \ \ \ subst_cls C (subst_of_map Var \) \# D)" abbreviation subsumes_list_modulo where "subsumes_list_modulo Ls Ks \ \ subsumes_modulo (mset Ls) (mset Ks) \" lemma vars_clause_add_mset[simp]: "vars_clause (add_mset L C) = vars_lit L \ vars_clause C" unfolding vars_clause_def by auto lemma subsumes_list_modulo_Cons: "subsumes_list_modulo (L # Ls) Ks \ \ (\K \ set Ks. \\. extends_subst \ \ \ dom \ = vars_lit L \ dom \ \ L \lit (subst_of_map Var \) = K \ subsumes_list_modulo Ls (remove1 K Ks) \)" unfolding subsumes_modulo_def proof (safe, goal_cases left_right right_left) case (left_right \) then show ?case by (intro bexI[of _ "L \lit subst_of_map Var \"] exI[of _ "\x. if x \ vars_lit L \ dom \ then \ x else None"], intro conjI exI[of _ \]) (auto 0 3 simp: extends_subst_def dom_def split: if_splits simp: insert_subset_eq_iff subst_lit_def intro!: extends_subst_cong_lit) next case (right_left K \ \') then show ?case by (intro bexI[of _ "L \lit subst_of_map Var \"] exI[of _ \'], intro conjI exI[of _ \]) (auto simp: insert_subset_eq_iff subst_lit_def extends_subst_cong_lit intro: extends_subst_trans) qed lemma decompose_Some_var_terms: "decompose (Fun f ss) (Fun g ts) = Some eqs \ f = g \ length ss = length ts \ eqs = zip ss ts \ (\(t, u)\set ((Fun f ss, Fun g ts) # P). vars_term t) = (\(t, u)\set (eqs @ P). vars_term t)" by (drule decompose_Some) (fastforce simp: in_set_zip in_set_conv_nth Bex_def image_iff) lemma match_term_list_sound: "match_term_list tus \ = Some \ \ extends_subst \ \ \ dom \ = (\(t, u)\set tus. vars_term t) \ dom \ \ (\(t,u)\set tus. t \ subst_of_map Var \ = u)" proof (induct tus \ rule: match_term_list.induct) case (2 x t P \) then show ?case by (auto 0 3 simp: extends_subst_fun_upd_new extends_subst_fun_upd_matching subst_of_map_def dest: extends_subst_extends simp del: fun_upd_apply split: if_splits option.splits) next case (3 f ss g ts P \) from 3(2) obtain eqs where "decompose (Fun f ss) (Fun g ts) = Some eqs" "match_term_list (eqs @ P) \ = Some \" by (auto split: option.splits) with 3(1)[OF this] show ?case proof (elim decompose_Some_var_terms[where P = P, elim_format] conjE, intro conjI, goal_cases extend dom subst) case subst from subst(3,5,6,7) show ?case by (auto 0 6 simp: in_set_conv_nth list_eq_iff_nth_eq Ball_def) qed auto qed auto lemma match_term_list_complete: "match_term_list tus \ = None \ extends_subst \ \ \ dom \ = (\(t, u)\set tus. vars_term t) \ dom \ \ (\(t,u)\set tus. t \ subst_of_map Var \ \ u)" proof (induct tus \ arbitrary: \ rule: match_term_list.induct) case (2 x t P \) then show ?case by (auto simp: extends_subst_fun_upd_new extends_subst_fun_upd_matching subst_of_map_def dest: extends_subst_extends simp del: fun_upd_apply split: if_splits option.splits) next case (3 f ss g ts P \) show ?case proof (cases "decompose (Fun f ss) (Fun g ts) = None") case False with 3(2) obtain eqs where "decompose (Fun f ss) (Fun g ts) = Some eqs" "match_term_list (eqs @ P) \ = None" by (auto split: option.splits) with 3(1)[OF this 3(3) trans[OF 3(4) arg_cong[of _ _ "\x. x \ dom \"]]] show ?thesis proof (elim decompose_Some_var_terms[where P = P, elim_format] conjE, goal_cases subst) case subst from subst(1)[OF subst(6)] subst(4,5) show ?case by (auto 0 3 simp: in_set_conv_nth list_eq_iff_nth_eq Ball_def) qed qed auto qed auto lemma unique_extends_subst: assumes extends: "extends_subst \ \" "extends_subst \ \" and dom: "dom \ = vars_term t \ dom \" "dom \ = vars_term t \ dom \" and eq: "t \ subst_of_map Var \ = t \ subst_of_map Var \" shows "\ = \" proof fix x consider (a) "x \ dom \" | (b) "x \ vars_term t" | (c) "x \ dom \" using assms by auto then show "\ x = \ x" proof cases case a then show ?thesis using extends unfolding extends_subst_def by auto next case b with eq show ?thesis proof (induct t) case (Var x) with trans[OF dom(1) dom(2)[symmetric]] show ?case by (auto simp: subst_of_map_def split: option.splits) qed auto next case c then have "\ x = None" "\ x = None" using dom by auto then show ?thesis by simp qed qed lemma subsumes_list_alt: "subsumes_list Ls Ks \ \ subsumes_list_modulo Ls Ks \" proof (induction Ls Ks \ rule: subsumes_list.induct[case_names Nil Cons]) case (Cons L Ls Ks \) show ?case unfolding subsumes_list_modulo_Cons subsumes_list.simps proof ((intro bex_cong[OF refl] ext iffI; elim exE conjE), goal_cases LR RL) case (LR K) show ?case by (insert LR; cases K; cases L; auto simp: Cons.IH split: option.splits dest!: match_term_list_sound) next case (RL K \) then show ?case proof (cases "match_term_list [(atm_of L, atm_of K)] \") case None with RL show ?thesis by (auto simp: Cons.IH dest!: match_term_list_complete) next case (Some \') with RL show ?thesis using unique_extends_subst[of \ \ \' "atm_of L"] by (auto simp: Cons.IH dest!: match_term_list_sound) qed qed qed (auto simp: subsumes_modulo_def subst_cls_def vars_clause_def intro: extends_subst_refl) lemma subsumes_subsumes_list[code_unfold]: "subsumes (mset Ls) (mset Ks) = subsumes_list Ls Ks Map.empty" unfolding subsumes_list_alt[of Ls Ks Map.empty] proof assume "subsumes (mset Ls) (mset Ks)" then obtain \ where "subst_cls (mset Ls) \ \# mset Ks" unfolding subsumes_def by blast moreover define \ where "\ = (\x. if x \ vars_clause (mset Ls) then Some (\ x) else None)" ultimately show "subsumes_list_modulo Ls Ks Map.empty" unfolding subsumes_modulo_def by (subst (asm) same_on_vars_clause[of _ \ "subst_of_map Var \"]) (auto intro!: exI[of _ \] simp: subst_of_map_def[abs_def] split: if_splits) qed (auto simp: subsumes_modulo_def subst_lit_def subsumes_def) lemma strictly_subsumes_subsumes_list[code_unfold]: "strictly_subsumes (mset Ls) (mset Ks) = (subsumes_list Ls Ks Map.empty \ \ subsumes_list Ks Ls Map.empty)" unfolding strictly_subsumes_def subsumes_subsumes_list by simp lemma subsumes_list_filterD: "subsumes_list Ls (filter P Ks) \ \ subsumes_list Ls Ks \" proof (induction Ls arbitrary: Ks \) case (Cons L Ls) from Cons.prems show ?case by (auto dest!: Cons.IH simp: filter_remove1[symmetric] split: option.splits) qed simp lemma subsumes_list_filterI: assumes match: "(\L K \ \. L \ set Ls \ match_term_list [(atm_of L, atm_of K)] \ = Some \ \ is_pos L = is_pos K \ P K)" shows "subsumes_list Ls Ks \ \ subsumes_list Ls (filter P Ks) \" using assms proof (induction Ls Ks \ rule: subsumes_list.induct[case_names Nil Cons]) case (Cons L Ls Ks \) from Cons.prems show ?case unfolding subsumes_list.simps set_filter bex_simps conj_assoc by (elim bexE conjE) (rule exI, rule conjI, assumption, auto split: option.splits simp: filter_remove1[symmetric] intro!: Cons.IH) qed simp lemma subsumes_list_Cons_filter_iff: assumes sorted_wrt: "sorted_wrt leq (L # Ls)" and trans: "transp leq" and match: "(\L K \ \. match_term_list [(atm_of L, atm_of K)] \ = Some \ \ is_pos L = is_pos K \ leq L K)" shows "subsumes_list (L # Ls) (filter (leq L) Ks) \ \ subsumes_list (L # Ls) Ks \" apply (rule iffI[OF subsumes_list_filterD subsumes_list_filterI]; assumption?) unfolding list.set insert_iff apply (elim disjE) subgoal by (auto split: option.splits elim!: match) subgoal for L K \ \ using sorted_wrt unfolding List.sorted_wrt.simps(2) apply (elim conjE) apply (drule bspec, assumption) apply (erule transpD[OF trans]) apply (erule match) by auto done definition leq_head :: "('f::linorder, 'v) term \ ('f, 'v) term \ bool" where "leq_head t u = (case (root t, root u) of (None, _) \ True | (_, None) \ False | (Some f, Some g) \ f \ g)" definition "leq_lit L K = (case (K, L) of (Neg _, Pos _) \ True | (Pos _, Neg _) \ False | _ \ leq_head (atm_of L) (atm_of K))" lemma transp_leq_lit[simp]: "transp leq_lit" unfolding transp_def leq_lit_def leq_head_def by (force split: option.splits literal.splits) -lemma reflp_leq_lit[simp]: "reflp_on leq_lit A" +lemma reflp_leq_lit[simp]: "reflp_on A leq_lit" unfolding reflp_on_def leq_lit_def leq_head_def by (auto split: option.splits literal.splits) lemma total_leq_lit[simp]: "totalp_on A leq_lit" unfolding totalp_on_def leq_lit_def leq_head_def by (auto split: option.splits literal.splits) lemma leq_head_subst[simp]: "leq_head t (t \ \)" by (induct t) (auto simp: leq_head_def) lemma leq_lit_match: fixes L K :: "('f :: linorder, 'v) term literal" shows "match_term_list [(atm_of L, atm_of K)] \ = Some \ \ is_pos L = is_pos K \ leq_lit L K" by (cases L; cases K) (auto simp: leq_lit_def dest!: match_term_list_sound split: option.splits) subsection \Optimized Implementation of Clause Subsumption\ fun subsumes_list_filter where "subsumes_list_filter [] Ks \ = True" | "subsumes_list_filter (L # Ls) Ks \ = (let Ks = filter (leq_lit L) Ks in (\K \ set Ks. is_pos K = is_pos L \ (case match_term_list [(atm_of L, atm_of K)] \ of None \ False | Some \ \ subsumes_list_filter Ls (remove1 K Ks) \)))" lemma sorted_wrt_subsumes_list_subsumes_list_filter: "sorted_wrt leq_lit Ls \ subsumes_list Ls Ks \ = subsumes_list_filter Ls Ks \" proof (induction Ls arbitrary: Ks \) case (Cons L Ls) from Cons.prems have "subsumes_list (L # Ls) Ks \ = subsumes_list (L # Ls) (filter (leq_lit L) Ks) \" by (intro subsumes_list_Cons_filter_iff[symmetric]) (auto dest: leq_lit_match) also have "subsumes_list (L # Ls) (filter (leq_lit L) Ks) \ = subsumes_list_filter (L # Ls) Ks \" using Cons.prems by (auto simp: Cons.IH split: option.splits) finally show ?case . qed simp subsection \Definition of Deterministic QuickSort\ text \ This is the functional description of the standard variant of deterministic QuickSort that always chooses the first list element as the pivot as given by Hoare in 1962. For a list that is already sorted, this leads to $n(n-1)$ comparisons, but as is well known, the average case is much better. The code below is adapted from Manuel Eberl's \Quick_Sort_Cost\ AFP entry, but without invoking probability theory and using a predicate instead of a set. \ fun quicksort :: "('a \ 'a \ bool) \ 'a list \ 'a list" where "quicksort _ [] = []" | "quicksort R (x # xs) = quicksort R (filter (\y. R y x) xs) @ [x] @ quicksort R (filter (\y. \ R y x) xs)" text \ We can easily show that this QuickSort is correct: \ theorem mset_quicksort [simp]: "mset (quicksort R xs) = mset xs" by (induction R xs rule: quicksort.induct) simp_all corollary set_quicksort [simp]: "set (quicksort R xs) = set xs" by (induction R xs rule: quicksort.induct) auto theorem sorted_wrt_quicksort: - assumes "transp R" and "totalp_on (set xs) R" and "reflp_on R (set xs)" + assumes "transp R" and "totalp_on (set xs) R" and "reflp_on (set xs) R" shows "sorted_wrt R (quicksort R xs)" using assms proof (induction R xs rule: quicksort.induct) case (2 R x xs) have total: "R a b" if "\ R b a" "a \ set (x#xs)" "b \ set (x#xs)" for a b using "2.prems" that unfolding totalp_on_def reflp_on_def by (cases "a = b") auto have "sorted_wrt R (quicksort R (filter (\y. R y x) xs))" "sorted_wrt R (quicksort R (filter (\y. \ R y x) xs))" using "2.prems" by (intro "2.IH"; auto simp: totalp_on_def reflp_on_def)+ then show ?case by (auto simp: sorted_wrt_append \transp R\ intro: transpD[OF \transp R\] dest!: total) qed auto text \ End of the material adapted from Eberl's \Quick_Sort_Cost\. \ lemma subsumes_list_subsumes_list_filter[abs_def, code_unfold]: "subsumes_list Ls Ks \ = subsumes_list_filter (quicksort leq_lit Ls) Ks \" by (rule trans[OF box_equals[OF _ subsumes_list_alt[symmetric] subsumes_list_alt[symmetric]] sorted_wrt_subsumes_list_subsumes_list_filter]) (auto simp: sorted_wrt_quicksort) end diff --git a/thys/Open_Induction/Restricted_Predicates.thy b/thys/Open_Induction/Restricted_Predicates.thy --- a/thys/Open_Induction/Restricted_Predicates.thy +++ b/thys/Open_Induction/Restricted_Predicates.thy @@ -1,687 +1,663 @@ (* Title: Well-Quasi-Orders Author: Christian Sternagel Maintainer: Christian Sternagel License: LGPL *) section \Binary Predicates Restricted to Elements of a Given Set\ theory Restricted_Predicates imports Main begin text \ A subset \C\ of \A\ is a \emph{chain} on \A\ (w.r.t.\ \P\) iff for all pairs of elements of \C\, one is less than or equal to the other one. \ abbreviation "chain_on P C A \ pred_on.chain A P C" lemmas chain_on_def = pred_on.chain_def lemma chain_on_subset: "A \ B \ chain_on P C A \ chain_on P C B" by (force simp: chain_on_def) lemma chain_on_imp_subset: "chain_on P C A \ C \ A" by (simp add: chain_on_def) lemma subchain_on: assumes "C \ D" and "chain_on P D A" shows "chain_on P C A" using assms by (auto simp: chain_on_def) definition restrict_to :: "('a \ 'a \ bool) \ 'a set \ ('a \ 'a \ bool)" where "restrict_to P A = (\x y. x \ A \ y \ A \ P x y)" -definition reflp_on :: "('a \ 'a \ bool) \ 'a set \ bool" where - "reflp_on P A \ (\a\A. P a a)" - definition transp_on :: "('a \ 'a \ bool) \ 'a set \ bool" where "transp_on P A \ (\x\A. \y\A. \z\A. P x y \ P y z \ P x z)" -definition total_on :: "('a \ 'a \ bool) \ 'a set \ bool" where - "total_on P A \ (\x\A. \y\A. x = y \ P x y \ P y x)" - abbreviation "strict P \ \x y. P x y \ \ (P y x)" abbreviation "incomparable P \ \x y. \ P x y \ \ P y x" abbreviation "antichain_on P f A \ \(i::nat) j. f i \ A \ (i < j \ incomparable P (f i) (f j))" lemma strict_reflclp_conv [simp]: "strict (P\<^sup>=\<^sup>=) = strict P" by auto -lemma reflp_onI [Pure.intro]: - "(\a. a \ A \ P a a) \ reflp_on P A" - unfolding reflp_on_def by blast - lemma transp_onI [Pure.intro]: "(\x y z. \x \ A; y \ A; z \ A; P x y; P y z\ \ P x z) \ transp_on P A" unfolding transp_on_def by blast -lemma total_onI [Pure.intro]: - "(\x y. \x \ A; y \ A\ \ x = y \ P x y \ P y x) \ total_on P A" - unfolding total_on_def by blast - lemma reflp_on_reflclp_simp [simp]: - assumes "reflp_on P A" and "a \ A" and "b \ A" + assumes "reflp_on A P" and "a \ A" and "b \ A" shows "P\<^sup>=\<^sup>= a b = P a b" using assms by (auto simp: reflp_on_def) -lemma reflp_on_reflclp: - "reflp_on (P\<^sup>=\<^sup>=) A" - by (auto simp: reflp_on_def) - -lemma reflp_on_converse_simp [simp]: - "reflp_on P\\ A \ reflp_on P A" - by (auto simp: reflp_on_def) +lemmas reflp_on_converse_simp = reflp_on_conversp lemma transp_on_converse: "transp_on P A \ transp_on P\\ A" unfolding transp_on_def by blast lemma transp_on_converse_simp [simp]: "transp_on P\\ A \ transp_on P A" unfolding transp_on_def by blast lemma transp_on_reflclp: "transp_on P A \ transp_on P\<^sup>=\<^sup>= A" unfolding transp_on_def by blast lemma transp_on_strict: "transp_on P A \ transp_on (strict P) A" unfolding transp_on_def by blast -lemma reflp_on_subset: - "A \ B \ reflp_on P B \ reflp_on P A" - by (auto simp: reflp_on_def) - lemma transp_on_subset: "A \ B \ transp_on P B \ transp_on P A" by (auto simp: transp_on_def) definition wfp_on :: "('a \ 'a \ bool) \ 'a set \ bool" where "wfp_on P A \ \ (\f. \i. f i \ A \ P (f (Suc i)) (f i))" definition inductive_on :: "('a \ 'a \ bool) \ 'a set \ bool" where "inductive_on P A \ (\Q. (\y\A. (\x\A. P x y \ Q x) \ Q y) \ (\x\A. Q x))" lemma inductive_onI [Pure.intro]: assumes "\Q x. \x \ A; (\y. \y \ A; \x. \x \ A; P x y\ \ Q x\ \ Q y)\ \ Q x" shows "inductive_on P A" using assms unfolding inductive_on_def by metis text \ If @{term P} is well-founded on @{term A} then every non-empty subset @{term Q} of @{term A} has a minimal element @{term z} w.r.t. @{term P}, i.e., all elements that are @{term P}-smaller than @{term z} are not in @{term Q}. \ lemma wfp_on_imp_minimal: assumes "wfp_on P A" shows "\Q x. x \ Q \ Q \ A \ (\z\Q. \y. P y z \ y \ Q)" proof (rule ccontr) assume "\ ?thesis" then obtain Q x where *: "x \ Q" "Q \ A" and "\z. \y. z \ Q \ P y z \ y \ Q" by metis from choice [OF this(3)] obtain f where **: "\x\Q. P (f x) x \ f x \ Q" by blast let ?S = "\i. (f ^^ i) x" have ***: "\i. ?S i \ Q" proof fix i show "?S i \ Q" by (induct i) (auto simp: * **) qed then have "\i. ?S i \ A" using * by blast moreover have "\i. P (?S (Suc i)) (?S i)" proof fix i show "P (?S (Suc i)) (?S i)" by (induct i) (auto simp: * ** ***) qed ultimately have "\i. ?S i \ A \ P (?S (Suc i)) (?S i)" by blast with assms(1) show False unfolding wfp_on_def by fast qed lemma minimal_imp_inductive_on: assumes "\Q x. x \ Q \ Q \ A \ (\z\Q. \y. P y z \ y \ Q)" shows "inductive_on P A" proof (rule ccontr) assume "\ ?thesis" then obtain Q x where *: "\y\A. (\x\A. P x y \ Q x) \ Q y" and **: "x \ A" "\ Q x" by (auto simp: inductive_on_def) let ?Q = "{x\A. \ Q x}" from ** have "x \ ?Q" by auto moreover have "?Q \ A" by auto ultimately obtain z where "z \ ?Q" and min: "\y. P y z \ y \ ?Q" using assms [THEN spec [of _ ?Q], THEN spec [of _ x]] by blast from \z \ ?Q\ have "z \ A" and "\ Q z" by auto with * obtain y where "y \ A" and "P y z" and "\ Q y" by auto then have "y \ ?Q" by auto with \P y z\ and min show False by auto qed lemmas wfp_on_imp_inductive_on = wfp_on_imp_minimal [THEN minimal_imp_inductive_on] lemma inductive_on_induct [consumes 2, case_names less, induct pred: inductive_on]: assumes "inductive_on P A" and "x \ A" and "\y. \ y \ A; \x. \ x \ A; P x y \ \ Q x \ \ Q y" shows "Q x" using assms unfolding inductive_on_def by metis lemma inductive_on_imp_wfp_on: assumes "inductive_on P A" shows "wfp_on P A" proof - let ?Q = "\x. \ (\f. f 0 = x \ (\i. f i \ A \ P (f (Suc i)) (f i)))" { fix x assume "x \ A" with assms have "?Q x" proof (induct rule: inductive_on_induct) fix y assume "y \ A" and IH: "\x. x \ A \ P x y \ ?Q x" show "?Q y" proof (rule ccontr) assume "\ ?Q y" then obtain f where *: "f 0 = y" "\i. f i \ A \ P (f (Suc i)) (f i)" by auto then have "P (f (Suc 0)) (f 0)" and "f (Suc 0) \ A" by auto with IH and * have "?Q (f (Suc 0))" by auto with * show False by auto qed qed } then show ?thesis unfolding wfp_on_def by blast qed definition antisymp_on :: "('a \ 'a \ bool) \ 'a set \ bool" where "antisymp_on P A \ (\a\A. \b\A. P a b \ P b a \ a = b)" lemma antisymp_onI [Pure.intro]: "(\a b. \a \ A; b \ A; P a b; P b a\ \ a = b) \ antisymp_on P A" by (auto simp: antisymp_on_def) lemma antisymp_on_reflclp [simp]: "antisymp_on P\<^sup>=\<^sup>= A = antisymp_on P A" by (auto simp: antisymp_on_def) definition qo_on :: "('a \ 'a \ bool) \ 'a set \ bool" where - "qo_on P A \ reflp_on P A \ transp_on P A" + "qo_on P A \ reflp_on A P \ transp_on P A" definition irreflp_on :: "('a \ 'a \ bool) \ 'a set \ bool" where "irreflp_on P A \ (\a\A. \ P a a)" definition po_on :: "('a \ 'a \ bool) \ 'a set \ bool" where "po_on P A \ (irreflp_on P A \ transp_on P A)" lemma po_onI [Pure.intro]: "\irreflp_on P A; transp_on P A\ \ po_on P A" by (auto simp: po_on_def) lemma irreflp_onI [Pure.intro]: "(\a. a \ A \ \ P a a) \ irreflp_on P A" unfolding irreflp_on_def by blast lemma irreflp_on_converse: "irreflp_on P A \ irreflp_on P\\ A" unfolding irreflp_on_def by blast lemma irreflp_on_converse_simp [simp]: "irreflp_on P\\ A \ irreflp_on P A" by (auto simp: irreflp_on_def) lemma po_on_converse_simp [simp]: "po_on P\\ A \ po_on P A" by (simp add: po_on_def) lemma po_on_imp_qo_on: "po_on P A \ qo_on (P\<^sup>=\<^sup>=) A" unfolding po_on_def qo_on_def by (metis reflp_on_reflclp transp_on_reflclp) lemma po_on_imp_irreflp_on: "po_on P A \ irreflp_on P A" by (auto simp: po_on_def) lemma po_on_imp_transp_on: "po_on P A \ transp_on P A" by (auto simp: po_on_def) lemma irreflp_on_subset: assumes "A \ B" and "irreflp_on P B" shows "irreflp_on P A" using assms by (auto simp: irreflp_on_def) lemma po_on_subset: assumes "A \ B" and "po_on P B" shows "po_on P A" using transp_on_subset and irreflp_on_subset and assms unfolding po_on_def by blast lemma transp_on_irreflp_on_imp_antisymp_on: assumes "transp_on P A" and "irreflp_on P A" shows "antisymp_on (P\<^sup>=\<^sup>=) A" proof fix a b assume "a \ A" and "b \ A" and "P\<^sup>=\<^sup>= a b" and "P\<^sup>=\<^sup>= b a" show "a = b" proof (rule ccontr) assume "a \ b" with \P\<^sup>=\<^sup>= a b\ and \P\<^sup>=\<^sup>= b a\ have "P a b" and "P b a" by auto with \transp_on P A\ and \a \ A\ and \b \ A\ have "P a a" unfolding transp_on_def by blast with \irreflp_on P A\ and \a \ A\ show False unfolding irreflp_on_def by blast qed qed lemma po_on_imp_antisymp_on: assumes "po_on P A" shows "antisymp_on P A" using transp_on_irreflp_on_imp_antisymp_on [of P A] and assms by (auto simp: po_on_def) lemma strict_reflclp [simp]: assumes "x \ A" and "y \ A" and "transp_on P A" and "irreflp_on P A" shows "strict (P\<^sup>=\<^sup>=) x y = P x y" using assms unfolding transp_on_def irreflp_on_def by blast lemma qo_on_imp_reflp_on: - "qo_on P A \ reflp_on P A" + "qo_on P A \ reflp_on A P" by (auto simp: qo_on_def) lemma qo_on_imp_transp_on: "qo_on P A \ transp_on P A" by (auto simp: qo_on_def) lemma qo_on_subset: "A \ B \ qo_on P B \ qo_on P A" unfolding qo_on_def using reflp_on_subset and transp_on_subset by blast text \ Quasi-orders are instances of the @{class preorder} class. \ lemma qo_on_UNIV_conv: "qo_on P UNIV \ class.preorder P (strict P)" (is "?lhs = ?rhs") proof assume "?lhs" then show "?rhs" unfolding qo_on_def class.preorder_def using qo_on_imp_reflp_on [of P UNIV] and qo_on_imp_transp_on [of P UNIV] by (auto simp: reflp_on_def) (unfold transp_on_def, blast) next assume "?rhs" then show "?lhs" unfolding class.preorder_def by (auto simp: qo_on_def reflp_on_def transp_on_def) qed lemma wfp_on_iff_inductive_on: "wfp_on P A \ inductive_on P A" by (blast intro: inductive_on_imp_wfp_on wfp_on_imp_inductive_on) lemma wfp_on_iff_minimal: "wfp_on P A \ (\Q x. x \ Q \ Q \ A \ (\z\Q. \y. P y z \ y \ Q))" using wfp_on_imp_minimal [of P A] and minimal_imp_inductive_on [of A P] and inductive_on_imp_wfp_on [of P A] by blast text \ Every non-empty well-founded set @{term A} has a minimal element, i.e., an element that is not greater than any other element. \ lemma wfp_on_imp_has_min_elt: assumes "wfp_on P A" and "A \ {}" shows "\x\A. \y\A. \ P y x" using assms unfolding wfp_on_iff_minimal by force lemma wfp_on_induct [consumes 2, case_names less, induct pred: wfp_on]: assumes "wfp_on P A" and "x \ A" and "\y. \ y \ A; \x. \ x \ A; P x y \ \ Q x \ \ Q y" shows "Q x" using assms and inductive_on_induct [of P A x] unfolding wfp_on_iff_inductive_on by blast lemma wfp_on_UNIV [simp]: "wfp_on P UNIV \ wfP P" unfolding wfp_on_iff_inductive_on inductive_on_def wfP_def wf_def by force subsection \Measures on Sets (Instead of Full Types)\ definition inv_image_betw :: "('b \ 'b \ bool) \ ('a \ 'b) \ 'a set \ 'b set \ ('a \ 'a \ bool)" where "inv_image_betw P f A B = (\x y. x \ A \ y \ A \ f x \ B \ f y \ B \ P (f x) (f y))" definition measure_on :: "('a \ nat) \ 'a set \ 'a \ 'a \ bool" where "measure_on f A = inv_image_betw (<) f A UNIV" lemma in_inv_image_betw [simp]: "inv_image_betw P f A B x y \ x \ A \ y \ A \ f x \ B \ f y \ B \ P (f x) (f y)" by (auto simp: inv_image_betw_def) lemma in_measure_on [simp, code_unfold]: "measure_on f A x y \ x \ A \ y \ A \ f x < f y" by (simp add: measure_on_def) lemma wfp_on_inv_image_betw [simp, intro!]: assumes "wfp_on P B" shows "wfp_on (inv_image_betw P f A B) A" (is "wfp_on ?P A") proof (rule ccontr) assume "\ ?thesis" then obtain g where "\i. g i \ A \ ?P (g (Suc i)) (g i)" by (auto simp: wfp_on_def) with assms show False by (auto simp: wfp_on_def) qed lemma wfp_less: "wfp_on (<) (UNIV :: nat set)" using wf_less by (auto simp: wfP_def) lemma wfp_on_measure_on [iff]: "wfp_on (measure_on f A) A" unfolding measure_on_def by (rule wfp_less [THEN wfp_on_inv_image_betw]) lemma wfp_on_mono: "A \ B \ (\x y. x \ A \ y \ A \ P x y \ Q x y) \ wfp_on Q B \ wfp_on P A" unfolding wfp_on_def by (metis subsetD) lemma wfp_on_subset: "A \ B \ wfp_on P B \ wfp_on P A" using wfp_on_mono by blast lemma restrict_to_iff [iff]: "restrict_to P A x y \ x \ A \ y \ A \ P x y" by (simp add: restrict_to_def) lemma wfp_on_restrict_to [simp]: "wfp_on (restrict_to P A) A = wfp_on P A" by (auto simp: wfp_on_def) lemma irreflp_on_strict [simp, intro]: "irreflp_on (strict P) A" by (auto simp: irreflp_on_def) lemma transp_on_map': assumes "transp_on Q B" and "g ` A \ B" and "h ` A \ B" and "\x. x \ A \ Q\<^sup>=\<^sup>= (h x) (g x)" shows "transp_on (\x y. Q (g x) (h y)) A" using assms unfolding transp_on_def by auto (metis imageI subsetD) lemma transp_on_map: assumes "transp_on Q B" and "h ` A \ B" shows "transp_on (\x y. Q (h x) (h y)) A" using transp_on_map' [of Q B h A h, simplified, OF assms] by blast lemma irreflp_on_map: assumes "irreflp_on Q B" and "h ` A \ B" shows "irreflp_on (\x y. Q (h x) (h y)) A" using assms unfolding irreflp_on_def by auto lemma po_on_map: assumes "po_on Q B" and "h ` A \ B" shows "po_on (\x y. Q (h x) (h y)) A" using assms and transp_on_map and irreflp_on_map unfolding po_on_def by auto lemma chain_transp_on_less: assumes "\i. f i \ A \ P (f i) (f (Suc i))" and "transp_on P A" and "i < j" shows "P (f i) (f j)" using \i < j\ proof (induct j) case 0 then show ?case by simp next case (Suc j) show ?case proof (cases "i = j") case True with Suc show ?thesis using assms(1) by simp next case False with Suc have "P (f i) (f j)" by force moreover from assms have "P (f j) (f (Suc j))" by auto ultimately show ?thesis using assms(1, 2) unfolding transp_on_def by blast qed qed lemma wfp_on_imp_irreflp_on: assumes "wfp_on P A" shows "irreflp_on P A" proof fix x assume "x \ A" show "\ P x x" proof let ?f = "\_. x" assume "P x x" then have "\i. P (?f (Suc i)) (?f i)" by blast with \x \ A\ have "\ wfp_on P A" by (auto simp: wfp_on_def) with assms show False by contradiction qed qed inductive accessible_on :: "('a \ 'a \ bool) \ 'a set \ 'a \ bool" for P and A where accessible_onI [Pure.intro]: "\x \ A; \y. \y \ A; P y x\ \ accessible_on P A y\ \ accessible_on P A x" lemma accessible_on_imp_mem: assumes "accessible_on P A a" shows "a \ A" using assms by (induct) auto lemma accessible_on_induct [consumes 1, induct pred: accessible_on]: assumes *: "accessible_on P A a" and IH: "\x. \accessible_on P A x; \y. \y \ A; P y x\ \ Q y\ \ Q x" shows "Q a" by (rule * [THEN accessible_on.induct]) (auto intro: IH accessible_onI) lemma accessible_on_downward: "accessible_on P A b \ a \ A \ P a b \ accessible_on P A a" by (cases rule: accessible_on.cases) fast lemma accessible_on_restrict_to_downwards: assumes "(restrict_to P A)\<^sup>+\<^sup>+ a b" and "accessible_on P A b" shows "accessible_on P A a" using assms by (induct) (auto dest: accessible_on_imp_mem accessible_on_downward) lemma accessible_on_imp_inductive_on: assumes "\x\A. accessible_on P A x" shows "inductive_on P A" proof fix Q x assume "x \ A" and *: "\y. \y \ A; \x. \x \ A; P x y\ \ Q x\ \ Q y" with assms have "accessible_on P A x" by auto then show "Q x" proof (induct) case (1 z) then have "z \ A" by (blast dest: accessible_on_imp_mem) show ?case by (rule *) fact+ qed qed lemmas accessible_on_imp_wfp_on = accessible_on_imp_inductive_on [THEN inductive_on_imp_wfp_on] lemma wfp_on_tranclp_imp_wfp_on: assumes "wfp_on (P\<^sup>+\<^sup>+) A" shows "wfp_on P A" by (rule ccontr) (insert assms, auto simp: wfp_on_def) lemma inductive_on_imp_accessible_on: assumes "inductive_on P A" shows "\x\A. accessible_on P A x" proof fix x assume "x \ A" with assms show "accessible_on P A x" by (induct) (auto intro: accessible_onI) qed lemma inductive_on_accessible_on_conv: "inductive_on P A \ (\x\A. accessible_on P A x)" using inductive_on_imp_accessible_on and accessible_on_imp_inductive_on by blast lemmas wfp_on_imp_accessible_on = wfp_on_imp_inductive_on [THEN inductive_on_imp_accessible_on] lemma wfp_on_accessible_on_iff: "wfp_on P A \ (\x\A. accessible_on P A x)" by (blast dest: wfp_on_imp_accessible_on accessible_on_imp_wfp_on) lemma accessible_on_tranclp: assumes "accessible_on P A x" shows "accessible_on ((restrict_to P A)\<^sup>+\<^sup>+) A x" (is "accessible_on ?P A x") using assms proof (induct) case (1 x) then have "x \ A" by (blast dest: accessible_on_imp_mem) then show ?case proof (rule accessible_onI) fix y assume "y \ A" assume "?P y x" then show "accessible_on ?P A y" proof (cases) assume "restrict_to P A y x" with 1 and \y \ A\ show ?thesis by blast next fix z assume "?P y z" and "restrict_to P A z x" with 1 have "accessible_on ?P A z" by (auto simp: restrict_to_def) from accessible_on_downward [OF this \y \ A\ \?P y z\] show ?thesis . qed qed qed lemma wfp_on_restrict_to_tranclp: assumes "wfp_on P A" shows "wfp_on ((restrict_to P A)\<^sup>+\<^sup>+) A" using wfp_on_imp_accessible_on [OF assms] and accessible_on_tranclp [of P A] and accessible_on_imp_wfp_on [of A "(restrict_to P A)\<^sup>+\<^sup>+"] by blast lemma wfp_on_restrict_to_tranclp': assumes "wfp_on (restrict_to P A)\<^sup>+\<^sup>+ A" shows "wfp_on P A" by (rule ccontr) (insert assms, auto simp: wfp_on_def) lemma wfp_on_restrict_to_tranclp_wfp_on_conv: "wfp_on (restrict_to P A)\<^sup>+\<^sup>+ A \ wfp_on P A" using wfp_on_restrict_to_tranclp [of P A] and wfp_on_restrict_to_tranclp' [of P A] by blast lemma tranclp_idemp [simp]: "(P\<^sup>+\<^sup>+)\<^sup>+\<^sup>+ = P\<^sup>+\<^sup>+" (is "?l = ?r") proof (intro ext) fix x y show "?l x y = ?r x y" proof assume "?l x y" then show "?r x y" by (induct) auto next assume "?r x y" then show "?l x y" by (induct) auto qed qed (*TODO: move the following 3 lemmas to Transitive_Closure?*) lemma stepfun_imp_tranclp: assumes "f 0 = x" and "f (Suc n) = z" and "\i\n. P (f i) (f (Suc i))" shows "P\<^sup>+\<^sup>+ x z" using assms by (induct n arbitrary: x z) (auto intro: tranclp.trancl_into_trancl) lemma tranclp_imp_stepfun: assumes "P\<^sup>+\<^sup>+ x z" shows "\f n. f 0 = x \ f (Suc n) = z \ (\i\n. P (f i) (f (Suc i)))" (is "\f n. ?P x z f n") using assms proof (induct rule: tranclp_induct) case (base y) let ?f = "(\_. y)(0 := x)" have "?f 0 = x" and "?f (Suc 0) = y" by auto moreover have "\i\0. P (?f i) (?f (Suc i))" using base by auto ultimately show ?case by blast next case (step y z) then obtain f n where IH: "?P x y f n" by blast then have *: "\i\n. P (f i) (f (Suc i))" and [simp]: "f 0 = x" "f (Suc n) = y" by auto let ?n = "Suc n" let ?f = "f(Suc ?n := z)" have "?f 0 = x" and "?f (Suc ?n) = z" by auto moreover have "\i\?n. P (?f i) (?f (Suc i))" using \P y z\ and * by auto ultimately show ?case by blast qed lemma tranclp_stepfun_conv: "P\<^sup>+\<^sup>+ x y \ (\f n. f 0 = x \ f (Suc n) = y \ (\i\n. P (f i) (f (Suc i))))" using tranclp_imp_stepfun and stepfun_imp_tranclp by metis subsection \Facts About Predecessor Sets\ lemma qo_on_predecessor_subset_conv': assumes "qo_on P A" and "B \ A" and "C \ A" shows "{x\A. \y\B. P x y} \ {x\A. \y\C. P x y} \ (\x\B. \y\C. P x y)" using assms by (auto simp: subset_eq qo_on_def reflp_on_def, unfold transp_on_def) metis+ lemma qo_on_predecessor_subset_conv: "\qo_on P A; x \ A; y \ A\ \ {z\A. P z x} \ {z\A. P z y} \ P x y" using qo_on_predecessor_subset_conv' [of P A "{x}" "{y}"] by simp lemma po_on_predecessors_eq_conv: assumes "po_on P A" and "x \ A" and "y \ A" shows "{z\A. P\<^sup>=\<^sup>= z x} = {z\A. P\<^sup>=\<^sup>= z y} \ x = y" using assms(2-) - and reflp_on_reflclp [of P A] + and reflp_on_reflclp [of A P] and po_on_imp_antisymp_on [OF \po_on P A\] unfolding antisymp_on_def reflp_on_def by blast lemma restrict_to_rtranclp: assumes "transp_on P A" and "x \ A" and "y \ A" shows "(restrict_to P A)\<^sup>*\<^sup>* x y \ P\<^sup>=\<^sup>= x y" proof - { assume "(restrict_to P A)\<^sup>*\<^sup>* x y" then have "P\<^sup>=\<^sup>= x y" using assms by (induct) (auto, unfold transp_on_def, blast) } with assms show ?thesis by auto qed lemma reflp_on_restrict_to_rtranclp: - assumes "reflp_on P A" and "transp_on P A" + assumes "reflp_on A P" and "transp_on P A" and "x \ A" and "y \ A" shows "(restrict_to P A)\<^sup>*\<^sup>* x y \ P x y" unfolding restrict_to_rtranclp [OF assms(2-)] unfolding reflp_on_reflclp_simp [OF assms(1, 3-)] .. end 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 \ + \totalp_on (insert x (set xs)) R \ 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) + (auto dest: transpD reflpD simp: totalp_on_def) lemma sorted_wrt_insort_key_rel2: - \total_on R (insert x (set xs)) \ transp R \ x \ set xs \ + \totalp_on (insert x (set xs)) R \ 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) + (auto dest: transpD simp: totalp_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 (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_Polynomials_Operations.thy b/thys/PAC_Checker/PAC_Polynomials_Operations.thy --- a/thys/PAC_Checker/PAC_Polynomials_Operations.thy +++ b/thys/PAC_Checker/PAC_Polynomials_Operations.thy @@ -1,1272 +1,1271 @@ theory PAC_Polynomials_Operations imports PAC_Polynomials_Term PAC_Checker_Specification begin subsection \Addition\ text \In this section, we refine the polynomials to list. These lists will be used in our checker to represent the polynomials and execute operations. There is one \<^emph>\key\ difference between the list representation and the usual representation: in the former, coefficients can be zero and monomials can appear several times. This makes it easier to reason on intermediate representation where this has not yet been sanitized. \ fun add_poly_l' :: \llist_polynomial \ llist_polynomial \ llist_polynomial\ where \add_poly_l' (p, []) = p\ | \add_poly_l' ([], q) = q\ | \add_poly_l' ((xs, n) # p, (ys, m) # q) = (if xs = ys then if n + m = 0 then add_poly_l' (p, q) else let pq = add_poly_l' (p, q) in ((xs, n + m) # pq) else if (xs, ys) \ term_order_rel then let pq = add_poly_l' (p, (ys, m) # q) in ((xs, n) # pq) else let pq = add_poly_l' ((xs, n) # p, q) in ((ys, m) # pq) )\ definition add_poly_l :: \llist_polynomial \ llist_polynomial \ llist_polynomial nres\ where \add_poly_l = REC\<^sub>T (\add_poly_l (p, q). case (p,q) of (p, []) \ RETURN p | ([], q) \ RETURN q | ((xs, n) # p, (ys, m) # q) \ (if xs = ys then if n + m = 0 then add_poly_l (p, q) else do { pq \ add_poly_l (p, q); RETURN ((xs, n + m) # pq) } else if (xs, ys) \ term_order_rel then do { pq \ add_poly_l (p, (ys, m) # q); RETURN ((xs, n) # pq) } else do { pq \ add_poly_l ((xs, n) # p, q); RETURN ((ys, m) # pq) }))\ definition nonzero_coeffs where \nonzero_coeffs a \ 0 \# snd `# a\ lemma nonzero_coeffs_simps[simp]: \nonzero_coeffs {#}\ \nonzero_coeffs (add_mset (xs, n) a) \ nonzero_coeffs a \ n \ 0\ by (auto simp: nonzero_coeffs_def) lemma nonzero_coeffsD: \nonzero_coeffs a \ (x, n) \# a \ n \ 0\ by (auto simp: nonzero_coeffs_def) lemma sorted_poly_list_rel_ConsD: \((ys, n) # p, a) \ sorted_poly_list_rel S \ (p, remove1_mset (mset ys, n) a) \ sorted_poly_list_rel S \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys \ ys \ set (map fst p) \ n \ 0 \ nonzero_coeffs a\ unfolding sorted_poly_list_rel_wrt_def prod.case mem_Collect_eq list_rel_def apply (clarsimp) apply (subst (asm) list.rel_sel) apply (intro conjI) apply (rename_tac y, rule_tac b = \tl y\ in relcompI) apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def list.tl_def term_poly_list_rel_def nonzero_coeffs_def split: list.splits) done lemma sorted_poly_list_rel_Cons_iff: \((ys, n) # p, a) \ sorted_poly_list_rel S \ (p, remove1_mset (mset ys, n) a) \ sorted_poly_list_rel S \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys \ ys \ set (map fst p) \ n \ 0 \ nonzero_coeffs a\ apply (rule iffI) subgoal by (auto dest!: sorted_poly_list_rel_ConsD) subgoal unfolding sorted_poly_list_rel_wrt_def prod.case mem_Collect_eq list_rel_def apply (clarsimp) apply (intro conjI) apply (rename_tac y; rule_tac b = \(mset ys, n) # y\ in relcompI) by (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def term_poly_list_rel_def add_mset_eq_add_mset eq_commute[of _ \mset _\] nonzero_coeffs_def dest!: multi_member_split) done lemma sorted_repeat_poly_list_rel_ConsD: \((ys, n) # p, a) \ sorted_repeat_poly_list_rel S \ (p, remove1_mset (mset ys, n) a) \ sorted_repeat_poly_list_rel S \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys \ n \ 0 \ nonzero_coeffs a\ unfolding sorted_repeat_poly_list_rel_wrt_def prod.case mem_Collect_eq list_rel_def apply (clarsimp) apply (subst (asm) list.rel_sel) apply (intro conjI) apply (rename_tac y, rule_tac b = \tl y\ in relcompI) apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def list.tl_def term_poly_list_rel_def nonzero_coeffs_def split: list.splits) done lemma sorted_repeat_poly_list_rel_Cons_iff: \((ys, n) # p, a) \ sorted_repeat_poly_list_rel S \ (p, remove1_mset (mset ys, n) a) \ sorted_repeat_poly_list_rel S \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys \ n \ 0 \ nonzero_coeffs a\ apply (rule iffI) subgoal by (auto dest!: sorted_repeat_poly_list_rel_ConsD) subgoal unfolding sorted_repeat_poly_list_rel_wrt_def prod.case mem_Collect_eq list_rel_def apply (clarsimp) apply (intro conjI) apply (rename_tac y, rule_tac b = \(mset ys, n) # y\ in relcompI) by (auto simp: sorted_repeat_poly_list_rel_wrt_def list_mset_rel_def br_def term_poly_list_rel_def add_mset_eq_add_mset eq_commute[of _ \mset _\] nonzero_coeffs_def dest!: multi_member_split) done lemma add_poly_p_add_mset_sum_0: \n + m = 0 \add_poly_p\<^sup>*\<^sup>* (A, Aa, {#}) ({#}, {#}, r) \ add_poly_p\<^sup>*\<^sup>* (add_mset (mset ys, n) A, add_mset (mset ys, m) Aa, {#}) ({#}, {#}, r)\ apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_new_coeff_r) apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_same_coeff_l) apply (rule converse_rtranclp_into_rtranclp) apply (auto intro: add_poly_p.rem_0_coeff) done lemma monoms_add_poly_l'D: \(aa, ba) \ set (add_poly_l' x) \ aa \ fst ` set (fst x) \ aa \ fst ` set (snd x)\ by (induction x rule: add_poly_l'.induct) (auto split: if_splits) lemma add_poly_p_add_to_result: \add_poly_p\<^sup>*\<^sup>* (A, B, r) (A', B', r') \ add_poly_p\<^sup>*\<^sup>* (A, B, p + r) (A', B', p + r')\ apply (induction rule: rtranclp_induct[of add_poly_p \(_, _, _)\ \(_, _, _)\, split_format(complete), of for r]) subgoal by auto by (elim add_poly_pE) (metis (no_types, lifting) Pair_inject add_poly_p.intros rtranclp.simps union_mset_add_mset_right)+ lemma add_poly_p_add_mset_comb: \add_poly_p\<^sup>*\<^sup>* (A, Aa, {#}) ({#}, {#}, r) \ add_poly_p\<^sup>*\<^sup>* (add_mset (xs, n) A, Aa, {#}) ({#}, {#}, add_mset (xs, n) r)\ apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_new_coeff_l) using add_poly_p_add_to_result[of A Aa \{#}\ \{#}\ \{#}\ r \{#(xs, n)#}\] by auto lemma add_poly_p_add_mset_comb2: \add_poly_p\<^sup>*\<^sup>* (A, Aa, {#}) ({#}, {#}, r) \ add_poly_p\<^sup>*\<^sup>* (add_mset (ys, n) A, add_mset (ys, m) Aa, {#}) ({#}, {#}, add_mset (ys, n + m) r)\ apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_new_coeff_r) apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_same_coeff_l) using add_poly_p_add_to_result[of A Aa \{#}\ \{#}\ \{#}\ r \{#(ys, n+m)#}\] by auto lemma add_poly_p_add_mset_comb3: \add_poly_p\<^sup>*\<^sup>* (A, Aa, {#}) ({#}, {#}, r) \ add_poly_p\<^sup>*\<^sup>* (A, add_mset (ys, m) Aa, {#}) ({#}, {#}, add_mset (ys, m) r)\ apply (rule converse_rtranclp_into_rtranclp) apply (rule add_poly_p.add_new_coeff_r) using add_poly_p_add_to_result[of A Aa \{#}\ \{#}\ \{#}\ r \{#(ys, m)#}\] by auto lemma total_on_lexord: \Relation.total_on UNIV R \ Relation.total_on UNIV (lexord R)\ apply (auto simp: Relation.total_on_def) by (meson lexord_linear) lemma antisym_lexord: \antisym R \ irrefl R \ antisym (lexord R)\ by (auto simp: antisym_def lexord_def irrefl_def elim!: list_match_lel_lel) lemma less_than_char_linear: \(a, b) \ less_than_char \ a = b \ (b, a) \ less_than_char\ by (auto simp: less_than_char_def) lemma total_on_lexord_less_than_char_linear: \xs \ ys \ (xs, ys) \ lexord (lexord less_than_char) \ (ys, xs) \ lexord (lexord less_than_char)\ using lexord_linear[of \lexord less_than_char\ xs ys] using lexord_linear[of \less_than_char\] less_than_char_linear using lexord_irrefl[OF irrefl_less_than_char] antisym_lexord[OF antisym_lexord[OF antisym_less_than_char irrefl_less_than_char]] apply (auto simp: antisym_def Relation.total_on_def) done lemma sorted_poly_list_rel_nonzeroD: \(p, r) \ sorted_poly_list_rel term_order \ nonzero_coeffs (r)\ \(p, r) \ sorted_poly_list_rel (rel2p (lexord (lexord less_than_char))) \ nonzero_coeffs (r)\ by (auto simp: sorted_poly_list_rel_wrt_def nonzero_coeffs_def) lemma add_poly_l'_add_poly_p: assumes \(pq, pq') \ sorted_poly_rel \\<^sub>r sorted_poly_rel\ shows \\r. (add_poly_l' pq, r) \ sorted_poly_rel \ add_poly_p\<^sup>*\<^sup>* (fst pq', snd pq', {#}) ({#}, {#}, r)\ supply [[goals_limit=1]] using assms apply (induction \pq\ arbitrary: pq' rule: add_poly_l'.induct) subgoal for p pq' using add_poly_p_empty_l[of \fst pq'\ \{#}\ \{#}\] by (cases pq') (auto intro!: exI[of _ \fst pq'\]) subgoal for x p pq' using add_poly_p_empty_r[of \{#}\ \snd pq'\ \{#}\] by (cases pq') (auto intro!: exI[of _ \snd pq'\]) subgoal premises p for xs n p ys m q pq' apply (cases pq') \ \Isabelle does a completely stupid case distinction here\ apply (cases \xs = ys\) subgoal apply (cases \n + m = 0\) subgoal using p(1)[of \(remove1_mset (mset xs, n) (fst pq'), remove1_mset (mset ys, m) (snd pq'))\] p(5-) apply (auto dest!: sorted_poly_list_rel_ConsD multi_member_split ) using add_poly_p_add_mset_sum_0 by blast subgoal using p(2)[of \(remove1_mset (mset xs, n) (fst pq'), remove1_mset (mset ys, m) (snd pq'))\] p(5-) apply (auto dest!: sorted_poly_list_rel_ConsD multi_member_split) apply (rule_tac x = \add_mset (mset ys, n + m) r\ in exI) apply (fastforce dest!: monoms_add_poly_l'D simp: sorted_poly_list_rel_Cons_iff rel2p_def sorted_poly_list_rel_nonzeroD var_order_rel_def intro: add_poly_p_add_mset_comb2) done done subgoal apply (cases \(xs, ys) \ term_order_rel\) subgoal using p(3)[of \(remove1_mset (mset xs, n) (fst pq'), (snd pq'))\] p(5-) apply (auto dest!: multi_member_split simp: sorted_poly_list_rel_Cons_iff rel2p_def) apply (rule_tac x = \add_mset (mset xs, n) r\ in exI) apply (auto dest!: monoms_add_poly_l'D) apply (auto intro: lexord_trans add_poly_p_add_mset_comb simp: lexord_transI var_order_rel_def) apply (rule lexord_trans) apply assumption apply (auto intro: lexord_trans add_poly_p_add_mset_comb simp: lexord_transI sorted_poly_list_rel_nonzeroD var_order_rel_def) using total_on_lexord_less_than_char_linear by fastforce subgoal using p(4)[of \(fst pq', remove1_mset (mset ys, m) (snd pq'))\] p(5-) apply (auto dest!: multi_member_split simp: sorted_poly_list_rel_Cons_iff rel2p_def var_order_rel_def) apply (rule_tac x = \add_mset (mset ys, m) r\ in exI) apply (auto dest!: monoms_add_poly_l'D simp: total_on_lexord_less_than_char_linear) apply (auto intro: lexord_trans add_poly_p_add_mset_comb simp: lexord_transI total_on_lexord_less_than_char_linear var_order_rel_def) apply (rule lexord_trans) apply assumption apply (auto intro: lexord_trans add_poly_p_add_mset_comb3 simp: lexord_transI sorted_poly_list_rel_nonzeroD var_order_rel_def) using total_on_lexord_less_than_char_linear by fastforce done done done lemma add_poly_l_add_poly: \add_poly_l x = RETURN (add_poly_l' x)\ unfolding add_poly_l_def by (induction x rule: add_poly_l'.induct) (solves \subst RECT_unfold, refine_mono, simp split: list.split\)+ lemma add_poly_l_spec: \(add_poly_l, uncurry (\p q. SPEC(\r. add_poly_p\<^sup>*\<^sup>* (p, q, {#}) ({#}, {#}, r)))) \ sorted_poly_rel \\<^sub>r sorted_poly_rel \\<^sub>f \sorted_poly_rel\nres_rel\ unfolding add_poly_l_add_poly apply (intro nres_relI frefI) apply (drule add_poly_l'_add_poly_p) apply (auto simp: conc_fun_RES) done definition sort_poly_spec :: \llist_polynomial \ llist_polynomial nres\ where \sort_poly_spec p = SPEC(\p'. mset p = mset p' \ sorted_wrt (rel2p (Id \ term_order_rel)) (map fst p'))\ lemma sort_poly_spec_id: assumes \(p, p') \ unsorted_poly_rel\ shows \sort_poly_spec p \ \ (sorted_repeat_poly_rel) (RETURN p')\ proof - obtain y where py: \(p, y) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ and p'_y: \p' = mset y\ and zero: \0 \# snd `# p'\ using assms unfolding sort_poly_spec_def poly_list_rel_def sorted_poly_list_rel_wrt_def by (auto simp: list_mset_rel_def br_def) then have [simp]: \length y = length p\ by (auto simp: list_rel_def list_all2_conv_all_nth) have H: \(x, p') \ \term_poly_list_rel \\<^sub>r int_rel\list_rel O list_mset_rel\ if px: \mset p = mset x\ and \sorted_wrt (rel2p (Id \ lexord var_order_rel)) (map fst x)\ for x :: \llist_polynomial\ proof - from px have \length x = length p\ by (metis size_mset) from px have \mset x = mset p\ by simp then obtain f where \f permutes {.. \permute_list f p = x\ by (rule mset_eq_permutation) with \length x = length p\ have f: \bij_betw f {.. by (simp add: permutes_imp_bij) from \f permutes {.. \permute_list f p = x\ [symmetric] have [simp]: \\i. i < length x \ x ! i = p ! (f i)\ by (simp add: permute_list_nth) let ?y = \map (\i. y ! f i) [0 ..< length x]\ have \i < length y \ (p ! f i, y ! f i) \ term_poly_list_rel \\<^sub>r int_rel\ for i using list_all2_nthD[of _ p y \f i\, OF py[unfolded list_rel_def mem_Collect_eq prod.case]] mset_eq_length[OF px] f by (auto simp: list_rel_def list_all2_conv_all_nth bij_betw_def) then have \(x, ?y) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ and xy: \length x = length y\ using py list_all2_nthD[of \rel2p (term_poly_list_rel \\<^sub>r int_rel)\ p y \f i\ for i, simplified] mset_eq_length[OF px] by (auto simp: list_rel_def list_all2_conv_all_nth) moreover { have f: \mset_set {0.. using f mset_eq_length[OF px] by (auto simp: bij_betw_def lessThan_atLeast0 image_mset_mset_set) have \mset y = {#y ! f x. x \# mset_set {0.. by (subst drop_0[symmetric], subst mset_drop_upto, subst xy[symmetric], subst f) auto then have \(?y, p') \ list_mset_rel\ by (auto simp: list_mset_rel_def br_def p'_y) } ultimately show ?thesis by (auto intro!: relcompI[of _ ?y]) qed show ?thesis using zero unfolding sort_poly_spec_def poly_list_rel_def sorted_repeat_poly_list_rel_wrt_def by refine_rcg (auto intro: H) qed subsection \Multiplication\ fun mult_monoms :: \term_poly_list \ term_poly_list \ term_poly_list\ where \mult_monoms p [] = p\ | \mult_monoms [] p = p\ | \mult_monoms (x # p) (y # q) = (if x = y then x # mult_monoms p q else if (x, y) \ var_order_rel then x # mult_monoms p (y # q) else y # mult_monoms (x # p) q)\ lemma term_poly_list_rel_empty_iff[simp]: \([], q') \ term_poly_list_rel \ q' = {#}\ by (auto simp: term_poly_list_rel_def) lemma mset_eqD_set_mset: \mset xs = A \ set xs = set_mset A\ by auto lemma term_poly_list_rel_Cons_iff: \(y # p, p') \ term_poly_list_rel \ (p, remove1_mset y p') \ term_poly_list_rel \ y \# p' \ y \ set p \ y \# remove1_mset y p' \ (\x\#mset p. (y, x) \ var_order_rel)\ by (auto simp: term_poly_list_rel_def rel2p_def dest!: multi_member_split mset_eqD_set_mset) lemma var_order_rel_antisym[simp]: \(y, y) \ var_order_rel\ by (simp add: less_than_char_def lexord_irreflexive var_order_rel_def) lemma term_poly_list_rel_remdups_mset: \(p, p') \ term_poly_list_rel \ (p, remdups_mset p') \ term_poly_list_rel\ by (auto simp: term_poly_list_rel_def distinct_mset_remdups_mset_id simp flip: distinct_mset_mset_distinct) lemma var_notin_notin_mult_monomsD: \y \ set (mult_monoms p q) \ y \ set p \ y \ set q\ by (induction p q arbitrary: p' q' rule: mult_monoms.induct) (auto split: if_splits) lemma term_poly_list_rel_set_mset: \(p, q) \ term_poly_list_rel \ set p = set_mset q\ by (auto simp: term_poly_list_rel_def) lemma mult_monoms_spec: \(mult_monoms, (\a b. remdups_mset (a + b))) \ term_poly_list_rel \ term_poly_list_rel \ term_poly_list_rel\ proof - have [dest]: \remdups_mset (A + Aa) = add_mset y Ab \ y \# A \ y \# Aa \ False\ for Aa Ab y A by (metis set_mset_remdups_mset union_iff union_single_eq_member) show ?thesis apply (intro fun_relI) apply (rename_tac p p' q q') subgoal for p p' q q' apply (induction p q arbitrary: p' q' rule: mult_monoms.induct) subgoal by (auto simp: term_poly_list_rel_Cons_iff rel2p_def term_poly_list_rel_remdups_mset) subgoal for x p p' q' by (auto simp: term_poly_list_rel_Cons_iff rel2p_def term_poly_list_rel_remdups_mset dest!: multi_member_split[of _ q']) subgoal premises p for x p y q p' q' apply (cases \x = y\) subgoal using p(1)[of \remove1_mset y p'\ \remove1_mset y q'\] p(4-) by (auto simp: term_poly_list_rel_Cons_iff rel2p_def dest!: var_notin_notin_mult_monomsD dest!: multi_member_split) apply (cases \(x, y) \ var_order_rel\) subgoal using p(2)[of \remove1_mset x p'\ \q'\] p(4-) apply (auto simp: term_poly_list_rel_Cons_iff term_poly_list_rel_set_mset rel2p_def var_order_rel_def dest!: multi_member_split[of _ p'] multi_member_split[of _ q'] var_notin_notin_mult_monomsD split: if_splits) apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear) apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear) apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear) using lexord_trans trans_less_than_char var_order_rel_antisym unfolding var_order_rel_def apply blast+ done subgoal using p(3)[of \p'\ \remove1_mset y q'\] p(4-) apply (auto simp: term_poly_list_rel_Cons_iff rel2p_def term_poly_list_rel_set_mset rel2p_def var_order_rel_antisym dest!: multi_member_split[of _ p'] multi_member_split[of _ q'] var_notin_notin_mult_monomsD split: if_splits) using lexord_trans trans_less_than_char var_order_rel_antisym unfolding var_order_rel_def apply blast apply (meson lexord_cons_cons list.inject total_on_lexord_less_than_char_linear) by (meson less_than_char_linear lexord_linear lexord_trans trans_less_than_char) done done done qed definition mult_monomials :: \term_poly_list \ int \ term_poly_list \ int \ term_poly_list \ int\ where \mult_monomials = (\(x, a) (y, b). (mult_monoms x y, a * b))\ definition mult_poly_raw :: \llist_polynomial \ llist_polynomial \ llist_polynomial\ where \mult_poly_raw p q = foldl (\b x. map (mult_monomials x) q @ b) [] p\ fun map_append where \map_append f b [] = b\ | \map_append f b (x # xs) = f x # map_append f b xs\ lemma map_append_alt_def: \map_append f b xs = map f xs @ b\ by (induction f b xs rule: map_append.induct) auto lemma foldl_append_empty: \NO_MATCH [] xs \ foldl (\b x. f x @ b) xs p = foldl (\b x. f x @ b) [] p @ xs\ apply (induction p arbitrary: xs) apply simp by (metis (mono_tags, lifting) NO_MATCH_def append.assoc append_self_conv foldl_Cons) lemma poly_list_rel_empty_iff[simp]: \([], r) \ poly_list_rel R \ r = {#}\ by (auto simp: poly_list_rel_def list_mset_rel_def br_def) lemma mult_poly_raw_simp[simp]: \mult_poly_raw [] q = []\ \mult_poly_raw (x # p) q = mult_poly_raw p q @ map (mult_monomials x) q\ subgoal by (auto simp: mult_poly_raw_def) subgoal by (induction p) (auto simp: mult_poly_raw_def foldl_append_empty) done lemma sorted_poly_list_relD: \(q, q') \ sorted_poly_list_rel R \ q' = (\(a, b). (mset a, b)) `# mset q\ apply (induction q arbitrary: q') apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def list_rel_split_right_iff) apply (subst (asm)(2) term_poly_list_rel_def) apply (simp add: relcomp.relcompI) done lemma list_all2_in_set_ExD: \list_all2 R p q \ x \ set p \ \y \ set q. R x y\ by (induction p q rule: list_all2_induct) auto inductive_cases mult_poly_p_elim: \mult_poly_p q (A, r) (B, r')\ lemma mult_poly_p_add_mset_same: \(mult_poly_p q')\<^sup>*\<^sup>* (A, r) (B, r') \ (mult_poly_p q')\<^sup>*\<^sup>* (add_mset x A, r) (add_mset x B, r')\ apply (induction rule: rtranclp_induct[of \mult_poly_p q'\ \(_, r)\ \(p', q'')\ for p' q'', split_format(complete)]) subgoal by simp apply (rule rtranclp.rtrancl_into_rtrancl) apply assumption by (auto elim!: mult_poly_p_elim intro: mult_poly_p.intros intro: rtranclp.rtrancl_into_rtrancl simp: add_mset_commute[of x]) lemma mult_poly_raw_mult_poly_p: assumes \(p, p') \ sorted_poly_rel\ and \(q, q') \ sorted_poly_rel\ shows \\r. (mult_poly_raw p q, r) \ unsorted_poly_rel \ (mult_poly_p q')\<^sup>*\<^sup>* (p', {#}) ({#}, r)\ proof - have H: \(q, q') \ sorted_poly_list_rel term_order \ n < length q \ distinct aa \ sorted_wrt var_order aa \ (mult_monoms aa (fst (q ! n)), mset (mult_monoms aa (fst (q ! n)))) \ term_poly_list_rel\ for aa n using mult_monoms_spec[unfolded fun_rel_def, simplified] apply - apply (drule bspec[of _ _ \(aa, (mset aa))\]) apply (auto simp: term_poly_list_rel_def)[] unfolding prod.case sorted_poly_list_rel_wrt_def apply clarsimp subgoal for y apply (drule bspec[of _ _ \(fst (q ! n), mset (fst (q ! n)))\]) apply (cases \q ! n\; cases \y ! n\) using param_nth[of n y n q \term_poly_list_rel \\<^sub>r int_rel\] by (auto simp: list_rel_imp_same_length term_poly_list_rel_def) done have H': \(q, q') \ sorted_poly_list_rel term_order \ distinct aa \ sorted_wrt var_order aa \ (ab, ba) \ set q \ remdups_mset (mset aa + mset ab) = mset (mult_monoms aa ab)\ for aa n ab ba using mult_monoms_spec[unfolded fun_rel_def, simplified] apply - apply (drule bspec[of _ _ \(aa, (mset aa))\]) apply (auto simp: term_poly_list_rel_def)[] unfolding prod.case sorted_poly_list_rel_wrt_def apply clarsimp subgoal for y apply (drule bspec[of _ _ \(ab, mset ab)\]) apply (auto simp: list_rel_imp_same_length term_poly_list_rel_def list_rel_def dest: list_all2_in_set_ExD) done done have H: \(q, q') \ sorted_poly_list_rel term_order \ a = (aa, b) \ (pq, r) \ unsorted_poly_rel \ p' = add_mset (mset aa, b) A \ \x\set p. term_order aa (fst x) \ sorted_wrt var_order aa \ distinct aa \ b\ 0 \ (\aaa. (aaa, 0) \# q') \ (pq @ map (mult_monomials (aa, b)) q, {#case x of (ys, n) \ (remdups_mset (mset aa + ys), n * b) . x \# q'#} + r) \ unsorted_poly_rel\ for a p p' pq aa b r apply (auto simp: poly_list_rel_def) apply (rule_tac b = \y @ map (\(a,b). (mset a, b)) (map (mult_monomials (aa, b)) q)\ in relcompI) apply (auto simp: list_rel_def list_all2_append list_all2_lengthD H list_mset_rel_def br_def mult_monomials_def case_prod_beta intro!: list_all2_all_nthI simp: sorted_poly_list_relD) apply (subst sorted_poly_list_relD[of q q' term_order]) apply (auto simp: case_prod_beta H' intro!: image_mset_cong) done show ?thesis using assms apply (induction p arbitrary: p') subgoal by auto subgoal premises p for a p p' using p(1)[of \remove1_mset (mset (fst a), snd a) p'\] p(2-) apply (cases a) apply (auto simp: sorted_poly_list_rel_Cons_iff dest!: multi_member_split) apply (rule_tac x = \(\(ys, n). (remdups_mset (mset (fst a) + ys), n * snd a)) `# q' + r\ in exI) apply (auto 5 3 intro: mult_poly_p.intros simp: intro!: H dest: sorted_poly_list_rel_nonzeroD nonzero_coeffsD) apply (rule rtranclp_trans) apply (rule mult_poly_p_add_mset_same) apply assumption apply (rule converse_rtranclp_into_rtranclp) apply (auto intro!: mult_poly_p.intros simp: ac_simps) done done qed fun merge_coeffs :: \llist_polynomial \ llist_polynomial\ where \merge_coeffs [] = []\ | \merge_coeffs [(xs, n)] = [(xs, n)]\ | \merge_coeffs ((xs, n) # (ys, m) # p) = (if xs = ys then if n + m \ 0 then merge_coeffs ((xs, n + m) # p) else merge_coeffs p else (xs, n) # merge_coeffs ((ys, m) # p))\ abbreviation (in -)mononoms :: \llist_polynomial \ term_poly_list set\ where \mononoms p \ fst `set p\ lemma fst_normalize_polynomial_subset: \mononoms (merge_coeffs p) \ mononoms p\ by (induction p rule: merge_coeffs.induct) auto lemma fst_normalize_polynomial_subsetD: \(a, b) \ set (merge_coeffs p) \ a \ mononoms p\ apply (induction p rule: merge_coeffs.induct) subgoal by auto subgoal by auto subgoal by (auto split: if_splits) done lemma distinct_merge_coeffs: assumes \sorted_wrt R (map fst xs)\ and \transp R\ \antisymp R\ shows \distinct (map fst (merge_coeffs xs))\ using assms by (induction xs rule: merge_coeffs.induct) (auto 5 4 dest: antisympD dest!: fst_normalize_polynomial_subsetD) lemma in_set_merge_coeffsD: \(a, b) \ set (merge_coeffs p) \\b. (a, b) \ set p\ by (auto dest!: fst_normalize_polynomial_subsetD) lemma rtranclp_normalize_poly_add_mset: \normalize_poly_p\<^sup>*\<^sup>* A r \ normalize_poly_p\<^sup>*\<^sup>* (add_mset x A) (add_mset x r)\ by (induction rule: rtranclp_induct) (auto dest: normalize_poly_p.keep_coeff[of _ _ x]) lemma nonzero_coeffs_diff: \nonzero_coeffs A \ nonzero_coeffs (A - B)\ by (auto simp: nonzero_coeffs_def dest: in_diffD) lemma merge_coeffs_is_normalize_poly_p: \(xs, ys) \ sorted_repeat_poly_rel \ \r. (merge_coeffs xs, r) \ sorted_poly_rel \ normalize_poly_p\<^sup>*\<^sup>* ys r\ apply (induction xs arbitrary: ys rule: merge_coeffs.induct) subgoal by (auto simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def) subgoal by (auto simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def) subgoal premises p for xs n ys m p ysa apply (cases \xs = ys\, cases \m+n \ 0\) subgoal using p(1)[of \add_mset (mset ys, m+n) ysa - {#(mset ys, m), (mset ys, n)#}\] p(4-) apply (auto simp: sorted_poly_list_rel_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \r\ in exI) using normalize_poly_p.merge_dup_coeff[of \ysa - {#(mset ys, m), (mset ys, n)#}\ \ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\ m n] by (auto dest!: multi_member_split simp del: normalize_poly_p.merge_dup_coeff simp: add_mset_commute intro: converse_rtranclp_into_rtranclp) subgoal using p(2)[of \ysa - {#(mset ys, m), (mset ys, n)#}\] p(4-) apply (auto simp: sorted_poly_list_rel_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \r\ in exI) using normalize_poly_p.rem_0_coeff[of \add_mset (mset ys, m +n) ysa - {#(mset ys, m), (mset ys, n)#}\ \add_mset (mset ys, m +n) ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\] using normalize_poly_p.merge_dup_coeff[of \ysa - {#(mset ys, m), (mset ys, n)#}\ \ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\ m n] by (force intro: add_mset_commute[of \(mset ys, n)\ \(mset ys, -n)\] converse_rtranclp_into_rtranclp dest!: multi_member_split simp del: normalize_poly_p.rem_0_coeff simp: add_eq_0_iff2 intro: normalize_poly_p.rem_0_coeff) subgoal using p(3)[of \add_mset (mset ys, m) ysa - {#(mset xs, n), (mset ys, m)#}\] p(4-) apply (auto simp: sorted_poly_list_rel_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \add_mset (mset xs, n) r\ in exI) apply (auto dest!: in_set_merge_coeffsD) apply (auto intro: normalize_poly_p.intros rtranclp_normalize_poly_add_mset simp: rel2p_def var_order_rel_def dest!: multi_member_split dest: sorted_poly_list_rel_nonzeroD) using total_on_lexord_less_than_char_linear apply fastforce using total_on_lexord_less_than_char_linear apply fastforce done done done subsection \Normalisation\ definition normalize_poly where \normalize_poly p = do { p \ sort_poly_spec p; RETURN (merge_coeffs p) }\ definition sort_coeff :: \string list \ string list nres\ where \sort_coeff ys = SPEC(\xs. mset xs = mset ys \ sorted_wrt (rel2p (Id \ var_order_rel)) xs)\ lemma distinct_var_order_Id_var_order: \distinct a \ sorted_wrt (rel2p (Id \ var_order_rel)) a \ sorted_wrt var_order a\ by (induction a) (auto simp: rel2p_def) definition sort_all_coeffs :: \llist_polynomial \ llist_polynomial nres\ where \sort_all_coeffs xs = monadic_nfoldli xs (\_. RETURN True) (\(a, n) b. do {a \ sort_coeff a; RETURN ((a, n) # b)}) []\ lemma sort_all_coeffs_gen: assumes \(\xs \ mononoms xs'. sorted_wrt (rel2p (var_order_rel)) xs)\ and \\x \ mononoms (xs @ xs'). distinct x\ shows \monadic_nfoldli xs (\_. RETURN True) (\(a, n) b. do {a \ sort_coeff a; RETURN ((a, n) # b)}) xs' \ \Id (SPEC(\ys. map (\(a,b). (mset a, b)) (rev xs @ xs') = map (\(a,b). (mset a, b)) (ys) \ (\xs \ mononoms ys. sorted_wrt (rel2p (var_order_rel)) xs)))\ proof - have H: \ \x\set xs'. sorted_wrt var_order (fst x) \ sorted_wrt (rel2p (Id \ var_order_rel)) x \ (aaa, ba) \ set xs' \ sorted_wrt (rel2p (Id \ var_order_rel)) aaa\ for xs xs' ba aa b x aaa by (metis UnCI fst_eqD rel2p_def sorted_wrt_mono_rel) show ?thesis using assms unfolding sort_all_coeffs_def sort_coeff_def apply (induction xs arbitrary: xs') subgoal using assms by auto subgoal premises p for a xs using p(2-) apply (cases a, simp only: monadic_nfoldli_simp bind_to_let_conv Let_def if_True Refine_Basic.nres_monad3 intro_spec_refine_iff prod.case) by (auto 5 3 simp: intro_spec_refine_iff image_Un dest: same_mset_distinct_iff intro!: p(1)[THEN order_trans] distinct_var_order_Id_var_order simp: H) done qed definition shuffle_coefficients where \shuffle_coefficients xs = (SPEC(\ys. map (\(a,b). (mset a, b)) (rev xs) = map (\(a,b). (mset a, b)) ys \ (\xs \ mononoms ys. sorted_wrt (rel2p (var_order_rel)) xs)))\ lemma sort_all_coeffs: \\x \ mononoms xs. distinct x \ sort_all_coeffs xs \ \ Id (shuffle_coefficients xs)\ unfolding sort_all_coeffs_def shuffle_coefficients_def by (rule sort_all_coeffs_gen[THEN order_trans]) auto lemma unsorted_term_poly_list_rel_mset: \(ys, aa) \ unsorted_term_poly_list_rel \ mset ys = aa\ by (auto simp: unsorted_term_poly_list_rel_def) lemma RETURN_map_alt_def: \RETURN o (map f) = REC\<^sub>T (\g xs. case xs of [] \ RETURN [] | x # xs \ do {xs \ g xs; RETURN (f x # xs)})\ unfolding comp_def apply (subst eq_commute) apply (intro ext) apply (induct_tac x) subgoal apply (subst RECT_unfold) apply refine_mono apply auto done subgoal apply (subst RECT_unfold) apply refine_mono apply auto done done lemma fully_unsorted_poly_rel_Cons_iff: \((ys, n) # p, a) \ fully_unsorted_poly_rel \ (p, remove1_mset (mset ys, n) a) \ fully_unsorted_poly_rel \ (mset ys, n) \# a \ distinct ys\ apply (auto simp: poly_list_rel_def list_rel_split_right_iff list_mset_rel_def br_def unsorted_term_poly_list_rel_def nonzero_coeffs_def fully_unsorted_poly_list_rel_def dest!: multi_member_split) apply blast apply (rule_tac b = \(mset ys, n) # y\ in relcompI) apply auto done lemma map_mset_unsorted_term_poly_list_rel: \(\a. a \ mononoms s \ distinct a) \ \x \ mononoms s. distinct x \ (\xs \ mononoms s. sorted_wrt (rel2p (Id \ var_order_rel)) xs) \ (s, map (\(a, y). (mset a, y)) s) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ by (induction s) (auto simp: term_poly_list_rel_def distinct_var_order_Id_var_order) lemma list_rel_unsorted_term_poly_list_relD: \(p, y) \ \unsorted_term_poly_list_rel \\<^sub>r int_rel\list_rel \ mset y = (\(a, y). (mset a, y)) `# mset p \ (\x \ mononoms p. distinct x)\ by (induction p arbitrary: y) (auto simp: list_rel_split_right_iff unsorted_term_poly_list_rel_def) lemma shuffle_terms_distinct_iff: assumes \map (\(a, y). (mset a, y)) p = map (\(a, y). (mset a, y)) s\ shows \(\x\set p. distinct (fst x)) \ (\x\set s. distinct (fst x))\ proof - have \\x\set s. distinct (fst x)\ if m: \map (\(a, y). (mset a, y)) p = map (\(a, y). (mset a, y)) s\ and dist: \\x\set p. distinct (fst x)\ for s p proof standard+ fix x assume x: \x \ set s\ obtain v n where [simp]: \x = (v, n)\ by (cases x) then have \(mset v, n) \ set (map (\(a, y). (mset a, y)) p)\ using x unfolding m by auto then obtain v' where \(v', n) \ set p\ and \mset v' = mset v\ by (auto simp: image_iff) then show \distinct (fst x)\ using dist by (metis \x = (v, n)\ distinct_mset_mset_distinct fst_conv) qed from this[of p s] this[of s p] show \?thesis\ unfolding assms by blast qed lemma \(p, y) \ \unsorted_term_poly_list_rel \\<^sub>r int_rel\list_rel \ (a, b) \ set p \ distinct a\ using list_rel_unsorted_term_poly_list_relD by fastforce lemma sort_all_coeffs_unsorted_poly_rel_with0: assumes \(p, p') \ fully_unsorted_poly_rel\ shows \sort_all_coeffs p \ \ (unsorted_poly_rel_with0) (RETURN p')\ proof - have H: \(map (\(a, y). (mset a, y)) (rev p)) = map (\(a, y). (mset a, y)) s \ (map (\(a, y). (mset a, y)) p) = map (\(a, y). (mset a, y)) (rev s)\ for s by (auto simp flip: rev_map simp: eq_commute[of \rev (map _ _)\ \map _ _\]) have 1: \\s y. (p, y) \ \unsorted_term_poly_list_rel \\<^sub>r int_rel\list_rel \ p' = mset y \ map (\(a, y). (mset a, y)) (rev p) = map (\(a, y). (mset a, y)) s \ \x\set s. sorted_wrt var_order (fst x) \ (s, map (\(a, y). (mset a, y)) s) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ by (auto 4 4 simp: rel2p_def dest!: list_rel_unsorted_term_poly_list_relD dest: shuffle_terms_distinct_iff["THEN" iffD1] intro!: map_mset_unsorted_term_poly_list_rel sorted_wrt_mono_rel[of _ \rel2p (var_order_rel)\ \rel2p (Id \ var_order_rel)\]) have 2: \\s y. (p, y) \ \unsorted_term_poly_list_rel \\<^sub>r int_rel\list_rel \ p' = mset y \ map (\(a, y). (mset a, y)) (rev p) = map (\(a, y). (mset a, y)) s \ \x\set s. sorted_wrt var_order (fst x) \ mset y = {#case x of (a, x) \ (mset a, x). x \# mset s#}\ by (metis (no_types, lifting) list_rel_unsorted_term_poly_list_relD mset_map mset_rev) show ?thesis apply (rule sort_all_coeffs[THEN order_trans]) using assms by (auto simp: shuffle_coefficients_def poly_list_rel_def RETURN_def fully_unsorted_poly_list_rel_def list_mset_rel_def br_def dest: list_rel_unsorted_term_poly_list_relD intro!: RES_refine relcompI[of _ \map (\(a, y). (mset a, y)) (rev p)\] 1 2) qed lemma sort_poly_spec_id': assumes \(p, p') \ unsorted_poly_rel_with0\ shows \sort_poly_spec p \ \ (sorted_repeat_poly_rel_with0) (RETURN p')\ proof - obtain y where py: \(p, y) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ and p'_y: \p' = mset y\ using assms unfolding fully_unsorted_poly_list_rel_def poly_list_rel_def sorted_poly_list_rel_wrt_def by (auto simp: list_mset_rel_def br_def) then have [simp]: \length y = length p\ by (auto simp: list_rel_def list_all2_conv_all_nth) have H: \(x, p') \ \term_poly_list_rel \\<^sub>r int_rel\list_rel O list_mset_rel\ if px: \mset p = mset x\ and \sorted_wrt (rel2p (Id \ lexord var_order_rel)) (map fst x)\ for x :: \llist_polynomial\ proof - from px have \length x = length p\ by (metis size_mset) from px have \mset x = mset p\ by simp then obtain f where \f permutes {.. \permute_list f p = x\ by (rule mset_eq_permutation) with \length x = length p\ have f: \bij_betw f {.. by (simp add: permutes_imp_bij) from \f permutes {.. \permute_list f p = x\ [symmetric] have [simp]: \\i. i < length x \ x ! i = p ! (f i)\ by (simp add: permute_list_nth) let ?y = \map (\i. y ! f i) [0 ..< length x]\ have \i < length y \ (p ! f i, y ! f i) \ term_poly_list_rel \\<^sub>r int_rel\ for i using list_all2_nthD[of _ p y \f i\, OF py[unfolded list_rel_def mem_Collect_eq prod.case]] mset_eq_length[OF px] f by (auto simp: list_rel_def list_all2_conv_all_nth bij_betw_def) then have \(x, ?y) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel\ and xy: \length x = length y\ using py list_all2_nthD[of \rel2p (term_poly_list_rel \\<^sub>r int_rel)\ p y \f i\ for i, simplified] mset_eq_length[OF px] by (auto simp: list_rel_def list_all2_conv_all_nth) moreover { have f: \mset_set {0.. using f mset_eq_length[OF px] by (auto simp: bij_betw_def lessThan_atLeast0 image_mset_mset_set) have \mset y = {#y ! f x. x \# mset_set {0.. by (subst drop_0[symmetric], subst mset_drop_upto, subst xy[symmetric], subst f) auto then have \(?y, p') \ list_mset_rel\ by (auto simp: list_mset_rel_def br_def p'_y) } ultimately show ?thesis by (auto intro!: relcompI[of _ ?y]) qed show ?thesis unfolding sort_poly_spec_def poly_list_rel_def sorted_repeat_poly_list_rel_with0_wrt_def by refine_rcg (auto intro: H) qed fun merge_coeffs0 :: \llist_polynomial \ llist_polynomial\ where \merge_coeffs0 [] = []\ | \merge_coeffs0 [(xs, n)] = (if n = 0 then [] else [(xs, n)])\ | \merge_coeffs0 ((xs, n) # (ys, m) # p) = (if xs = ys then if n + m \ 0 then merge_coeffs0 ((xs, n + m) # p) else merge_coeffs0 p else if n = 0 then merge_coeffs0 ((ys, m) # p) else(xs, n) # merge_coeffs0 ((ys, m) # p))\ lemma sorted_repeat_poly_list_rel_with0_wrt_ConsD: \((ys, n) # p, a) \ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel \ (p, remove1_mset (mset ys, n) a) \ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys\ unfolding sorted_repeat_poly_list_rel_with0_wrt_def prod.case mem_Collect_eq list_rel_def apply (clarsimp) apply (subst (asm) list.rel_sel) apply (intro conjI) apply (rule_tac b = \tl y\ in relcompI) apply (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def) apply (case_tac \lead_coeff y\; case_tac y) apply (auto simp: term_poly_list_rel_def) apply (case_tac \lead_coeff y\; case_tac y) apply (auto simp: term_poly_list_rel_def) apply (case_tac \lead_coeff y\; case_tac y) apply (auto simp: term_poly_list_rel_def) apply (case_tac \lead_coeff y\; case_tac y) apply (auto simp: term_poly_list_rel_def) done lemma sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff: \((ys, n) # p, a) \ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel \ (p, remove1_mset (mset ys, n) a) \ sorted_repeat_poly_list_rel_with0_wrt S term_poly_list_rel \ (mset ys, n) \# a \ (\x \ set p. S ys (fst x)) \ sorted_wrt (rel2p var_order_rel) ys \ distinct ys\ apply (rule iffI) subgoal by (auto dest!: sorted_repeat_poly_list_rel_with0_wrt_ConsD) subgoal unfolding sorted_poly_list_rel_wrt_def prod.case mem_Collect_eq list_rel_def sorted_repeat_poly_list_rel_with0_wrt_def apply (clarsimp) apply (rule_tac b = \(mset ys, n) # y\ in relcompI) by (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def term_poly_list_rel_def add_mset_eq_add_mset eq_commute[of _ \mset _\] nonzero_coeffs_def dest!: multi_member_split) done lemma fst_normalize0_polynomial_subsetD: \(a, b) \ set (merge_coeffs0 p) \ a \ mononoms p\ apply (induction p rule: merge_coeffs0.induct) subgoal by auto subgoal by (auto split: if_splits) subgoal by (auto split: if_splits) done lemma in_set_merge_coeffs0D: \(a, b) \ set (merge_coeffs0 p) \\b. (a, b) \ set p\ by (auto dest!: fst_normalize0_polynomial_subsetD) lemma merge_coeffs0_is_normalize_poly_p: \(xs, ys) \ sorted_repeat_poly_rel_with0 \ \r. (merge_coeffs0 xs, r) \ sorted_poly_rel \ normalize_poly_p\<^sup>*\<^sup>* ys r\ apply (induction xs arbitrary: ys rule: merge_coeffs0.induct) subgoal by (auto simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def sorted_repeat_poly_list_rel_with0_wrt_def list_mset_rel_def br_def) subgoal for xs n ys by (force simp: sorted_repeat_poly_list_rel_wrt_def sorted_poly_list_rel_wrt_def sorted_repeat_poly_list_rel_with0_wrt_def list_mset_rel_def br_def list_rel_split_right_iff) subgoal premises p for xs n ys m p ysa apply (cases \xs = ys\, cases \m+n \ 0\) subgoal using p(1)[of \add_mset (mset ys, m+n) ysa - {#(mset ys, m), (mset ys, n)#}\] p(5-) apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff) apply (auto intro: normalize_poly_p.intros add_mset_commute add_mset_commute converse_rtranclp_into_rtranclp dest!: multi_member_split simp del: normalize_poly_p.merge_dup_coeff) apply (rule_tac x = \r\ in exI) using normalize_poly_p.merge_dup_coeff[of \ysa - {#(mset ys, m), (mset ys, n)#}\ \ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\ m n] by (auto intro: normalize_poly_p.intros converse_rtranclp_into_rtranclp dest!: multi_member_split simp: add_mset_commute[of \(mset ys, n)\ \(mset ys, m)\] simp del: normalize_poly_p.merge_dup_coeff) subgoal using p(2)[of \ysa - {#(mset ys, m), (mset ys, n)#}\] p(5-) apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If nonzero_coeffs_diff sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \r\ in exI) using normalize_poly_p.rem_0_coeff[of \add_mset (mset ys, m +n) ysa - {#(mset ys, m), (mset ys, n)#}\ \add_mset (mset ys, m +n) ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\] using normalize_poly_p.merge_dup_coeff[of \ysa - {#(mset ys, m), (mset ys, n)#}\ \ysa - {#(mset ys, m), (mset ys, n)#}\ \mset ys\ m n] by (force intro: normalize_poly_p.intros converse_rtranclp_into_rtranclp dest!: multi_member_split simp del: normalize_poly_p.rem_0_coeff simp: add_mset_commute[of \(mset ys, n)\ \(mset ys, m)\]) apply (cases \n = 0\) subgoal using p(3)[of \add_mset (mset ys, m) ysa - {#(mset xs, n), (mset ys, m)#}\] p(4-) apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \r\ in exI) apply (auto dest!: in_set_merge_coeffsD) by (force intro: rtranclp_normalize_poly_add_mset converse_rtranclp_into_rtranclp simp: rel2p_def var_order_rel_def sorted_poly_list_rel_Cons_iff dest!: multi_member_split dest: sorted_poly_list_rel_nonzeroD) subgoal using p(4)[of \add_mset (mset ys, m) ysa - {#(mset xs, n), (mset ys, m)#}\] p(5-) apply (auto simp: sorted_repeat_poly_list_rel_with0_wrtl_Cons_iff ac_simps add_mset_commute remove1_mset_add_mset_If sorted_repeat_poly_list_rel_Cons_iff) apply (rule_tac x = \add_mset (mset xs, n) r\ in exI) apply (auto dest!: in_set_merge_coeffs0D) apply (auto intro: normalize_poly_p.intros rtranclp_normalize_poly_add_mset simp: rel2p_def var_order_rel_def sorted_poly_list_rel_Cons_iff dest!: multi_member_split dest: sorted_poly_list_rel_nonzeroD) using in_set_merge_coeffs0D total_on_lexord_less_than_char_linear apply fastforce using in_set_merge_coeffs0D total_on_lexord_less_than_char_linear apply fastforce done done done definition full_normalize_poly where \full_normalize_poly p = do { p \ sort_all_coeffs p; p \ sort_poly_spec p; RETURN (merge_coeffs0 p) }\ fun sorted_remdups where \sorted_remdups (x # y # zs) = (if x = y then sorted_remdups (y # zs) else x # sorted_remdups (y # zs))\ | \sorted_remdups zs = zs\ lemma set_sorted_remdups[simp]: \set (sorted_remdups xs) = set xs\ by (induction xs rule: sorted_remdups.induct) auto lemma distinct_sorted_remdups: - \sorted_wrt R xs \ transp R \ Restricted_Predicates.total_on R UNIV \ - antisymp R \ distinct (sorted_remdups xs)\ + \sorted_wrt R xs \ antisymp R \ distinct (sorted_remdups xs)\ by (induction xs rule: sorted_remdups.induct) (auto dest: antisympD) lemma full_normalize_poly_normalize_poly_p: assumes \(p, p') \ fully_unsorted_poly_rel\ shows \full_normalize_poly p \ \ (sorted_poly_rel) (SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p' r))\ (is \?A \ \ ?R ?B\) proof - have 1: \?B = do { p' \ RETURN p'; p' \ RETURN p'; SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p' r) }\ by auto have [refine0]: \sort_all_coeffs p \ SPEC(\p. (p, p') \ unsorted_poly_rel_with0)\ by (rule sort_all_coeffs_unsorted_poly_rel_with0[OF assms, THEN order_trans]) (auto simp: conc_fun_RES RETURN_def) have [refine0]: \sort_poly_spec p \ SPEC (\c. (c, p') \ sorted_repeat_poly_rel_with0)\ if \(p, p') \ unsorted_poly_rel_with0\ for p p' by (rule sort_poly_spec_id'[THEN order_trans, OF that]) (auto simp: conc_fun_RES RETURN_def) show ?thesis apply (subst 1) unfolding full_normalize_poly_def by (refine_rcg) (auto intro!: RES_refine dest!: merge_coeffs0_is_normalize_poly_p simp: RETURN_def) qed definition mult_poly_full :: \_\ where \mult_poly_full p q = do { let pq = mult_poly_raw p q; normalize_poly pq }\ lemma normalize_poly_normalize_poly_p: assumes \(p, p') \ unsorted_poly_rel\ shows \normalize_poly p \ \ (sorted_poly_rel) (SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p' r))\ proof - have 1: \SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p' r) = do { p' \ RETURN p'; SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p' r) }\ by auto show ?thesis unfolding normalize_poly_def apply (subst 1) apply (refine_rcg sort_poly_spec_id[OF assms] merge_coeffs_is_normalize_poly_p) subgoal by (drule merge_coeffs_is_normalize_poly_p) (auto intro!: RES_refine simp: RETURN_def) done qed subsection \Multiplication and normalisation\ definition mult_poly_p' :: \_\ where \mult_poly_p' p' q' = do { pq \ SPEC(\r. (mult_poly_p q')\<^sup>*\<^sup>* (p', {#}) ({#}, r)); SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* pq r) }\ lemma unsorted_poly_rel_fully_unsorted_poly_rel: \unsorted_poly_rel \ fully_unsorted_poly_rel\ proof - have \term_poly_list_rel \\<^sub>r int_rel \ unsorted_term_poly_list_rel \\<^sub>r int_rel\ by (auto simp: unsorted_term_poly_list_rel_def term_poly_list_rel_def) from list_rel_mono[OF this] show ?thesis unfolding poly_list_rel_def fully_unsorted_poly_list_rel_def by (auto simp:) qed lemma mult_poly_full_mult_poly_p': assumes \(p, p') \ sorted_poly_rel\ \(q, q') \ sorted_poly_rel\ shows \mult_poly_full p q \ \ (sorted_poly_rel) (mult_poly_p' p' q')\ unfolding mult_poly_full_def mult_poly_p'_def apply (refine_rcg full_normalize_poly_normalize_poly_p normalize_poly_normalize_poly_p) apply (subst RETURN_RES_refine_iff) apply (subst Bex_def) apply (subst mem_Collect_eq) apply (subst conj_commute) apply (rule mult_poly_raw_mult_poly_p[OF assms(1,2)]) subgoal by blast done definition add_poly_spec :: \_\ where \add_poly_spec p q = SPEC (\r. p + q - r \ ideal polynomial_bool)\ definition add_poly_p' :: \_\ where \add_poly_p' p q = SPEC(\r. add_poly_p\<^sup>*\<^sup>* (p, q, {#}) ({#}, {#}, r))\ lemma add_poly_l_add_poly_p': assumes \(p, p') \ sorted_poly_rel\ \(q, q') \ sorted_poly_rel\ shows \add_poly_l (p, q) \ \ (sorted_poly_rel) (add_poly_p' p' q')\ unfolding add_poly_p'_def apply (refine_rcg add_poly_l_spec[THEN fref_to_Down_curry_right, THEN order_trans, of _ p' q']) subgoal by auto subgoal using assms by auto subgoal by auto done subsection \Correctness\ context poly_embed begin definition mset_poly_rel where \mset_poly_rel = {(a, b). b = polynomial_of_mset a}\ definition var_rel where \var_rel = br \ (\_. True)\ lemma normalize_poly_p_normalize_poly_spec: \(p, p') \ mset_poly_rel \ SPEC (\r. normalize_poly_p\<^sup>*\<^sup>* p r) \ \mset_poly_rel (normalize_poly_spec p')\ by (auto simp: mset_poly_rel_def rtranclp_normalize_poly_p_poly_of_mset ideal.span_zero normalize_poly_spec_def intro!: RES_refine) lemma mult_poly_p'_mult_poly_spec: \(p, p') \ mset_poly_rel \ (q, q') \ mset_poly_rel \ mult_poly_p' p q \ \mset_poly_rel (mult_poly_spec p' q')\ unfolding mult_poly_p'_def mult_poly_spec_def apply refine_rcg apply (auto simp: mset_poly_rel_def dest!: rtranclp_mult_poly_p_mult_ideal_final) apply (intro RES_refine) using ideal.span_add_eq2 ideal.span_zero by (fastforce dest!: rtranclp_normalize_poly_p_poly_of_mset intro: ideal.span_add_eq2) lemma add_poly_p'_add_poly_spec: \(p, p') \ mset_poly_rel \ (q, q') \ mset_poly_rel \ add_poly_p' p q \ \mset_poly_rel (add_poly_spec p' q')\ unfolding add_poly_p'_def add_poly_spec_def apply (auto simp: mset_poly_rel_def dest!: rtranclp_add_poly_p_polynomial_of_mset_full) apply (intro RES_refine) apply (auto simp: rtranclp_add_poly_p_polynomial_of_mset_full ideal.span_zero) done end definition weak_equality_l :: \llist_polynomial \ llist_polynomial \ bool nres\ where \weak_equality_l p q = RETURN (p = q)\ definition weak_equality :: \int mpoly \ int mpoly \ bool nres\ where \weak_equality p q = SPEC (\r. r \ p = q)\ definition weak_equality_spec :: \mset_polynomial \ mset_polynomial \ bool nres\ where \weak_equality_spec p q = SPEC (\r. r \ p = q)\ lemma term_poly_list_rel_same_rightD: \(a, aa) \ term_poly_list_rel \ (a, ab) \ term_poly_list_rel \ aa = ab\ by (auto simp: term_poly_list_rel_def) lemma list_rel_term_poly_list_rel_same_rightD: \(xa, y) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel \ (xa, ya) \ \term_poly_list_rel \\<^sub>r int_rel\list_rel \ y = ya\ by (induction xa arbitrary: y ya) (auto simp: list_rel_split_right_iff dest: term_poly_list_rel_same_rightD) lemma weak_equality_l_weak_equality_spec: \(uncurry weak_equality_l, uncurry weak_equality_spec) \ sorted_poly_rel \\<^sub>r sorted_poly_rel \\<^sub>f \bool_rel\nres_rel\ by (intro frefI nres_relI) (auto simp: weak_equality_l_def weak_equality_spec_def sorted_poly_list_rel_wrt_def list_mset_rel_def br_def dest: list_rel_term_poly_list_rel_same_rightD) end diff --git a/thys/Polynomials/Power_Products.thy b/thys/Polynomials/Power_Products.thy --- a/thys/Polynomials/Power_Products.thy +++ b/thys/Polynomials/Power_Products.thy @@ -1,2698 +1,2698 @@ (* Author: Fabian Immler, Alexander Maletzky *) section \Abstract Power-Products\ theory Power_Products imports Complex_Main "HOL-Library.Function_Algebras" "HOL-Library.Countable" "More_MPoly_Type" "Utils" Well_Quasi_Orders.Well_Quasi_Orders begin text \This theory formalizes the concept of "power-products". A power-product can be thought of as the product of some indeterminates, such as $x$, $x^2\,y$, $x\,y^3\,z^7$, etc., without any scalar coefficient. The approach in this theory is to capture the notion of "power-product" (also called "monomial") as type class. A canonical instance for power-product is the type @{typ "'var \\<^sub>0 nat"}, which is interpreted as mapping from variables in the power-product to exponents. A slightly unintuitive (but fitting better with the standard type class instantiations of @{typ "'a \\<^sub>0 'b"}) approach is to write addition to denote "multiplication" of power products. For example, $x^2y$ would be represented as a function \p = (X \ 2, Y \ 1)\, $xz$ as a function \q = (X \ 1, Z \ 1)\. With the (pointwise) instantiation of addition of @{typ "'a \\<^sub>0 'b"}, we will write \p + q = (X \ 3, Y \ 1, Z \ 1)\ for the product $x^2y \cdot xz = x^3yz$ \ subsection \Constant @{term Keys}\ text \Legacy:\ lemmas keys_eq_empty_iff = keys_eq_empty definition Keys :: "('a \\<^sub>0 'b::zero) set \ 'a set" where "Keys F = \(keys ` F)" lemma in_Keys: "s \ Keys F \ (\f\F. s \ keys f)" unfolding Keys_def by simp lemma in_KeysI: assumes "s \ keys f" and "f \ F" shows "s \ Keys F" unfolding in_Keys using assms .. lemma in_KeysE: assumes "s \ Keys F" obtains f where "s \ keys f" and "f \ F" using assms unfolding in_Keys .. lemma Keys_mono: assumes "A \ B" shows "Keys A \ Keys B" using assms by (auto simp add: Keys_def) lemma Keys_insert: "Keys (insert a A) = keys a \ Keys A" by (simp add: Keys_def) lemma Keys_Un: "Keys (A \ B) = Keys A \ Keys B" by (simp add: Keys_def) lemma finite_Keys: assumes "finite A" shows "finite (Keys A)" unfolding Keys_def by (rule, fact assms, rule finite_keys) lemma Keys_not_empty: assumes "a \ A" and "a \ 0" shows "Keys A \ {}" proof assume "Keys A = {}" from \a \ 0\ have "keys a \ {}" using aux by fastforce then obtain s where "s \ keys a" by blast from this assms(1) have "s \ Keys A" by (rule in_KeysI) with \Keys A = {}\ show False by simp qed lemma Keys_empty [simp]: "Keys {} = {}" by (simp add: Keys_def) lemma Keys_zero [simp]: "Keys {0} = {}" by (simp add: Keys_def) lemma keys_subset_Keys: assumes "f \ F" shows "keys f \ Keys F" using in_KeysI[OF _ assms] by auto lemma Keys_minus: "Keys (A - B) \ Keys A" by (auto simp add: Keys_def) lemma Keys_minus_zero: "Keys (A - {0}) = Keys A" proof (cases "0 \ A") case True hence "(A - {0}) \ {0} = A" by auto hence "Keys A = Keys ((A - {0}) \ {0})" by simp also have "... = Keys (A - {0}) \ Keys {0::('a \\<^sub>0 'b)}" by (fact Keys_Un) also have "... = Keys (A - {0})" by simp finally show ?thesis by simp next case False hence "A - {0} = A" by simp thus ?thesis by simp qed subsection \Constant @{term except}\ definition except_fun :: "('a \ 'b) \ 'a set \ ('a \ 'b::zero)" where "except_fun f S = (\x. (f x when x \ S))" lift_definition except :: "('a \\<^sub>0 'b) \ 'a set \ ('a \\<^sub>0 'b::zero)" is except_fun proof - fix p::"'a \ 'b" and S::"'a set" assume "finite {t. p t \ 0}" show "finite {t. except_fun p S t \ 0}" proof (rule finite_subset[of _ "{t. p t \ 0}"], rule) fix u assume "u \ {t. except_fun p S t \ 0}" hence "p u \ 0" by (simp add: except_fun_def) thus "u \ {t. p t \ 0}" by simp qed fact qed lemma lookup_except_when: "lookup (except p S) = (\t. lookup p t when t \ S)" by (auto simp: except.rep_eq except_fun_def) lemma lookup_except: "lookup (except p S) = (\t. if t \ S then 0 else lookup p t)" by (rule ext) (simp add: lookup_except_when) lemma lookup_except_singleton: "lookup (except p {t}) t = 0" by (simp add: lookup_except) lemma except_zero [simp]: "except 0 S = 0" by (rule poly_mapping_eqI) (simp add: lookup_except) lemma lookup_except_eq_idI: assumes "t \ S" shows "lookup (except p S) t = lookup p t" using assms by (simp add: lookup_except) lemma lookup_except_eq_zeroI: assumes "t \ S" shows "lookup (except p S) t = 0" using assms by (simp add: lookup_except) lemma except_empty [simp]: "except p {} = p" by (rule poly_mapping_eqI) (simp add: lookup_except) lemma except_eq_zeroI: assumes "keys p \ S" shows "except p S = 0" proof (rule poly_mapping_eqI, simp) fix t show "lookup (except p S) t = 0" proof (cases "t \ S") case True thus ?thesis by (rule lookup_except_eq_zeroI) next case False then show ?thesis by (metis assms in_keys_iff lookup_except_eq_idI subset_eq) qed qed lemma except_eq_zeroE: assumes "except p S = 0" shows "keys p \ S" by (metis assms aux in_keys_iff lookup_except_eq_idI subset_iff) lemma except_eq_zero_iff: "except p S = 0 \ keys p \ S" by (rule, elim except_eq_zeroE, elim except_eq_zeroI) lemma except_keys [simp]: "except p (keys p) = 0" by (rule except_eq_zeroI, rule subset_refl) lemma plus_except: "p = Poly_Mapping.single t (lookup p t) + except p {t}" by (rule poly_mapping_eqI, simp add: lookup_add lookup_single lookup_except when_def split: if_split) lemma keys_except: "keys (except p S) = keys p - S" by (transfer, auto simp: except_fun_def) lemma except_single: "except (Poly_Mapping.single u c) S = (Poly_Mapping.single u c when u \ S)" by (rule poly_mapping_eqI) (simp add: lookup_except lookup_single when_def) lemma except_plus: "except (p + q) S = except p S + except q S" by (rule poly_mapping_eqI) (simp add: lookup_except lookup_add) lemma except_minus: "except (p - q) S = except p S - except q S" by (rule poly_mapping_eqI) (simp add: lookup_except lookup_minus) lemma except_uminus: "except (- p) S = - except p S" by (rule poly_mapping_eqI) (simp add: lookup_except) lemma except_except: "except (except p S) T = except p (S \ T)" by (rule poly_mapping_eqI) (simp add: lookup_except) lemma poly_mapping_keys_eqI: assumes a1: "keys p = keys q" and a2: "\t. t \ keys p \ lookup p t = lookup q t" shows "p = q" proof (rule poly_mapping_eqI) fix t show "lookup p t = lookup q t" proof (cases "t \ keys p") case True thus ?thesis by (rule a2) next case False moreover from this have "t \ keys q" unfolding a1 . ultimately have "lookup p t = 0" and "lookup q t = 0" unfolding in_keys_iff by simp_all thus ?thesis by simp qed qed lemma except_id_iff: "except p S = p \ keys p \ S = {}" by (metis Diff_Diff_Int Diff_eq_empty_iff Diff_triv inf_le2 keys_except lookup_except_eq_idI lookup_except_eq_zeroI not_in_keys_iff_lookup_eq_zero poly_mapping_keys_eqI) lemma keys_subset_wf: "wfP (\p q::('a, 'b::zero) poly_mapping. keys p \ keys q)" unfolding wfP_def proof (intro wfI_min) fix x::"('a, 'b) poly_mapping" and Q assume x_in: "x \ Q" let ?Q0 = "card ` keys ` Q" from x_in have "card (keys x) \ ?Q0" by simp from wfE_min[OF wf this] obtain z0 where z0_in: "z0 \ ?Q0" and z0_min: "\y. (y, z0) \ {(x, y). x < y} \ y \ ?Q0" by auto from z0_in obtain z where z0_def: "z0 = card (keys z)" and "z \ Q" by auto show "\z\Q. \y. (y, z) \ {(p, q). keys p \ keys q} \ y \ Q" proof (intro bexI[of _ z], rule, rule) fix y::"('a, 'b) poly_mapping" let ?y0 = "card (keys y)" assume "(y, z) \ {(p, q). keys p \ keys q}" hence "keys y \ keys z" by simp hence "?y0 < z0" unfolding z0_def by (simp add: psubset_card_mono) hence "(?y0, z0) \ {(x, y). x < y}" by simp from z0_min[OF this] show "y \ Q" by auto qed (fact) qed lemma poly_mapping_except_induct: assumes base: "P 0" and ind: "\p t. p \ 0 \ t \ keys p \ P (except p {t}) \ P p" shows "P p" proof (induct rule: wfP_induct[OF keys_subset_wf]) fix p::"('a, 'b) poly_mapping" assume "\q. keys q \ keys p \ P q" hence IH: "\q. keys q \ keys p \ P q" by simp show "P p" proof (cases "p = 0") case True thus ?thesis using base by simp next case False hence "keys p \ {}" by simp then obtain t where "t \ keys p" by blast show ?thesis proof (rule ind, fact, fact, rule IH, simp only: keys_except, rule, rule Diff_subset, rule) assume "keys p - {t} = keys p" hence "t \ keys p" by blast from this \t \ keys p\ show False .. qed qed qed lemma poly_mapping_except_induct': assumes "\p. (\t. t \ keys p \ P (except p {t})) \ P p" shows "P p" proof (induct "card (keys p)" arbitrary: p) case 0 with finite_keys[of p] have "keys p = {}" by simp show ?case by (rule assms, simp add: \keys p = {}\) next case step: (Suc n) show ?case proof (rule assms) fix t assume "t \ keys p" show "P (except p {t})" proof (rule step(1), simp add: keys_except) from step(2) \t \ keys p\ finite_keys[of p] show "n = card (keys p - {t})" by simp qed qed qed lemma poly_mapping_plus_induct: assumes "P 0" and "\p c t. c \ 0 \ t \ keys p \ P p \ P (Poly_Mapping.single t c + p)" shows "P p" proof (induct "card (keys p)" arbitrary: p) case 0 with finite_keys[of p] have "keys p = {}" by simp hence "p = 0" by simp with assms(1) show ?case by simp next case step: (Suc n) from step(2) obtain t where t: "t \ keys p" by (metis card_eq_SucD insert_iff) define c where "c = lookup p t" define q where "q = except p {t}" have *: "p = Poly_Mapping.single t c + q" by (rule poly_mapping_eqI, simp add: lookup_add lookup_single Poly_Mapping.when_def, intro conjI impI, simp add: q_def lookup_except c_def, simp add: q_def lookup_except_eq_idI) show ?case proof (simp only: *, rule assms(2)) from t show "c \ 0" using c_def by auto next show "t \ keys q" by (simp add: q_def keys_except) next show "P q" proof (rule step(1)) from step(2) \t \ keys p\ show "n = card (keys q)" unfolding q_def keys_except by (metis Suc_inject card.remove finite_keys) qed qed qed lemma except_Diff_singleton: "except p (keys p - {t}) = Poly_Mapping.single t (lookup p t)" by (rule poly_mapping_eqI) (simp add: lookup_single in_keys_iff lookup_except when_def) lemma except_Un_plus_Int: "except p (U \ V) + except p (U \ V) = except p U + except p V" by (rule poly_mapping_eqI) (simp add: lookup_except lookup_add) corollary except_Int: assumes "keys p \ U \ V" shows "except p (U \ V) = except p U + except p V" proof - from assms have "except p (U \ V) = 0" by (rule except_eq_zeroI) hence "except p (U \ V) = except p (U \ V) + except p (U \ V)" by simp also have "\ = except p U + except p V" by (fact except_Un_plus_Int) finally show ?thesis . qed lemma except_keys_Int [simp]: "except p (keys p \ U) = except p U" by (rule poly_mapping_eqI) (simp add: in_keys_iff lookup_except) lemma except_Int_keys [simp]: "except p (U \ keys p) = except p U" by (simp only: Int_commute[of U] except_keys_Int) lemma except_keys_Diff: "except p (keys p - U) = except p (- U)" proof - have "except p (keys p - U) = except p (keys p \ (- U))" by (simp only: Diff_eq) also have "\ = except p (- U)" by simp finally show ?thesis . qed lemma except_decomp: "p = except p U + except p (- U)" by (rule poly_mapping_eqI) (simp add: lookup_except lookup_add) corollary except_Compl: "except p (- U) = p - except p U" by (metis add_diff_cancel_left' except_decomp) subsection \'Divisibility' on Additive Structures\ context plus begin definition adds :: "'a \ 'a \ bool" (infix "adds" 50) where "b adds a \ (\k. a = b + k)" lemma addsI [intro?]: "a = b + k \ b adds a" unfolding adds_def .. lemma addsE [elim?]: "b adds a \ (\k. a = b + k \ P) \ P" unfolding adds_def by blast end context comm_monoid_add begin lemma adds_refl [simp]: "a adds a" proof show "a = a + 0" by simp qed lemma adds_trans [trans]: assumes "a adds b" and "b adds c" shows "a adds c" proof - from assms obtain v where "b = a + v" by (auto elim!: addsE) moreover from assms obtain w where "c = b + w" by (auto elim!: addsE) ultimately have "c = a + (v + w)" by (simp add: add.assoc) then show ?thesis .. qed lemma subset_divisors_adds: "{c. c adds a} \ {c. c adds b} \ a adds b" by (auto simp add: subset_iff intro: adds_trans) lemma strict_subset_divisors_adds: "{c. c adds a} \ {c. c adds b} \ a adds b \ \ b adds a" by (auto simp add: subset_iff intro: adds_trans) lemma zero_adds [simp]: "0 adds a" by (auto intro!: addsI) lemma adds_plus_right [simp]: "a adds c \ a adds (b + c)" by (auto intro!: add.left_commute addsI elim!: addsE) lemma adds_plus_left [simp]: "a adds b \ a adds (b + c)" using adds_plus_right [of a b c] by (simp add: ac_simps) lemma adds_triv_right [simp]: "a adds b + a" by (rule adds_plus_right) (rule adds_refl) lemma adds_triv_left [simp]: "a adds a + b" by (rule adds_plus_left) (rule adds_refl) lemma plus_adds_mono: assumes "a adds b" and "c adds d" shows "a + c adds b + d" proof - from \a adds b\ obtain b' where "b = a + b'" .. moreover from \c adds d\ obtain d' where "d = c + d'" .. ultimately have "b + d = (a + c) + (b' + d')" by (simp add: ac_simps) then show ?thesis .. qed lemma plus_adds_left: "a + b adds c \ a adds c" by (simp add: adds_def add.assoc) blast lemma plus_adds_right: "a + b adds c \ b adds c" using plus_adds_left [of b a c] by (simp add: ac_simps) end class ninv_comm_monoid_add = comm_monoid_add + assumes plus_eq_zero: "s + t = 0 \ s = 0" begin lemma plus_eq_zero_2: "t = 0" if "s + t = 0" using that by (simp only: add_commute[of s t] plus_eq_zero) lemma adds_zero: "s adds 0 \ (s = 0)" proof assume "s adds 0" from this obtain k where "0 = s + k" unfolding adds_def .. from this plus_eq_zero[of s k] show "s = 0" by blast next assume "s = 0" thus "s adds 0" by simp qed end context canonically_ordered_monoid_add begin subclass ninv_comm_monoid_add by (standard, simp) end class comm_powerprod = cancel_comm_monoid_add begin lemma adds_canc: "s + u adds t + u \ s adds t" for s t u::'a unfolding adds_def apply auto apply (metis local.add.left_commute local.add_diff_cancel_left' local.add_diff_cancel_right') using add_assoc add_commute by auto lemma adds_canc_2: "u + s adds u + t \ s adds t" by (simp add: adds_canc ac_simps) lemma add_minus_2: "(s + t) - s = t" by simp lemma adds_minus: assumes "s adds t" shows "(t - s) + s = t" proof - from assms adds_def[of s t] obtain u where u: "t = u + s" by (auto simp: ac_simps) then have "t - s = u" by simp thus ?thesis using u by simp qed lemma plus_adds_0: assumes "(s + t) adds u" shows "s adds (u - t)" proof - from assms have "(s + t) adds ((u - t) + t)" using adds_minus local.plus_adds_right by presburger thus ?thesis using adds_canc[of s t "u - t"] by simp qed lemma plus_adds_2: assumes "t adds u" and "s adds (u - t)" shows "(s + t) adds u" by (metis adds_canc adds_minus assms) lemma plus_adds: shows "(s + t) adds u \ (t adds u \ s adds (u - t))" proof assume a1: "(s + t) adds u" show "t adds u \ s adds (u - t)" proof from plus_adds_right[OF a1] show "t adds u" . next from plus_adds_0[OF a1] show "s adds (u - t)" . qed next assume "t adds u \ s adds (u - t)" hence "t adds u" and "s adds (u - t)" by auto from plus_adds_2[OF \t adds u\ \s adds (u - t)\] show "(s + t) adds u" . qed lemma minus_plus: assumes "s adds t" shows "(t - s) + u = (t + u) - s" proof - from assms obtain k where k: "t = s + k" unfolding adds_def .. hence "t - s = k" by simp also from k have "(t + u) - s = k + u" by (simp add: add_assoc) finally show ?thesis by simp qed lemma minus_plus_minus: assumes "s adds t" and "u adds v" shows "(t - s) + (v - u) = (t + v) - (s + u)" using add_commute assms(1) assms(2) diff_diff_add minus_plus by auto lemma minus_plus_minus_cancel: assumes "u adds t" and "s adds u" shows "(t - u) + (u - s) = t - s" by (metis assms(1) assms(2) local.add_diff_cancel_left' local.add_diff_cancel_right local.addsE minus_plus) end text \Instances of class \lcs_powerprod\ are types of commutative power-products admitting (not necessarily unique) least common sums (inspired from least common multiplies). Note that if the components of indeterminates are arbitrary integers (as for instance in Laurent polynomials), then no unique lcss exist.\ class lcs_powerprod = comm_powerprod + fixes lcs::"'a \ 'a \ 'a" assumes adds_lcs: "s adds (lcs s t)" assumes lcs_adds: "s adds u \ t adds u \ (lcs s t) adds u" assumes lcs_comm: "lcs s t = lcs t s" begin lemma adds_lcs_2: "t adds (lcs s t)" by (simp only: lcs_comm[of s t], rule adds_lcs) lemma lcs_adds_plus: "lcs s t adds s + t" by (simp add: lcs_adds) text \"gcs" stands for "greatest common summand".\ definition gcs :: "'a \ 'a \ 'a" where "gcs s t = (s + t) - (lcs s t)" lemma gcs_plus_lcs: "(gcs s t) + (lcs s t) = s + t" unfolding gcs_def by (rule adds_minus, fact lcs_adds_plus) lemma gcs_adds: "(gcs s t) adds s" proof - have "t adds (lcs s t)" (is "t adds ?l") unfolding lcs_comm[of s t] by (fact adds_lcs) then obtain u where eq1: "?l = t + u" unfolding adds_def .. from lcs_adds_plus[of s t] obtain v where eq2: "s + t = ?l + v" unfolding adds_def .. hence "t + s = t + (u + v)" unfolding eq1 by (simp add: ac_simps) hence s: "s = u + v" unfolding add_left_cancel . show ?thesis unfolding eq2 gcs_def unfolding s by simp qed lemma gcs_comm: "gcs s t = gcs t s" unfolding gcs_def by (simp add: lcs_comm ac_simps) lemma gcs_adds_2: "(gcs s t) adds t" by (simp only: gcs_comm[of s t], rule gcs_adds) end class ulcs_powerprod = lcs_powerprod + ninv_comm_monoid_add begin lemma adds_antisym: assumes "s adds t" "t adds s" shows "s = t" proof - from \s adds t\ obtain u where u_def: "t = s + u" unfolding adds_def .. from \t adds s\ obtain v where v_def: "s = t + v" unfolding adds_def .. from u_def v_def have "s = (s + u) + v" by (simp add: ac_simps) hence "s + 0 = s + (u + v)" by (simp add: ac_simps) hence "u + v = 0" by simp hence "u = 0" using plus_eq_zero[of u v] by simp thus ?thesis using u_def by simp qed lemma lcs_unique: assumes "s adds l" and "t adds l" and *: "\u. s adds u \ t adds u \ l adds u" shows "l = lcs s t" by (rule adds_antisym, rule *, fact adds_lcs, fact adds_lcs_2, rule lcs_adds, fact+) lemma lcs_zero: "lcs 0 t = t" by (rule lcs_unique[symmetric], fact zero_adds, fact adds_refl) lemma lcs_plus_left: "lcs (u + s) (u + t) = u + lcs s t" proof (rule lcs_unique[symmetric], simp_all only: adds_canc_2, fact adds_lcs, fact adds_lcs_2, simp add: add.commute[of u] plus_adds) fix v assume "u adds v \ s adds v - u" hence "s adds v - u" .. assume "t adds v - u" with \s adds v - u\ show "lcs s t adds v - u" by (rule lcs_adds) qed lemma lcs_plus_right: "lcs (s + u) (t + u) = (lcs s t) + u" using lcs_plus_left[of u s t] by (simp add: ac_simps) lemma adds_gcs: assumes "u adds s" and "u adds t" shows "u adds (gcs s t)" proof - from assms have "s + u adds s + t" and "t + u adds t + s" by (simp_all add: plus_adds_mono) hence "lcs (s + u) (t + u) adds s + t" by (auto intro: lcs_adds simp add: ac_simps) hence "u + (lcs s t) adds s + t" unfolding lcs_plus_right by (simp add: ac_simps) hence "u adds (s + t) - (lcs s t)" unfolding plus_adds .. thus ?thesis unfolding gcs_def . qed lemma gcs_unique: assumes "g adds s" and "g adds t" and *: "\u. u adds s \ u adds t \ u adds g" shows "g = gcs s t" by (rule adds_antisym, rule adds_gcs, fact, fact, rule *, fact gcs_adds, fact gcs_adds_2) lemma gcs_plus_left: "gcs (u + s) (u + t) = u + gcs s t" proof - have "u + s + (u + t) - (u + lcs s t) = u + s + (u + t) - u - lcs s t" by (simp only: diff_diff_add) also have "... = u + s + t + (u - u) - lcs s t" by (simp add: add.left_commute) also have "... = u + s + t - lcs s t" by simp also have "... = u + (s + t - lcs s t)" using add_assoc add_commute local.lcs_adds_plus local.minus_plus by auto finally show ?thesis unfolding gcs_def lcs_plus_left . qed lemma gcs_plus_right: "gcs (s + u) (t + u) = (gcs s t) + u" using gcs_plus_left[of u s t] by (simp add: ac_simps) lemma lcs_same [simp]: "lcs s s = s" proof - have "lcs s s adds s" by (rule lcs_adds, simp_all) moreover have "s adds lcs s s" by (rule adds_lcs) ultimately show ?thesis by (rule adds_antisym) qed lemma gcs_same [simp]: "gcs s s = s" proof - have "gcs s s adds s" by (rule gcs_adds) moreover have "s adds gcs s s" by (rule adds_gcs, simp_all) ultimately show ?thesis by (rule adds_antisym) qed end subsection \Dickson Classes\ definition (in plus) dickson_grading :: "('a \ nat) \ bool" where "dickson_grading d \ ((\s t. d (s + t) = max (d s) (d t)) \ (\n::nat. almost_full_on (adds) {x. d x \ n}))" definition dgrad_set :: "('a \ nat) \ nat \ 'a set" where "dgrad_set d m = {t. d t \ m}" definition dgrad_set_le :: "('a \ nat) \ ('a set) \ ('a set) \ bool" where "dgrad_set_le d S T \ (\s\S. \t\T. d s \ d t)" lemma dickson_gradingI: assumes "\s t. d (s + t) = max (d s) (d t)" assumes "\n::nat. almost_full_on (adds) {x. d x \ n}" shows "dickson_grading d" unfolding dickson_grading_def using assms by blast lemma dickson_gradingD1: "dickson_grading d \ d (s + t) = max (d s) (d t)" by (auto simp add: dickson_grading_def) lemma dickson_gradingD2: "dickson_grading d \ almost_full_on (adds) {x. d x \ n}" by (auto simp add: dickson_grading_def) lemma dickson_gradingD2': assumes "dickson_grading (d::'a::comm_monoid_add \ nat)" shows "wqo_on (adds) {x. d x \ n}" proof (intro wqo_onI transp_onI) fix x y z :: 'a assume "x adds y" and "y adds z" thus "x adds z" by (rule adds_trans) next from assms show "almost_full_on (adds) {x. d x \ n}" by (rule dickson_gradingD2) qed lemma dickson_gradingE: assumes "dickson_grading d" and "\i::nat. d ((seq::nat \ 'a::plus) i) \ n" obtains i j where "i < j" and "seq i adds seq j" proof - from assms(1) have "almost_full_on (adds) {x. d x \ n}" by (rule dickson_gradingD2) moreover from assms(2) have "\i. seq i \ {x. d x \ n}" by simp ultimately obtain i j where "i < j" and "seq i adds seq j" by (rule almost_full_onD) thus ?thesis .. qed lemma dickson_grading_adds_imp_le: assumes "dickson_grading d" and "s adds t" shows "d s \ d t" proof - from assms(2) obtain u where "t = s + u" .. hence "d t = max (d s) (d u)" by (simp only: dickson_gradingD1[OF assms(1)]) thus ?thesis by simp qed lemma dickson_grading_minus: assumes "dickson_grading d" and "s adds (t::'a::cancel_ab_semigroup_add)" shows "d (t - s) \ d t" proof - from assms(2) obtain u where "t = s + u" .. hence "t - s = u" by simp from assms(1) have "d t = ord_class.max (d s) (d u)" unfolding \t = s + u\ by (rule dickson_gradingD1) thus ?thesis by (simp add: \t - s = u\) qed lemma dickson_grading_lcs: assumes "dickson_grading d" shows "d (lcs s t) \ max (d s) (d t)" proof - from assms have "d (lcs s t) \ d (s + t)" by (rule dickson_grading_adds_imp_le, intro lcs_adds_plus) thus ?thesis by (simp only: dickson_gradingD1[OF assms]) qed lemma dickson_grading_lcs_minus: assumes "dickson_grading d" shows "d (lcs s t - s) \ max (d s) (d t)" proof - from assms have "d (lcs s t - s) \ d (lcs s t)" by (rule dickson_grading_minus, intro adds_lcs) also from assms have "... \ max (d s) (d t)" by (rule dickson_grading_lcs) finally show ?thesis . qed lemma dgrad_set_leI: assumes "\s. s \ S \ \t\T. d s \ d t" shows "dgrad_set_le d S T" using assms by (auto simp: dgrad_set_le_def) lemma dgrad_set_leE: assumes "dgrad_set_le d S T" and "s \ S" obtains t where "t \ T" and "d s \ d t" using assms by (auto simp: dgrad_set_le_def) lemma dgrad_set_exhaust_expl: assumes "finite F" shows "F \ dgrad_set d (Max (d ` F))" proof fix f assume "f \ F" hence "d f \ d ` F" by simp with _ have "d f \ Max (d ` F)" proof (rule Max_ge) from assms show "finite (d ` F)" by auto qed hence "dgrad_set d (d f) \ dgrad_set d (Max (d ` F))" by (auto simp: dgrad_set_def) moreover have "f \ dgrad_set d (d f)" by (simp add: dgrad_set_def) ultimately show "f \ dgrad_set d (Max (d ` F))" .. qed lemma dgrad_set_exhaust: assumes "finite F" obtains m where "F \ dgrad_set d m" proof from assms show "F \ dgrad_set d (Max (d ` F))" by (rule dgrad_set_exhaust_expl) qed lemma dgrad_set_le_trans [trans]: assumes "dgrad_set_le d S T" and "dgrad_set_le d T U" shows "dgrad_set_le d S U" unfolding dgrad_set_le_def proof fix s assume "s \ S" with assms(1) obtain t where "t \ T" and 1: "d s \ d t" by (auto simp add: dgrad_set_le_def) from assms(2) this(1) obtain u where "u \ U" and 2: "d t \ d u" by (auto simp add: dgrad_set_le_def) from this(1) show "\u\U. d s \ d u" proof from 1 2 show "d s \ d u" by (rule le_trans) qed qed lemma dgrad_set_le_Un: "dgrad_set_le d (S \ T) U \ (dgrad_set_le d S U \ dgrad_set_le d T U)" by (auto simp add: dgrad_set_le_def) lemma dgrad_set_le_subset: assumes "S \ T" shows "dgrad_set_le d S T" unfolding dgrad_set_le_def using assms by blast lemma dgrad_set_le_refl: "dgrad_set_le d S S" by (rule dgrad_set_le_subset, fact subset_refl) lemma dgrad_set_le_dgrad_set: assumes "dgrad_set_le d F G" and "G \ dgrad_set d m" shows "F \ dgrad_set d m" proof fix f assume "f \ F" with assms(1) obtain g where "g \ G" and *: "d f \ d g" by (auto simp add: dgrad_set_le_def) from assms(2) this(1) have "g \ dgrad_set d m" .. hence "d g \ m" by (simp add: dgrad_set_def) with * have "d f \ m" by (rule le_trans) thus "f \ dgrad_set d m" by (simp add: dgrad_set_def) qed lemma dgrad_set_dgrad: "p \ dgrad_set d (d p)" by (simp add: dgrad_set_def) lemma dgrad_setI [intro]: assumes "d t \ m" shows "t \ dgrad_set d m" using assms by (auto simp: dgrad_set_def) lemma dgrad_setD: assumes "t \ dgrad_set d m" shows "d t \ m" using assms by (simp add: dgrad_set_def) lemma dgrad_set_zero [simp]: "dgrad_set (\_. 0) m = UNIV" by auto lemma subset_dgrad_set_zero: "F \ dgrad_set (\_. 0) m" by simp lemma dgrad_set_subset: assumes "m \ n" shows "dgrad_set d m \ dgrad_set d n" using assms by (auto simp: dgrad_set_def) lemma dgrad_set_closed_plus: assumes "dickson_grading d" and "s \ dgrad_set d m" and "t \ dgrad_set d m" shows "s + t \ dgrad_set d m" proof - from assms(1) have "d (s + t) = ord_class.max (d s) (d t)" by (rule dickson_gradingD1) also from assms(2, 3) have "... \ m" by (simp add: dgrad_set_def) finally show ?thesis by (simp add: dgrad_set_def) qed lemma dgrad_set_closed_minus: assumes "dickson_grading d" and "s \ dgrad_set d m" and "t adds (s::'a::cancel_ab_semigroup_add)" shows "s - t \ dgrad_set d m" proof - from assms(1, 3) have "d (s - t) \ d s" by (rule dickson_grading_minus) also from assms(2) have "... \ m" by (simp add: dgrad_set_def) finally show ?thesis by (simp add: dgrad_set_def) qed lemma dgrad_set_closed_lcs: assumes "dickson_grading d" and "s \ dgrad_set d m" and "t \ dgrad_set d m" shows "lcs s t \ dgrad_set d m" proof - from assms(1) have "d (lcs s t) \ ord_class.max (d s) (d t)" by (rule dickson_grading_lcs) also from assms(2, 3) have "... \ m" by (simp add: dgrad_set_def) finally show ?thesis by (simp add: dgrad_set_def) qed lemma dickson_gradingD_dgrad_set: "dickson_grading d \ almost_full_on (adds) (dgrad_set d m)" by (auto dest: dickson_gradingD2 simp: dgrad_set_def) lemma ex_finite_adds: assumes "dickson_grading d" and "S \ dgrad_set d m" obtains T where "finite T" and "T \ S" and "\s. s \ S \ (\t\T. t adds (s::'a::cancel_comm_monoid_add))" proof - have "reflp ((adds)::'a \ _)" by (simp add: reflp_def) moreover from assms(2) have "almost_full_on (adds) S" proof (rule almost_full_on_subset) from assms(1) show "almost_full_on (adds) (dgrad_set d m)" by (rule dickson_gradingD_dgrad_set) qed ultimately obtain T where "finite T" and "T \ S" and "\s. s \ S \ (\t\T. t adds s)" by (rule almost_full_on_finite_subsetE, blast) thus ?thesis .. qed class graded_dickson_powerprod = ulcs_powerprod + assumes ex_dgrad: "\d::'a \ nat. dickson_grading d" begin definition dgrad_dummy where "dgrad_dummy = (SOME d. dickson_grading d)" lemma dickson_grading_dgrad_dummy: "dickson_grading dgrad_dummy" unfolding dgrad_dummy_def using ex_dgrad by (rule someI_ex) end (* graded_dickson_powerprod *) class dickson_powerprod = ulcs_powerprod + assumes dickson: "almost_full_on (adds) UNIV" begin lemma dickson_grading_zero: "dickson_grading (\_::'a. 0)" by (simp add: dickson_grading_def dickson) subclass graded_dickson_powerprod by (standard, rule, fact dickson_grading_zero) end (* dickson_powerprod *) text \Class @{class graded_dickson_powerprod} is a slightly artificial construction. It is needed, because type @{typ "nat \\<^sub>0 nat"} does not satisfy the usual conditions of a "Dickson domain" (as formulated in class @{class dickson_powerprod}), but we still want to use that type as the type of power-products in the computation of Gr\"obner bases. So, we exploit the fact that in a finite set of polynomials (which is the input of Buchberger's algorithm) there is always some "highest" indeterminate that occurs with non-zero exponent, and no "higher" indeterminates are generated during the execution of the algorithm. This allows us to prove that the algorithm terminates, even though there are in principle infinitely many indeterminates.\ subsection \Additive Linear Orderings\ lemma group_eq_aux: "a + (b - a) = (b::'a::ab_group_add)" proof - have "a + (b - a) = b - a + a" by simp also have "... = b" by simp finally show ?thesis . qed class semi_canonically_ordered_monoid_add = ordered_comm_monoid_add + assumes le_imp_add: "a \ b \ (\c. b = a + c)" context canonically_ordered_monoid_add begin subclass semi_canonically_ordered_monoid_add by (standard, simp only: le_iff_add) end class add_linorder_group = ordered_ab_semigroup_add_imp_le + ab_group_add + linorder class add_linorder = ordered_ab_semigroup_add_imp_le + cancel_comm_monoid_add + semi_canonically_ordered_monoid_add + linorder begin subclass ordered_comm_monoid_add .. subclass ordered_cancel_comm_monoid_add .. lemma le_imp_inv: assumes "a \ b" shows "b = a + (b - a)" using le_imp_add[OF assms] by auto lemma max_eq_sum: obtains y where "max a b = a + y" unfolding max_def proof (cases "a \ b") case True hence "b = a + (b - a)" by (rule le_imp_inv) then obtain c where eq: "b = a + c" .. show ?thesis proof from True show "max a b = a + c" unfolding max_def eq by simp qed next case False show ?thesis proof from False show "max a b = a + 0" unfolding max_def by simp qed qed lemma min_plus_max: shows "(min a b) + (max a b) = a + b" proof (cases "a \ b") case True thus ?thesis unfolding min_def max_def by simp next case False thus ?thesis unfolding min_def max_def by (simp add: ac_simps) qed end (* add_linorder *) class add_linorder_min = add_linorder + assumes zero_min: "0 \ x" begin subclass ninv_comm_monoid_add proof fix x y assume *: "x + y = 0" show "x = 0" proof - from zero_min[of x] have "0 = x \ x > 0" by auto thus ?thesis proof assume "x > 0" have "0 \ y" by (fact zero_min) also have "... = 0 + y" by simp also from \x > 0\ have "... < x + y" by (rule add_strict_right_mono) finally have "0 < x + y" . hence "x + y \ 0" by simp from this * show ?thesis .. qed simp qed qed lemma leq_add_right: shows "x \ x + y" using add_left_mono[OF zero_min[of y], of x] by simp lemma leq_add_left: shows "x \ y + x" using add_right_mono[OF zero_min[of y], of x] by simp subclass canonically_ordered_monoid_add by (standard, rule, elim le_imp_add, elim exE, simp add: leq_add_right) end (* add_linorder_min *) class add_wellorder = add_linorder_min + wellorder instantiation nat :: add_linorder begin instance by (standard, simp) end (* add_linorder *) instantiation nat :: add_linorder_min begin instance by (standard, simp) end instantiation nat :: add_wellorder begin instance .. end context add_linorder_group begin subclass add_linorder proof (standard, intro exI) fix a b show "b = a + (b - a)" using add_commute local.diff_add_cancel by auto qed end (* add_linorder_group *) instantiation int :: add_linorder_group begin instance .. end instantiation rat :: add_linorder_group begin instance .. end instantiation real :: add_linorder_group begin instance .. end subsection \Ordered Power-Products\ locale ordered_powerprod = ordered_powerprod_lin: linorder ord ord_strict for ord::"'a \ 'a::comm_powerprod \ bool" (infixl "\" 50) and ord_strict::"'a \ 'a::comm_powerprod \ bool" (infixl "\" 50) + assumes zero_min: "0 \ t" assumes plus_monotone: "s \ t \ s + u \ t + u" begin abbreviation ord_conv (infixl "\" 50) where "ord_conv \ (\)\\" abbreviation ord_strict_conv (infixl "\" 50) where "ord_strict_conv \ (\)\\" lemma ord_canc: assumes "s + u \ t + u" shows "s \ t" proof (rule ordered_powerprod_lin.le_cases[of s t], simp) assume "t \ s" from assms plus_monotone[OF this, of u] have "t + u = s + u" using ordered_powerprod_lin.order.eq_iff by simp hence "t = s" by simp thus "s \ t" by simp qed lemma ord_adds: assumes "s adds t" shows "s \ t" proof - from assms have "\u. t = s + u" unfolding adds_def by simp then obtain k where "t = s + k" .. thus ?thesis using plus_monotone[OF zero_min[of k], of s] by (simp add: ac_simps) qed lemma ord_canc_left: assumes "u + s \ u + t" shows "s \ t" using assms unfolding add.commute[of u] by (rule ord_canc) lemma ord_strict_canc: assumes "s + u \ t + u" shows "s \ t" using assms ord_canc[of s u t] add_right_cancel[of s u t] ordered_powerprod_lin.le_imp_less_or_eq ordered_powerprod_lin.order.strict_implies_order by blast lemma ord_strict_canc_left: assumes "u + s \ u + t" shows "s \ t" using assms unfolding add.commute[of u] by (rule ord_strict_canc) lemma plus_monotone_left: assumes "s \ t" shows "u + s \ u + t" using assms by (simp add: add.commute, rule plus_monotone) lemma plus_monotone_strict: assumes "s \ t" shows "s + u \ t + u" using assms by (simp add: ordered_powerprod_lin.order.strict_iff_order plus_monotone) lemma plus_monotone_strict_left: assumes "s \ t" shows "u + s \ u + t" using assms by (simp add: ordered_powerprod_lin.order.strict_iff_order plus_monotone_left) end locale gd_powerprod = ordered_powerprod ord ord_strict for ord::"'a \ 'a::graded_dickson_powerprod \ bool" (infixl "\" 50) and ord_strict (infixl "\" 50) begin definition dickson_le :: "('a \ nat) \ nat \ 'a \ 'a \ bool" where "dickson_le d m s t \ (d s \ m \ d t \ m \ s \ t)" definition dickson_less :: "('a \ nat) \ nat \ 'a \ 'a \ bool" where "dickson_less d m s t \ (d s \ m \ d t \ m \ s \ t)" lemma dickson_leI: assumes "d s \ m" and "d t \ m" and "s \ t" shows "dickson_le d m s t" using assms by (simp add: dickson_le_def) lemma dickson_leD1: assumes "dickson_le d m s t" shows "d s \ m" using assms by (simp add: dickson_le_def) lemma dickson_leD2: assumes "dickson_le d m s t" shows "d t \ m" using assms by (simp add: dickson_le_def) lemma dickson_leD3: assumes "dickson_le d m s t" shows "s \ t" using assms by (simp add: dickson_le_def) lemma dickson_le_trans: assumes "dickson_le d m s t" and "dickson_le d m t u" shows "dickson_le d m s u" using assms by (auto simp add: dickson_le_def) lemma dickson_lessI: assumes "d s \ m" and "d t \ m" and "s \ t" shows "dickson_less d m s t" using assms by (simp add: dickson_less_def) lemma dickson_lessD1: assumes "dickson_less d m s t" shows "d s \ m" using assms by (simp add: dickson_less_def) lemma dickson_lessD2: assumes "dickson_less d m s t" shows "d t \ m" using assms by (simp add: dickson_less_def) lemma dickson_lessD3: assumes "dickson_less d m s t" shows "s \ t" using assms by (simp add: dickson_less_def) lemma dickson_less_irrefl: "\ dickson_less d m t t" by (simp add: dickson_less_def) lemma dickson_less_trans: assumes "dickson_less d m s t" and "dickson_less d m t u" shows "dickson_less d m s u" using assms by (auto simp add: dickson_less_def) lemma transp_dickson_less: "transp (dickson_less d m)" by (rule transpI, fact dickson_less_trans) lemma wfp_on_ord_strict: assumes "dickson_grading d" shows "wfp_on (\) {x. d x \ n}" proof - let ?A = "{x. d x \ n}" have "strict (\) = (\)" by (intro ext, simp only: ordered_powerprod_lin.less_le_not_le) have "qo_on (adds) ?A" by (auto simp: qo_on_def reflp_on_def transp_on_def dest: adds_trans) moreover from assms have "wqo_on (adds) ?A" by (rule dickson_gradingD2') ultimately have "(\Q. (\x\?A. \y\?A. x adds y \ Q x y) \ qo_on Q ?A \ wfp_on (strict Q) ?A)" by (simp only: wqo_extensions_wf_conv) hence "(\x\?A. \y\?A. x adds y \ x \ y) \ qo_on (\) ?A \ wfp_on (strict (\)) ?A" .. thus ?thesis unfolding \strict (\) = (\)\ proof show "(\x\?A. \y\?A. x adds y \ x \ y) \ qo_on (\) ?A" proof (intro conjI ballI impI ord_adds) show "qo_on (\) ?A" by (auto simp: qo_on_def reflp_on_def transp_on_def) qed qed qed lemma wf_dickson_less: assumes "dickson_grading d" shows "wfP (dickson_less d m)" proof (rule wfP_chain) show "\ (\seq. \i. dickson_less d m (seq (Suc i)) (seq i))" proof assume "\seq. \i. dickson_less d m (seq (Suc i)) (seq i)" then obtain seq::"nat \ 'a" where "\i. dickson_less d m (seq (Suc i)) (seq i)" .. hence *: "\i. dickson_less d m (seq (Suc i)) (seq i)" .. with transp_dickson_less have seq_decr: "\i j. i < j \ dickson_less d m (seq j) (seq i)" by (rule transp_sequence) from assms obtain i j where "i < j" and i_adds_j: "seq i adds seq j" proof (rule dickson_gradingE) fix i from * show "d (seq i) \ m" by (rule dickson_lessD2) qed from \i < j\ have "dickson_less d m (seq j) (seq i)" by (rule seq_decr) hence "seq j \ seq i" by (rule dickson_lessD3) moreover from i_adds_j have "seq i \ seq j" by (rule ord_adds) ultimately show False by simp qed qed end text \\gd_powerprod\ stands for @{emph \graded ordered Dickson power-products\}.\ locale od_powerprod = ordered_powerprod ord ord_strict for ord::"'a \ 'a::dickson_powerprod \ bool" (infixl "\" 50) and ord_strict (infixl "\" 50) begin sublocale gd_powerprod by standard lemma wf_ord_strict: "wfP (\)" proof (rule wfP_chain) show "\ (\seq. \i. seq (Suc i) \ seq i)" proof assume "\seq. \i. seq (Suc i) \ seq i" then obtain seq::"nat \ 'a" where "\i. seq (Suc i) \ seq i" .. hence "\i. seq (Suc i) \ seq i" .. with ordered_powerprod_lin.transp_less have seq_decr: "\i j. i < j \ (seq j) \ (seq i)" by (rule transp_sequence) from dickson obtain i j::nat where "i < j" and i_adds_j: "seq i adds seq j" by (auto elim!: almost_full_onD) from seq_decr[OF \i < j\] have "seq j \ seq i \ seq j \ seq i" by auto hence "seq j \ seq i" and "seq j \ seq i" by simp_all from \seq j \ seq i\ \seq j \ seq i\ ord_adds[OF i_adds_j] ordered_powerprod_lin.order.eq_iff[of "seq j" "seq i"] show False by simp qed qed end text \\od_powerprod\ stands for @{emph \ordered Dickson power-products\}.\ subsection \Functions as Power-Products\ lemma finite_neq_0: assumes fin_A: "finite {x. f x \ 0}" and fin_B: "finite {x. g x \ 0}" and "\x. h x 0 0 = 0" shows "finite {x. h x (f x) (g x) \ 0}" proof - from fin_A fin_B have "finite ({x. f x \ 0} \ {x. g x \ 0})" by (intro finite_UnI) hence finite_union: "finite {x. (f x \ 0) \ (g x \ 0)}" by (simp only: Collect_disj_eq) have "{x. h x (f x) (g x) \ 0} \ {x. (f x \ 0) \ (g x \ 0)}" proof (intro Collect_mono, rule) fix x::'a assume h_not_zero: "h x (f x) (g x) \ 0" have "f x = 0 \ g x \ 0" proof assume "f x = 0" "g x = 0" thus False using h_not_zero \h x 0 0 = 0\ by simp qed thus "f x \ 0 \ g x \ 0" by auto qed from finite_subset[OF this] finite_union show "finite {x. h x (f x) (g x) \ 0}" . qed lemma finite_neq_0': assumes "finite {x. f x \ 0}" and "finite {x. g x \ 0}" and "h 0 0 = 0" shows "finite {x. h (f x) (g x) \ 0}" using assms by (rule finite_neq_0) lemma finite_neq_0_inv: assumes fin_A: "finite {x. h x (f x) (g x) \ 0}" and fin_B: "finite {x. f x \ 0}" and "\x y. h x 0 y = y" shows "finite {x. g x \ 0}" proof - from fin_A and fin_B have "finite ({x. h x (f x) (g x) \ 0} \ {x. f x \ 0})" by (intro finite_UnI) hence finite_union: "finite {x. (h x (f x) (g x) \ 0) \ f x \ 0}" by (simp only: Collect_disj_eq) have "{x. g x \ 0} \ {x. (h x (f x) (g x) \ 0) \ f x \ 0}" by (intro Collect_mono, rule, rule disjCI, simp add: assms(3)) from this finite_union show "finite {x. g x \ 0}" by (rule finite_subset) qed lemma finite_neq_0_inv': assumes inf_A: "finite {x. h (f x) (g x) \ 0}" and fin_B: "finite {x. f x \ 0}" and "\x. h 0 x = x" shows "finite {x. g x \ 0}" using assms by (rule finite_neq_0_inv) subsubsection \@{typ "'a \ 'b"} belongs to class @{class comm_powerprod}\ instance "fun" :: (type, cancel_comm_monoid_add) comm_powerprod by standard subsubsection \@{typ "'a \ 'b"} belongs to class @{class ninv_comm_monoid_add}\ instance "fun" :: (type, ninv_comm_monoid_add) ninv_comm_monoid_add by (standard, simp only: plus_fun_def zero_fun_def fun_eq_iff, intro allI, rule plus_eq_zero, auto) subsubsection \@{typ "'a \ 'b"} belongs to class @{class lcs_powerprod}\ instantiation "fun" :: (type, add_linorder) lcs_powerprod begin definition lcs_fun::"('a \ 'b) \ ('a \ 'b) \ ('a \ 'b)" where "lcs f g = (\x. max (f x) (g x))" lemma adds_funI: assumes "s \ t" shows "s adds (t::'a \ 'b)" proof (rule addsI, rule) fix x from assms have "s x \ t x" unfolding le_fun_def .. hence "t x = s x + (t x - s x)" by (rule le_imp_inv) thus "t x = (s + (t - s)) x" by simp qed lemma adds_fun_iff: "f adds (g::'a \ 'b) \ (\x. f x adds g x)" unfolding adds_def plus_fun_def by metis lemma adds_fun_iff': "f adds (g::'a \ 'b) \ (\x. \y. g x = f x + y)" unfolding adds_fun_iff unfolding adds_def plus_fun_def .. lemma adds_lcs_fun: shows "s adds (lcs s (t::'a \ 'b))" by (rule adds_funI, simp only: le_fun_def lcs_fun_def, auto simp: max_def) lemma lcs_comm_fun: "lcs s t = lcs t (s::'a \ 'b)" unfolding lcs_fun_def by (auto simp: max_def intro!: ext) lemma lcs_adds_fun: assumes "s adds u" and "t adds (u::'a \ 'b)" shows "(lcs s t) adds u" using assms unfolding lcs_fun_def adds_fun_iff' proof - assume a1: "\x. \y. u x = s x + y" and a2: "\x. \y. u x = t x + y" show "\x. \y. u x = max (s x) (t x) + y" proof fix x from a1 have b1: "\y. u x = s x + y" .. from a2 have b2: "\y. u x = t x + y" .. show "\y. u x = max (s x) (t x) + y" unfolding max_def by (split if_split, intro conjI impI, rule b2, rule b1) qed qed instance apply standard subgoal by (rule adds_lcs_fun) subgoal by (rule lcs_adds_fun) subgoal by (rule lcs_comm_fun) done end lemma leq_lcs_fun_1: "s \ (lcs s (t::'a \ 'b::add_linorder))" by (simp add: lcs_fun_def le_fun_def) lemma leq_lcs_fun_2: "t \ (lcs s (t::'a \ 'b::add_linorder))" by (simp add: lcs_fun_def le_fun_def) lemma lcs_leq_fun: assumes "s \ u" and "t \ (u::'a \ 'b::add_linorder)" shows "(lcs s t) \ u" using assms by (simp add: lcs_fun_def le_fun_def) lemma adds_fun: "s adds t \ s \ t" for s t::"'a \ 'b::add_linorder_min" proof assume "s adds t" from this obtain k where "t = s + k" .. show "s \ t" unfolding \t = s + k\ le_fun_def plus_fun_def le_iff_add by (simp add: leq_add_right) qed (rule adds_funI) lemma gcs_fun: "gcs s (t::'a \ ('b::add_linorder)) = (\x. min (s x) (t x))" proof - show ?thesis unfolding gcs_def lcs_fun_def fun_diff_def proof (simp, rule) fix x have eq: "s x + t x = max (s x) (t x) + min (s x) (t x)" by (metis add.commute min_def max_def) thus "s x + t x - max (s x) (t x) = min (s x) (t x)" by simp qed qed lemma gcs_leq_fun_1: "(gcs s (t::'a \ 'b::add_linorder)) \ s" by (simp add: gcs_fun le_fun_def) lemma gcs_leq_fun_2: "(gcs s (t::'a \ 'b::add_linorder)) \ t" by (simp add: gcs_fun le_fun_def) lemma leq_gcs_fun: assumes "u \ s" and "u \ (t::'a \ 'b::add_linorder)" shows "u \ (gcs s t)" using assms by (simp add: gcs_fun le_fun_def) subsubsection \@{typ "'a \ 'b"} belongs to class @{class ulcs_powerprod}\ instance "fun" :: (type, add_linorder_min) ulcs_powerprod .. subsubsection \Power-products in a given set of indeterminates\ definition supp_fun::"('a \ 'b::zero) \ 'a set" where "supp_fun f = {x. f x \ 0}" text \@{term supp_fun} for general functions is like @{term keys} for @{type poly_mapping}, but does not need to be finite.\ lemma keys_eq_supp: "keys s = supp_fun (lookup s)" unfolding supp_fun_def by (transfer, rule) lemma supp_fun_zero [simp]: "supp_fun 0 = {}" by (auto simp: supp_fun_def) lemma supp_fun_eq_zero_iff: "supp_fun f = {} \ f = 0" by (auto simp: supp_fun_def) lemma sub_supp_empty: "supp_fun s \ {} \ (s = 0)" by (auto simp: supp_fun_def) lemma except_fun_idI: "supp_fun f \ V = {} \ except_fun f V = f" by (auto simp: except_fun_def supp_fun_def when_def intro!: ext) lemma supp_except_fun: "supp_fun (except_fun s V) = supp_fun s - V" by (auto simp: except_fun_def supp_fun_def) lemma supp_fun_plus_subset: "supp_fun (s + t) \ supp_fun s \ supp_fun (t::'a \ 'b::monoid_add)" unfolding supp_fun_def by force lemma fun_eq_zeroI: assumes "\x. x \ supp_fun f \ f x = 0" shows "f = 0" proof (rule, simp) fix x show "f x = 0" proof (cases "x \ supp_fun f") case True then show ?thesis by (rule assms) next case False then show ?thesis by (simp add: supp_fun_def) qed qed lemma except_fun_cong1: "supp_fun s \ ((V - U) \ (U - V)) \ {} \ except_fun s V = except_fun s U" by (auto simp: except_fun_def when_def supp_fun_def intro!: ext) lemma adds_except_fun: "s adds t = (except_fun s V adds except_fun t V \ except_fun s (- V) adds except_fun t (- V))" for s t :: "'a \ 'b::add_linorder" by (auto simp: supp_fun_def except_fun_def adds_fun_iff when_def) lemma adds_except_fun_singleton: "s adds t = (except_fun s {v} adds except_fun t {v} \ s v adds t v)" for s t :: "'a \ 'b::add_linorder" by (auto simp: supp_fun_def except_fun_def adds_fun_iff when_def) subsubsection \Dickson's lemma for power-products in finitely many indeterminates\ lemma Dickson_fun: assumes "finite V" shows "almost_full_on (adds) {x::'a \ 'b::add_wellorder. supp_fun x \ V}" using assms proof (induct V) case empty have "finite {0}" by simp - moreover have "reflp_on (adds) {0::'a \ 'b}" by (simp add: reflp_on_def) + moreover have "reflp_on {0::'a \ 'b} (adds)" by (simp add: reflp_on_def) ultimately have "almost_full_on (adds) {0::'a \ 'b}" by (rule finite_almost_full_on) thus ?case by (simp add: supp_fun_eq_zero_iff) next case (insert v V) show ?case proof (rule almost_full_onI) fix seq::"nat \ 'a \ 'b" assume "\i. seq i \ {x. supp_fun x \ insert v V}" hence a: "supp_fun (seq i) \ insert v V" for i by simp define seq' where "seq' = (\i. (except_fun (seq i) {v}, except_fun (seq i) V))" have "almost_full_on (adds) {x::'a \ 'b. supp_fun x \ {v}}" proof (rule almost_full_onI) fix f::"nat \ 'a \ 'b" assume "\i. f i \ {x. supp_fun x \ {v}}" hence b: "supp_fun (f i) \ {v}" for i by simp let ?f = "\i. f i v" have "wfP ((<)::'b \ _)" by (simp add: wf wfP_def) hence "\f::nat \ 'b. \i. f i \ f (Suc i)" by (simp add: wf_iff_no_infinite_down_chain[to_pred] not_less) hence "\i. ?f i \ ?f (Suc i)" .. then obtain i where "?f i \ ?f (Suc i)" .. have "i < Suc i" by simp moreover have "f i adds f (Suc i)" unfolding adds_fun_iff proof fix x show "f i x adds f (Suc i) x" proof (cases "x = v") case True with \?f i \ ?f (Suc i)\ show ?thesis by (simp add: adds_def le_iff_add) next case False with b have "x \ supp_fun (f i)" and "x \ supp_fun (f (Suc i))" by blast+ thus ?thesis by (simp add: supp_fun_def) qed qed ultimately show "good (adds) f" by (meson goodI) qed with insert(3) have "almost_full_on (prod_le (adds) (adds)) ({x::'a \ 'b. supp_fun x \ V} \ {x::'a \ 'b. supp_fun x \ {v}})" (is "almost_full_on ?P ?A") by (rule almost_full_on_Sigma) moreover from a have "seq' i \ ?A" for i by (auto simp add: seq'_def supp_except_fun) ultimately obtain i j where "i < j" and "?P (seq' i) (seq' j)" by (rule almost_full_onD) have "seq i adds seq j" unfolding adds_except_fun[where s="seq i" and V=V] proof from \?P (seq' i) (seq' j)\ show "except_fun (seq i) V adds except_fun (seq j) V" by (simp add: prod_le_def seq'_def) next from \?P (seq' i) (seq' j)\ have "except_fun (seq i) {v} adds except_fun (seq j) {v}" by (simp add: prod_le_def seq'_def) moreover have "except_fun (seq i) (- V) = except_fun (seq i) {v}" by (rule except_fun_cong1; use a[of i] insert.hyps(2) in blast) moreover have "except_fun (seq j) (- V) = except_fun (seq j) {v}" by (rule except_fun_cong1; use a[of j] insert.hyps(2) in blast) ultimately show "except_fun (seq i) (- V) adds except_fun (seq j) (- V)" by simp qed with \i < j\ show "good (adds) seq" by (meson goodI) qed qed instance "fun" :: (finite, add_wellorder) dickson_powerprod proof have "finite (UNIV::'a set)" by simp hence "almost_full_on (adds) {x::'a \ 'b. supp_fun x \ UNIV}" by (rule Dickson_fun) thus "almost_full_on (adds) (UNIV::('a \ 'b) set)" by simp qed subsubsection \Lexicographic Term Order\ text \Term orders are certain linear orders on power-products, satisfying additional requirements. Further information on term orders can be found, e.\,g., in @{cite Robbiano1985}.\ context wellorder begin lemma neq_fun_alt: assumes "s \ (t::'a \ 'b)" obtains x where "s x \ t x" and "\y. s y \ t y \ x \ y" proof - from assms ext[of s t] have "\x. s x \ t x" by auto with exists_least_iff[of "\x. s x \ t x"] obtain x where x1: "s x \ t x" and x2: "\y. y < x \ s y = t y" by auto show ?thesis proof from x1 show "s x \ t x" . next fix y assume "s y \ t y" with x2[of y] have "\ y < x" by auto thus "x \ y" by simp qed qed definition lex_fun::"('a \ 'b) \ ('a \ 'b::order) \ bool" where "lex_fun s t \ (\x. s x \ t x \ (\y t y))" definition "lex_fun_strict s t \ lex_fun s t \ \ lex_fun t s" text \Attention! @{term lex_fun} reverses the order of the indeterminates: if @{term x} is smaller than @{term y} w.r.t. the order on @{typ 'a}, then the @{emph \power-product\} @{term x} is @{emph \greater\} than the @{emph \power-product\} @{term y}.\ lemma lex_fun_alt: shows "lex_fun s t = (s = t \ (\x. s x < t x \ (\y t" from neq_fun_alt[OF this] obtain x0 where x0_neq: "s x0 \ t x0" and x0_min: "\z. s z \ t z \ x0 \ z" by auto show ?R proof (intro disjI2, rule exI[of _ x0], intro conjI) from \?L\ have "s x0 \ t x0 \ (\y. y < x0 \ s y \ t y)" unfolding lex_fun_def .. thus "s x0 < t x0" proof assume "s x0 \ t x0" from this x0_neq show ?thesis by simp next assume "\y. y < x0 \ s y \ t y" then obtain y where "y < x0" and y_neq: "s y \ t y" by auto from \y < x0\ x0_min[OF y_neq] show ?thesis by simp qed next show "\y x0 \ y" by simp from this x0_min[of y] show "s y = t y" by auto qed qed qed next assume ?R thus ?L proof assume "s = t" thus ?thesis by (simp add: lex_fun_def) next assume "\x. s x < t x \ (\yz t x \ (\y t y)" proof (cases "s x \ t x") assume "s x \ t x" thus ?thesis by simp next assume x: "\ s x \ t x" show ?thesis proof (intro disjI2, rule exI[of _ y], intro conjI) have "\ x \ y" proof assume "x \ y" hence "x < y \ y = x" by auto thus False proof assume "x < y" from x y_min[rule_format, OF this] show ?thesis by simp next assume "y = x" from this x y show ?thesis by (auto simp: preorder_class.less_le_not_le) qed qed thus "y < x" by simp next from y show "s y \ t y" by simp qed qed qed qed qed lemma lex_fun_refl: "lex_fun s s" unfolding lex_fun_alt by simp lemma lex_fun_antisym: assumes "lex_fun s t" and "lex_fun t s" shows "s = t" proof fix x from assms(1) have "s = t \ (\x. s x < t x \ (\yx. s x < t x \ (\yy (\x. t x < s x \ (\yx. t x < s x \ (\yy x1 < x0 \ x1 = x0" using local.antisym_conv3 by auto show ?thesis proof (rule linorder_cases[of x0 x1]) assume "x1 < x0" from x0_min[rule_format, OF this] x1 show ?thesis by simp next assume "x0 = x1" from this x0 x1 show ?thesis by simp next assume "x0 < x1" from x1_min[rule_format, OF this] x0 show ?thesis by simp qed qed qed qed lemma lex_fun_trans: assumes "lex_fun s t" and "lex_fun t u" shows "lex_fun s u" proof - from assms(1) have "s = t \ (\x. s x < t x \ (\yx. s x < t x \ (\yy (\x. t x < u x \ (\yx. t x < u x \ (\yyx. s x < u x \ (\yx1 < x0\] x1 show "s x1 < u x1" by simp next show "\yx1 < x0\ have "y < x0" by simp from x0_min[rule_format, OF this] x1_min[rule_format, OF \y < x1\] show "s y = u y" by simp qed qed next assume "x0 < x1" show ?thesis proof (rule exI[of _ x0], intro conjI) from x1_min[rule_format, OF \x0 < x1\] x0 show "s x0 < u x0" by simp next show "\yx0 < x1\ have "y < x1" by simp from x0_min[rule_format, OF \y < x0\] x1_min[rule_format, OF this] show "s y = u y" by simp qed qed next assume "x0 = x1" show ?thesis proof (rule exI[of _ x1], intro conjI) from \x0 = x1\ x0 x1 show "s x1 < u x1" by simp next show "\yx0 = x1\ by simp from x0_min[rule_format, OF this] x1_min[rule_format, OF \y < x1\] show "s y = u y" by simp qed qed qed qed qed qed qed lemma lex_fun_lin: "lex_fun s t \ lex_fun t s" for s t::"'a \ 'b::{ordered_comm_monoid_add, linorder}" proof (intro disjCI) assume "\ lex_fun t s" hence a: "\x. \ (t x < s x) \ (\y s y)" unfolding lex_fun_alt by auto show "lex_fun s t" unfolding lex_fun_def proof fix x from a have "\ (t x < s x) \ (\y s y)" .. thus "s x \ t x \ (\y t y)" by auto qed qed corollary lex_fun_strict_alt [code]: "lex_fun_strict s t = (\ lex_fun t s)" for s t::"'a \ 'b::{ordered_comm_monoid_add, linorder}" unfolding lex_fun_strict_def using lex_fun_lin[of s t] by auto lemma lex_fun_zero_min: "lex_fun 0 s" for s::"'a \ 'b::add_linorder_min" by (simp add: lex_fun_def zero_min) lemma lex_fun_plus_monotone: "lex_fun (s + u) (t + u)" if "lex_fun s t" for s t::"'a \ 'b::ordered_cancel_comm_monoid_add" unfolding lex_fun_def proof fix x from that have "s x \ t x \ (\y t y)" unfolding lex_fun_def .. thus "(s + u) x \ (t + u) x \ (\y (t + u) y)" proof assume a1: "s x \ t x" show ?thesis proof (intro disjI1) from a1 show "(s + u) x \ (t + u) x" by (auto simp: add_right_mono) qed next assume "\y t y" then obtain y where "y < x" and a2: "s y \ t y" by auto show ?thesis proof (intro disjI2, rule exI[of _ y], intro conjI, fact) from a2 show "(s + u) y \ (t + u) y" by (auto simp: add_right_mono) qed qed qed end (* wellorder *) subsubsection \Degree\ definition deg_fun::"('a \ 'b::comm_monoid_add) \ 'b" where "deg_fun s \ \x\(supp_fun s). s x" lemma deg_fun_zero[simp]: "deg_fun 0 = 0" by (auto simp: deg_fun_def) lemma deg_fun_eq_0_iff: assumes "finite (supp_fun (s::'a \ 'b::add_linorder_min))" shows "deg_fun s = 0 \ s = 0" proof assume "deg_fun s = 0" hence *: "(\x\(supp_fun s). s x) = 0" by (simp only: deg_fun_def) have **: "\x. 0 \ s x" by (rule zero_min) from * have "\x. x \ supp_fun s \ s x = 0" by (simp only: sum_nonneg_eq_0_iff[OF assms **]) thus "s = 0" by (rule fun_eq_zeroI) qed simp lemma deg_fun_superset: fixes A::"'a set" assumes "supp_fun s \ A" and "finite A" shows "deg_fun s = (\x\A. s x)" unfolding deg_fun_def proof (rule sum.mono_neutral_cong_left, fact, fact, rule) fix x assume "x \ A - supp_fun s" hence "x \ supp_fun s" by simp thus "s x = 0" by (simp add: supp_fun_def) qed rule lemma deg_fun_plus: assumes "finite (supp_fun s)" and "finite (supp_fun t)" shows "deg_fun (s + t) = deg_fun s + deg_fun (t::'a \ 'b::comm_monoid_add)" proof - from assms have fin: "finite (supp_fun s \ supp_fun t)" by simp have "deg_fun (s + t) = (\x\(supp_fun (s + t)). s x + t x)" by (simp add: deg_fun_def) also from fin have "... = (\x\(supp_fun s \ supp_fun t). s x + t x)" proof (rule sum.mono_neutral_cong_left) show "\x\supp_fun s \ supp_fun t - supp_fun (s + t). s x + t x = 0" proof fix x assume "x \ supp_fun s \ supp_fun t - supp_fun (s + t)" hence "x \ supp_fun (s + t)" by simp thus "s x + t x = 0" by (simp add: supp_fun_def) qed qed (rule supp_fun_plus_subset, rule) also have "\ = (\x\(supp_fun s \ supp_fun t). s x) + (\x\(supp_fun s \ supp_fun t). t x)" by (rule sum.distrib) also from fin have "(\x\(supp_fun s \ supp_fun t). s x) = deg_fun s" unfolding deg_fun_def proof (rule sum.mono_neutral_cong_right) show "\x\supp_fun s \ supp_fun t - supp_fun s. s x = 0" proof fix x assume "x \ supp_fun s \ supp_fun t - supp_fun s" hence "x \ supp_fun s" by simp thus "s x = 0" by (simp add: supp_fun_def) qed qed simp_all also from fin have "(\x\(supp_fun s \ supp_fun t). t x) = deg_fun t" unfolding deg_fun_def proof (rule sum.mono_neutral_cong_right) show "\x\supp_fun s \ supp_fun t - supp_fun t. t x = 0" proof fix x assume "x \ supp_fun s \ supp_fun t - supp_fun t" hence "x \ supp_fun t" by simp thus "t x = 0" by (simp add: supp_fun_def) qed qed simp_all finally show ?thesis . qed lemma deg_fun_leq: assumes "finite (supp_fun s)" and "finite (supp_fun t)" and "s \ (t::'a \ 'b::ordered_comm_monoid_add)" shows "deg_fun s \ deg_fun t" proof - let ?A = "supp_fun s \ supp_fun t" from assms(1) assms(2) have 1: "finite ?A" by simp have s: "supp_fun s \ ?A" and t: "supp_fun t \ ?A" by simp_all show ?thesis unfolding deg_fun_superset[OF s 1] deg_fun_superset[OF t 1] proof (rule sum_mono) fix i from assms(3) show "s i \ t i" unfolding le_fun_def .. qed qed subsubsection \General Degree-Orders\ context linorder begin lemma ex_min: assumes "finite (A::'a set)" and "A \ {}" shows "\y\A. (\z\A. y \ z)" using assms proof (induct rule: finite_induct) assume "{} \ {}" thus "\y\{}. \z\{}. y \ z" by simp next fix a::'a and A::"'a set" assume "a \ A" and IH: "A \ {} \ \y\A. (\z\A. y \ z)" show "\y\insert a A. (\z\insert a A. y \ z)" proof (cases "A = {}") case True show ?thesis proof (rule bexI[of _ a], intro ballI) fix z assume "z \ insert a A" from this True have "z = a" by simp thus "a \ z" by simp qed (simp) next case False from IH[OF False] obtain y where "y \ A" and y_min: "\z\A. y \ z" by auto from linear[of a y] show ?thesis proof assume "y \ a" show ?thesis proof (rule bexI[of _ y], intro ballI) fix z assume "z \ insert a A" hence "z = a \ z \ A" by simp thus "y \ z" proof assume "z = a" from this \y \ a\ show "y \ z" by simp next assume "z \ A" from y_min[rule_format, OF this] show "y \ z" . qed next from \y \ A\ show "y \ insert a A" by simp qed next assume "a \ y" show ?thesis proof (rule bexI[of _ a], intro ballI) fix z assume "z \ insert a A" hence "z = a \ z \ A" by simp thus "a \ z" proof assume "z = a" from this show "a \ z" by simp next assume "z \ A" from y_min[rule_format, OF this] \a \ y\ show "a \ z" by simp qed qed (simp) qed qed qed definition dord_fun::"(('a \ 'b::ordered_comm_monoid_add) \ ('a \ 'b) \ bool) \ ('a \ 'b) \ ('a \ 'b) \ bool" where "dord_fun ord s t \ (let d1 = deg_fun s; d2 = deg_fun t in (d1 < d2 \ (d1 = d2 \ ord s t)))" lemma dord_fun_degD: assumes "dord_fun ord s t" shows "deg_fun s \ deg_fun t" using assms unfolding dord_fun_def Let_def by auto lemma dord_fun_refl: assumes "ord s s" shows "dord_fun ord s s" using assms unfolding dord_fun_def by simp lemma dord_fun_antisym: assumes ord_antisym: "ord s t \ ord t s \ s = t" and "dord_fun ord s t" and "dord_fun ord t s" shows "s = t" proof - from assms(3) have ts: "deg_fun t < deg_fun s \ (deg_fun t = deg_fun s \ ord t s)" unfolding dord_fun_def Let_def . from assms(2) have st: "deg_fun s < deg_fun t \ (deg_fun s = deg_fun t \ ord s t)" unfolding dord_fun_def Let_def . thus ?thesis proof assume "deg_fun s < deg_fun t" thus ?thesis using ts by auto next assume "deg_fun s = deg_fun t \ ord s t" hence "deg_fun s = deg_fun t" and "ord s t" by simp_all from \deg_fun s = deg_fun t\ ts have "ord t s" by simp with \ord s t\ show ?thesis by (rule ord_antisym) qed qed lemma dord_fun_trans: assumes ord_trans: "ord s t \ ord t u \ ord s u" and "dord_fun ord s t" and "dord_fun ord t u" shows "dord_fun ord s u" proof - from assms(3) have ts: "deg_fun t < deg_fun u \ (deg_fun t = deg_fun u \ ord t u)" unfolding dord_fun_def Let_def . from assms(2) have st: "deg_fun s < deg_fun t \ (deg_fun s = deg_fun t \ ord s t)" unfolding dord_fun_def Let_def . thus ?thesis proof assume "deg_fun s < deg_fun t" from this dord_fun_degD[OF assms(3)] have "deg_fun s < deg_fun u" by simp thus ?thesis by (simp add: dord_fun_def Let_def) next assume "deg_fun s = deg_fun t \ ord s t" hence "deg_fun s = deg_fun t" and "ord s t" by simp_all from ts show ?thesis proof assume "deg_fun t < deg_fun u" hence "deg_fun s < deg_fun u" using \deg_fun s = deg_fun t\ by simp thus ?thesis by (simp add: dord_fun_def Let_def) next assume "deg_fun t = deg_fun u \ ord t u" hence "deg_fun t = deg_fun u" and "ord t u" by simp_all from ord_trans[OF \ord s t\ \ord t u\] \deg_fun s = deg_fun t\ \deg_fun t = deg_fun u\ show ?thesis by (simp add: dord_fun_def Let_def) qed qed qed lemma dord_fun_lin: "dord_fun ord s t \ dord_fun ord t s" if "ord s t \ ord t s" for s t::"'a \ 'b::{ordered_comm_monoid_add, linorder}" proof (intro disjCI) assume "\ dord_fun ord t s" hence "deg_fun s \ deg_fun t \ (deg_fun t \ deg_fun s \ \ ord t s)" unfolding dord_fun_def Let_def by auto hence "deg_fun s \ deg_fun t" and dis1: "deg_fun t \ deg_fun s \ \ ord t s" by simp_all show "dord_fun ord s t" unfolding dord_fun_def Let_def proof (intro disjCI) assume "\ (deg_fun s = deg_fun t \ ord s t)" hence dis2: "deg_fun s \ deg_fun t \ \ ord s t" by simp show "deg_fun s < deg_fun t" proof (cases "deg_fun s = deg_fun t") case True from True dis1 have "\ ord t s" by simp from True dis2 have "\ ord s t" by simp from \\ ord s t\ \\ ord t s\ that show ?thesis by simp next case False from this \deg_fun s \ deg_fun t\ show ?thesis by simp qed qed qed lemma dord_fun_zero_min: fixes s t::"'a \ 'b::add_linorder_min" assumes ord_refl: "\t. ord t t" and "finite (supp_fun s)" shows "dord_fun ord 0 s" unfolding dord_fun_def Let_def deg_fun_zero proof (rule disjCI) assume "\ (0 = deg_fun s \ ord 0 s)" hence dis: "deg_fun s \ 0 \ \ ord 0 s" by simp show "0 < deg_fun s" proof (cases "deg_fun s = 0") case True hence "s = 0" using deg_fun_eq_0_iff[OF assms(2)] by auto hence "ord 0 s" using ord_refl by simp with True dis show ?thesis by simp next case False thus ?thesis by (auto simp: zero_less_iff_neq_zero) qed qed lemma dord_fun_plus_monotone: fixes s t u ::"'a \ 'b::{ordered_comm_monoid_add, ordered_ab_semigroup_add_imp_le}" assumes ord_monotone: "ord s t \ ord (s + u) (t + u)" and "finite (supp_fun s)" and "finite (supp_fun t)" and "finite (supp_fun u)" and "dord_fun ord s t" shows "dord_fun ord (s + u) (t + u)" proof - from assms(5) have "deg_fun s < deg_fun t \ (deg_fun s = deg_fun t \ ord s t)" unfolding dord_fun_def Let_def . thus ?thesis proof assume "deg_fun s < deg_fun t" hence "deg_fun (s + u) < deg_fun (t + u)" by (auto simp: deg_fun_plus[OF _ assms(4)] assms(2) assms(3)) thus ?thesis unfolding dord_fun_def Let_def by simp next assume "deg_fun s = deg_fun t \ ord s t" hence "deg_fun s = deg_fun t" and "ord s t" by simp_all from \deg_fun s = deg_fun t\ have "deg_fun (s + u) = deg_fun (t + u)" by (auto simp: deg_fun_plus[OF _ assms(4)] assms(2) assms(3)) from this ord_monotone[OF \ord s t\] show ?thesis unfolding dord_fun_def Let_def by simp qed qed end (* linorder *) context wellorder begin subsubsection \Degree-Lexicographic Term Order\ definition dlex_fun::"('a \ 'b::ordered_comm_monoid_add) \ ('a \ 'b) \ bool" where "dlex_fun \ dord_fun lex_fun" definition "dlex_fun_strict s t \ dlex_fun s t \ \ dlex_fun t s" lemma dlex_fun_refl: shows "dlex_fun s s" unfolding dlex_fun_def by (rule dord_fun_refl, rule lex_fun_refl) lemma dlex_fun_antisym: assumes "dlex_fun s t" and "dlex_fun t s" shows "s = t" by (rule dord_fun_antisym, erule lex_fun_antisym, assumption, simp_all only: dlex_fun_def[symmetric], fact+) lemma dlex_fun_trans: assumes "dlex_fun s t" and "dlex_fun t u" shows "dlex_fun s u" by (simp only: dlex_fun_def, rule dord_fun_trans, erule lex_fun_trans, assumption, simp_all only: dlex_fun_def[symmetric], fact+) lemma dlex_fun_lin: "dlex_fun s t \ dlex_fun t s" for s t::"('a \ 'b::{ordered_comm_monoid_add, linorder})" unfolding dlex_fun_def by (rule dord_fun_lin, rule lex_fun_lin) corollary dlex_fun_strict_alt [code]: "dlex_fun_strict s t = (\ dlex_fun t s)" for s t::"'a \ 'b::{ordered_comm_monoid_add, linorder}" unfolding dlex_fun_strict_def using dlex_fun_lin by auto lemma dlex_fun_zero_min: fixes s t::"('a \ 'b::add_linorder_min)" assumes "finite (supp_fun s)" shows "dlex_fun 0 s" unfolding dlex_fun_def by (rule dord_fun_zero_min, rule lex_fun_refl, fact) lemma dlex_fun_plus_monotone: fixes s t u::"'a \ 'b::{ordered_cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}" assumes "finite (supp_fun s)" and "finite (supp_fun t)" and "finite (supp_fun u)" and "dlex_fun s t" shows "dlex_fun (s + u) (t + u)" using lex_fun_plus_monotone[of s t u] assms unfolding dlex_fun_def by (rule dord_fun_plus_monotone) subsubsection \Degree-Reverse-Lexicographic Term Order\ abbreviation rlex_fun::"('a \ 'b) \ ('a \ 'b::order) \ bool" where "rlex_fun s t \ lex_fun t s" text \Note that @{const rlex_fun} is not precisely the reverse-lexicographic order relation on power-products. Normally, the @{emph \last\} (i.\,e. highest) indeterminate whose exponent differs in the two power-products to be compared is taken, but since we do not require the domain to be finite, there might not be such a last indeterminate. Therefore, we simply take the converse of @{const lex_fun}.\ definition drlex_fun::"('a \ 'b::ordered_comm_monoid_add) \ ('a \ 'b) \ bool" where "drlex_fun \ dord_fun rlex_fun" definition "drlex_fun_strict s t \ drlex_fun s t \ \ drlex_fun t s" lemma drlex_fun_refl: shows "drlex_fun s s" unfolding drlex_fun_def by (rule dord_fun_refl, fact lex_fun_refl) lemma drlex_fun_antisym: assumes "drlex_fun s t" and "drlex_fun t s" shows "s = t" by (rule dord_fun_antisym, erule lex_fun_antisym, assumption, simp_all only: drlex_fun_def[symmetric], fact+) lemma drlex_fun_trans: assumes "drlex_fun s t" and "drlex_fun t u" shows "drlex_fun s u" by (simp only: drlex_fun_def, rule dord_fun_trans, erule lex_fun_trans, assumption, simp_all only: drlex_fun_def[symmetric], fact+) lemma drlex_fun_lin: "drlex_fun s t \ drlex_fun t s" for s t::"('a \ 'b::{ordered_comm_monoid_add, linorder})" unfolding drlex_fun_def by (rule dord_fun_lin, rule lex_fun_lin) corollary drlex_fun_strict_alt [code]: "drlex_fun_strict s t = (\ drlex_fun t s)" for s t::"'a \ 'b::{ordered_comm_monoid_add, linorder}" unfolding drlex_fun_strict_def using drlex_fun_lin by auto lemma drlex_fun_zero_min: fixes s t::"('a \ 'b::add_linorder_min)" assumes "finite (supp_fun s)" shows "drlex_fun 0 s" unfolding drlex_fun_def by (rule dord_fun_zero_min, rule lex_fun_refl, fact) lemma drlex_fun_plus_monotone: fixes s t u::"'a \ 'b::{ordered_cancel_comm_monoid_add, ordered_ab_semigroup_add_imp_le}" assumes "finite (supp_fun s)" and "finite (supp_fun t)" and "finite (supp_fun u)" and "drlex_fun s t" shows "drlex_fun (s + u) (t + u)" using lex_fun_plus_monotone[of t s u] assms unfolding drlex_fun_def by (rule dord_fun_plus_monotone) end (* wellorder *) text\Every finite linear ordering is also a well-ordering. This fact is particularly useful when working with fixed finite sets of indeterminates.\ class finite_linorder = finite + linorder begin subclass wellorder proof fix P::"'a \ bool" and a assume hyp: "\x. (\y. (y < x) \ P y) \ P x" show "P a" proof (rule ccontr) assume "\ P a" have "finite {x. \ P x}" (is "finite ?A") by simp from \\ P a\ have "a \ ?A" by simp hence "?A \ {}" by auto from ex_min[OF \finite ?A\ this] obtain b where "b \ ?A" and b_min: "\y\?A. b \ y" by auto from \b \ ?A\ have "\ P b" by simp with hyp[of b] obtain y where "y < b" and "\ P y" by auto from \\ P y\ have "y \ ?A" by simp with b_min have "b \ y" by simp with \y < b\ show False by simp qed qed end subsection \Type @{type poly_mapping}\ lemma poly_mapping_eq_zeroI: assumes "keys s = {}" shows "s = (0::('a, 'b::zero) poly_mapping)" proof (rule poly_mapping_eqI, simp) fix x from assms show "lookup s x = 0" by auto qed lemma keys_plus_ninv_comm_monoid_add: "keys (s + t) = keys s \ keys (t::'a \\<^sub>0 'b::ninv_comm_monoid_add)" proof (rule, fact Poly_Mapping.keys_add, rule) fix x assume "x \ keys s \ keys t" thus "x \ keys (s + t)" proof assume "x \ keys s" thus ?thesis by (metis in_keys_iff lookup_add plus_eq_zero) next assume "x \ keys t" thus ?thesis by (metis in_keys_iff lookup_add plus_eq_zero_2) qed qed lemma lookup_zero_fun: "lookup 0 = 0" by (simp only: zero_poly_mapping.rep_eq zero_fun_def) lemma lookup_plus_fun: "lookup (s + t) = lookup s + lookup t" by (simp only: plus_poly_mapping.rep_eq plus_fun_def) lemma lookup_uminus_fun: "lookup (- s) = - lookup s" by (fact uminus_poly_mapping.rep_eq) lemma lookup_minus_fun: "lookup (s - t) = lookup s - lookup t" by (simp only: minus_poly_mapping.rep_eq, rule, simp only: minus_apply) lemma poly_mapping_adds_iff: "s adds t \ lookup s adds lookup t" unfolding adds_def proof assume "\k. t = s + k" then obtain k where *: "t = s + k" .. show "\k. lookup t = lookup s + k" proof from * show "lookup t = lookup s + lookup k" by (simp only: lookup_plus_fun) qed next assume "\k. lookup t = lookup s + k" then obtain k where *: "lookup t = lookup s + k" .. have **: "k \ {f. finite {x. f x \ 0}}" proof have "finite {x. lookup t x \ 0}" by transfer hence "finite {x. lookup s x + k x \ 0}" by (simp only: * plus_fun_def) moreover have "finite {x. lookup s x \ 0}" by transfer ultimately show "finite {x. k x \ 0}" by (rule finite_neq_0_inv', simp) qed show "\k. t = s + k" proof show "t = s + Abs_poly_mapping k" by (rule poly_mapping_eqI, simp add: * lookup_add Abs_poly_mapping_inverse[OF **]) qed qed subsubsection \@{typ "('a, 'b) poly_mapping"} belongs to class @{class comm_powerprod}\ instance poly_mapping :: (type, cancel_comm_monoid_add) comm_powerprod by standard subsubsection \@{typ "('a, 'b) poly_mapping"} belongs to class @{class ninv_comm_monoid_add}\ instance poly_mapping :: (type, ninv_comm_monoid_add) ninv_comm_monoid_add proof (standard, transfer) fix s t::"'a \ 'b" assume "(\k. s k + t k) = (\_. 0)" hence "s + t = 0" by (simp only: plus_fun_def zero_fun_def) hence "s = 0" by (rule plus_eq_zero) thus "s = (\_. 0)" by (simp only: zero_fun_def) qed subsubsection \@{typ "('a, 'b) poly_mapping"} belongs to class @{class lcs_powerprod}\ instantiation poly_mapping :: (type, add_linorder) lcs_powerprod begin lift_definition lcs_poly_mapping::"('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b)" is "\s t. \x. max (s x) (t x)" proof - fix fun1 fun2::"'a \ 'b" assume "finite {t. fun1 t \ 0}" and "finite {t. fun2 t \ 0}" from finite_neq_0'[OF this, of max] show "finite {t. max (fun1 t) (fun2 t) \ 0}" by (auto simp: max_def) qed lemma adds_poly_mappingI: assumes "lookup s \ lookup (t::'a \\<^sub>0 'b)" shows "s adds t" unfolding poly_mapping_adds_iff using assms by (rule adds_funI) lemma lookup_lcs_fun: "lookup (lcs s t) = lcs (lookup s) (lookup (t:: 'a \\<^sub>0 'b))" by (simp only: lcs_poly_mapping.rep_eq lcs_fun_def) instance by (standard, simp_all only: poly_mapping_adds_iff lookup_lcs_fun, rule adds_lcs, elim lcs_adds, assumption, rule poly_mapping_eqI, simp only: lookup_lcs_fun lcs_comm) end lemma adds_poly_mapping: "s adds t \ lookup s \ lookup t" for s t::"'a \\<^sub>0 'b::add_linorder_min" by (simp only: poly_mapping_adds_iff adds_fun) lemma lookup_gcs_fun: "lookup (gcs s (t::'a \\<^sub>0 ('b::add_linorder))) = gcs (lookup s) (lookup t)" proof fix x show "lookup (gcs s t) x = gcs (lookup s) (lookup t) x" by (simp add: gcs_def lookup_minus lookup_add lookup_lcs_fun) qed subsubsection \@{typ "('a, 'b) poly_mapping"} belongs to class @{class ulcs_powerprod}\ instance poly_mapping :: (type, add_linorder_min) ulcs_powerprod .. subsubsection \Power-products in a given set of indeterminates.\ lemma adds_except: "s adds t = (except s V adds except t V \ except s (- V) adds except t (- V))" for s t :: "'a \\<^sub>0 'b::add_linorder" by (simp add: poly_mapping_adds_iff adds_except_fun[of "lookup s", where V=V] except.rep_eq) lemma adds_except_singleton: "s adds t \ (except s {v} adds except t {v} \ lookup s v adds lookup t v)" for s t :: "'a \\<^sub>0 'b::add_linorder" by (simp add: poly_mapping_adds_iff adds_except_fun_singleton[of "lookup s", where v=v] except.rep_eq) subsubsection \Dickson's lemma for power-products in finitely many indeterminates\ context countable begin definition elem_index :: "'a \ nat" where "elem_index = (SOME f. inj f)" lemma inj_elem_index: "inj elem_index" unfolding elem_index_def using ex_inj by (rule someI_ex) lemma elem_index_inj: assumes "elem_index x = elem_index y" shows "x = y" using inj_elem_index assms by (rule injD) lemma finite_nat_seg: "finite {x. elem_index x < n}" proof (rule finite_imageD) have "elem_index ` {x. elem_index x < n} \ {0..\<^sub>0 'b::add_wellorder. keys x \ V}" proof (rule almost_full_onI) fix seq::"nat \ 'a \\<^sub>0 'b" assume a: "\i. seq i \ {x::'a \\<^sub>0 'b. keys x \ V}" define seq' where "seq' = (\i. lookup (seq i))" from assms have "almost_full_on (adds) {x::'a \ 'b. supp_fun x \ V}" by (rule Dickson_fun) moreover from a have "\i. seq' i \ {x::'a \ 'b. supp_fun x \ V}" by (auto simp: seq'_def keys_eq_supp) ultimately obtain i j where "i < j" and "seq' i adds seq' j" by (rule almost_full_onD) from this(2) have "seq i adds seq j" by (simp add: seq'_def poly_mapping_adds_iff) with \i < j\ show "good (adds) seq" by (rule goodI) qed definition varnum :: "'x set \ ('x::countable \\<^sub>0 'b::zero) \ nat" where "varnum X t = (if keys t - X = {} then 0 else Suc (Max (elem_index ` (keys t - X))))" lemma elem_index_less_varnum: assumes "x \ keys t" obtains "x \ X" | "elem_index x < varnum X t" proof (cases "x \ X") case True thus ?thesis .. next case False with assms have 1: "x \ keys t - X" by simp hence "keys t - X \ {}" by blast hence eq: "varnum X t = Suc (Max (elem_index ` (keys t - X)))" by (simp add: varnum_def) hence "elem_index x < varnum X t" using 1 by (simp add: less_Suc_eq_le) thus ?thesis .. qed lemma varnum_plus: "varnum X (s + t) = max (varnum X s) (varnum X (t::'x::countable \\<^sub>0 'b::ninv_comm_monoid_add))" proof (simp add: varnum_def keys_plus_ninv_comm_monoid_add image_Un Un_Diff del: Diff_eq_empty_iff, intro impI) assume 1: "keys s - X \ {}" and 2: "keys t - X \ {}" have "finite (elem_index ` (keys s - X))" by simp moreover from 1 have "elem_index ` (keys s - X) \ {}" by simp moreover have "finite (elem_index ` (keys t - X))" by simp moreover from 2 have "elem_index ` (keys t - X) \ {}" by simp ultimately show "Max (elem_index ` (keys s - X) \ elem_index ` (keys t - X)) = max (Max (elem_index ` (keys s - X))) (Max (elem_index ` (keys t - X)))" by (rule Max_Un) qed lemma dickson_grading_varnum: assumes "finite X" shows "dickson_grading ((varnum X)::('x::countable \\<^sub>0 'b::add_wellorder) \ nat)" using varnum_plus proof (rule dickson_gradingI) fix m::nat let ?V = "X \ {x. elem_index x < m}" have "{t::'x \\<^sub>0 'b. varnum X t \ m} \ {t. keys t \ ?V}" proof (rule, simp, intro subsetI, simp) fix t::"'x \\<^sub>0 'b" and x::'x assume "varnum X t \ m" assume "x \ keys t" thus "x \ X \ elem_index x < m" proof (rule elem_index_less_varnum) assume "x \ X" thus ?thesis .. next assume "elem_index x < varnum X t" hence "elem_index x < m" using \varnum X t \ m\ by (rule less_le_trans) thus ?thesis .. qed qed thus "almost_full_on (adds) {t::'x \\<^sub>0 'b. varnum X t \ m}" proof (rule almost_full_on_subset) from assms finite_nat_seg have "finite ?V" by (rule finite_UnI) thus "almost_full_on (adds) {t::'x \\<^sub>0 'b. keys t \ ?V}" by (rule Dickson_poly_mapping) qed qed corollary dickson_grading_varnum_empty: "dickson_grading ((varnum {})::(_ \\<^sub>0 _::add_wellorder) \ nat)" using finite.emptyI by (rule dickson_grading_varnum) lemma varnum_le_iff: "varnum X t \ n \ keys t \ X \ {x. elem_index x < n}" by (auto simp: varnum_def Suc_le_eq) lemma varnum_zero [simp]: "varnum X 0 = 0" by (simp add: varnum_def) lemma varnum_empty_eq_zero_iff: "varnum {} t = 0 \ t = 0" proof assume "varnum {} t = 0" hence "keys t = {}" by (simp add: varnum_def split: if_splits) thus "t = 0" by (rule poly_mapping_eq_zeroI) qed simp instance poly_mapping :: (countable, add_wellorder) graded_dickson_powerprod by standard (rule, fact dickson_grading_varnum_empty) instance poly_mapping :: (finite, add_wellorder) dickson_powerprod proof have "finite (UNIV::'a set)" by simp hence "almost_full_on (adds) {x::'a \\<^sub>0 'b. keys x \ UNIV}" by (rule Dickson_poly_mapping) thus "almost_full_on (adds) (UNIV::('a \\<^sub>0 'b) set)" by simp qed subsubsection \Lexicographic Term Order\ definition lex_pm :: "('a \\<^sub>0 'b) \ ('a::linorder \\<^sub>0 'b::{zero,linorder}) \ bool" where "lex_pm = (\)" definition lex_pm_strict :: "('a \\<^sub>0 'b) \ ('a::linorder \\<^sub>0 'b::{zero,linorder}) \ bool" where "lex_pm_strict = (<)" lemma lex_pm_alt: "lex_pm s t = (s = t \ (\x. lookup s x < lookup t x \ (\y lex_pm t s \ s = t" by (simp add: lex_pm_def) lemma lex_pm_trans: "lex_pm s t \ lex_pm t u \ lex_pm s u" by (simp add: lex_pm_def) lemma lex_pm_lin: "lex_pm s t \ lex_pm t s" by (simp add: lex_pm_def linear) corollary lex_pm_strict_alt [code]: "lex_pm_strict s t = (\ lex_pm t s)" by (auto simp: lex_pm_strict_def lex_pm_def) lemma lex_pm_zero_min: "lex_pm 0 s" for s::"_ \\<^sub>0 _::add_linorder_min" proof (rule ccontr) assume "\ lex_pm 0 s" hence "lex_pm_strict s 0" by (simp add: lex_pm_strict_alt) thus False by (simp add: lex_pm_strict_def less_poly_mapping.rep_eq less_fun_def) qed lemma lex_pm_plus_monotone: "lex_pm s t \ lex_pm (s + u) (t + u)" for s t::"_ \\<^sub>0 _::{ordered_comm_monoid_add, ordered_ab_semigroup_add_imp_le}" by (simp add: lex_pm_def add_right_mono) subsubsection \Degree\ lift_definition deg_pm::"('a \\<^sub>0 'b::comm_monoid_add) \ 'b" is deg_fun . lemma deg_pm_zero[simp]: "deg_pm 0 = 0" by (simp add: deg_pm.rep_eq lookup_zero_fun) lemma deg_pm_eq_0_iff[simp]: "deg_pm s = 0 \ s = 0" for s::"'a \\<^sub>0 'b::add_linorder_min" by (simp only: deg_pm.rep_eq poly_mapping_eq_iff lookup_zero_fun, rule deg_fun_eq_0_iff, simp add: keys_eq_supp[symmetric]) lemma deg_pm_superset: assumes "keys s \ A" and "finite A" shows "deg_pm s = (\x\A. lookup s x)" using assms by (simp only: deg_pm.rep_eq keys_eq_supp, elim deg_fun_superset) lemma deg_pm_plus: "deg_pm (s + t) = deg_pm s + deg_pm (t::'a \\<^sub>0 'b::comm_monoid_add)" by (simp only: deg_pm.rep_eq lookup_plus_fun, rule deg_fun_plus, simp_all add: keys_eq_supp[symmetric]) lemma deg_pm_single: "deg_pm (Poly_Mapping.single x k) = k" proof - have "keys (Poly_Mapping.single x k) \ {x}" by simp moreover have "finite {x}" by simp ultimately have "deg_pm (Poly_Mapping.single x k) = (\y\{x}. lookup (Poly_Mapping.single x k) y)" by (rule deg_pm_superset) also have "... = k" by simp finally show ?thesis . qed subsubsection \General Degree-Orders\ context linorder begin lift_definition dord_pm::"(('a \\<^sub>0 'b::ordered_comm_monoid_add) \ ('a \\<^sub>0 'b) \ bool) \ ('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b) \ bool" is dord_fun by (metis local.dord_fun_def) lemma dord_pm_alt: "dord_pm ord = (\x y. deg_pm x < deg_pm y \ (deg_pm x = deg_pm y \ ord x y))" by (intro ext) (transfer, simp add: dord_fun_def Let_def) lemma dord_pm_degD: assumes "dord_pm ord s t" shows "deg_pm s \ deg_pm t" using assms by (simp only: dord_pm.rep_eq deg_pm.rep_eq, elim dord_fun_degD) lemma dord_pm_refl: assumes "ord s s" shows "dord_pm ord s s" using assms by (simp only: dord_pm.rep_eq, intro dord_fun_refl, simp add: lookup_inverse) lemma dord_pm_antisym: assumes "ord s t \ ord t s \ s = t" and "dord_pm ord s t" and "dord_pm ord t s" shows "s = t" using assms proof (simp only: dord_pm.rep_eq poly_mapping_eq_iff) assume 1: "(ord s t \ ord t s \ lookup s = lookup t)" assume 2: "dord_fun (map_fun Abs_poly_mapping id \ ord \ Abs_poly_mapping) (lookup s) (lookup t)" assume 3: "dord_fun (map_fun Abs_poly_mapping id \ ord \ Abs_poly_mapping) (lookup t) (lookup s)" from _ 2 3 show "lookup s = lookup t" by (rule dord_fun_antisym, simp add: lookup_inverse 1) qed lemma dord_pm_trans: assumes "ord s t \ ord t u \ ord s u" and "dord_pm ord s t" and "dord_pm ord t u" shows "dord_pm ord s u" using assms proof (simp only: dord_pm.rep_eq poly_mapping_eq_iff) assume 1: "(ord s t \ ord t u \ ord s u)" assume 2: "dord_fun (map_fun Abs_poly_mapping id \ ord \ Abs_poly_mapping) (lookup s) (lookup t)" assume 3: "dord_fun (map_fun Abs_poly_mapping id \ ord \ Abs_poly_mapping) (lookup t) (lookup u)" from _ 2 3 show "dord_fun (map_fun Abs_poly_mapping id \ ord \ Abs_poly_mapping) (lookup s) (lookup u)" by (rule dord_fun_trans, simp add: lookup_inverse 1) qed lemma dord_pm_lin: "dord_pm ord s t \ dord_pm ord t s" if "ord s t \ ord t s" for s t::"'a \\<^sub>0 'b::{ordered_comm_monoid_add, linorder}" using that by (simp only: dord_pm.rep_eq, intro dord_fun_lin, simp add: lookup_inverse) lemma dord_pm_zero_min: "dord_pm ord 0 s" if ord_refl: "\t. ord t t" for s t::"'a \\<^sub>0 'b::add_linorder_min" using that by (simp only: dord_pm.rep_eq lookup_zero_fun, intro dord_fun_zero_min, simp add: lookup_inverse, simp add: keys_eq_supp[symmetric]) lemma dord_pm_plus_monotone: fixes s t u ::"'a \\<^sub>0 'b::{ordered_comm_monoid_add, ordered_ab_semigroup_add_imp_le}" assumes "ord s t \ ord (s + u) (t + u)" and "dord_pm ord s t" shows "dord_pm ord (s + u) (t + u)" using assms by (simp only: dord_pm.rep_eq lookup_plus_fun, intro dord_fun_plus_monotone, simp add: lookup_inverse lookup_plus_fun[symmetric], simp add: keys_eq_supp[symmetric], simp add: keys_eq_supp[symmetric], simp add: keys_eq_supp[symmetric], simp add: lookup_inverse) end (* linorder *) subsubsection \Degree-Lexicographic Term Order\ definition dlex_pm::"('a::linorder \\<^sub>0 'b::{ordered_comm_monoid_add,linorder}) \ ('a \\<^sub>0 'b) \ bool" where "dlex_pm \ dord_pm lex_pm" definition "dlex_pm_strict s t \ dlex_pm s t \ \ dlex_pm t s" lemma dlex_pm_refl: "dlex_pm s s" unfolding dlex_pm_def using lex_pm_refl by (rule dord_pm_refl) lemma dlex_pm_antisym: "dlex_pm s t \ dlex_pm t s \ s = t" unfolding dlex_pm_def using lex_pm_antisym by (rule dord_pm_antisym) lemma dlex_pm_trans: "dlex_pm s t \ dlex_pm t u \ dlex_pm s u" unfolding dlex_pm_def using lex_pm_trans by (rule dord_pm_trans) lemma dlex_pm_lin: "dlex_pm s t \ dlex_pm t s" unfolding dlex_pm_def using lex_pm_lin by (rule dord_pm_lin) corollary dlex_pm_strict_alt [code]: "dlex_pm_strict s t = (\ dlex_pm t s)" unfolding dlex_pm_strict_def using dlex_pm_lin by auto lemma dlex_pm_zero_min: "dlex_pm 0 s" for s t::"(_ \\<^sub>0 _::add_linorder_min)" unfolding dlex_pm_def using lex_pm_refl by (rule dord_pm_zero_min) lemma dlex_pm_plus_monotone: "dlex_pm s t \ dlex_pm (s + u) (t + u)" for s t::"_ \\<^sub>0 _::{ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add}" unfolding dlex_pm_def using lex_pm_plus_monotone by (rule dord_pm_plus_monotone) subsubsection \Degree-Reverse-Lexicographic Term Order\ definition drlex_pm::"('a::linorder \\<^sub>0 'b::{ordered_comm_monoid_add,linorder}) \ ('a \\<^sub>0 'b) \ bool" where "drlex_pm \ dord_pm (\s t. lex_pm t s)" definition "drlex_pm_strict s t \ drlex_pm s t \ \ drlex_pm t s" lemma drlex_pm_refl: "drlex_pm s s" unfolding drlex_pm_def using lex_pm_refl by (rule dord_pm_refl) lemma drlex_pm_antisym: "drlex_pm s t \ drlex_pm t s \ s = t" unfolding drlex_pm_def using lex_pm_antisym by (rule dord_pm_antisym) lemma drlex_pm_trans: "drlex_pm s t \ drlex_pm t u \ drlex_pm s u" unfolding drlex_pm_def using lex_pm_trans by (rule dord_pm_trans) lemma drlex_pm_lin: "drlex_pm s t \ drlex_pm t s" unfolding drlex_pm_def using lex_pm_lin by (rule dord_pm_lin) corollary drlex_pm_strict_alt [code]: "drlex_pm_strict s t = (\ drlex_pm t s)" unfolding drlex_pm_strict_def using drlex_pm_lin by auto lemma drlex_pm_zero_min: "drlex_pm 0 s" for s t::"(_ \\<^sub>0 _::add_linorder_min)" unfolding drlex_pm_def using lex_pm_refl by (rule dord_pm_zero_min) lemma drlex_pm_plus_monotone: "drlex_pm s t \ drlex_pm (s + u) (t + u)" for s t::"_ \\<^sub>0 _::{ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add}" unfolding drlex_pm_def using lex_pm_plus_monotone by (rule dord_pm_plus_monotone) end (* theory *) diff --git a/thys/Well_Quasi_Orders/Almost_Full.thy b/thys/Well_Quasi_Orders/Almost_Full.thy --- a/thys/Well_Quasi_Orders/Almost_Full.thy +++ b/thys/Well_Quasi_Orders/Almost_Full.thy @@ -1,551 +1,551 @@ (* Title: Well-Quasi-Orders Author: Christian Sternagel Maintainer: Christian Sternagel License: LGPL *) section \The Almost-Full Property\ theory Almost_Full imports "HOL-Library.Sublist" "HOL-Library.Ramsey" "Regular-Sets.Regexp_Method" "Abstract-Rewriting.Seq" Least_Enum Infinite_Sequences Open_Induction.Restricted_Predicates begin (*TODO: move*) lemma le_Suc_eq': "x \ Suc y \ x = 0 \ (\x'. x = Suc x' \ x' \ y)" by (cases x) auto lemma ex_leq_Suc: "(\i\Suc j. P i) \ P 0 \ (\i\j. P (Suc i))" by (auto simp: le_Suc_eq') lemma ex_less_Suc: "(\i P 0 \ (\iBasic Definitions and Facts\ text \ An infinite sequence is \emph{good} whenever there are indices @{term "i < j"} such that @{term "P (f i) (f j)"}. \ definition good :: "('a \ 'a \ bool) \ (nat \ 'a) \ bool" where "good P f \ (\i j. i < j \ P (f i) (f j))" text \A sequence that is not good is called \emph{bad}.\ abbreviation "bad P f \ \ good P f" lemma goodI: "\i < j; P (f i) (f j)\ \ good P f" by (auto simp: good_def) lemma goodE [elim]: "good P f \ (\i j. \i < j; P (f i) (f j)\ \ Q) \ Q" by (auto simp: good_def) lemma badE [elim]: "bad P f \ ((\i j. i < j \ \ P (f i) (f j)) \ Q) \ Q" by (auto simp: good_def) definition almost_full_on :: "('a \ 'a \ bool) \ 'a set \ bool" where "almost_full_on P A \ (\f \ SEQ A. good P f)" lemma almost_full_onI [Pure.intro]: "(\f. \i. f i \ A \ good P f) \ almost_full_on P A" unfolding almost_full_on_def by blast lemma almost_full_onD: fixes f :: "nat \ 'a" and A :: "'a set" assumes "almost_full_on P A" and "\i. f i \ A" obtains i j where "i < j" and "P (f i) (f j)" using assms unfolding almost_full_on_def by blast subsection \An equivalent inductive definition\ inductive af for A where now: "(\x y. x \ A \ y \ A \ P x y) \ af A P" | later: "(\x. x \ A \ af A (\y z. P y z \ P x y)) \ af A P" lemma af_imp_almost_full_on: assumes "af A P" shows "almost_full_on P A" proof fix f :: "nat \ 'a" assume "\i. f i \ A" with assms obtain i and j where "i < j" and "P (f i) (f j)" proof (induct arbitrary: f thesis) case (later P) define g where [simp]: "g i = f (Suc i)" for i have "f 0 \ A" and "\i. g i \ A" using later by auto then obtain i and j where "i < j" and "P (g i) (g j) \ P (f 0) (g i)" using later by blast then consider "P (g i) (g j)" | "P (f 0) (g i)" by blast then show ?case using \i < j\ by (cases) (auto intro: later) qed blast then show "good P f" by (auto simp: good_def) qed lemma af_mono: assumes "af A P" and "\x y. x \ A \ y \ A \ P x y \ Q x y" shows "af A Q" using assms proof (induct arbitrary: Q) case (now P) then have "\x y. x \ A \ y \ A \ Q x y" by blast then show ?case by (rule af.now) next case (later P) show ?case proof (intro af.later [of A Q]) fix x assume "x \ A" then show "af A (\y z. Q y z \ Q x y)" using later(3) by (intro later(2) [of x]) auto qed qed lemma accessible_on_imp_af: assumes "accessible_on P A x" shows "af A (\u v. \ P v u \ \ P u x)" using assms proof (induct) case (1 x) then have "af A (\u v. (\ P v u \ \ P u x) \ \ P u y \ \ P y x)" if "y \ A" for y using that by (cases "P y x") (auto intro: af.now af_mono) then show ?case by (rule af.later) qed lemma wfp_on_imp_af: assumes "wfp_on P A" shows "af A (\x y. \ P y x)" using assms by (auto simp: wfp_on_accessible_on_iff intro: accessible_on_imp_af af.later) lemma af_leq: "af UNIV ((\) :: nat \ nat \ bool)" using wf_less [folded wfP_def wfp_on_UNIV, THEN wfp_on_imp_af] by (simp add: not_less) definition "NOTAF A P = (SOME x. x \ A \ \ af A (\y z. P y z \ P x y))" lemma not_af: "\ af A P \ (\x y. x \ A \ y \ A \ \ P x y) \ (\x\A. \ af A (\y z. P y z \ P x y))" unfolding af.simps [of A P] by blast fun F where "F A P 0 = NOTAF A P" | "F A P (Suc i) = (let x = NOTAF A P in F A (\y z. P y z \ P x y) i)" lemma almost_full_on_imp_af: assumes af: "almost_full_on P A" shows "af A P" proof (rule ccontr) assume "\ af A P" then have *: "F A P n \ A \ \ af A (\y z. P y z \ (\i\n. P (F A P i) y) \ (\j\n. \i. i < j \ P (F A P i) (F A P j)))" for n proof (induct n arbitrary: P) case 0 from \\ af A P\ have "\x. x \ A \ \ af A (\y z. P y z \ P x y)" by (auto intro: af.intros) then have "NOTAF A P \ A \ \ af A (\y z. P y z \ P (NOTAF A P) y)" unfolding NOTAF_def by (rule someI_ex) with 0 show ?case by simp next case (Suc n) from \\ af A P\ have "\x. x \ A \ \ af A (\y z. P y z \ P x y)" by (auto intro: af.intros) then have "NOTAF A P \ A \ \ af A (\y z. P y z \ P (NOTAF A P) y)" unfolding NOTAF_def by (rule someI_ex) from Suc(1) [OF this [THEN conjunct2]] show ?case by (fastforce simp: ex_leq_Suc ex_less_Suc elim!: back_subst [where P = "\x. \ af A x"]) qed then have "F A P \ SEQ A" by auto from af [unfolded almost_full_on_def, THEN bspec, OF this] and not_af [OF * [THEN conjunct2]] show False unfolding good_def by blast qed hide_const NOTAF F lemma almost_full_on_UNIV: "almost_full_on (\_ _. True) UNIV" by (auto simp: almost_full_on_def good_def) lemma almost_full_on_imp_reflp_on: assumes "almost_full_on P A" - shows "reflp_on P A" + shows "reflp_on A P" using assms by (auto simp: almost_full_on_def reflp_on_def) lemma almost_full_on_subset: "A \ B \ almost_full_on P B \ almost_full_on P A" by (auto simp: almost_full_on_def) lemma almost_full_on_mono: assumes "A \ B" and "\x y. Q x y \ P x y" and "almost_full_on Q B" shows "almost_full_on P A" using assms by (metis almost_full_on_def almost_full_on_subset good_def) text \ Every sequence over elements of an almost-full set has a homogeneous subsequence. \ lemma almost_full_on_imp_homogeneous_subseq: assumes "almost_full_on P A" and "\i::nat. f i \ A" shows "\\::nat \ nat. \i j. i < j \ \ i < \ j \ P (f (\ i)) (f (\ j))" proof - define X where "X = {{i, j} | i j::nat. i < j \ P (f i) (f j)}" define Y where "Y = - X" define h where "h = (\Z. if Z \ X then 0 else Suc 0)" have [iff]: "\x y. h {x, y} = 0 \ {x, y} \ X" by (auto simp: h_def) have [iff]: "\x y. h {x, y} = Suc 0 \ {x, y} \ Y" by (auto simp: h_def Y_def) have "\x\UNIV. \y\UNIV. x \ y \ h {x, y} < 2" by (simp add: h_def) from Ramsey2 [OF infinite_UNIV_nat this] obtain I c where "infinite I" and "c < 2" and *: "\x\I. \y\I. x \ y \ h {x, y} = c" by blast then interpret infinitely_many1 "\i. i \ I" by (unfold_locales) (simp add: infinite_nat_iff_unbounded) have "c = 0 \ c = 1" using \c < 2\ by arith then show ?thesis proof assume [simp]: "c = 0" have "\i j. i < j \ P (f (enum i)) (f (enum j))" proof (intro allI impI) fix i j :: nat assume "i < j" from * and enum_P and enum_less [OF \i < j\] have "{enum i, enum j} \ X" by auto with enum_less [OF \i < j\] show "P (f (enum i)) (f (enum j))" by (auto simp: X_def doubleton_eq_iff) qed then show ?thesis using enum_less by blast next assume [simp]: "c = 1" have "\i j. i < j \ \ P (f (enum i)) (f (enum j))" proof (intro allI impI) fix i j :: nat assume "i < j" from * and enum_P and enum_less [OF \i < j\] have "{enum i, enum j} \ Y" by auto with enum_less [OF \i < j\] show "\ P (f (enum i)) (f (enum j))" by (auto simp: Y_def X_def doubleton_eq_iff) qed then have "\ good P (f \ enum)" by auto moreover have "\i. f (enum i) \ A" using assms by auto ultimately show ?thesis using \almost_full_on P A\ by (simp add: almost_full_on_def) qed qed text \ Almost full relations do not admit infinite antichains. \ lemma almost_full_on_imp_no_antichain_on: assumes "almost_full_on P A" shows "\ antichain_on P f A" proof assume *: "antichain_on P f A" then have "\i. f i \ A" by simp with assms have "good P f" by (auto simp: almost_full_on_def) then obtain i j where "i < j" and "P (f i) (f j)" unfolding good_def by auto moreover with * have "incomparable P (f i) (f j)" by auto ultimately show False by blast qed text \ If the image of a function is almost-full then also its preimage is almost-full. \ lemma almost_full_on_map: assumes "almost_full_on Q B" and "h ` A \ B" shows "almost_full_on (\x y. Q (h x) (h y)) A" (is "almost_full_on ?P A") proof fix f assume "\i::nat. f i \ A" then have "\i. h (f i) \ B" using \h ` A \ B\ by auto with \almost_full_on Q B\ [unfolded almost_full_on_def, THEN bspec, of "h \ f"] show "good ?P f" unfolding good_def comp_def by blast qed text \ The homomorphic image of an almost-full set is almost-full. \ lemma almost_full_on_hom: fixes h :: "'a \ 'b" assumes hom: "\x y. \x \ A; y \ A; P x y\ \ Q (h x) (h y)" and af: "almost_full_on P A" shows "almost_full_on Q (h ` A)" proof fix f :: "nat \ 'b" assume "\i. f i \ h ` A" then have "\i. \x. x \ A \ f i = h x" by (auto simp: image_def) from choice [OF this] obtain g where *: "\i. g i \ A \ f i = h (g i)" by blast show "good Q f" proof (rule ccontr) assume bad: "bad Q f" { fix i j :: nat assume "i < j" from bad have "\ Q (f i) (f j)" using \i < j\ by (auto simp: good_def) with hom have "\ P (g i) (g j)" using * by auto } then have "bad P g" by (auto simp: good_def) with af and * show False by (auto simp: good_def almost_full_on_def) qed qed text \ The monomorphic preimage of an almost-full set is almost-full. \ lemma almost_full_on_mon: assumes mon: "\x y. \x \ A; y \ A\ \ P x y = Q (h x) (h y)" "bij_betw h A B" and af: "almost_full_on Q B" shows "almost_full_on P A" proof fix f :: "nat \ 'a" assume *: "\i. f i \ A" then have **: "\i. (h \ f) i \ B" using mon by (auto simp: bij_betw_def) show "good P f" proof (rule ccontr) assume bad: "bad P f" { fix i j :: nat assume "i < j" from bad have "\ P (f i) (f j)" using \i < j\ by (auto simp: good_def) with mon have "\ Q (h (f i)) (h (f j))" using * by (auto simp: bij_betw_def inj_on_def) } then have "bad Q (h \ f)" by (auto simp: good_def) with af and ** show False by (auto simp: good_def almost_full_on_def) qed qed text \ Every total and well-founded relation is almost-full. \ lemma total_on_and_wfp_on_imp_almost_full_on: - assumes "total_on P A" and "wfp_on P A" + assumes "totalp_on A P" and "wfp_on P A" shows "almost_full_on P\<^sup>=\<^sup>= A" proof (rule ccontr) assume "\ almost_full_on P\<^sup>=\<^sup>= A" then obtain f :: "nat \ 'a" where *: "\i. f i \ A" and "\i j. i < j \ \ P\<^sup>=\<^sup>= (f i) (f j)" unfolding almost_full_on_def by (auto dest: badE) - with \total_on P A\ have "\i j. i < j \ P (f j) (f i)" - unfolding total_on_def by blast + with \totalp_on A P\ have "\i j. i < j \ P (f j) (f i)" + unfolding totalp_on_def by blast then have "\i. P (f (Suc i)) (f i)" by auto with \wfp_on P A\ and * show False unfolding wfp_on_def by blast qed lemma Nil_imp_good_list_emb [simp]: assumes "f i = []" shows "good (list_emb P) f" proof (rule ccontr) assume "bad (list_emb P) f" moreover have "(list_emb P) (f i) (f (Suc i))" unfolding assms by auto ultimately show False unfolding good_def by auto qed lemma ne_lists: assumes "xs \ []" and "xs \ lists A" shows "hd xs \ A" and "tl xs \ lists A" using assms by (case_tac [!] xs) simp_all lemma list_emb_eq_length_induct [consumes 2, case_names Nil Cons]: assumes "length xs = length ys" and "list_emb P xs ys" and "Q [] []" and "\x y xs ys. \P x y; list_emb P xs ys; Q xs ys\ \ Q (x#xs) (y#ys)" shows "Q xs ys" using assms(2, 1, 3-) by (induct) (auto dest: list_emb_length) lemma list_emb_eq_length_P: assumes "length xs = length ys" and "list_emb P xs ys" shows "\iSpecial Case: Finite Sets\ text \ Every reflexive relation on a finite set is almost-full. \ lemma finite_almost_full_on: assumes finite: "finite A" - and refl: "reflp_on P A" + and refl: "reflp_on A P" shows "almost_full_on P A" proof fix f :: "nat \ 'a" assume *: "\i. f i \ A" let ?I = "UNIV::nat set" have "f ` ?I \ A" using * by auto with finite and finite_subset have 1: "finite (f ` ?I)" by blast have "infinite ?I" by auto from pigeonhole_infinite [OF this 1] obtain k where "infinite {j. f j = f k}" by auto then obtain l where "k < l" and "f l = f k" unfolding infinite_nat_iff_unbounded by auto then have "P (f k) (f l)" using refl and * by (auto simp: reflp_on_def) with \k < l\ show "good P f" by (auto simp: good_def) qed lemma eq_almost_full_on_finite_set: assumes "finite A" shows "almost_full_on (=) A" using finite_almost_full_on [OF assms, of "(=)"] by (auto simp: reflp_on_def) subsection \Further Results\ lemma af_trans_extension_imp_wf: assumes subrel: "\x y. P x y \ Q x y" and af: "almost_full_on P A" and trans: "transp_on Q A" shows "wfp_on (strict Q) A" proof (unfold wfp_on_def, rule notI) assume "\f. \i. f i \ A \ strict Q (f (Suc i)) (f i)" then obtain f where *: "\i. f i \ A \ ((strict Q)\\) (f i) (f (Suc i))" by blast from chain_transp_on_less [OF this] and transp_on_strict [THEN transp_on_converse, OF trans] have "\i j. i < j \ \ Q (f i) (f j)" by blast with subrel have "\i j. i < j \ \ P (f i) (f j)" by blast with af show False using * by (auto simp: almost_full_on_def good_def) qed lemma af_trans_imp_wf: assumes "almost_full_on P A" and "transp_on P A" shows "wfp_on (strict P) A" using assms by (intro af_trans_extension_imp_wf) lemma wf_and_no_antichain_imp_qo_extension_wf: assumes wf: "wfp_on (strict P) A" and anti: "\ (\f. antichain_on P f A)" and subrel: "\x\A. \y\A. P x y \ Q x y" and qo: "qo_on Q A" shows "wfp_on (strict Q) A" proof (rule ccontr) have "transp_on (strict Q) A" using qo unfolding qo_on_def transp_on_def by blast then have *: "transp_on ((strict Q)\\) A" by (rule transp_on_converse) assume "\ wfp_on (strict Q) A" then obtain f :: "nat \ 'a" where A: "\i. f i \ A" and "\i. strict Q (f (Suc i)) (f i)" unfolding wfp_on_def by blast+ then have "\i. f i \ A \ ((strict Q)\\) (f i) (f (Suc i))" by auto from chain_transp_on_less [OF this *] have *: "\i j. i < j \ \ P (f i) (f j)" using subrel and A by blast show False proof (cases) assume "\k. \i>k. \j>i. P (f j) (f i)" then obtain k where "\i>k. \j>i. P (f j) (f i)" by auto from subchain [of k _ f, OF this] obtain g where "\i j. i < j \ g i < g j" and "\i. P (f (g (Suc i))) (f (g i))" by auto with * have "\i. strict P (f (g (Suc i))) (f (g i))" by blast with wf [unfolded wfp_on_def not_ex, THEN spec, of "\i. f (g i)"] and A show False by fast next assume "\ (\k. \i>k. \j>i. P (f j) (f i))" then have "\k. \i>k. \j>i. \ P (f j) (f i)" by auto from choice [OF this] obtain h where "\k. h k > k" and **: "\k. (\j>h k. \ P (f j) (f (h k)))" by auto define \ where [simp]: "\ = (\i. (h ^^ Suc i) 0)" have "\i. \ i < \ (Suc i)" using \\k. h k > k\ by (induct_tac i) auto then have mono: "\i j. i < j \ \ i < \ j" by (metis lift_Suc_mono_less) then have "\i j. i < j \ \ P (f (\ j)) (f (\ i))" using ** by auto with mono [THEN *] have "\i j. i < j \ incomparable P (f (\ j)) (f (\ i))" by blast moreover have "\i j. i < j \ \ incomparable P (f (\ i)) (f (\ j))" using anti [unfolded not_ex, THEN spec, of "\i. f (\ i)"] and A by blast ultimately show False by blast qed qed lemma every_qo_extension_wf_imp_af: assumes ext: "\Q. (\x\A. \y\A. P x y \ Q x y) \ qo_on Q A \ wfp_on (strict Q) A" and "qo_on P A" shows "almost_full_on P A" proof from \qo_on P A\ - have refl: "reflp_on P A" + have refl: "reflp_on A P" and trans: "transp_on P A" by (auto intro: qo_on_imp_reflp_on qo_on_imp_transp_on) fix f :: "nat \ 'a" assume "\i. f i \ A" then have A: "\i. f i \ A" .. show "good P f" proof (rule ccontr) assume "\ ?thesis" then have bad: "\i j. i < j \ \ P (f i) (f j)" by (auto simp: good_def) then have *: "\i j. P (f i) (f j) \ i \ j" by (metis not_le_imp_less) define D where [simp]: "D = (\x y. \i. x = f (Suc i) \ y = f i)" define P' where "P' = restrict_to P A" define Q where [simp]: "Q = (sup P' D)\<^sup>*\<^sup>*" have **: "\i j. (D OO P'\<^sup>*\<^sup>*)\<^sup>+\<^sup>+ (f i) (f j) \ i > j" proof - fix i j assume "(D OO P'\<^sup>*\<^sup>*)\<^sup>+\<^sup>+ (f i) (f j)" then show "i > j" apply (induct "f i" "f j" arbitrary: j) apply (insert A, auto dest!: * simp: P'_def reflp_on_restrict_to_rtranclp [OF refl trans]) apply (metis "*" dual_order.strict_trans1 less_Suc_eq_le refl reflp_on_def) by (metis le_imp_less_Suc less_trans) qed have "\x\A. \y\A. P x y \ Q x y" by (auto simp: P'_def) moreover have "qo_on Q A" by (auto simp: qo_on_def reflp_on_def transp_on_def) ultimately have "wfp_on (strict Q) A" using ext [THEN spec, of Q] by blast moreover have "\i. f i \ A \ strict Q (f (Suc i)) (f i)" proof fix i have "\ Q (f i) (f (Suc i))" proof assume "Q (f i) (f (Suc i))" then have "(sup P' D)\<^sup>*\<^sup>* (f i) (f (Suc i))" by auto moreover have "(sup P' D)\<^sup>*\<^sup>* = sup (P'\<^sup>*\<^sup>*) (P'\<^sup>*\<^sup>* OO (D OO P'\<^sup>*\<^sup>*)\<^sup>+\<^sup>+)" proof - have "\A B. (A \ B)\<^sup>* = A\<^sup>* \ A\<^sup>* O (B O A\<^sup>*)\<^sup>+" by regexp from this [to_pred] show ?thesis by blast qed ultimately have "sup (P'\<^sup>*\<^sup>*) (P'\<^sup>*\<^sup>* OO (D OO P'\<^sup>*\<^sup>*)\<^sup>+\<^sup>+) (f i) (f (Suc i))" by simp then have "(P'\<^sup>*\<^sup>* OO (D OO P'\<^sup>*\<^sup>*)\<^sup>+\<^sup>+) (f i) (f (Suc i))" by auto then have "Suc i < i" using ** apply auto by (metis (lifting, mono_tags) less_le relcompp.relcompI tranclp_into_tranclp2) then show False by auto qed with A [of i] show "f i \ A \ strict Q (f (Suc i)) (f i)" by auto qed ultimately show False unfolding wfp_on_def by blast qed qed end diff --git a/thys/Well_Quasi_Orders/Well_Quasi_Orders.thy b/thys/Well_Quasi_Orders/Well_Quasi_Orders.thy --- a/thys/Well_Quasi_Orders/Well_Quasi_Orders.thy +++ b/thys/Well_Quasi_Orders/Well_Quasi_Orders.thy @@ -1,317 +1,317 @@ (* Title: Well-Quasi-Orders Author: Christian Sternagel Maintainer: Christian Sternagel License: LGPL *) section \Well-Quasi-Orders\ theory Well_Quasi_Orders imports Almost_Full_Relations begin subsection \Basic Definitions\ definition wqo_on :: "('a \ 'a \ bool) \ 'a set \ bool" where "wqo_on P A \ transp_on P A \ almost_full_on P A" lemma wqo_on_UNIV: "wqo_on (\_ _. True) UNIV" using almost_full_on_UNIV by (auto simp: wqo_on_def transp_on_def) lemma wqo_onI [Pure.intro]: "\transp_on P A; almost_full_on P A\ \ wqo_on P A" unfolding wqo_on_def almost_full_on_def by blast lemma wqo_on_imp_reflp_on: - "wqo_on P A \ reflp_on P A" + "wqo_on P A \ reflp_on A P" using almost_full_on_imp_reflp_on by (auto simp: wqo_on_def) lemma wqo_on_imp_transp_on: "wqo_on P A \ transp_on P A" by (auto simp: wqo_on_def) lemma wqo_on_imp_almost_full_on: "wqo_on P A \ almost_full_on P A" by (auto simp: wqo_on_def) lemma wqo_on_imp_qo_on: "wqo_on P A \ qo_on P A" by (metis qo_on_def wqo_on_imp_reflp_on wqo_on_imp_transp_on) lemma wqo_on_imp_good: "wqo_on P A \ \i. f i \ A \ good P f" by (auto simp: wqo_on_def almost_full_on_def) lemma wqo_on_subset: "A \ B \ wqo_on P B \ wqo_on P A" using almost_full_on_subset [of A B P] and transp_on_subset [of A B P] unfolding wqo_on_def by blast subsection \Equivalent Definitions\ text \ Given a quasi-order @{term P}, the following statements are equivalent: \begin{enumerate} \item @{term P} is a almost-full. \item @{term P} does neither allow decreasing chains nor antichains. \item Every quasi-order extending @{term P} is well-founded. \end{enumerate} \ lemma wqo_af_conv: assumes "qo_on P A" shows "wqo_on P A \ almost_full_on P A" using assms by (metis qo_on_def wqo_on_def) lemma wqo_wf_and_no_antichain_conv: assumes "qo_on P A" shows "wqo_on P A \ wfp_on (strict P) A \ \ (\f. antichain_on P f A)" unfolding wqo_af_conv [OF assms] using af_trans_imp_wf [OF _ assms [THEN qo_on_imp_transp_on]] and almost_full_on_imp_no_antichain_on [of P A] and wf_and_no_antichain_imp_qo_extension_wf [of P A] and every_qo_extension_wf_imp_af [OF _ assms] by blast lemma wqo_extensions_wf_conv: assumes "qo_on P A" shows "wqo_on P A \ (\Q. (\x\A. \y\A. P x y \ Q x y) \ qo_on Q A \ wfp_on (strict Q) A)" unfolding wqo_af_conv [OF assms] using af_trans_imp_wf [OF _ assms [THEN qo_on_imp_transp_on]] and almost_full_on_imp_no_antichain_on [of P A] and wf_and_no_antichain_imp_qo_extension_wf [of P A] and every_qo_extension_wf_imp_af [OF _ assms] by blast lemma wqo_on_imp_wfp_on: "wqo_on P A \ wfp_on (strict P) A" by (metis (no_types) wqo_on_imp_qo_on wqo_wf_and_no_antichain_conv) text \ The homomorphic image of a wqo set is wqo. \ lemma wqo_on_hom: assumes "transp_on Q (h ` A)" and "\x\A. \y\A. P x y \ Q (h x) (h y)" and "wqo_on P A" shows "wqo_on Q (h ` A)" using assms and almost_full_on_hom [of A P Q h] unfolding wqo_on_def by blast text \ The monomorphic preimage of a wqo set is wqo. \ lemma wqo_on_mon: assumes *: "\x\A. \y\A. P x y \ Q (h x) (h y)" and bij: "bij_betw h A B" and wqo: "wqo_on Q B" shows "wqo_on P A" proof - have "transp_on P A" proof fix x y z assume [intro!]: "x \ A" "y \ A" "z \ A" and "P x y" and "P y z" with * have "Q (h x) (h y)" and "Q (h y) (h z)" by blast+ with wqo_on_imp_transp_on [OF wqo] have "Q (h x) (h z)" using bij by (auto simp: bij_betw_def transp_on_def) with * show "P x z" by blast qed with assms and almost_full_on_mon [of A P Q h] show ?thesis unfolding wqo_on_def by blast qed subsection \A Type Class for Well-Quasi-Orders\ text \ In a well-quasi-order (wqo) every infinite sequence is good. \ class wqo = preorder + assumes good: "good (\) f" lemma wqo_on_class [simp, intro]: "wqo_on (\) (UNIV :: ('a :: wqo) set)" using good by (auto simp: wqo_on_def transp_on_def almost_full_on_def dest: order_trans) lemma wqo_on_UNIV_class_wqo [intro!]: "wqo_on P UNIV \ class.wqo P (strict P)" by (unfold_locales) (auto simp: wqo_on_def almost_full_on_def, unfold transp_on_def, blast) text \ The following lemma converts between @{const wqo_on} (for the special case that the domain is the universe of a type) and the class predicate @{const class.wqo}. \ lemma wqo_on_UNIV_conv: "wqo_on P UNIV \ class.wqo P (strict P)" (is "?lhs = ?rhs") proof assume "?lhs" then show "?rhs" by auto next assume "?rhs" then show "?lhs" unfolding class.wqo_def class.preorder_def class.wqo_axioms_def by (auto simp: wqo_on_def almost_full_on_def transp_on_def) qed text \ The strict part of a wqo is well-founded. \ lemma (in wqo) "wfP (<)" proof - have "class.wqo (\) (<)" .. hence "wqo_on (\) UNIV" unfolding less_le_not_le [abs_def] wqo_on_UNIV_conv [symmetric] . from wqo_on_imp_wfp_on [OF this] show ?thesis unfolding less_le_not_le [abs_def] wfp_on_UNIV . qed lemma wqo_on_with_bot: assumes "wqo_on P A" shows "wqo_on (option_le P) A\<^sub>\" (is "wqo_on ?P ?A") proof - { from assms have trans [unfolded transp_on_def]: "transp_on P A" by (auto simp: wqo_on_def) have "transp_on ?P ?A" by (auto simp: transp_on_def elim!: with_bot_cases, insert trans) blast } moreover { from assms and almost_full_on_with_bot have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) } ultimately show ?thesis by (auto simp: wqo_on_def) qed lemma wqo_on_option_UNIV [intro]: "wqo_on P UNIV \ wqo_on (option_le P) UNIV" using wqo_on_with_bot [of P UNIV] by simp text \ When two sets are wqo, then their disjoint sum is wqo. \ lemma wqo_on_Plus: assumes "wqo_on P A" and "wqo_on Q B" shows "wqo_on (sum_le P Q) (A <+> B)" (is "wqo_on ?P ?A") proof - { from assms have trans [unfolded transp_on_def]: "transp_on P A" "transp_on Q B" by (auto simp: wqo_on_def) have "transp_on ?P ?A" unfolding transp_on_def by (auto, insert trans) (blast+) } moreover { from assms and almost_full_on_Plus have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) } ultimately show ?thesis by (auto simp: wqo_on_def) qed lemma wqo_on_sum_UNIV [intro]: "wqo_on P UNIV \ wqo_on Q UNIV \ wqo_on (sum_le P Q) UNIV" using wqo_on_Plus [of P UNIV Q UNIV] by simp subsection \Dickson's Lemma\ lemma wqo_on_Sigma: fixes A1 :: "'a set" and A2 :: "'b set" assumes "wqo_on P1 A1" and "wqo_on P2 A2" shows "wqo_on (prod_le P1 P2) (A1 \ A2)" (is "wqo_on ?P ?A") proof - { from assms have "transp_on P1 A1" and "transp_on P2 A2" by (auto simp: wqo_on_def) hence "transp_on ?P ?A" unfolding transp_on_def prod_le_def by blast } moreover { from assms and almost_full_on_Sigma [of P1 A1 P2 A2] have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) } ultimately show ?thesis by (auto simp: wqo_on_def) qed lemmas dickson = wqo_on_Sigma lemma wqo_on_prod_UNIV [intro]: "wqo_on P UNIV \ wqo_on Q UNIV \ wqo_on (prod_le P Q) UNIV" using wqo_on_Sigma [of P UNIV Q UNIV] by simp subsection \Higman's Lemma\ lemma transp_on_list_emb: assumes "transp_on P A" shows "transp_on (list_emb P) (lists A)" using assms and list_emb_trans [of _ _ _ P] unfolding transp_on_def by blast lemma wqo_on_lists: assumes "wqo_on P A" shows "wqo_on (list_emb P) (lists A)" using assms and almost_full_on_lists and transp_on_list_emb by (auto simp: wqo_on_def) lemmas higman = wqo_on_lists lemma wqo_on_list_UNIV [intro]: "wqo_on P UNIV \ wqo_on (list_emb P) UNIV" using wqo_on_lists [of P UNIV] by simp text \ Every reflexive and transitive relation on a finite set is a wqo. \ lemma finite_wqo_on: - assumes "finite A" and refl: "reflp_on P A" and "transp_on P A" + assumes "finite A" and refl: "reflp_on A P" and "transp_on P A" shows "wqo_on P A" using assms and finite_almost_full_on by (auto simp: wqo_on_def) lemma finite_eq_wqo_on: assumes "finite A" shows "wqo_on (=) A" using finite_wqo_on [OF assms, of "(=)"] by (auto simp: reflp_on_def transp_on_def) lemma wqo_on_lists_over_finite_sets: "wqo_on (list_emb (=)) (UNIV::('a::finite) list set)" using wqo_on_lists [OF finite_eq_wqo_on [OF finite [of "UNIV::('a::finite) set"]]] by simp lemma wqo_on_map: fixes P and Q and h defines "P' \ \x y. P x y \ Q (h x) (h y)" assumes "wqo_on P A" and "wqo_on Q B" and subset: "h ` A \ B" shows "wqo_on P' A" proof let ?Q = "\x y. Q (h x) (h y)" from \wqo_on P A\ have "transp_on P A" by (rule wqo_on_imp_transp_on) then show "transp_on P' A" using \wqo_on Q B\ and subset unfolding wqo_on_def transp_on_def P'_def by blast from \wqo_on P A\ have "almost_full_on P A" by (rule wqo_on_imp_almost_full_on) from \wqo_on Q B\ have "almost_full_on Q B" by (rule wqo_on_imp_almost_full_on) show "almost_full_on P' A" proof fix f assume *: "\i::nat. f i \ A" from almost_full_on_imp_homogeneous_subseq [OF \almost_full_on P A\ this] obtain g :: "nat \ nat" where g: "\i j. i < j \ g i < g j" and **: "\i. f (g i) \ A \ P (f (g i)) (f (g (Suc i)))" using * by auto from chain_transp_on_less [OF ** \transp_on P A\] have **: "\i j. i < j \ P (f (g i)) (f (g j))" . let ?g = "\i. h (f (g i))" from * and subset have B: "\i. ?g i \ B" by auto with \almost_full_on Q B\ [unfolded almost_full_on_def good_def, THEN bspec, of ?g] obtain i j :: nat where "i < j" and "Q (?g i) (?g j)" by blast with ** [OF \i < j\] have "P' (f (g i)) (f (g j))" by (auto simp: P'_def) with g [OF \i < j\] show "good P' f" by (auto simp: good_def) qed qed lemma wqo_on_UNIV_nat: "wqo_on (\) (UNIV :: nat set)" unfolding wqo_on_def transp_on_def using almost_full_on_UNIV_nat by simp end