# Theory General

section ‹General Utilities› theory General imports Polynomials.Utils begin text ‹A couple of general-purpose functions and lemmas, mainly related to lists.› subsection ‹Lists› lemma distinct_reorder: "distinct (xs @ (y # ys)) = distinct (y # (xs @ ys))" by auto lemma set_reorder: "set (xs @ (y # ys)) = set (y # (xs @ ys))" by simp lemma distinctI: assumes "⋀i j. i < j ⟹ i < length xs ⟹ j < length xs ⟹ xs ! i ≠ xs ! j" shows "distinct xs" using assms proof (induct xs) case Nil show ?case by simp next case (Cons x xs) show ?case proof (simp, intro conjI, rule) assume "x ∈ set xs" then obtain j where "j < length xs" and "x = xs ! j" by (metis in_set_conv_nth) hence "Suc j < length (x # xs)" by simp have "(x # xs) ! 0 ≠ (x # xs) ! (Suc j)" by (rule Cons(2), simp, simp, fact) thus False by (simp add: ‹x = xs ! j›) next show "distinct xs" proof (rule Cons(1)) fix i j assume "i < j" and "i < length xs" and "j < length xs" hence "Suc i < Suc j" and "Suc i < length (x # xs)" and "Suc j < length (x # xs)" by simp_all hence "(x # xs) ! (Suc i) ≠ (x # xs) ! (Suc j)" by (rule Cons(2)) thus "xs ! i ≠ xs ! j" by simp qed qed qed lemma filter_nth_pairE: assumes "i < j" and "i < length (filter P xs)" and "j < length (filter P xs)" obtains i' j' where "i' < j'" and "i' < length xs" and "j' < length xs" and "(filter P xs) ! i = xs ! i'" and "(filter P xs) ! j = xs ! j'" using assms proof (induct xs arbitrary: i j thesis) case Nil from Nil(3) show ?case by simp next case (Cons x xs) let ?ys = "filter P (x # xs)" show ?case proof (cases "P x") case True hence *: "?ys = x # (filter P xs)" by simp from ‹i < j› obtain j0 where j: "j = Suc j0" using lessE by blast have len_ys: "length ?ys = Suc (length (filter P xs))" and ys_j: "?ys ! j = (filter P xs) ! j0" by (simp only: * length_Cons, simp only: j * nth_Cons_Suc) from Cons(5) have "j0 < length (filter P xs)" unfolding len_ys j by auto show ?thesis proof (cases "i = 0") case True from ‹j0 < length (filter P xs)› obtain j' where "j' < length xs" and **: "(filter P xs) ! j0 = xs ! j'" by (metis (no_types, lifting) in_set_conv_nth mem_Collect_eq nth_mem set_filter) have "0 < Suc j'" by simp thus ?thesis by (rule Cons(2), simp, simp add: ‹j' < length xs›, simp only: True * nth_Cons_0, simp only: ys_j nth_Cons_Suc **) next case False then obtain i0 where i: "i = Suc i0" using lessE by blast have ys_i: "?ys ! i = (filter P xs) ! i0" by (simp only: i * nth_Cons_Suc) from Cons(3) have "i0 < j0" by (simp add: i j) from Cons(4) have "i0 < length (filter P xs)" unfolding len_ys i by auto from _ ‹i0 < j0› this ‹j0 < length (filter P xs)› obtain i' j' where "i' < j'" and "i' < length xs" and "j' < length xs" and i': "filter P xs ! i0 = xs ! i'" and j': "filter P xs ! j0 = xs ! j'" by (rule Cons(1)) from ‹i' < j'› have "Suc i' < Suc j'" by simp thus ?thesis by (rule Cons(2), simp add: ‹i' < length xs›, simp add: ‹j' < length xs›, simp only: ys_i nth_Cons_Suc i', simp only: ys_j nth_Cons_Suc j') qed next case False hence *: "?ys = filter P xs" by simp with Cons(4) Cons(5) have "i < length (filter P xs)" and "j < length (filter P xs)" by simp_all with _ ‹i < j› obtain i' j' where "i' < j'" and "i' < length xs" and "j' < length xs" and i': "filter P xs ! i = xs ! i'" and j': "filter P xs ! j = xs ! j'" by (rule Cons(1)) from ‹i' < j'› have "Suc i' < Suc j'" by simp thus ?thesis by (rule Cons(2), simp add: ‹i' < length xs›, simp add: ‹j' < length xs›, simp only: * nth_Cons_Suc i', simp only: * nth_Cons_Suc j') qed qed lemma distinct_filterI: assumes "⋀i j. i < j ⟹ i < length xs ⟹ j < length xs ⟹ P (xs ! i) ⟹ P (xs ! j) ⟹ xs ! i ≠ xs ! j" shows "distinct (filter P xs)" proof (rule distinctI) fix i j::nat assume "i < j" and "i < length (filter P xs)" and "j < length (filter P xs)" then obtain i' j' where "i' < j'" and "i' < length xs" and "j' < length xs" and i: "(filter P xs) ! i = xs ! i'" and j: "(filter P xs) ! j = xs ! j'" by (rule filter_nth_pairE) from ‹i' < j'› ‹i' < length xs› ‹j' < length xs› show "(filter P xs) ! i ≠ (filter P xs) ! j" unfolding i j proof (rule assms) from ‹i < length (filter P xs)› show "P (xs ! i')" unfolding i[symmetric] using nth_mem by force next from ‹j < length (filter P xs)› show "P (xs ! j')" unfolding j[symmetric] using nth_mem by force qed qed lemma set_zip_map: "set (zip (map f xs) (map g xs)) = (λx. (f x, g x)) ` (set xs)" proof - have "{(map f xs ! i, map g xs ! i) |i. i < length xs} = {(f (xs ! i), g (xs ! i)) |i. i < length xs}" proof (rule Collect_eqI, rule, elim exE conjE, intro exI conjI, simp add: map_nth, assumption, elim exE conjE, intro exI) fix x i assume "x = (f (xs ! i), g (xs ! i))" and "i < length xs" thus "x = (map f xs ! i, map g xs ! i) ∧ i < length xs" by (simp add: map_nth) qed also have "... = (λx. (f x, g x)) ` {xs ! i | i. i < length xs}" by blast finally show "set (zip (map f xs) (map g xs)) = (λx. (f x, g x)) ` (set xs)" by (simp add: set_zip set_conv_nth[symmetric]) qed lemma set_zip_map1: "set (zip (map f xs) xs) = (λx. (f x, x)) ` (set xs)" proof - have "set (zip (map f xs) (map id xs)) = (λx. (f x, id x)) ` (set xs)" by (rule set_zip_map) thus ?thesis by simp qed lemma set_zip_map2: "set (zip xs (map f xs)) = (λx. (x, f x)) ` (set xs)" proof - have "set (zip (map id xs) (map f xs)) = (λx. (id x, f x)) ` (set xs)" by (rule set_zip_map) thus ?thesis by simp qed lemma UN_upt: "(⋃i∈{0..<length xs}. f (xs ! i)) = (⋃x∈set xs. f x)" by (metis image_image map_nth set_map set_upt) lemma sum_list_zeroI': assumes "⋀i. i < length xs ⟹ xs ! i = 0" shows "sum_list xs = 0" proof (rule sum_list_zeroI, rule, simp) fix x assume "x ∈ set xs" then obtain i where "i < length xs" and "x = xs ! i" by (metis in_set_conv_nth) from this(1) show "x = 0" unfolding ‹x = xs ! i› by (rule assms) qed lemma sum_list_map2_plus: assumes "length xs = length ys" shows "sum_list (map2 (+) xs ys) = sum_list xs + sum_list (ys::'a::comm_monoid_add list)" using assms proof (induct rule: list_induct2) case Nil show ?case by simp next case (Cons x xs y ys) show ?case by (simp add: Cons(2) ac_simps) qed lemma sum_list_eq_nthI: assumes "i < length xs" and "⋀j. j < length xs ⟹ j ≠ i ⟹ xs ! j = 0" shows "sum_list xs = xs ! i" using assms proof (induct xs arbitrary: i) case Nil from Nil(1) show ?case by simp next case (Cons x xs) have *: "xs ! j = 0" if "j < length xs" and "Suc j ≠ i" for j proof - have "xs ! j = (x # xs) ! (Suc j)" by simp also have "... = 0" by (rule Cons(3), simp add: ‹j < length xs›, fact) finally show ?thesis . qed show ?case proof (cases i) case 0 have "sum_list xs = 0" by (rule sum_list_zeroI', erule *, simp add: 0) with 0 show ?thesis by simp next case (Suc k) with Cons(2) have "k < length xs" by simp hence "sum_list xs = xs ! k" proof (rule Cons(1)) fix j assume "j < length xs" assume "j ≠ k" hence "Suc j ≠ i" by (simp add: Suc) with ‹j < length xs› show "xs ! j = 0" by (rule *) qed moreover have "x = 0" proof - have "x = (x # xs) ! 0" by simp also have "... = 0" by (rule Cons(3), simp_all add: Suc) finally show ?thesis . qed ultimately show ?thesis by (simp add: Suc) qed qed subsubsection ‹‹max_list›› fun (in ord) max_list :: "'a list ⇒ 'a" where "max_list (x # xs) = (case xs of [] ⇒ x | _ ⇒ max x (max_list xs))" context linorder begin lemma max_list_Max: "xs ≠ [] ⟹ max_list xs = Max (set xs)" by (induct xs rule: induct_list012, auto) lemma max_list_ge: assumes "x ∈ set xs" shows "x ≤ max_list xs" proof - from assms have "xs ≠ []" by auto from finite_set assms have "x ≤ Max (set xs)" by (rule Max_ge) also from ‹xs ≠ []› have "Max (set xs) = max_list xs" by (rule max_list_Max[symmetric]) finally show ?thesis . qed lemma max_list_boundedI: assumes "xs ≠ []" and "⋀x. x ∈ set xs ⟹ x ≤ a" shows "max_list xs ≤ a" proof - from assms(1) have "set xs ≠ {}" by simp from assms(1) have "max_list xs = Max (set xs)" by (rule max_list_Max) also from finite_set ‹set xs ≠ {}› assms(2) have "… ≤ a" by (rule Max.boundedI) finally show ?thesis . qed end subsubsection ‹‹insort_wrt›› primrec insort_wrt :: "('c ⇒ 'c ⇒ bool) ⇒ 'c ⇒ 'c list ⇒ 'c list" where "insort_wrt _ x [] = [x]" | "insort_wrt r x (y # ys) = (if r x y then (x # y # ys) else y # (insort_wrt r x ys))" lemma insort_wrt_not_Nil [simp]: "insort_wrt r x xs ≠ []" by (induct xs, simp_all) lemma length_insort_wrt [simp]: "length (insort_wrt r x xs) = Suc (length xs)" by (induct xs, simp_all) lemma set_insort_wrt [simp]: "set (insort_wrt r x xs) = insert x (set xs)" by (induct xs, auto) lemma sorted_wrt_insort_wrt_imp_sorted_wrt: assumes "sorted_wrt r (insort_wrt s x xs)" shows "sorted_wrt r xs" using assms proof (induct xs) case Nil show ?case by simp next case (Cons a xs) show ?case proof (cases "s x a") case True with Cons.prems have "sorted_wrt r (x # a # xs)" by simp thus ?thesis by simp next case False with Cons(2) have "sorted_wrt r (a # (insort_wrt s x xs))" by simp hence *: "(∀y∈set xs. r a y)" and "sorted_wrt r (insort_wrt s x xs)" by (simp_all) from this(2) have "sorted_wrt r xs" by (rule Cons(1)) with * show ?thesis by (simp) qed qed lemma sorted_wrt_imp_sorted_wrt_insort_wrt: assumes "transp r" and "⋀a. r a x ∨ r x a" and "sorted_wrt r xs" shows "sorted_wrt r (insort_wrt r x xs)" using assms(3) proof (induct xs) case Nil show ?case by simp next case (Cons a xs) show ?case proof (cases "r x a") case True with Cons(2) assms(1) show ?thesis by (auto dest: transpD) next case False with assms(2) have "r a x" by blast from Cons(2) have *: "(∀y∈set xs. r a y)" and "sorted_wrt r xs" by (simp_all) from this(2) have "sorted_wrt r (insort_wrt r x xs)" by (rule Cons(1)) with ‹r a x› * show ?thesis by (simp add: False) qed qed corollary sorted_wrt_insort_wrt: assumes "transp r" and "⋀a. r a x ∨ r x a" shows "sorted_wrt r (insort_wrt r x xs) ⟷ sorted_wrt r xs" (is "?l ⟷ ?r") proof assume ?l then show ?r by (rule sorted_wrt_insort_wrt_imp_sorted_wrt) next assume ?r with assms show ?l by (rule sorted_wrt_imp_sorted_wrt_insort_wrt) qed subsubsection ‹‹diff_list› and ‹insert_list›› definition diff_list :: "'a list ⇒ 'a list ⇒ 'a list" (infixl "--" 65) where "diff_list xs ys = fold removeAll ys xs" lemma set_diff_list: "set (xs -- ys) = set xs - set ys" by (simp only: diff_list_def, induct ys arbitrary: xs, auto) lemma diff_list_disjoint: "set ys ∩ set (xs -- ys) = {}" unfolding set_diff_list by (rule Diff_disjoint) lemma subset_append_diff_cancel: assumes "set ys ⊆ set xs" shows "set (ys @ (xs -- ys)) = set xs" by (simp only: set_append set_diff_list Un_Diff_cancel, rule Un_absorb1, fact) definition insert_list :: "'a ⇒ 'a list ⇒ 'a list" where "insert_list x xs = (if x ∈ set xs then xs else x # xs)" lemma set_insert_list: "set (insert_list x xs) = insert x (set xs)" by (auto simp add: insert_list_def) subsubsection ‹‹remdups_wrt›› primrec remdups_wrt :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'a list" where remdups_wrt_base: "remdups_wrt _ [] = []" | remdups_wrt_rec: "remdups_wrt f (x # xs) = (if f x ∈ f ` set xs then remdups_wrt f xs else x # remdups_wrt f xs)" lemma set_remdups_wrt: "f ` set (remdups_wrt f xs) = f ` set xs" proof (induct xs) case Nil show ?case unfolding remdups_wrt_base .. next case (Cons a xs) show ?case unfolding remdups_wrt_rec proof (simp only: split: if_splits, intro conjI, intro impI) assume "f a ∈ f ` set xs" have "f ` set (a # xs) = insert (f a) (f ` set xs)" by simp have "f ` set (remdups_wrt f xs) = f ` set xs" by fact also from ‹f a ∈ f ` set xs› have "... = insert (f a) (f ` set xs)" by (simp add: insert_absorb) also have "... = f ` set (a # xs)" by simp finally show "f ` set (remdups_wrt f xs) = f ` set (a # xs)" . qed (simp add: Cons.hyps) qed lemma subset_remdups_wrt: "set (remdups_wrt f xs) ⊆ set xs" by (induct xs, auto) lemma remdups_wrt_distinct_wrt: assumes "x ∈ set (remdups_wrt f xs)" and "y ∈ set (remdups_wrt f xs)" and "x ≠ y" shows "f x ≠ f y" using assms(1) assms(2) proof (induct xs) case Nil thus ?case unfolding remdups_wrt_base by simp next case (Cons a xs) from Cons(2) Cons(3) show ?case unfolding remdups_wrt_rec proof (simp only: split: if_splits) assume "x ∈ set (remdups_wrt f xs)" and "y ∈ set (remdups_wrt f xs)" thus "f x ≠ f y" by (rule Cons.hyps) next assume "¬ True" thus "f x ≠ f y" by simp next assume "f a ∉ f ` set xs" and xin: "x ∈ set (a # remdups_wrt f xs)" and yin: "y ∈ set (a # remdups_wrt f xs)" from yin have y: "y = a ∨ y ∈ set (remdups_wrt f xs)" by simp from xin have "x = a ∨ x ∈ set (remdups_wrt f xs)" by simp thus "f x ≠ f y" proof assume "x = a" from y show ?thesis proof assume "y = a" with ‹x ≠ y› show ?thesis unfolding ‹x = a› by simp next assume "y ∈ set (remdups_wrt f xs)" have "y ∈ set xs" by (rule, fact, rule subset_remdups_wrt) hence "f y ∈ f ` set xs" by simp with ‹f a ∉ f ` set xs› show ?thesis unfolding ‹x = a› by auto qed next assume "x ∈ set (remdups_wrt f xs)" from y show ?thesis proof assume "y = a" have "x ∈ set xs" by (rule, fact, rule subset_remdups_wrt) hence "f x ∈ f ` set xs" by simp with ‹f a ∉ f ` set xs› show ?thesis unfolding ‹y = a› by auto next assume "y ∈ set (remdups_wrt f xs)" with ‹x ∈ set (remdups_wrt f xs)› show ?thesis by (rule Cons.hyps) qed qed qed qed lemma distinct_remdups_wrt: "distinct (remdups_wrt f xs)" proof (induct xs) case Nil show ?case unfolding remdups_wrt_base by simp next case (Cons a xs) show ?case unfolding remdups_wrt_rec proof (split if_split, intro conjI impI, rule Cons.hyps) assume "f a ∉ f ` set xs" hence "a ∉ set xs" by auto hence "a ∉ set (remdups_wrt f xs)" using subset_remdups_wrt[of f xs] by auto with Cons.hyps show "distinct (a # remdups_wrt f xs)" by simp qed qed lemma map_remdups_wrt: "map f (remdups_wrt f xs) = remdups (map f xs)" by (induct xs, auto) lemma remdups_wrt_append: "remdups_wrt f (xs @ ys) = (filter (λa. f a ∉ f ` set ys) (remdups_wrt f xs)) @ (remdups_wrt f ys)" by (induct xs, auto) subsubsection ‹‹map_idx›› primrec map_idx :: "('a ⇒ nat ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ 'b list" where "map_idx f [] n = []"| "map_idx f (x # xs) n = (f x n) # (map_idx f xs (Suc n))" lemma map_idx_eq_map2: "map_idx f xs n = map2 f xs [n..<n + length xs]" proof (induct xs arbitrary: n) case Nil show ?case by simp next case (Cons x xs) have eq: "[n..<n + length (x # xs)] = n # [Suc n..<Suc (n + length xs)]" by (metis add_Suc_right length_Cons less_add_Suc1 upt_conv_Cons) show ?case unfolding eq by (simp add: Cons del: upt_Suc) qed lemma length_map_idx [simp]: "length (map_idx f xs n) = length xs" by (simp add: map_idx_eq_map2) lemma map_idx_append: "map_idx f (xs @ ys) n = (map_idx f xs n) @ (map_idx f ys (n + length xs))" by (simp add: map_idx_eq_map2 ab_semigroup_add_class.add_ac(1) zip_append1) lemma map_idx_nth: assumes "i < length xs" shows "(map_idx f xs n) ! i = f (xs ! i) (n + i)" using assms by (simp add: map_idx_eq_map2) lemma map_map_idx: "map f (map_idx g xs n) = map_idx (λx i. f (g x i)) xs n" by (auto simp add: map_idx_eq_map2) lemma map_idx_map: "map_idx f (map g xs) n = map_idx (f ∘ g) xs n" by (simp add: map_idx_eq_map2 map_zip_map) lemma map_idx_no_idx: "map_idx (λx _. f x) xs n = map f xs" by (induct xs arbitrary: n, simp_all) lemma map_idx_no_elem: "map_idx (λ_. f) xs n = map f [n..<n + length xs]" proof (induct xs arbitrary: n) case Nil show ?case by simp next case (Cons x xs) have eq: "[n..<n + length (x # xs)] = n # [Suc n..<Suc (n + length xs)]" by (metis add_Suc_right length_Cons less_add_Suc1 upt_conv_Cons) show ?case unfolding eq by (simp add: Cons del: upt_Suc) qed lemma map_idx_eq_map: "map_idx f xs n = map (λi. f (xs ! i) (i + n)) [0..<length xs]" proof (induct xs arbitrary: n) case Nil show ?case by simp next case (Cons x xs) have eq: "[0..<length (x # xs)] = 0 # [Suc 0..<Suc (length xs)]" by (metis length_Cons upt_conv_Cons zero_less_Suc) have "map (λi. f ((x # xs) ! i) (i + n)) [Suc 0..<Suc (length xs)] = map ((λi. f ((x # xs) ! i) (i + n)) ∘ Suc) [0..<length xs]" by (metis map_Suc_upt map_map) also have "... = map (λi. f (xs ! i) (Suc (i + n))) [0..<length xs]" by (rule map_cong, fact refl, simp) finally show ?case unfolding eq by (simp add: Cons del: upt_Suc) qed lemma set_map_idx: "set (map_idx f xs n) = (λi. f (xs ! i) (i + n)) ` {0..<length xs}" by (simp add: map_idx_eq_map) subsubsection ‹‹map_dup›› primrec map_dup :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where "map_dup _ _ [] = []"| "map_dup f g (x # xs) = (if x ∈ set xs then g x else f x) # (map_dup f g xs)" lemma length_map_dup[simp]: "length (map_dup f g xs) = length xs" by (induct xs, simp_all) lemma map_dup_distinct: assumes "distinct xs" shows "map_dup f g xs = map f xs" using assms by (induct xs, simp_all) lemma filter_map_dup_const: "filter (λx. x ≠ c) (map_dup f (λ_. c) xs) = filter (λx. x ≠ c) (map f (remdups xs))" by (induct xs, simp_all) lemma filter_zip_map_dup_const: "filter (λ(a, b). a ≠ c) (zip (map_dup f (λ_. c) xs) xs) = filter (λ(a, b). a ≠ c) (zip (map f (remdups xs)) (remdups xs))" by (induct xs, simp_all) subsubsection ‹Filtering Minimal Elements› context fixes rel :: "'a ⇒ 'a ⇒ bool" begin primrec filter_min_aux :: "'a list ⇒ 'a list ⇒ 'a list" where "filter_min_aux [] ys = ys"| "filter_min_aux (x # xs) ys = (if (∃y∈(set xs ∪ set ys). rel y x) then (filter_min_aux xs ys) else (filter_min_aux xs (x # ys)))" definition filter_min :: "'a list ⇒ 'a list" where "filter_min xs = filter_min_aux xs []" definition filter_min_append :: "'a list ⇒ 'a list ⇒ 'a list" where "filter_min_append xs ys = (let P = (λzs. λx. ¬ (∃z∈set zs. rel z x)); ys1 = filter (P xs) ys in (filter (P ys1) xs) @ ys1)" lemma filter_min_aux_supset: "set ys ⊆ set (filter_min_aux xs ys)" proof (induct xs arbitrary: ys) case Nil show ?case by simp next case (Cons x xs) have "set ys ⊆ set (x # ys)" by auto also have "set (x # ys) ⊆ set (filter_min_aux xs (x # ys))" by (rule Cons.hyps) finally have "set ys ⊆ set (filter_min_aux xs (x # ys))" . moreover have "set ys ⊆ set (filter_min_aux xs ys)" by (rule Cons.hyps) ultimately show ?case by simp qed lemma filter_min_aux_subset: "set (filter_min_aux xs ys) ⊆ set xs ∪ set ys" proof (induct xs arbitrary: ys) case Nil show ?case by simp next case (Cons x xs) note Cons.hyps also have "set xs ∪ set ys ⊆ set (x # xs) ∪ set ys" by fastforce finally have c1: "set (filter_min_aux xs ys) ⊆ set (x # xs) ∪ set ys" . note Cons.hyps also have "set xs ∪ set (x # ys) = set (x # xs) ∪ set ys" by simp finally have "set (filter_min_aux xs (x # ys)) ⊆ set (x # xs) ∪ set ys" . with c1 show ?case by simp qed lemma filter_min_aux_relE: assumes "transp rel" and "x ∈ set xs" and "x ∉ set (filter_min_aux xs ys)" obtains y where "y ∈ set (filter_min_aux xs ys)" and "rel y x" using assms(2, 3) proof (induct xs arbitrary: x ys thesis) case Nil from Nil(2) show ?case by simp next case (Cons x0 xs) from Cons(3) have "x = x0 ∨ x ∈ set xs" by simp thus ?case proof assume "x = x0" from Cons(4) have *: "∃y∈set xs ∪ set ys. rel y x0" proof (simp add: ‹x = x0› split: if_splits) assume "x0 ∉ set (filter_min_aux xs (x0 # ys))" moreover from filter_min_aux_supset have "x0 ∈ set (filter_min_aux xs (x0 # ys))" by (rule subsetD) simp ultimately show False .. qed hence eq: "filter_min_aux (x0 # xs) ys = filter_min_aux xs ys" by simp from * obtain x1 where "x1 ∈ set xs ∪ set ys" and "rel x1 x" unfolding ‹x = x0› .. from this(1) show ?thesis proof assume "x1 ∈ set xs" show ?thesis proof (cases "x1 ∈ set (filter_min_aux xs ys)") case True hence "x1 ∈ set (filter_min_aux (x0 # xs) ys)" by (simp only: eq) thus ?thesis using ‹rel x1 x› by (rule Cons(2)) next case False with ‹x1 ∈ set xs› obtain y where "y ∈ set (filter_min_aux xs ys)" and "rel y x1" using Cons.hyps by blast from this(1) have "y ∈ set (filter_min_aux (x0 # xs) ys)" by (simp only: eq) moreover from assms(1) ‹rel y x1› ‹rel x1 x› have "rel y x" by (rule transpD) ultimately show ?thesis by (rule Cons(2)) qed next assume "x1 ∈ set ys" hence "x1 ∈ set (filter_min_aux (x0 # xs) ys)" using filter_min_aux_supset .. thus ?thesis using ‹rel x1 x› by (rule Cons(2)) qed next assume "x ∈ set xs" show ?thesis proof (cases "∃y∈set xs ∪ set ys. rel y x0") case True hence eq: "filter_min_aux (x0 # xs) ys = filter_min_aux xs ys" by simp with Cons(4) have "x ∉ set (filter_min_aux xs ys)" by simp with ‹x ∈ set xs› obtain y where "y ∈ set (filter_min_aux xs ys)" and "rel y x" using Cons.hyps by blast from this(1) have "y ∈ set (filter_min_aux (x0 # xs) ys)" by (simp only: eq) thus ?thesis using ‹rel y x› by (rule Cons(2)) next case False hence eq: "filter_min_aux (x0 # xs) ys = filter_min_aux xs (x0 # ys)" by simp with Cons(4) have "x ∉ set (filter_min_aux xs (x0 # ys))" by simp with ‹x ∈ set xs› obtain y where "y ∈ set (filter_min_aux xs (x0 # ys))" and "rel y x" using Cons.hyps by blast from this(1) have "y ∈ set (filter_min_aux (x0 # xs) ys)" by (simp only: eq) thus ?thesis using ‹rel y x› by (rule Cons(2)) qed qed qed lemma filter_min_aux_minimal: assumes "transp rel" and "x ∈ set (filter_min_aux xs ys)" and "y ∈ set (filter_min_aux xs ys)" and "rel x y" assumes "⋀a b. a ∈ set xs ∪ set ys ⟹ b ∈ set ys ⟹ rel a b ⟹ a = b" shows "x = y" using assms(2-5) proof (induct xs arbitrary: x y ys) case Nil from Nil(1) have "x ∈ set [] ∪ set ys" by simp moreover from Nil(2) have "y ∈ set ys" by simp ultimately show ?case using Nil(3) by (rule Nil(4)) next case (Cons x0 xs) show ?case proof (cases "∃y∈set xs ∪ set ys. rel y x0") case True hence eq: "filter_min_aux (x0 # xs) ys = filter_min_aux xs ys" by simp with Cons(2, 3) have "x ∈ set (filter_min_aux xs ys)" and "y ∈ set (filter_min_aux xs ys)" by simp_all thus ?thesis using Cons(4) proof (rule Cons.hyps) fix a b assume "a ∈ set xs ∪ set ys" hence "a ∈ set (x0 # xs) ∪ set ys" by simp moreover assume "b ∈ set ys" and "rel a b" ultimately show "a = b" by (rule Cons(5)) qed next case False hence eq: "filter_min_aux (x0 # xs) ys = filter_min_aux xs (x0 # ys)" by simp with Cons(2, 3) have "x ∈ set (filter_min_aux xs (x0 # ys))" and "y ∈ set (filter_min_aux xs (x0 # ys))" by simp_all thus ?thesis using Cons(4) proof (rule Cons.hyps) fix a b assume a: "a ∈ set xs ∪ set (x0 # ys)" and "b ∈ set (x0 # ys)" and "rel a b" from this(2) have "b = x0 ∨ b ∈ set ys" by simp thus "a = b" proof assume "b = x0" from a have "a = x0 ∨ a ∈ set xs ∪ set ys" by simp thus ?thesis proof assume "a = x0" with ‹b = x0› show ?thesis by simp next assume "a ∈ set xs ∪ set ys" hence "∃y∈set xs ∪ set ys. rel y x0" using ‹rel a b› unfolding ‹b = x0› .. with False show ?thesis .. qed next from a have "a ∈ set (x0 # xs) ∪ set ys" by simp moreover assume "b ∈ set ys" ultimately show ?thesis using ‹rel a b› by (rule Cons(5)) qed qed qed qed lemma filter_min_aux_distinct: assumes "reflp rel" and "distinct ys" shows "distinct (filter_min_aux xs ys)" using assms(2) proof (induct xs arbitrary: ys) case Nil thus ?case by simp next case (Cons x xs) show ?case proof (simp split: if_split, intro conjI impI) from Cons(2) show "distinct (filter_min_aux xs ys)" by (rule Cons.hyps) next assume a: "∀y∈set xs ∪ set ys. ¬ rel y x" show "distinct (filter_min_aux xs (x # ys))" proof (rule Cons.hyps) have "x ∉ set ys" proof assume "x ∈ set ys" hence "x ∈ set xs ∪ set ys" by simp with a have "¬ rel x x" .. moreover from assms(1) have "rel x x" by (rule reflpD) ultimately show False .. qed with Cons(2) show "distinct (x # ys)" by simp qed qed qed lemma filter_min_subset: "set (filter_min xs) ⊆ set xs" using filter_min_aux_subset[of xs "[]"] by (simp add: filter_min_def) lemma filter_min_cases: assumes "transp rel" and "x ∈ set xs" assumes "x ∈ set (filter_min xs) ⟹ thesis" assumes "⋀y. y ∈ set (filter_min xs) ⟹ x ∉ set (filter_min xs) ⟹ rel y x ⟹ thesis" shows thesis proof (cases "x ∈ set (filter_min xs)") case True thus ?thesis by (rule assms(3)) next case False with assms(1, 2) obtain y where "y ∈ set (filter_min xs)" and "rel y x" unfolding filter_min_def by (rule filter_min_aux_relE) from this(1) False this(2) show ?thesis by (rule assms(4)) qed corollary filter_min_relE: assumes "transp rel" and "reflp rel" and "x ∈ set xs" obtains y where "y ∈ set (filter_min xs)" and "rel y x" using assms(1, 3) proof (rule filter_min_cases) assume "x ∈ set (filter_min xs)" moreover from assms(2) have "rel x x" by (rule reflpD) ultimately show ?thesis .. qed lemma filter_min_minimal: assumes "transp rel" and "x ∈ set (filter_min xs)" and "y ∈ set (filter_min xs)" and "rel x y" shows "x = y" using assms unfolding filter_min_def by (rule filter_min_aux_minimal) simp lemma filter_min_distinct: assumes "reflp rel" shows "distinct (filter_min xs)" unfolding filter_min_def by (rule filter_min_aux_distinct, fact, simp) lemma filter_min_append_subset: "set (filter_min_append xs ys) ⊆ set xs ∪ set ys" by (auto simp: filter_min_append_def) lemma filter_min_append_cases: assumes "transp rel" and "x ∈ set xs ∪ set ys" assumes "x ∈ set (filter_min_append xs ys) ⟹ thesis" assumes "⋀y. y ∈ set (filter_min_append xs ys) ⟹ x ∉ set (filter_min_append xs ys) ⟹ rel y x ⟹ thesis" shows thesis proof (cases "x ∈ set (filter_min_append xs ys)") case True thus ?thesis by (rule assms(3)) next case False define P where "P = (λzs. λa. ¬ (∃z∈set zs. rel z a))" from assms(2) obtain y where "y ∈ set (filter_min_append xs ys)" and "rel y x" proof assume "x ∈ set xs" with False obtain y where "y ∈ set (filter_min_append xs ys)" and "rel y x" by (auto simp: filter_min_append_def P_def) thus ?thesis .. next assume "x ∈ set ys" with False obtain y where "y ∈ set xs" and "rel y x" by (auto simp: filter_min_append_def P_def) show ?thesis proof (cases "y ∈ set (filter_min_append xs ys)") case True thus ?thesis using ‹rel y x› .. next case False with ‹y ∈ set xs› obtain y' where y': "y' ∈ set (filter_min_append xs ys)" and "rel y' y" by (auto simp: filter_min_append_def P_def) from assms(1) this(2) ‹rel y x› have "rel y' x" by (rule transpD) with y' show ?thesis .. qed qed from this(1) False this(2) show ?thesis by (rule assms(4)) qed corollary filter_min_append_relE: assumes "transp rel" and "reflp rel" and "x ∈ set xs ∪ set ys" obtains y where "y ∈ set (filter_min_append xs ys)" and "rel y x" using assms(1, 3) proof (rule filter_min_append_cases) assume "x ∈ set (filter_min_append xs ys)" moreover from assms(2) have "rel x x" by (rule reflpD) ultimately show ?thesis .. qed lemma filter_min_append_minimal: assumes "⋀x' y'. x' ∈ set xs ⟹ y' ∈ set xs ⟹ rel x' y' ⟹ x' = y'" and "⋀x' y'. x' ∈ set ys ⟹ y' ∈ set ys ⟹ rel x' y' ⟹ x' = y'" and "x ∈ set (filter_min_append xs ys)" and "y ∈ set (filter_min_append xs ys)" and "rel x y" shows "x = y" proof - define P where "P = (λzs. λa. ¬ (∃z∈set zs. rel z a))" define ys1 where "ys1 = filter (P xs) ys" from assms(3) have "x ∈ set xs ∪ set ys1" by (auto simp: filter_min_append_def P_def ys1_def) moreover from assms(4) have "y ∈ set (filter (P ys1) xs) ∪ set ys1" by (simp add: filter_min_append_def P_def ys1_def) ultimately show ?thesis proof (elim UnE) assume "x ∈ set xs" assume "y ∈ set (filter (P ys1) xs)" hence "y ∈ set xs" by simp with ‹x ∈ set xs› show ?thesis using assms(5) by (rule assms(1)) next assume "y ∈ set ys1" hence "⋀z. z ∈ set xs ⟹ ¬ rel z y" by (simp add: ys1_def P_def) moreover assume "x ∈ set xs" ultimately have "¬ rel x y" by blast thus ?thesis using ‹rel x y› .. next assume "y ∈ set (filter (P ys1) xs)" hence "⋀z. z ∈ set ys1 ⟹ ¬ rel z y" by (simp add: P_def) moreover assume "x ∈ set ys1" ultimately have "¬ rel x y" by blast thus ?thesis using ‹rel x y› .. next assume "x ∈ set ys1" and "y ∈ set ys1" hence "x ∈ set ys" and "y ∈ set ys" by (simp_all add: ys1_def) thus ?thesis using assms(5) by (rule assms(2)) qed qed lemma filter_min_append_distinct: assumes "reflp rel" and "distinct xs" and "distinct ys" shows "distinct (filter_min_append xs ys)" proof - define P where "P = (λzs. λa. ¬ (∃z∈set zs. rel z a))" define ys1 where "ys1 = filter (P xs) ys" from assms(2) have "distinct (filter (P ys1) xs)" by simp moreover from assms(3) have "distinct ys1" by (simp add: ys1_def) moreover have "set (filter (P ys1) xs) ∩ set ys1 = {}" proof (simp add: set_eq_iff, intro allI impI notI) fix x assume "P ys1 x" hence "⋀z. z ∈ set ys1 ⟹ ¬ rel z x" by (simp add: P_def) moreover assume "x ∈ set ys1" ultimately have "¬ rel x x" by blast moreover from assms(1) have "rel x x" by (rule reflpD) ultimately show False .. qed ultimately show ?thesis by (simp add: filter_min_append_def ys1_def P_def) qed end end (* theory *)

# Theory Confluence

(* Author: Fabian Immler, Alexander Maletzky *) section ‹Properties of Binary Relations› theory Confluence imports "Abstract-Rewriting.Abstract_Rewriting" "Open_Induction.Restricted_Predicates" begin text ‹This theory formalizes some general properties of binary relations, in particular a very weak sufficient condition for a relation to be Church-Rosser.› (* Maybe one could build upon "Decreasing_Diagrams" / "Decreasing_Diagrams_II" from the AFP? *) subsection ‹@{const wfp_on}› (* Probably the converse direction holds, too. *) lemma wfp_on_imp_wfP: assumes "wfp_on r A" shows "wfP (λx y. r x y ∧ x ∈ A ∧ y ∈ A)" (is "wfP ?r") proof (simp add: wfP_def wf_def, intro allI impI) fix P x assume "∀x. (∀y. r y x ∧ y ∈ A ∧ x ∈ A ⟶ P y) ⟶ P x" hence *: "⋀x. (⋀y. x ∈ A ⟹ y ∈ A ⟹ r y x ⟹ P y) ⟹ P x" by blast from assms have **: "⋀a. a ∈ A ⟹ (⋀x. x ∈ A ⟹ (⋀y. y ∈ A ⟹ r y x ⟹ P y) ⟹ P x) ⟹ P a" by (rule wfp_on_induct) blast+ show "P x" proof (cases "x ∈ A") case True from this * show ?thesis by (rule **) next case False show ?thesis proof (rule *) fix y assume "x ∈ A" with False show "P y" .. qed qed qed lemma wfp_onI_min: assumes "⋀x Q. x ∈ Q ⟹ Q ⊆ A ⟹ ∃z∈Q. ∀y∈A. r y z ⟶ y ∉ Q" shows "wfp_on r A" proof (intro inductive_on_imp_wfp_on minimal_imp_inductive_on allI impI) fix Q x assume "x ∈ Q ∧ Q ⊆ A" hence "x ∈ Q" and "Q ⊆ A" by simp_all hence "∃z∈Q. ∀y∈A. r y z ⟶ y ∉ Q" by (rule assms) then obtain z where "z ∈ Q" and 1: "⋀y. y ∈ A ⟹ r y z ⟹ y ∉ Q" by blast show "∃z∈Q. ∀y. r y z ⟶ y ∉ Q" proof (intro bexI allI impI) fix y assume "r y z" show "y ∉ Q" proof (cases "y ∈ A") case True thus ?thesis using ‹r y z› by (rule 1) next case False with ‹Q ⊆ A› show ?thesis by blast qed qed fact qed lemma wfp_onE_min: assumes "wfp_on r A" and "x ∈ Q" and "Q ⊆ A" obtains z where "z ∈ Q" and "⋀y. r y z ⟹ y ∉ Q" using wfp_on_imp_minimal[OF assms(1)] assms(2, 3) by blast lemma wfp_onI_chain: "¬ (∃f. ∀i. f i ∈ A ∧ r (f (Suc i)) (f i)) ⟹ wfp_on r A" by (simp add: wfp_on_def) lemma finite_minimalE: assumes "finite A" and "A ≠ {}" and "irreflp rel" and "transp rel" obtains a where "a ∈ A" and "⋀b. rel b a ⟹ b ∉ A" using assms(1, 2) proof (induct arbitrary: thesis) case empty from empty(2) show ?case by simp next case (insert a A) show ?case proof (cases "A = {}") case True show ?thesis proof (rule insert(4)) fix b assume "rel b a" with assms(3) show "b ∉ insert a A" by (auto simp: True irreflp_def) qed simp next case False with insert(3) obtain z where "z ∈ A" and *: "⋀b. rel b z ⟹ b ∉ A" by blast show ?thesis proof (cases "rel a z") case True show ?thesis proof (rule insert(4)) fix b assume "rel b a" with assms(4) have "rel b z" using ‹rel a z› by (rule transpD) hence "b ∉ A" by (rule *) moreover from ‹rel b a› assms(3) have "b ≠ a" by (auto simp: irreflp_def) ultimately show "b ∉ insert a A" by simp qed simp next case False show ?thesis proof (rule insert(4)) fix b assume "rel b z" hence "b ∉ A" by (rule *) moreover from ‹rel b z› False have "b ≠ a" by blast ultimately show "b ∉ insert a A" by simp next from ‹z ∈ A› show "z ∈ insert a A" by simp qed qed qed qed lemma wfp_on_finite: assumes "irreflp rel" and "transp rel" and "finite A" shows "wfp_on rel A" proof (rule wfp_onI_min) fix x Q assume "x ∈ Q" and "Q ⊆ A" from this(2) assms(3) have "finite Q" by (rule finite_subset) moreover from ‹x ∈ Q› have "Q ≠ {}" by blast ultimately obtain z where "z ∈ Q" and "⋀y. rel y z ⟹ y ∉ Q" using assms(1, 2) by (rule finite_minimalE) blast thus "∃z∈Q. ∀y∈A. rel y z ⟶ y ∉ Q" by blast qed subsection ‹Relations› locale relation = fixes r::"'a ⇒ 'a ⇒ bool" (infixl "→" 50) begin abbreviation rtc::"'a ⇒ 'a ⇒ bool" (infixl "→⇧^{*}" 50) where "rtc a b ≡ r⇧^{*}⇧^{*}a b" abbreviation sc::"'a ⇒ 'a ⇒ bool" (infixl "↔" 50) where "sc a b ≡ a → b ∨ b → a" definition is_final::"'a ⇒ bool" where "is_final a ≡ ¬ (∃b. r a b)" definition srtc::"'a ⇒ 'a ⇒ bool" (infixl "↔⇧^{*}" 50) where "srtc a b ≡ sc⇧^{*}⇧^{*}a b" definition cs::"'a ⇒ 'a ⇒ bool" (infixl "↓⇧^{*}" 50) where "cs a b ≡ (∃s. (a →⇧^{*}s) ∧ (b →⇧^{*}s))" definition is_confluent_on :: "'a set ⇒ bool" where "is_confluent_on A ⟷ (∀a∈A. ∀b1 b2. (a →⇧^{*}b1 ∧ a →⇧^{*}b2) ⟶ b1 ↓⇧^{*}b2)" definition is_confluent :: bool where "is_confluent ≡ is_confluent_on UNIV" definition is_loc_confluent :: bool where "is_loc_confluent ≡ (∀a b1 b2. (a → b1 ∧ a → b2) ⟶ b1 ↓⇧^{*}b2)" definition is_ChurchRosser :: bool where "is_ChurchRosser ≡ (∀a b. a ↔⇧^{*}b ⟶ a ↓⇧^{*}b)" definition dw_closed :: "'a set ⇒ bool" where "dw_closed A ⟷ (∀a∈A. ∀b. a → b ⟶ b ∈ A)" lemma dw_closedI [intro]: assumes "⋀a b. a ∈ A ⟹ a → b ⟹ b ∈ A" shows "dw_closed A" unfolding dw_closed_def using assms by auto lemma dw_closedD: assumes "dw_closed A" and "a ∈ A" and "a → b" shows "b ∈ A" using assms unfolding dw_closed_def by auto lemma dw_closed_rtrancl: assumes "dw_closed A" and "a ∈ A" and "a →⇧^{*}b" shows "b ∈ A" using assms(3) proof (induct b) case base from assms(2) show ?case . next case (step y z) from assms(1) step(3) step(2) show ?case by (rule dw_closedD) qed lemma dw_closed_empty: "dw_closed {}" by (rule, simp) lemma dw_closed_UNIV: "dw_closed UNIV" by (rule, intro UNIV_I) subsection ‹Setup for Connection to Theory @{theory "Abstract-Rewriting.Abstract_Rewriting"}› abbreviation (input) relset::"('a * 'a) set" where "relset ≡ {(x, y). x → y}" lemma rtc_rtranclI: assumes "a →⇧^{*}b" shows "(a, b) ∈ relset⇧^{*}" using assms by (simp only: Enum.rtranclp_rtrancl_eq) lemma final_NF: "(is_final a) = (a ∈ NF relset)" unfolding is_final_def NF_def by simp lemma sc_symcl: "(a ↔ b) = ((a, b) ∈ relset⇧^{↔})" by simp lemma srtc_conversion: "(a ↔⇧^{*}b) = ((a, b) ∈ relset⇧^{↔}⇧^{*})" proof - have "{(a, b). (a, b) ∈ {(x, y). x → y}⇧^{↔}} = {(a, b). a → b}⇧^{↔}" by auto thus ?thesis unfolding srtc_def conversion_def sc_symcl Enum.rtranclp_rtrancl_eq by simp qed lemma cs_join: "(a ↓⇧^{*}b) = ((a, b) ∈ relset⇧^{↓})" unfolding cs_def join_def by (auto simp add: Enum.rtranclp_rtrancl_eq rtrancl_converse) lemma confluent_CR: "is_confluent = CR relset" by (auto simp add: is_confluent_def is_confluent_on_def CR_defs Enum.rtranclp_rtrancl_eq cs_join) lemma ChurchRosser_conversion: "is_ChurchRosser = (relset⇧^{↔}⇧^{*}⊆ relset⇧^{↓})" by (auto simp add: is_ChurchRosser_def cs_join srtc_conversion) lemma loc_confluent_WCR: shows "is_loc_confluent = WCR relset" unfolding is_loc_confluent_def WCR_defs by (auto simp add: cs_join) lemma wf_converse: shows "(wfP r^--1) = (wf (relset¯))" unfolding wfP_def converse_def by simp lemma wf_SN: shows "(wfP r^--1) = (SN relset)" unfolding wf_converse wf_iff_no_infinite_down_chain SN_on_def by auto subsection ‹Simple Lemmas› lemma rtrancl_is_final: assumes "a →⇧^{*}b" and "is_final a" shows "a = b" proof - from rtranclpD[OF ‹a →⇧^{*}b›] show ?thesis proof assume "a ≠ b ∧ (→)⇧^{+}⇧^{+}a b" hence "(→)⇧^{+}⇧^{+}a b" by simp from ‹is_final a› final_NF have "a ∈ NF relset" by simp from NF_no_trancl_step[OF this] have "(a, b) ∉ {(x, y). x → y}⇧^{+}" .. thus ?thesis using ‹(→)⇧^{+}⇧^{+}a b› unfolding tranclp_unfold .. qed qed lemma cs_refl: shows "x ↓⇧^{*}x" unfolding cs_def proof show "x →⇧^{*}x ∧ x →⇧^{*}x" by simp qed lemma cs_sym: assumes "x ↓⇧^{*}y" shows "y ↓⇧^{*}x" using assms unfolding cs_def proof fix z assume a: "x →⇧^{*}z ∧ y →⇧^{*}z" show "∃s. y →⇧^{*}s ∧ x →⇧^{*}s" proof from a show "y →⇧^{*}z ∧ x →⇧^{*}z" by simp qed qed lemma rtc_implies_cs: assumes "x →⇧^{*}y" shows "x ↓⇧^{*}y" proof - from joinI_left[OF rtc_rtranclI[OF assms]] cs_join show ?thesis by simp qed lemma rtc_implies_srtc: assumes "a →⇧^{*}b" shows "a ↔⇧^{*}b" proof - from conversionI'[OF rtc_rtranclI[OF assms]] srtc_conversion show ?thesis by simp qed lemma srtc_symmetric: assumes "a ↔⇧^{*}b" shows "b ↔⇧^{*}a" proof - from symD[OF conversion_sym[of relset], of a b] assms srtc_conversion show ?thesis by simp qed lemma srtc_transitive: assumes "a ↔⇧^{*}b" and "b ↔⇧^{*}c" shows "a ↔⇧^{*}c" proof - from rtranclp_trans[of "(↔)" a b c] assms show "a ↔⇧^{*}c" unfolding srtc_def . qed lemma cs_implies_srtc: assumes "a ↓⇧^{*}b" shows "a ↔⇧^{*}b" proof - from assms cs_join have "(a, b) ∈ relset⇧^{↓}" by simp hence "(a, b) ∈ relset⇧^{↔}⇧^{*}" using join_imp_conversion by auto thus ?thesis using srtc_conversion by simp qed lemma confluence_equiv_ChurchRosser: "is_confluent = is_ChurchRosser" by (simp only: ChurchRosser_conversion confluent_CR, fact CR_iff_conversion_imp_join) corollary confluence_implies_ChurchRosser: assumes is_confluent shows is_ChurchRosser using assms by (simp only: confluence_equiv_ChurchRosser) lemma ChurchRosser_unique_final: assumes "is_ChurchRosser" and "a →⇧^{*}b1" and "a →⇧^{*}b2" and "is_final b1" and "is_final b2" shows "b1 = b2" proof - from ‹is_ChurchRosser› confluence_equiv_ChurchRosser confluent_CR have "CR relset" by simp from CR_imp_UNF[OF this] assms show ?thesis unfolding UNF_defs normalizability_def by (auto simp add: Enum.rtranclp_rtrancl_eq final_NF) qed lemma wf_on_imp_nf_ex: assumes "wfp_on ((→)¯¯) A" and "dw_closed A" and "a ∈ A" obtains b where "a →⇧^{*}b" and "is_final b" proof - let ?A = "{b∈A. a →⇧^{*}b}" note assms(1) moreover from assms(3) have "a ∈ ?A" by simp moreover have "?A ⊆ A" by auto ultimately show ?thesis proof (rule wfp_onE_min) fix z assume "z ∈ ?A" and "⋀y. (→)¯¯ y z ⟹ y ∉ ?A" from this(2) have *: "⋀y. z → y ⟹ y ∉ ?A" by simp from ‹z ∈ ?A› have "z ∈ A" and "a →⇧^{*}z" by simp_all show thesis proof (rule, fact) show "is_final z" unfolding is_final_def proof assume "∃y. z → y" then obtain y where "z → y" .. hence "y ∉ ?A" by (rule *) moreover from assms(2) ‹z ∈ A› ‹z → y› have "y ∈ A" by (rule dw_closedD) ultimately have "¬ (a →⇧^{*}y)" by simp with rtranclp_trans[OF ‹a →⇧^{*}z›, of y] ‹z → y› show False by auto qed qed qed qed lemma unique_nf_imp_confluence_on: assumes major: "⋀a b1 b2. a ∈ A ⟹ (a →⇧^{*}b1) ⟹ (a →⇧^{*}b2) ⟹ is_final b1 ⟹ is_final b2 ⟹ b1 = b2" and wf: "wfp_on ((→)¯¯) A" and dw: "dw_closed A" shows "is_confluent_on A" unfolding is_confluent_on_def proof (intro ballI allI impI) fix a b1 b2 assume "a →⇧^{*}b1 ∧ a →⇧^{*}b2" hence "a →⇧^{*}b1" and "a →⇧^{*}b2" by simp_all assume "a ∈ A" from dw this ‹a →⇧^{*}b1› have "b1 ∈ A" by (rule dw_closed_rtrancl) from wf dw this obtain c1 where "b1 →⇧^{*}c1" and "is_final c1" by (rule wf_on_imp_nf_ex) from dw ‹a ∈ A› ‹a →⇧^{*}b2› have "b2 ∈ A" by (rule dw_closed_rtrancl) from wf dw this obtain c2 where "b2 →⇧^{*}c2" and "is_final c2" by (rule wf_on_imp_nf_ex) have "c1 = c2" by (rule major, fact, rule rtranclp_trans[OF ‹a →⇧^{*}b1›], fact, rule rtranclp_trans[OF ‹a →⇧^{*}b2›], fact+) show "b1 ↓⇧^{*}b2" unfolding cs_def proof (intro exI, intro conjI) show "b1 →⇧^{*}c1" by fact next show "b2 →⇧^{*}c1" unfolding ‹c1 = c2› by fact qed qed corollary wf_imp_nf_ex: assumes "wfP ((→)¯¯)" obtains b where "a →⇧^{*}b" and "is_final b" proof - from assms have "wfp_on (r^--1) UNIV" by simp moreover note dw_closed_UNIV moreover have "a ∈ UNIV" .. ultimately obtain b where "a →⇧^{*}b" and "is_final b" by (rule wf_on_imp_nf_ex) thus ?thesis .. qed corollary unique_nf_imp_confluence: assumes "⋀a b1 b2. (a →⇧^{*}b1) ⟹ (a →⇧^{*}b2) ⟹ is_final b1 ⟹ is_final b2 ⟹ b1 = b2" and "wfP ((→)¯¯)" shows "is_confluent" unfolding is_confluent_def by (rule unique_nf_imp_confluence_on, erule assms(1), assumption+, simp add: assms(2), fact dw_closed_UNIV) end (*relation*) subsection ‹Advanced Results and the Generalized Newman Lemma› definition relbelow_on :: "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool)" where "relbelow_on A ord z rel a b ≡ (a ∈ A ∧ b ∈ A ∧ rel a b ∧ ord a z ∧ ord b z)" definition cbelow_on_1 :: "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool)" where "cbelow_on_1 A ord z rel ≡ (relbelow_on A ord z rel)⇧^{+}⇧^{+}" definition cbelow_on :: "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool)" where "cbelow_on A ord z rel a b ≡ (a = b ∧ b ∈ A ∧ ord b z) ∨ cbelow_on_1 A ord z rel a b" text ‹Note that @{const cbelow_on} cannot be defined as the reflexive-transitive closure of @{const relbelow_on}, since it is in general not reflexive!› definition is_loc_connective_on :: "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool" where "is_loc_connective_on A ord r ⟷ (∀a∈A. ∀b1 b2. r a b1 ∧ r a b2 ⟶ cbelow_on A ord a (relation.sc r) b1 b2)" text ‹Note that @{const wfp_on} is @{emph ‹not›} the same as @{const SN_on}, since in the definition of @{const SN_on} only the @{emph ‹first›} element of the chain must be in the set.› lemma cbelow_on_first_below: assumes "cbelow_on A ord z rel a b" shows "ord a z" using assms unfolding cbelow_on_def proof assume "cbelow_on_1 A ord z rel a b" thus "ord a z" unfolding cbelow_on_1_def by (induct rule: tranclp_induct, simp add: relbelow_on_def) qed simp lemma cbelow_on_second_below: assumes "cbelow_on A ord z rel a b" shows "ord b z" using assms unfolding cbelow_on_def proof assume "cbelow_on_1 A ord z rel a b" thus "ord b z" unfolding cbelow_on_1_def by (induct rule: tranclp_induct, simp_all add: relbelow_on_def) qed simp lemma cbelow_on_first_in: assumes "cbelow_on A ord z rel a b" shows "a ∈ A" using assms unfolding cbelow_on_def proof assume "cbelow_on_1 A ord z rel a b" thus ?thesis unfolding cbelow_on_1_def by (induct rule: tranclp_induct, simp add: relbelow_on_def) qed simp lemma cbelow_on_second_in: assumes "cbelow_on A ord z rel a b" shows "b ∈ A" using assms unfolding cbelow_on_def proof assume "cbelow_on_1 A ord z rel a b" thus ?thesis unfolding cbelow_on_1_def by (induct rule: tranclp_induct, simp_all add: relbelow_on_def) qed simp lemma cbelow_on_intro [intro]: assumes main: "cbelow_on A ord z rel a b" and "c ∈ A" and "rel b c" and "ord c z" shows "cbelow_on A ord z rel a c" proof - from main have "b ∈ A" by (rule cbelow_on_second_in) from main show ?thesis unfolding cbelow_on_def proof (intro disjI2) assume cases: "(a = b ∧ b ∈ A ∧ ord b z) ∨ cbelow_on_1 A ord z rel a b" from ‹b ∈ A› ‹c ∈ A› ‹rel b c› ‹ord c z› cbelow_on_second_below[OF main] have bc: "relbelow_on A ord z rel b c" by (simp add: relbelow_on_def) from cases show "cbelow_on_1 A ord z rel a c" proof assume "a = b ∧ b ∈ A ∧ ord b z" from this bc have "relbelow_on A ord z rel a c" by simp thus ?thesis by (simp add: cbelow_on_1_def) next assume "cbelow_on_1 A ord z rel a b" from this bc show ?thesis unfolding cbelow_on_1_def by (rule tranclp.intros(2)) qed qed qed lemma cbelow_on_induct [consumes 1, case_names base step]: assumes a: "cbelow_on A ord z rel a b" and base: "a ∈ A ⟹ ord a z ⟹ P a" and ind: "⋀b c. [| cbelow_on A ord z rel a b; rel b c; c ∈ A; ord c z; P b |] ==> P c" shows "P b" using a unfolding cbelow_on_def proof assume "a = b ∧ b ∈ A ∧ ord b z" from this base show "P b" by simp next assume "cbelow_on_1 A ord z rel a b" thus "P b" unfolding cbelow_on_1_def proof (induct x≡a b) fix b assume "relbelow_on A ord z rel a b" hence "rel a b" and "a ∈ A" and "b ∈ A" and "ord a z" and "ord b z" by (simp_all add: relbelow_on_def) hence "cbelow_on A ord z rel a a" by (simp add: cbelow_on_def) from this ‹rel a b› ‹b ∈ A› ‹ord b z› base[OF ‹a ∈ A› ‹ord a z›] show "P b" by (rule ind) next fix b c assume IH: "(relbelow_on A ord z rel)⇧^{+}⇧^{+}a b" and "P b" and "relbelow_on A ord z rel b c" hence "rel b c" and "b ∈ A" and "c ∈ A" and "ord b z" and "ord c z" by (simp_all add: relbelow_on_def) from IH have "cbelow_on A ord z rel a b" by (simp add: cbelow_on_def cbelow_on_1_def) from this ‹rel b c› ‹c ∈ A› ‹ord c z› ‹P b› show "P c" by (rule ind) qed qed lemma cbelow_on_symmetric: assumes main: "cbelow_on A ord z rel a b" and "symp rel" shows "cbelow_on A ord z rel b a" using main unfolding cbelow_on_def proof assume a1: "a = b ∧ b ∈ A ∧ ord b z" show "b = a ∧ a ∈ A ∧ ord a z ∨ cbelow_on_1 A ord z rel b a" proof from a1 show "b = a ∧ a ∈ A ∧ ord a z" by simp qed next assume a2: "cbelow_on_1 A ord z rel a b" show "b = a ∧ a ∈ A ∧ ord a z ∨ cbelow_on_1 A ord z rel b a" proof (rule disjI2) from ‹symp rel› have "symp (relbelow_on A ord z rel)" unfolding symp_def proof (intro allI impI) fix x y assume rel_sym: "∀x y. rel x y ⟶ rel y x" assume "relbelow_on A ord z rel x y" hence "rel x y" and "x ∈ A" and "y ∈ A" and "ord x z" and "ord y z" by (simp_all add: relbelow_on_def) show "relbelow_on A ord z rel y x" unfolding relbelow_on_def proof (intro conjI) from rel_sym ‹rel x y› show "rel y x" by simp qed fact+ qed from sym_trancl[to_pred, OF this] a2 show "cbelow_on_1 A ord z rel b a" by (simp add: symp_def cbelow_on_1_def) qed qed lemma cbelow_on_transitive: assumes "cbelow_on A ord z rel a b" and "cbelow_on A ord z rel b c" shows "cbelow_on A ord z rel a c" proof (induct rule: cbelow_on_induct[OF ‹cbelow_on A ord z rel b c›]) from ‹cbelow_on A ord z rel a b› show "cbelow_on A ord z rel a b" . next fix c0 c assume "cbelow_on A ord z rel b c0" and "rel c0 c" and "c ∈ A" and "ord c z" and "cbelow_on A ord z rel a c0" show "cbelow_on A ord z rel a c" by (rule, fact+) qed lemma cbelow_on_mono: assumes "cbelow_on A ord z rel a b" and "A ⊆ B" shows "cbelow_on B ord z rel a b" using assms(1) proof (induct rule: cbelow_on_induct) case base show ?case by (simp add: cbelow_on_def, intro disjI1 conjI, rule, fact+) next case (step b c) from step(3) assms(2) have "c ∈ B" .. from step(5) this step(2) step (4) show ?case .. qed locale relation_order = relation + fixes ord::"'a ⇒ 'a ⇒ bool" fixes A::"'a set" assumes trans: "ord x y ⟹ ord y z ⟹ ord x z" assumes wf: "wfp_on ord A" assumes refines: "(→) ≤ ord¯¯" begin lemma relation_refines: assumes "a → b" shows "ord b a" using refines assms by auto lemma relation_wf: "wfp_on (→)¯¯ A" using subset_refl _ wf proof (rule wfp_on_mono) fix x y assume "(→)¯¯ x y" hence "y → x" by simp with refines have "(ord)¯¯ y x" .. thus "ord x y" by simp qed lemma rtc_implies_cbelow_on: assumes "dw_closed A" and main: "a →⇧^{*}b" and "a ∈ A" and "ord a c" shows "cbelow_on A ord c (↔) a b" using main proof (induct rule: rtranclp_induct) from assms(3) assms(4) show "cbelow_on A ord c (↔) a a" by (simp add: cbelow_on_def) next fix b0 b assume "a →⇧^{*}b0" and "b0 → b" and IH: "cbelow_on A ord c (↔) a b0" from assms(1) assms(3) ‹a →⇧^{*}b0› have "b0 ∈ A" by (rule dw_closed_rtrancl) from assms(1) this ‹b0 → b› have "b ∈ A" by (rule dw_closedD) show "cbelow_on A ord c (↔) a b" proof from ‹b0 → b› show "b0 ↔ b" by simp next from relation_refines[OF ‹b0 → b›] cbelow_on_second_below[OF IH] show "ord b c" by (rule trans) qed fact+ qed lemma cs_implies_cbelow_on: assumes "dw_closed A" and "a ↓⇧^{*}b" and "a ∈ A" and "b ∈ A" and "ord a c" and "ord b c" shows "cbelow_on A ord c (↔) a b" proof - from ‹a ↓⇧^{*}b› obtain s where "a →⇧^{*}s" and "b →⇧^{*}s" unfolding cs_def by auto have sym: "symp (↔)" unfolding symp_def proof (intro allI, intro impI) fix x y assume "x ↔ y" thus "y ↔ x" by auto qed from assms(1) ‹a →⇧^{*}s› assms(3) assms(5) have "cbelow_on A ord c (↔) a s" by (rule rtc_implies_cbelow_on) also have "cbelow_on A ord c (↔) s b" proof (rule cbelow_on_symmetric) from assms(1) ‹b →⇧^{*}s› assms(4) assms(6) show "cbelow_on A ord c (↔) b s" by (rule rtc_implies_cbelow_on) qed fact finally(cbelow_on_transitive) show ?thesis . qed text ‹The generalized Newman lemma, taken from @{cite Winkler1983}:› lemma loc_connectivity_implies_confluence: assumes "is_loc_connective_on A ord (→)" and "dw_closed A" shows "is_confluent_on A" using assms(1) unfolding is_loc_connective_on_def is_confluent_on_def proof (intro ballI allI impI) fix z x y::'a assume "∀a∈A. ∀b1 b2. a → b1 ∧ a → b2 ⟶ cbelow_on A ord a (↔) b1 b2" hence A: "⋀a b1 b2. a ∈ A ⟹ a → b1 ⟹ a → b2 ⟹ cbelow_on A ord a (↔) b1 b2" by simp assume "z ∈ A" and "z →⇧^{*}x ∧ z →⇧^{*}y" with wf show "x ↓⇧^{*}y" proof (induct z arbitrary: x y rule: wfp_on_induct) fix z x y::'a assume IH: "⋀z0 x0 y0. z0 ∈ A ⟹ ord z0 z ⟹ z0 →⇧^{*}x0 ∧ z0 →⇧^{*}y0 ⟹ x0 ↓⇧^{*}y0" and "z →⇧^{*}x ∧ z →⇧^{*}y" hence "z →⇧^{*}x" and "z →⇧^{*}y" by auto assume "z ∈ A" from converse_rtranclpE[OF ‹z →⇧^{*}x›] obtain x1 where "x = z ∨ (z → x1 ∧ x1 →⇧^{*}x)" by auto thus "x ↓⇧^{*}y" proof assume "x = z" show ?thesis unfolding cs_def proof from ‹x = z› ‹z →⇧^{*}y› show "x →⇧^{*}y ∧ y →⇧^{*}y" by simp qed next assume "z → x1 ∧ x1 →⇧^{*}x" hence "z → x1" and "x1 →⇧^{*}x" by auto from assms(2) ‹z ∈ A› this(1) have "x1 ∈ A" by (rule dw_closedD) from converse_rtranclpE[OF ‹z →⇧^{*}y›] obtain y1 where "y = z ∨ (z → y1 ∧ y1 →⇧^{*}y)" by auto thus ?thesis proof assume "y = z" show ?thesis unfolding cs_def proof from ‹y = z› ‹z →⇧^{*}x› show "x →⇧^{*}x ∧ y →⇧^{*}x" by simp qed next assume "z → y1 ∧ y1 →⇧^{*}y" hence "z → y1" and "y1 →⇧^{*}y" by auto from assms(2) ‹z ∈ A› this(1) have "y1 ∈ A" by (rule dw_closedD) have "x1 ↓⇧^{*}y1" proof (induct rule: cbelow_on_induct[OF A[OF ‹z ∈ A› ‹z → x1› ‹z → y1›]]) from cs_refl[of x1] show "x1 ↓⇧^{*}x1" . next fix b c assume "cbelow_on A ord z (↔) x1 b" and "b ↔ c" and "c ∈ A" and "ord c z" and "x1 ↓⇧^{*}b" from this(1) have "b ∈ A" by (rule cbelow_on_second_in) from ‹x1 ↓⇧^{*}b› obtain w1 where "x1 →⇧^{*}w1" and "b →⇧^{*}w1" unfolding cs_def by auto from ‹b ↔ c› show "x1 ↓⇧^{*}c" proof assume "b → c" hence "b →⇧^{*}c" by simp from ‹cbelow_on A ord z (↔) x1 b› have "ord b z" by (rule cbelow_on_second_below) from IH[OF ‹b ∈ A› this] ‹b →⇧^{*}c› ‹b →⇧^{*}w1› have "c ↓⇧^{*}w1" by simp then obtain w2 where "c →⇧^{*}w2" and "w1 →⇧^{*}w2" unfolding cs_def by auto show ?thesis unfolding cs_def proof from rtranclp_trans[OF ‹x1 →⇧^{*}w1› ‹w1 →⇧^{*}w2›] ‹c →⇧^{*}w2› show "x1 →⇧^{*}w2 ∧ c →⇧^{*}w2" by simp qed next assume "c → b" hence "c →⇧^{*}b" by simp show ?thesis unfolding cs_def proof from rtranclp_trans[OF ‹c →⇧^{*}b› ‹b →⇧^{*}w1›] ‹x1 →⇧^{*}w1› show "x1 →⇧^{*}w1 ∧ c →⇧^{*}w1" by simp qed qed qed then obtain w1 where "x1 →⇧^{*}w1" and "y1 →⇧^{*}w1" unfolding cs_def by auto from IH[OF ‹x1 ∈ A› relation_refines[OF ‹z → x1›]] ‹x1 →⇧^{*}x› ‹x1 →⇧^{*}w1› have "x ↓⇧^{*}w1" by simp then obtain v where "x →⇧^{*}v" and "w1 →⇧^{*}v" unfolding cs_def by auto from IH[OF ‹y1 ∈ A› relation_refines[OF ‹z → y1›]] rtranclp_trans[OF ‹y1 →⇧^{*}w1› ‹w1 →⇧^{*}v›] ‹y1 →⇧^{*}y› have "v ↓⇧^{*}y" by simp then obtain w where "v →⇧^{*}w" and "y →⇧^{*}w" unfolding cs_def by auto show ?thesis unfolding cs_def proof from rtranclp_trans[OF ‹x →⇧^{*}v› ‹v →⇧^{*}w›] ‹y →⇧^{*}w› show "x →⇧^{*}w ∧ y →⇧^{*}w" by simp qed qed qed qed qed end (* relation_order *) theorem loc_connectivity_equiv_ChurchRosser: assumes "relation_order r ord UNIV" shows "relation.is_ChurchRosser r = is_loc_connective_on UNIV ord r" proof assume "relation.is_ChurchRosser r" show "is_loc_connective_on UNIV ord r" unfolding is_loc_connective_on_def proof (intro ballI allI impI) fix a b1 b2 assume "r a b1 ∧ r a b2" hence "r a b1" and "r a b2" by simp_all hence "r⇧^{*}⇧^{*}a b1" and "r⇧^{*}⇧^{*}a b2" by simp_all from relation.rtc_implies_srtc[OF ‹r⇧^{*}⇧^{*}a b1›] have "relation.srtc r b1 a" by (rule relation.srtc_symmetric) from relation.srtc_transitive[OF this relation.rtc_implies_srtc[OF ‹r⇧^{*}⇧^{*}a b2›]] have "relation.srtc r b1 b2" . with ‹relation.is_ChurchRosser r› have "relation.cs r b1 b2" by (simp add: relation.is_ChurchRosser_def) from relation_order.cs_implies_cbelow_on[OF assms relation.dw_closed_UNIV this] relation_order.relation_refines[OF assms, of a] ‹r a b1› ‹r a b2› show "cbelow_on UNIV ord a (relation.sc r) b1 b2" by simp qed next assume "is_loc_connective_on UNIV ord r" from assms this relation.dw_closed_UNIV have "relation.is_confluent_on r UNIV" by (rule relation_order.loc_connectivity_implies_confluence) hence "relation.is_confluent r" by (simp only: relation.is_confluent_def) thus "relation.is_ChurchRosser r" by (simp add: relation.confluence_equiv_ChurchRosser) qed end

# Theory Reduction

(* Author: Fabian Immler, Alexander Maletzky *) section ‹Polynomial Reduction› theory Reduction imports "Polynomials.MPoly_Type_Class_Ordered" Confluence begin text ‹This theory formalizes the concept of @{emph ‹reduction›} of polynomials by polynomials.› context ordered_term begin definition red_single :: "('t ⇒⇩_{0}'b::field) ⇒ ('t ⇒⇩_{0}'b) ⇒ ('t ⇒⇩_{0}'b) ⇒ 'a ⇒ bool" where "red_single p q f t ⟷ (f ≠ 0 ∧ lookup p (t ⊕ lt f) ≠ 0 ∧ q = p - monom_mult ((lookup p (t ⊕ lt f)) / lc f) t f)" definition red :: "('t ⇒⇩_{0}'b::field) set ⇒ ('t ⇒⇩_{0}'b) ⇒ ('t ⇒⇩_{0}'b) ⇒ bool" where "red F p q ⟷ (∃f∈F. ∃t. red_single p q f t)" definition is_red :: "('t ⇒⇩_{0}'b::field) set ⇒ ('t ⇒⇩_{0}'b) ⇒ bool" where "is_red F a ⟷ ¬ relation.is_final (red F) a" subsection ‹Basic Properties of Reduction› lemma red_setI: assumes "f ∈ F" and a: "red_single p q f t" shows "red F p q" unfolding red_def proof from ‹f ∈ F› show "f ∈ F" . next from a show "∃t. red_single p q f t" .. qed lemma red_setE: assumes "red F p q" obtains f and t where "f ∈ F" and "red_single p q f t" proof - from assms obtain f where "f ∈ F" and t: "∃t. red_single p q f t" unfolding red_def by auto from t obtain t where "red_single p q f t" .. from ‹f ∈ F› this show "?thesis" .. qed lemma red_empty: "¬ red {} p q" by (rule, elim red_setE, simp) lemma red_singleton_zero: "¬ red {0} p q" by (rule, elim red_setE, simp add: red_single_def) lemma red_union: "red (F ∪ G) p q = (red F p q ∨ red G p q)" proof assume "red (F ∪ G) p q" from red_setE[OF this] obtain f t where "f ∈ F ∪ G" and r: "red_single p q f t" . from ‹f ∈ F ∪ G› have "f ∈ F ∨ f ∈ G" by simp thus "red F p q ∨ red G p q" proof assume "f ∈ F" show ?thesis by (intro disjI1, rule red_setI[OF ‹f ∈ F› r]) next assume "f ∈ G" show ?thesis by (intro disjI2, rule red_setI[OF ‹f ∈ G› r]) qed next assume "red F p q ∨ red G p q" thus "red (F ∪ G) p q" proof assume "red F p q" from red_setE[OF this] obtain f t where "f ∈ F" and "red_single p q f t" . show ?thesis by (intro red_setI[of f _ _ _ t], rule UnI1, rule ‹f ∈ F›, fact) next assume "red G p q" from red_setE[OF this] obtain f t where "f ∈ G" and "red_single p q f t" . show ?thesis by (intro red_setI[of f _ _ _ t], rule UnI2, rule ‹f ∈ G›, fact) qed qed lemma red_unionI1: assumes "red F p q" shows "red (F ∪ G) p q" unfolding red_union by (rule disjI1, fact) lemma red_unionI2: assumes "red G p q" shows "red (F ∪ G) p q" unfolding red_union by (rule disjI2, fact) lemma red_subset: assumes "red G p q" and "G ⊆ F" shows "red F p q" proof - from ‹G ⊆ F› obtain H where "F = G ∪ H" by auto show ?thesis unfolding ‹F = G ∪ H› by (rule red_unionI1, fact) qed lemma red_union_singleton_zero: "red (F ∪ {0}) = red F" by (intro ext, simp only: red_union red_singleton_zero, simp) lemma red_minus_singleton_zero: "red (F - {0}) = red F" by (metis Un_Diff_cancel2 red_union_singleton_zero) lemma red_rtrancl_subset: assumes major: "(red G)⇧^{*}⇧^{*}p q" and "G ⊆ F" shows "(red F)⇧^{*}⇧^{*}p q" using major proof (induct rule: rtranclp_induct) show "(red F)⇧^{*}⇧^{*}p p" .. next fix r q assume "red G r q" and "(red F)⇧^{*}⇧^{*}p r" show "(red F)⇧^{*}⇧^{*}p q" proof show "(red F)⇧^{*}⇧^{*}p r" by fact next from red_subset[OF ‹red G r q› ‹G ⊆ F›] show "red F r q" . qed qed lemma red_singleton: "red {f} p q ⟷ (∃t. red_single p q f t)" unfolding red_def proof assume "∃f∈{f}. ∃t. red_single p q f t" from this obtain f0 where "f0 ∈ {f}" and a: "∃t. red_single p q f0 t" .. from ‹f0 ∈ {f}› have "f0 = f" by simp from this a show "∃t. red_single p q f t" by simp next assume a: "∃t. red_single p q f t" show "∃f∈{f}. ∃t. red_single p q f t" proof (rule, simp) from a show "∃t. red_single p q f t" . qed qed lemma red_single_lookup: assumes "red_single p q f t" shows "lookup q (t ⊕ lt f) = 0" using assms unfolding red_single_def proof assume "f ≠ 0" and "lookup p (t ⊕ lt f) ≠ 0 ∧ q = p - monom_mult (lookup p (t ⊕ lt f) / lc f) t f" hence "lookup p (t ⊕ lt f) ≠ 0" and q_def: "q = p - monom_mult (lookup p (t ⊕ lt f) / lc f) t f" by auto from lookup_minus[of p "monom_mult (lookup p (t ⊕ lt f) / lc f) t f" "t ⊕ lt f"] lookup_monom_mult_plus[of "lookup p (t ⊕ lt f) / lc f" t f "lt f"] lc_not_0[OF ‹f ≠ 0›] show ?thesis unfolding q_def lc_def by simp qed lemma red_single_higher: assumes "red_single p q f t" shows "higher q (t ⊕ lt f) = higher p (t ⊕ lt f)" using assms unfolding higher_eq_iff red_single_def proof (intro allI, intro impI) fix u assume a: "t ⊕ lt f ≺⇩_{t}u" and "f ≠ 0 ∧ lookup p (t ⊕ lt f) ≠ 0 ∧ q = p - monom_mult (lookup p (t ⊕ lt f) / lc f) t f" hence "f ≠ 0" and "lookup p (t ⊕ lt f) ≠ 0" and q_def: "q = p - monom_mult (lookup p (t ⊕ lt f) / lc f) t f" by simp_all from ‹lookup p (t ⊕ lt f) ≠ 0› lc_not_0[OF ‹f ≠ 0›] have c_not_0: "lookup p (t ⊕ lt f) / lc f ≠ 0" by (simp add: field_simps) from q_def lookup_minus[of p "monom_mult (lookup p (t ⊕ lt f) / lc f) t f"] have q_lookup: "⋀s. lookup q s = lookup p s - lookup (monom_mult (lookup p (t ⊕ lt f) / lc f) t f) s" by simp from a lt_monom_mult[OF c_not_0 ‹f ≠ 0›, of t] have "¬ u ≼⇩_{t}lt (monom_mult (lookup p (t ⊕ lt f) / lc f) t f)" by simp with lt_max[of "monom_mult (lookup p (t ⊕ lt f) / lc f) t f" u] have "lookup (monom_mult (lookup p (t ⊕ lt f) / lc f) t f) u = 0" by auto thus "lookup q u = lookup p u" using q_lookup[of u] by simp qed lemma red_single_ord: assumes "red_single p q f t" shows "q ≺⇩_{p}p" unfolding ord_strict_higher proof (intro exI, intro conjI) from red_single_lookup[OF assms] show "lookup q (t ⊕ lt f) = 0" . next from assms show "lookup p (t ⊕ lt f) ≠ 0" unfolding red_single_def by simp next from red_single_higher[OF assms] show "higher q (t ⊕ lt f) = higher p (t ⊕ lt f)" . qed lemma red_single_nonzero1: assumes "red_single p q f t" shows "p ≠ 0" proof assume "p = 0" from this red_single_ord[OF assms] ord_p_zero_min[of q] show False by simp qed lemma red_single_nonzero2: assumes "red_single p q f t" shows "f ≠ 0" proof assume "f = 0" from assms monom_mult_zero_right have "f ≠ 0" by (simp add: red_single_def) from this ‹f = 0› show False by simp qed lemma red_single_self: assumes "p ≠ 0" shows "red_single p 0 p 0" proof - from lc_not_0[OF assms] have lc: "lc p ≠ 0" . show ?thesis unfolding red_single_def proof (intro conjI) show "p ≠ 0" by fact next from lc show "lookup p (0 ⊕ lt p) ≠ 0" unfolding lc_def by (simp add: term_simps) next from lc have "(lookup p (0 ⊕ lt p)) / lc p = 1" unfolding lc_def by (simp add: term_simps) from this monom_mult_one_left[of p] show "0 = p - monom_mult (lookup p (0 ⊕ lt p) / lc p) 0 p" by simp qed qed lemma red_single_trans: assumes "red_single p p0 f t" and "lt g adds⇩_{t}lt f" and "g ≠ 0" obtains p1 where "red_single p p1 g (t + (lp f - lp g))" proof - let ?s = "t + (lp f - lp g)" let ?p = "p - monom_mult (lookup p (?s ⊕ lt g) / lc g) ?s g" have "red_single p ?p g ?s" unfolding red_single_def proof (intro conjI) from assms(2) have eq: "?s ⊕ lt g = t ⊕ lt f" using adds_term_alt splus_assoc by (auto simp: term_simps) from ‹red_single p p0 f t› have "lookup p (t ⊕ lt f) ≠ 0" unfolding red_single_def by simp thus "lookup p (?s ⊕ lt g) ≠ 0" by (simp add: eq) qed (fact, fact refl) thus ?thesis .. qed lemma red_nonzero: assumes "red F p q" shows "p ≠ 0" proof - from red_setE[OF assms] obtain f t where "red_single p q f t" . show ?thesis by (rule red_single_nonzero1, fact) qed lemma red_self: assumes "p ≠ 0" shows "red {p} p 0" unfolding red_singleton proof from red_single_self[OF assms] show "red_single p 0 p 0" . qed lemma red_ord: assumes "red F p q" shows "q ≺⇩_{p}p" proof - from red_setE[OF assms] obtain f and t where "red_single p q f t" . from red_single_ord[OF this] show "q ≺⇩_{p}p" . qed lemma red_indI1: assumes "f ∈ F" and "f ≠ 0" and "p ≠ 0" and adds: "lt f adds⇩_{t}lt p" shows "red F p (p - monom_mult (lc p / lc f) (lp p - lp f) f)" proof (intro red_setI[OF ‹f ∈ F›]) let ?s = "lp p - lp f" have c: "lookup p (?s ⊕ lt f) = lc p" unfolding lc_def by (metis add_diff_cancel_right' adds adds_termE pp_of_term_splus) show "red_single p (p - monom_mult (lc p / lc f) ?s f) f ?s" unfolding red_single_def proof (intro conjI, fact) from c lc_not_0[OF ‹p ≠ 0›] show "lookup p (?s ⊕ lt f) ≠ 0" by simp next from c show "p - monom_mult (lc p / lc f) ?s f = p - monom_mult (lookup p (?s ⊕ lt f) / lc f) ?s f" by simp qed qed lemma red_indI2: assumes "p ≠ 0" and r: "red F (tail p) q" shows "red F p (q + monomial (lc p) (lt p))" proof - from red_setE[OF r] obtain f t where "f ∈ F" and rs: "red_single (tail p) q f t" by auto from rs have "f ≠ 0" and ct: "lookup (tail p) (t ⊕ lt f) ≠ 0" and q: "q = tail p - monom_mult (lookup (tail p) (t ⊕ lt f) / lc f) t f" unfolding red_single_def by simp_all from ct lookup_tail[of p "t ⊕ lt f"] have "t ⊕ lt f ≺⇩_{t}lt p" by (auto split: if_splits) hence c: "lookup (tail p) (t ⊕ lt f) = lookup p (t ⊕ lt f)" using lookup_tail[of p] by simp show ?thesis proof (intro red_setI[OF ‹f ∈ F›]) show "red_single p (q + Poly_Mapping.single (lt p) (lc p)) f t" unfolding red_single_def proof (intro conjI, fact) from ct c show "lookup p (t ⊕ lt f) ≠ 0" by simp next from q have "q + monomial (lc p) (lt p) = (monomial (lc p) (lt p) + tail p) - monom_mult (lookup (tail p) (t ⊕ lt f) / lc f) t f" by simp also have "… = p - monom_mult (lookup (tail p) (t ⊕ lt f) / lc f) t f" using leading_monomial_tail[of p] by auto finally show "q + monomial (lc p) (lt p) = p - monom_mult (lookup p (t ⊕ lt f) / lc f) t f" by (simp only: c) qed qed qed lemma red_indE: assumes "red F p q" shows "(∃f∈F. f ≠ 0 ∧ lt f adds⇩_{t}lt p ∧ (q = p - monom_mult (lc p / lc f) (lp p - lp f) f)) ∨ red F (tail p) (q - monomial (lc p) (lt p))" proof - from red_nonzero[OF assms] have "p ≠ 0" . from red_setE[OF assms] obtain f t where "f ∈ F" and rs: "red_single p q f t" by auto from rs have "f ≠ 0" and cn0: "lookup p (t ⊕ lt f) ≠ 0" and q: "q = p - monom_mult ((lookup p (t ⊕ lt f)) / lc f) t f" unfolding red_single_def by simp_all show ?thesis proof (cases "lt p = t ⊕ lt f") case True hence "lt f adds⇩_{t}lt p" by (simp add: term_simps) from True have eq1: "lp p - lp f = t" by (simp add: term_simps) from True have eq2: "lc p = lookup p (t ⊕ lt f)" unfolding lc_def by simp show ?thesis proof (intro disjI1, rule bexI[of _ f], intro conjI, fact+) from q eq1 eq2 show "q = p - monom_mult (lc p / lc f) (lp p - lp f) f" by simp qed (fact) next case False from this lookup_tail_2[of p "t ⊕ lt f"] have ct: "lookup (tail p) (t ⊕ lt f) = lookup p (t ⊕ lt f)" by simp show ?thesis proof (intro disjI2, intro red_setI[of f], fact) show "red_single (tail p) (q - monomial (lc p) (lt p)) f t" unfolding red_single_def proof (intro conjI, fact) from cn0 ct show "lookup (tail p) (t ⊕ lt f) ≠ 0" by simp next from leading_monomial_tail[of p] have "p - monomial (lc p) (lt p) = (monomial (lc p) (lt p) + tail p) - monomial (lc p) (lt p)" by simp also have "… = tail p" by simp finally have eq: "p - monomial (lc p) (lt p) = tail p" . from q have "q - monomial (lc p) (lt p) = (p - monomial (lc p) (lt p)) - monom_mult ((lookup p (t ⊕ lt f)) / lc f) t f" by simp also from eq have "… = tail p - monom_mult ((lookup p (t ⊕ lt f)) / lc f) t f" by simp finally show "q - monomial (lc p) (lt p) = tail p - monom_mult (lookup (tail p) (t ⊕ lt f) / lc f) t f" using ct by simp qed qed qed qed lemma is_redI: assumes "red F a b" shows "is_red F a" unfolding is_red_def relation.is_final_def by (simp, intro exI[of _ b], fact) lemma is_redE: assumes "is_red F a" obtains b where "red F a b" using assms unfolding is_red_def relation.is_final_def proof simp assume r: "⋀b. red F a b ⟹ thesis" and b: "∃x. red F a x" from b obtain b where "red F a b" .. show thesis by (rule r[of b], fact) qed lemma is_red_alt: shows "is_red F a ⟷ (∃b. red F a b)" proof assume "is_red F a" from is_redE[OF this] obtain b where "red F a b" . show "∃b. red F a b" by (intro exI[of _ b], fact) next assume "∃b. red F a b" from this obtain b where "red F a b" .. show "is_red F a" by (rule is_redI, fact) qed lemma is_red_singletonI: assumes "is_red F q" obtains p where "p ∈ F" and "is_red {p} q" proof - from assms obtain q0 where "red F q q0" unfolding is_red_alt .. from this red_def[of F q q0] obtain p where "p ∈ F" and t: "∃t. red_single q q0 p t" by auto have "is_red {p} q" unfolding is_red_alt proof from red_singleton[of p q q0] t show "red {p} q q0" by simp qed from ‹p ∈ F› this show ?thesis .. qed lemma is_red_singletonD: assumes "is_red {p} q" and "p ∈ F" shows "is_red F q" proof - from assms(1) obtain q0 where "red {p} q q0" unfolding is_red_alt .. from red_singleton[of p q q0] this have "∃t. red_single q q0 p t" .. from this obtain t where "red_single q q0 p t" .. show ?thesis unfolding is_red_alt by (intro exI[of _ q0], intro red_setI[OF assms(2), of q q0 t], fact) qed lemma is_red_singleton_trans: assumes "is_red {f} p" and "lt g adds⇩_{t}lt f" and "g ≠ 0" shows "is_red {g} p" proof - from ‹is_red {f} p› obtain q where "red {f} p q" unfolding is_red_alt .. from this red_singleton[of f p q] obtain t where "red_single p q f t" by auto from red_single_trans[OF this assms(2, 3)] obtain q0 where "red_single p q0 g (t + (lp f - lp g))" . show ?thesis proof (rule is_redI[of "{g}" p q0]) show "red {g} p q0" unfolding red_def by (intro bexI[of _ g], intro exI[of _ "t + (lp f - lp g)"], fact, simp) qed qed lemma is_red_singleton_not_0: assumes "is_red {f} p" shows "f ≠ 0" using assms unfolding is_red_alt proof fix q assume "red {f} p q" from this red_singleton[of f p q] obtain t where "red_single p q f t" by auto thus ?thesis unfolding red_single_def .. qed lemma irred_0: shows "¬ is_red F 0" proof (rule, rule is_redE) fix b assume "red F 0 b" from ord_p_zero_min[of b] red_ord[OF this] show False by simp qed lemma is_red_indI1: assumes "f ∈ F" and "f ≠ 0" and "p ≠ 0" and "lt f adds⇩_{t}lt p" shows "is_red F p" by (intro is_redI, rule red_indI1[OF assms]) lemma is_red_indI2: assumes "p ≠ 0" and "is_red F (tail p)" shows "is_red F p" proof - from is_redE[OF ‹is_red F (tail p)›] obtain q where "red F (tail p) q" . show ?thesis by (intro is_redI, rule red_indI2[OF ‹p ≠ 0›], fact) qed lemma is_red_indE: assumes "is_red F p" shows "(∃f∈F. f ≠ 0 ∧ lt f adds⇩_{t}lt p) ∨ is_red F (tail p)" proof - from is_redE[OF assms] obtain q where "red F p q" . from red_indE[OF this] show ?thesis proof assume "∃f∈F. f ≠ 0 ∧ lt f adds⇩_{t}lt p ∧ q = p - monom_mult (lc p / lc f) (lp p - lp f) f" from this obtain f where "f ∈ F" and "f ≠ 0" and "lt f adds⇩_{t}lt p" by auto show ?thesis by (intro disjI1, rule bexI[of _ f], intro conjI, fact+) next assume "red F (tail p) (q - monomial (lc p) (lt p))" show ?thesis by (intro disjI2, intro is_redI, fact) qed qed lemma rtrancl_0: assumes "(red F)⇧^{*}⇧^{*}0 x" shows "x = 0" proof - from irred_0[of F] have "relation.is_final (red F) 0" unfolding is_red_def by simp from relation.rtrancl_is_final[OF ‹(red F)⇧^{*}⇧^{*}0 x› this] show ?thesis by simp qed lemma red_rtrancl_ord: assumes "(red F)⇧^{*}⇧^{*}p q" shows "q ≼⇩_{p}p" using assms proof induct case base show ?case .. next case (step y z) from step(2) have "z ≺⇩_{p}y" by (rule red_ord) hence "z ≼⇩_{p}y" by simp also note step(3) finally show ?case . qed lemma components_red_subset: assumes "red F p q" shows "component_of_term ` keys q ⊆ component_of_term ` keys p ∪ component_of_term ` Keys F" proof - from assms obtain f t where "f ∈ F" and "red_single p q f t" by (rule red_setE) from this(2) have q: "q = p - monom_mult ((lookup p (t ⊕ lt f)) / lc f) t f" by (simp add: red_single_def) have "component_of_term ` keys q ⊆ component_of_term ` (keys p ∪ keys (monom_mult ((lookup p (t ⊕ lt f)) / lc f) t f))" by (rule image_mono, simp add: q keys_minus) also have "... ⊆ component_of_term ` keys p ∪ component_of_term ` Keys F" proof (simp add: image_Un, rule) fix k assume "k ∈ component_of_term ` keys (monom_mult (lookup p (t ⊕ lt f) / lc f) t f)" then obtain v where "v ∈ keys (monom_mult (lookup p (t ⊕ lt f) / lc f) t f)" and "k = component_of_term v" .. from this(1) keys_monom_mult_subset have "v ∈ (⊕) t ` keys f" .. then obtain u where "u ∈ keys f" and "v = t ⊕ u" .. have "k = component_of_term u" by (simp add: ‹k = component_of_term v› ‹v = t ⊕ u› term_simps) with ‹u ∈ keys f› have "k ∈ component_of_term ` keys f" by fastforce also have "... ⊆ component_of_term ` Keys F" by (rule image_mono, rule keys_subset_Keys, fact) finally show "k ∈ component_of_term ` keys p ∪ component_of_term ` Keys F" by simp qed finally show ?thesis . qed corollary components_red_rtrancl_subset: assumes "(red F)⇧^{*}⇧^{*}p q" shows "component_of_term ` keys q ⊆ component_of_term ` keys p ∪ component_of_term ` Keys F" using assms proof (induct) case base show ?case by simp next case (step q r) from step(2) have "component_of_term ` keys r ⊆ component_of_term ` keys q ∪ component_of_term ` Keys F" by (rule components_red_subset) also from step(3) have "... ⊆ component_of_term ` keys p ∪ component_of_term ` Keys F" by blast finally show ?case . qed subsection ‹Reducibility and Addition \& Multiplication› lemma red_single_monom_mult: assumes "red_single p q f t" and "c ≠ 0" shows "red_single (monom_mult c s p) (monom_mult c s q) f (s + t)" proof - from assms(1) have "f ≠ 0" and "lookup p (t ⊕ lt f) ≠ 0" and q_def: "q = p - monom_mult ((lookup p (t ⊕ lt f)) / lc f) t f" unfolding red_single_def by auto have assoc: "(s + t) ⊕ lt f = s ⊕ (t ⊕ lt f)" by (simp add: ac_simps) have g2: "lookup (monom_mult c s p) ((s + t) ⊕ lt f) ≠ 0" proof assume "lookup (monom_mult c s p) ((s + t) ⊕ lt f) = 0" hence "c * lookup p (t ⊕ lt f) = 0" using assoc by (simp add: lookup_monom_mult_plus) thus False using ‹c ≠ 0› ‹lookup p (t ⊕ lt f) ≠ 0› by simp qed have g3: "monom_mult c s q = (monom_mult c s p) - monom_mult ((lookup (monom_mult c s p) ((s + t) ⊕ lt f)) / lc f) (s + t) f" proof - from q_def monom_mult_dist_right_minus[of c s p] have "monom_mult c s q = monom_mult c s p - monom_mult c s (monom_mult (lookup p (t ⊕ lt f) / lc f) t f)" by simp also from monom_mult_assoc[of c s "lookup p (t ⊕ lt f) / lc f" t f] assoc have "monom_mult c s (monom_mult (lookup p (t ⊕ lt f) / lc f) t f) = monom_mult ((lookup (monom_mult c s p) ((s + t) ⊕ lt f)) / lc f) (s + t) f" by (simp add: lookup_monom_mult_plus) finally show ?thesis . qed from ‹f ≠ 0› g2 g3 show ?thesis unfolding red_single_def by auto qed lemma red_single_plus_1: assumes "red_single p q f t" and "t ⊕ lt f ∉ keys (p + r)" shows "red_single (q + r) (p + r) f t" proof - from assms have "f ≠ 0" and "lookup p (t ⊕ lt f) ≠ 0" and q: "q = p - monom_mult ((lookup p (t ⊕ lt f)) / lc f) t f" by (simp_all add: red_single_def) from assms(1) have cq_0: "lookup q (t ⊕ lt f) = 0" by (rule red_single_lookup) from assms(2) have "lookup (p + r) (t ⊕ lt f) = 0" by (simp add: in_keys_iff) with neg_eq_iff_add_eq_0[of "lookup p (t ⊕ lt f)" "lookup r (t ⊕ lt f)"] have cr: "lookup r (t ⊕ lt f) = - (lookup p (t ⊕ lt f))" by (simp add: lookup_add) hence cr_not_0: "lookup r (t ⊕ lt f) ≠ 0" using ‹lookup p (t ⊕ lt f) ≠ 0› by simp from ‹f ≠ 0› show ?thesis unfolding red_single_def proof (intro conjI) from cr_not_0 show "lookup (q + r) (t ⊕ lt f) ≠ 0" by (simp add: lookup_add cq_0) next from lc_not_0[OF ‹f ≠ 0›] have "monom_mult ((lookup (q + r) (t ⊕ lt f)) / lc f) t f = monom_mult ((lookup r (t ⊕ lt f)) / lc f) t f" by (simp add: field_simps lookup_add cq_0) thus "p + r = q + r - monom_mult (lookup (q + r) (t ⊕ lt f) / lc f) t f" by (simp add: cr q monom_mult_uminus_left) qed qed lemma red_single_plus_2: assumes "red_single p q f t" and "t ⊕ lt f ∉ keys (q + r)" shows "red_single (p + r) (q + r) f t" proof - from assms have "f ≠ 0" and cp: "lookup p (t ⊕ lt f) ≠ 0" and q: "q = p - monom_mult ((lookup p (t ⊕ lt f)) / lc f) t f" by (simp_all add: red_single_def) from assms(1) have cq_0: "lookup q (t ⊕ lt f) = 0" by (rule red_single_lookup) with assms(2) have cr_0: "lookup r (t ⊕ lt f) = 0" by (simp add: lookup_add in_keys_iff) from ‹f ≠ 0› show ?thesis unfolding red_single_def proof (intro conjI) from cp show "lookup (p + r) (t ⊕ lt f) ≠ 0" by (simp add: lookup_add cr_0) next show "q + r = p + r - monom_mult (lookup (p + r) (t ⊕ lt f) / lc f) t f" by (simp add: cr_0 q lookup_add) qed qed lemma red_single_plus_3: assumes "red_single p q f t" and "t ⊕ lt f ∈ keys (p + r)" and "t ⊕ lt f ∈ keys (q + r)" shows "∃s. red_single (p + r) s f t ∧ red_single (q + r) s f t" proof - let ?t = "t ⊕ lt f" from assms have "f ≠ 0" and "lookup p ?t ≠ 0" and q: "q = p - monom_mult ((lookup p ?t) / lc f) t f" by (simp_all add: red_single_def) from assms(2) have cpr: "lookup (p + r) ?t ≠ 0" by (simp add: in_keys_iff) from assms(3) have cqr: "lookup (q + r) ?t ≠ 0" by (simp add: in_keys_iff) from assms(1) have cq_0: "lookup q ?t = 0" by (rule red_single_lookup) let ?s = "(p + r) - monom_mult ((lookup (p + r) ?t) / lc f) t f" from ‹f ≠ 0› cpr have "red_single (p + r) ?s f t" by (simp add: red_single_def) moreover from ‹f ≠ 0› have "red_single (q + r) ?s f t" unfolding red_single_def proof (intro conjI) from cqr show "lookup (q + r) ?t ≠ 0" . next from lc_not_0[OF ‹f ≠ 0›] monom_mult_dist_left[of "(lookup p ?t) / lc f" "(lookup r ?t) / lc f" t f] have "monom_mult ((lookup (p + r) ?t) / lc f) t f = (monom_mult ((lookup p ?t) / lc f) t f) + (monom_mult ((lookup r ?t) / lc f) t f)" by (simp add: field_simps lookup_add) moreover from lc_not_0[OF ‹f ≠ 0›] monom_mult_dist_left[of "(lookup q ?t) / lc f" "(lookup r ?t) / lc f" t f] have "monom_mult ((lookup (q + r) ?t) / lc f) t f = monom_mult ((lookup r ?t) / lc f) t f" by (simp add: field_simps lookup_add cq_0) ultimately show "p + r - monom_mult (lookup (p + r) ?t / lc f) t f = q + r - monom_mult (lookup (q + r) ?t / lc f) t f" by (simp add: q) qed ultimately show ?thesis by auto qed lemma red_single_plus: assumes "red_single p q f t" shows "red_single (p + r) (q + r) f t ∨ red_single (q + r) (p + r) f t ∨ (∃s. red_single (p + r) s f t ∧ red_single (q + r) s f t)" (is "?A ∨ ?B ∨ ?C") proof (cases "t ⊕ lt f ∈ keys (p + r)") case True show ?thesis proof (cases "t ⊕ lt f ∈ keys (q + r)") case True with assms ‹t ⊕ lt f ∈ keys (p + r)› have ?C by (rule red_single_plus_3) thus ?thesis by simp next case False with assms have ?A by (rule red_single_plus_2) thus ?thesis .. qed next case False with assms have ?B by (rule red_single_plus_1) thus ?thesis by simp qed lemma red_single_diff: assumes "red_single (p - q) r f t" shows "red_single p (r + q) f t ∨ red_single q (p - r) f t ∨ (∃p' q'. red_single p p' f t ∧ red_single q q' f t ∧ r = p' - q')" (is "?A ∨ ?B ∨ ?C") proof - let ?s = "t ⊕ lt f" from assms have "f ≠ 0" and "lookup (p - q) ?s ≠ 0" and r: "r = p - q - monom_mult ((lookup (p - q) ?s) / lc f) t f" unfolding red_single_def by auto from this(2) have diff: "lookup p ?s ≠ lookup q ?s" by (simp add: lookup_minus) show ?thesis proof (cases "lookup p ?s = 0") case True with diff have "?s ∈ keys q" by (simp add: in_keys_iff) moreover have "lookup (p - q) ?s = - lookup q ?s" by (simp add: lookup_minus True) ultimately have ?B using ‹f ≠ 0› by (simp add: in_keys_iff red_single_def r monom_mult_uminus_left) thus ?thesis by simp next case False hence "?s ∈ keys p" by (simp add: in_keys_iff) show ?thesis proof (cases "lookup q ?s = 0") case True hence "lookup (p - q) ?s = lookup p ?s" by (simp add: lookup_minus) hence ?A using ‹f ≠ 0› ‹?s ∈ keys p› by (simp add: in_keys_iff red_single_def r monom_mult_uminus_left) thus ?thesis .. next case False hence "?s ∈ keys q" by (simp add: in_keys_iff) let ?p = "p - monom_mult ((lookup p ?s) / lc f) t f" let ?q = "q - monom_mult ((lookup q ?s) / lc f) t f" have ?C proof (intro exI conjI) from ‹f ≠ 0› ‹?s ∈ keys p› show "red_single p ?p f t" by (simp add: in_keys_iff red_single_def) next from ‹f ≠ 0› ‹?s ∈ keys q› show "red_single q ?q f t" by (simp add: in_keys_iff red_single_def) next from ‹f ≠ 0› have "lc f ≠ 0" by (rule lc_not_0) hence eq: "(lookup p ?s - lookup q ?s) / lc f = lookup p ?s / lc f - lookup q ?s / lc f" by (simp add: field_simps) show "r = ?p - ?q" by (simp add: r lookup_minus eq monom_mult_dist_left_minus) qed thus ?thesis by simp qed qed qed lemma red_monom_mult: assumes a: "red F p q" and "c ≠ 0" shows "red F (monom_mult c s p) (monom_mult c s q)" proof - from red_setE[OF a] obtain f and t where "f ∈ F" and rs: "red_single p q f t" by auto from red_single_monom_mult[OF rs ‹c ≠ 0›, of s] show ?thesis by (intro red_setI[OF ‹f ∈ F›]) qed lemma red_plus_keys_disjoint: assumes "red F p q" and "keys p ∩ keys r = {}" shows "red F (p + r) (q + r)" proof - from assms(1) obtain f t where "f ∈ F" and *: "red_single p q f t" by (rule red_setE) from this(2) have "red_single (p + r) (q + r) f t" proof (rule red_single_plus_2) from * have "lookup q (t ⊕ lt f) = 0" by (simp add: red_single_def lookup_minus lookup_monom_mult lc_def[symmetric] lc_not_0 term_simps) hence "t ⊕ lt f ∉ keys q" by (simp add: in_keys_iff) moreover have "t ⊕ lt f ∉ keys r" proof assume "t ⊕ lt f ∈ keys r" moreover from * have "t ⊕ lt f ∈ keys p" by (simp add: in_keys_iff red_single_def) ultimately have "t ⊕ lt f ∈ keys p ∩ keys r" by simp with assms(2) show False by simp qed ultimately have "t ⊕ lt f ∉ keys q ∪ keys r" by simp thus "t ⊕ lt f ∉ keys (q + r)" by (meson Poly_Mapping.keys_add subsetD) qed with ‹f ∈ F› show ?thesis by (rule red_setI) qed lemma red_plus: assumes "red F p q" obtains s where "(red F)⇧^{*}⇧^{*}(p + r) s" and "(red F)⇧^{*}⇧^{*}(q + r) s" proof - from red_setE[OF assms] obtain f and t where "f ∈ F" and rs: "red_single p q f t" by auto from red_single_plus[OF rs, of r] show ?thesis proof assume c1: "red_single (p + r) (q + r) f t" show ?thesis proof from c1 show "(red F)⇧^{*}⇧^{*}(p + r) (q + r)" by (intro r_into_rtranclp, intro red_setI[OF ‹f ∈ F›]) next show "(red F)⇧^{*}⇧^{*}(q + r) (q + r)" .. qed next assume "red_single (q + r) (p + r) f t ∨ (∃s. red_single (p + r) s f t ∧ red_single (q + r) s f t)" thus ?thesis proof assume c2: "red_single (q + r) (p + r) f t" show ?thesis proof show "(red F)⇧^{*}⇧^{*}(p + r) (p + r)" .. next from c2 show "(red F)⇧^{*}⇧^{*}(q + r) (p + r)" by (intro r_into_rtranclp, intro red_setI[OF ‹f ∈ F›]) qed next assume "∃s. red_single (p + r) s f t ∧ red_single (q + r) s f t" then obtain s where s1: "red_single (p + r) s f t" and s2: "red_single (q + r) s f t" by auto show ?thesis proof from s1 show "(red F)⇧^{*}⇧^{*}(p + r) s" by (intro r_into_rtranclp, intro red_setI[OF ‹f ∈ F›]) next from s2 show "(red F)⇧^{*}⇧^{*}(q + r) s" by (intro r_into_rtranclp, intro red_setI[OF ‹f ∈ F›]) qed qed qed qed corollary red_plus_cs: assumes "red F p q" shows "relation.cs (red F) (p + r) (q + r)" unfolding relation.cs_def proof - from assms obtain s where "(red F)⇧^{*}⇧^{*}(p + r) s" and "(red F)⇧^{*}⇧^{*}(q + r) s" by (rule red_plus) show "∃s. (red F)⇧^{*}⇧^{*}(p + r) s ∧ (red F)⇧^{*}⇧^{*}(q + r) s" by (intro exI, intro conjI, fact, fact) qed lemma red_uminus: assumes "red F p q" shows "red F (-p) (-q)" using red_monom_mult[OF assms, of "-1" 0] by (simp add: uminus_monom_mult) lemma red_diff: assumes "red F (p - q) r" obtains p' q' where "(red F)⇧^{*}⇧^{*}p p'" and "(red F)⇧^{*}⇧^{*}q q'" and "r = p' - q'" proof - from assms obtain f t where "f ∈ F" and "red_single (p - q) r f t" by (rule red_setE) from red_single_diff[OF this(2)] show ?thesis proof (elim disjE) assume "red_single p (r + q) f t" with ‹f ∈ F› have *: "red F p (r + q)" by (rule red_setI) show ?thesis proof from * show "(red F)⇧^{*}⇧^{*}p (r + q)" .. next show "(red F)⇧^{*}⇧^{*}q q" .. qed simp next assume "red_single q (p - r) f t" with ‹f ∈ F› have *: "red F q (p - r)" by (rule red_setI) show ?thesis proof show "(red F)⇧^{*}⇧^{*}p p" .. next from * show "(red F)⇧^{*}⇧^{*}q (p - r)" .. qed simp next assume "∃p' q'. red_single p p' f t ∧ red_single q q' f t ∧ r = p' - q'" then obtain p' q' where 1: "red_single p p' f t" and 2: "red_single q q' f t" and "r = p' - q'" by blast from ‹f ∈ F› 2 have "red F q q'" by (rule red_setI) from ‹f ∈ F› 1 have "red F p p'" by (rule red_setI) hence "(red F)⇧^{*}⇧^{*}p p'" .. moreover from ‹red F q q'› have "(red F)⇧^{*}⇧^{*}q q'" .. moreover note ‹r = p' - q'› ultimately show ?thesis .. qed qed lemma red_diff_rtrancl': assumes "(red F)⇧^{*}⇧^{*}(p - q) r" obtains p' q' where "(red F)⇧^{*}⇧^{*}p p'" and "(red F)⇧^{*}⇧^{*}q q'" and "r = p' - q'" using assms proof (induct arbitrary: thesis rule: rtranclp_induct) case base show ?case by (rule base, fact rtrancl_refl[to_pred], fact rtrancl_refl[to_pred], fact refl) next case (step y z) obtain p1 q1 where p1: "(red F)⇧^{*}⇧^{*}p p1" and q1: "(red F)⇧^{*}⇧^{*}q q1" and y: "y = p1 - q1" by (rule step(3)) from step(2) obtain p' q' where p': "(red F)⇧^{*}⇧^{*}p1 p'" and q': "(red F)⇧^{*}⇧^{*}q1 q'" and z: "z = p' - q'" unfolding y by (rule red_diff) show ?case proof (rule step(4)) from p1 p' show "(red F)⇧^{*}⇧^{*}p p'" by simp next from q1 q' show "(red F)⇧^{*}⇧^{*}q q'" by simp qed fact qed lemma red_diff_rtrancl: assumes "(red F)⇧^{*}⇧^{*}(p - q) 0" obtains s where "(red F)⇧^{*}⇧^{*}p s" and "(red F)⇧^{*}⇧^{*}q s" proof - from assms obtain p' q' where p': "(red F)⇧^{*}⇧^{*}p p'" and q': "(red F)⇧^{*}⇧^{*}q q'" and "0 = p' - q'" by (rule red_diff_rtrancl') from this(3) have "q' = p'" by simp from p' q' show ?thesis unfolding ‹q' = p'› .. qed corollary red_diff_rtrancl_cs: assumes "(red F)⇧^{*}⇧^{*}(p - q) 0" shows "relation.cs (red F) p q" unfolding relation.cs_def proof - from assms obtain s where "(red F)⇧^{*}⇧^{*}p s" and "(red F)⇧^{*}⇧^{*}q s" by (rule red_diff_rtrancl) show "∃s. (red F)⇧^{*}⇧^{*}p s ∧ (red F)⇧^{*}⇧^{*}q s" by (intro exI, intro conjI, fact, fact) qed subsection ‹Confluence of Reducibility› lemma confluent_distinct_aux: assumes r1: "red_single p q1 f1 t1" and r2: "red_single p q2 f2 t2" and "t1 ⊕ lt f1 ≺⇩_{t}t2 ⊕ lt f2" and "f1 ∈ F" and "f2 ∈ F" obtains s where "(red F)⇧^{*}⇧^{*}q1 s" and "(red F)⇧^{*}⇧^{*}q2 s" proof - from r1 have "f1 ≠ 0" and c1: "lookup p (t1 ⊕ lt f1) ≠ 0" and q1_def: "q1 = p - monom_mult (lookup p (t1 ⊕ lt f1) / lc f1) t1 f1" unfolding red_single_def by auto from r2 have "f2 ≠ 0" and c2: "lookup p (t2 ⊕ lt f2) ≠ 0" and q2_def: "q2 = p - monom_mult (lookup p (t2 ⊕ lt f2) / lc f2) t2 f2" unfolding red_single_def by auto from ‹t1 ⊕ lt f1 ≺⇩_{t}t2 ⊕ lt f2› have "lookup (monom_mult (lookup p (t1 ⊕ lt f1) / lc f1) t1 f1) (t2 ⊕ lt f2) = 0" by (simp add: lookup_monom_mult_eq_zero) from lookup_minus[of p _ "t2 ⊕ lt f2"] this have c: "lookup q1 (t2 ⊕ lt f2) = lookup p (t2 ⊕ lt f2)" unfolding q1_def by simp define q3 where "q3 ≡ q1 - monom_mult ((lookup q1 (t2 ⊕ lt f2)) / lc f2) t2 f2" have "red_single q1 q3 f2 t2" unfolding red_single_def proof (rule, fact, rule) from c c2 show "lookup q1 (t2 ⊕ lt f2) ≠ 0" by simp next show "q3 = q1 - monom_mult (lookup q1 (t2 ⊕ lt f2) / lc f2) t2 f2" unfolding q3_def .. qed hence "red F q1 q3" by (intro red_setI[OF ‹f2 ∈ F›]) hence q1q3: "(red F)⇧^{*}⇧^{*}q1 q3" by (intro r_into_rtranclp) from r1 have "red F p q1" by (intro red_setI[OF ‹f1 ∈ F›]) from red_plus[OF this, of "- monom_mult ((lookup p (t2 ⊕ lt f2)) / lc f2) t2 f2"] obtain s where r3: "(red F)⇧^{*}⇧^{*}(p - monom_mult (lookup p (t2 ⊕ lt f2) / lc f2) t2 f2) s" and r4: "(red F)⇧^{*}⇧^{*}(q1 - monom_mult (lookup p (t2 ⊕ lt f2) / lc f2) t2 f2) s" by auto from r3 have q2s: "(red F)⇧^{*}⇧^{*}q2 s" unfolding q2_def by simp from r4 c have q3s: "(red F)⇧^{*}⇧^{*}q3 s" unfolding q3_def by simp show ?thesis proof from rtranclp_trans[OF q1q3 q3s] show "(red F)⇧^{*}⇧^{*}q1 s" . next from q2s show "(red F)⇧^{*}⇧^{*}q2 s" . qed qed lemma confluent_distinct: assumes r1: "red_single p q1 f1 t1" and r2: "red_single p q2 f2 t2" and ne: "t1 ⊕ lt f1 ≠ t2 ⊕ lt f2" and "f1 ∈ F" and "f2 ∈ F" obtains s where "(red F)⇧^{*}⇧^{*}q1 s" and "(red F)⇧^{*}⇧^{*}q2 s" proof - from ne have "t1 ⊕ lt f1 ≺⇩_{t}t2 ⊕ lt f2 ∨ t2 ⊕ lt f2 ≺⇩_{t}t1 ⊕ lt f1" by auto thus ?thesis proof assume a1: "t1 ⊕ lt f1 ≺⇩_{t}t2 ⊕ lt f2" from confluent_distinct_aux[OF r1 r2 a1 ‹f1 ∈ F› ‹f2 ∈ F›] obtain s where "(red F)⇧^{*}⇧^{*}q1 s" and "(red F)⇧^{*}⇧^{*}q2 s" . thus ?thesis .. next assume a2: "t2 ⊕ lt f2 ≺⇩_{t}t1 ⊕ lt f1" from confluent_distinct_aux[OF r2 r1 a2 ‹f2 ∈ F› ‹f1 ∈ F›] obtain s where "(red F)⇧^{*}⇧^{*}q1 s" and "(red F)⇧^{*}⇧^{*}q2 s" . thus ?thesis .. qed qed corollary confluent_same: assumes r1: "red_single p q1 f t1" and r2: "red_single p q2 f t2" and "f ∈ F" obtains s where "(red F)⇧^{*}⇧^{*}q1 s" and "(red F)⇧^{*}⇧^{*}q2 s" proof (cases "t1 = t2") case True with r1 r2 have "q1 = q2" by (simp add: red_single_def) show ?thesis proof show "(red F)⇧^{*}⇧^{*}q1 q2" unfolding ‹q1 = q2› .. next show "(red F)⇧^{*}⇧^{*}q2 q2" .. qed next case False hence "t1 ⊕ lt f ≠ t2 ⊕ lt f" by (simp add: term_simps) from r1 r2 this ‹f ∈ F› ‹f ∈ F› obtain s where "(red F)⇧^{*}⇧^{*}q1 s" and "(red F)⇧^{*}⇧^{*}q2 s" by (rule confluent_distinct) thus ?thesis .. qed subsection ‹Reducibility and Module Membership› lemma srtc_in_pmdl: assumes "relation.srtc (red F) p q" shows "p - q ∈ pmdl F" using assms unfolding relation.srtc_def proof (induct rule: rtranclp.induct) fix p show "p - p ∈ pmdl F" by (simp add: pmdl.span_zero) next fix p r q assume pr_in: "p - r ∈ pmdl F" and red: "red F r q ∨ red F q r" from red obtain f c t where "f ∈ F" and "q = r - monom_mult c t f" proof assume "red F r q" from red_setE[OF this] obtain f t where "f ∈ F" and "red_single r q f t" . hence "q = r - monom_mult (lookup r (t ⊕ lt f) / lc f) t f" by (simp add: red_single_def) show thesis by (rule, fact, fact) next assume "red F q r" from red_setE[OF this] obtain f t where "f ∈ F" and "red_single q r f t" . hence "r = q - monom_mult (lookup q (t ⊕ lt f) / lc f) t f" by (simp add: red_single_def) hence "q = r + monom_mult (lookup q (t ⊕ lt f) / lc f) t f" by simp hence "q = r - monom_mult (-(lookup q (t ⊕ lt f) / lc f)) t f" using monom_mult_uminus_left[of _ t f] by simp show thesis by (rule, fact, fact) qed hence eq: "p - q = (p - r) + monom_mult c t f" by simp show "p - q ∈ pmdl F" unfolding eq by (rule pmdl.span_add, fact, rule monom_mult_in_pmdl, fact) qed lemma in_pmdl_srtc: assumes "p ∈ pmdl F" shows "relation.srtc (red F) p 0" using assms proof (induct p rule: pmdl_induct) show "relation.srtc (red F) 0 0" unfolding relation.srtc_def .. next fix a f c t assume a_in: "a ∈ pmdl F" and IH: "relation.srtc (red F) a 0" and "f ∈ F" show "relation.srtc (red F) (a + monom_mult c t f) 0" proof (cases "c = 0") assume "c = 0" hence "a + monom_mult c t f = a" by simp thus ?thesis using IH by simp next assume "c ≠ 0" show ?thesis proof (cases "f = 0") assume "f = 0" hence "a + monom_mult c t f = a" by simp thus ?thesis using IH by simp next assume "f ≠ 0" from lc_not_0[OF this] have "lc f ≠ 0" . have "red F (monom_mult c t f) 0" proof (intro red_setI[OF ‹f ∈ F›]) from lookup_monom_mult_plus[of c t f "lt f"] have eq: "lookup (monom_mult c t f) (t ⊕ lt f) = c * lc f" unfolding lc_def . show "red_single (monom_mult c t f) 0 f t" unfolding red_single_def eq proof (intro conjI, fact) from ‹c ≠ 0› ‹lc f ≠ 0› show "c * lc f ≠ 0" by simp next from ‹lc f ≠ 0› show "0 = monom_mult c t f - monom_mult (c * lc f / lc f) t f" by simp qed qed from red_plus[OF this, of a] obtain s where s1: "(red F)⇧^{*}⇧^{*}(monom_mult c t f + a) s" and s2: "(red F)⇧^{*}⇧^{*}(0 + a) s" . have "relation.cs (red F) (a + monom_mult c t f) a" unfolding relation.cs_def proof (intro exI[of _ s], intro conjI) from s1 show "(red F)⇧^{*}⇧^{*}(a + monom_mult c t f) s" by (simp only: add.commute) next from s2 show "(red F)⇧^{*}⇧^{*}a s" by simp qed from relation.srtc_transitive[OF relation.cs_implies_srtc[OF this] IH] show ?thesis . qed qed qed lemma red_rtranclp_diff_in_pmdl: assumes "(red F)⇧^{*}⇧^{*}p q" shows "p - q ∈ pmdl F" proof - from assms have "relation.srtc (red F) p q" by (simp add: r_into_rtranclp relation.rtc_implies_srtc) thus ?thesis by (rule srtc_in_pmdl) qed corollary red_diff_in_pmdl: assumes "red F p q" shows "p - q ∈ pmdl F" by (rule red_rtranclp_diff_in_pmdl, rule r_into_rtranclp, fact) corollary red_rtranclp_0_in_pmdl: assumes "(red F)⇧^{*}⇧^{*}p 0" shows "p ∈ pmdl F" using assms red_rtranclp_diff_in_pmdl by fastforce lemma pmdl_closed_red: assumes "pmdl B ⊆ pmdl A" and "p ∈ pmdl A" and "red B p q" shows "q ∈ pmdl A" proof - have "q - p ∈ pmdl A" proof have "p - q ∈ pmdl B" by (rule red_diff_in_pmdl, fact) hence "- (p - q) ∈ pmdl B" by (rule pmdl.span_neg) thus "q - p ∈ pmdl B" by simp qed fact from pmdl.span_add[OF this ‹p ∈ pmdl A›] show ?thesis by simp qed subsection ‹More Properties of @{const red}, @{const red_single} and @{const is_red}› lemma red_rtrancl_mult: assumes "(red F)⇧^{*}⇧^{*}p q" shows "(red F)⇧^{*}⇧^{*}(monom_mult c t p) (monom_mult c t q)" proof (cases "c = 0") case True have "(red F)⇧^{*}⇧^{*}0 0" by simp thus ?thesis by (simp only: True monom_mult_zero_left) next case False from assms show ?thesis proof (induct rule: rtranclp_induct) show "(red F)⇧^{*}⇧^{*}(monom_mult c t p) (monom_mult c t p)" by simp next fix q0 q assume "(red F)⇧^{*}⇧^{*}p q0" and "red F q0 q" and "(red F)⇧^{*}⇧^{*}(monom_mult c t p) (monom_mult c t q0)" show "(red F)⇧^{*}⇧^{*}(monom_mult c t p) (monom_mult c t q)" proof (rule rtranclp.intros(2)[OF ‹(red F)⇧^{*}⇧^{*}(monom_mult c t p) (monom_mult c t q0)›]) from red_monom_mult[OF ‹red F q0 q› False, of t] show "red F (monom_mult c t q0) (monom_mult c t q)" . qed qed qed corollary red_rtrancl_uminus: assumes "(red F)⇧^{*}⇧^{*}p q" shows "(red F)⇧^{*}⇧^{*}(-p) (-q)" using red_rtrancl_mult[OF assms, of "-1" 0] by (simp add: uminus_monom_mult) lemma red_rtrancl_diff_induct [consumes 1, case_names base step]: assumes a: "(red F)⇧^{*}⇧^{*}(p - q) r" and cases: "P p p" "!!y z. [| (red F)⇧^{*}⇧^{*}(p - q) z; red F z y; P p (q + z)|] ==> P p (q + y)" shows "P p (q + r)" using a proof (induct rule: rtranclp_induct) from cases(1) show "P p (q + (p - q))" by simp next fix y z assume "(red F)⇧^{*}⇧^{*}(p - q) z" "red F z y" "P p (q + z)" thus "P p (q + y)" using cases(2) by simp qed lemma red_rtrancl_diff_0_induct [consumes 1, case_names base step]: assumes a: "(red F)⇧^{*}⇧^{*}(p - q) 0" and base: "P p p" and ind: "⋀y z. [| (red F)⇧^{*}⇧^{*}(p - q) y; red F y z; P p (y + q)|] ==> P p (z + q)" shows "P p q" proof - from ind red_rtrancl_diff_induct[of F p q 0 P, OF a base] have "P p (0 + q)" by (simp add: ac_simps) thus ?thesis by simp qed lemma is_red_union: "is_red (A ∪ B) p ⟷ (is_red A p ∨ is_red B p)" unfolding is_red_alt red_union by auto lemma red_single_0_lt: assumes "red_single f 0 h t" shows "lt f = t ⊕ lt h" proof - from red_single_nonzero1[OF assms] have "f ≠ 0" . { assume "h ≠ 0" and neq: "lookup f (t ⊕ lt h) ≠ 0" and eq: "f = monom_mult (lookup f (t ⊕ lt h) / lc h) t h" from lc_not_0[OF ‹h ≠ 0›] have "lc h ≠ 0" . with neq have "(lookup f (t ⊕ lt h) / lc h) ≠ 0" by simp from eq lt_monom_mult[OF this ‹h ≠ 0›, of t] have "lt f = t ⊕ lt h" by simp hence "lt f = t ⊕ lt h" by (simp add: ac_simps) } with assms show ?thesis unfolding red_single_def by auto qed lemma red_single_lt_distinct_lt: assumes rs: "red_single f g h t" and "g ≠ 0" and "lt g ≠ lt f" shows "lt f = t ⊕ lt h" proof - from red_single_nonzero1[OF rs] have "f ≠ 0" . from red_single_ord[OF rs] have "g ≼⇩_{p}f" by simp from ord_p_lt[OF this] ‹lt g ≠ lt f› have "lt g ≺⇩_{t}lt f" by simp { assume "h ≠ 0" and neq: "lookup f (t ⊕ lt h) ≠ 0" and eq: "f = g + monom_mult (lookup f (t ⊕ lt h) / lc h) t h" (is "f = g + ?R") from lc_not_0[OF ‹h ≠ 0›] have "lc h ≠ 0" . with neq have "(lookup f (t ⊕ lt h) / lc h) ≠ 0" (is "?c ≠ 0") by simp from eq lt_monom_mult[OF this ‹h ≠ 0›, of t] have ltR: "lt ?R = t ⊕ lt h" by simp from monom_mult_eq_zero_iff[of ?c t h] ‹?c ≠ 0› ‹h ≠ 0› have "?R ≠ 0" by auto from lt_plus_lessE[of g] eq ‹lt g ≺⇩_{t}lt f› have "lt g ≺⇩_{t}lt ?R" by auto from lt_plus_eqI[OF this] eq ltR have "lt f = t ⊕ lt h" by (simp add: ac_simps) } with assms show ?thesis unfolding red_single_def by auto qed lemma zero_reducibility_implies_lt_divisibility': assumes "(red F)⇧^{*}⇧^{*}f 0" and "f ≠ 0" shows "∃h∈F. h ≠ 0 ∧ (lt h adds⇩_{t}lt f)" using assms proof (induct rule: converse_rtranclp_induct) case base then show ?case by simp next case (step f g) show ?case proof (cases "g = 0") case True with step.hyps have "red F f 0" by simp from red_setE[OF this] obtain h t where "h ∈ F" and rs: "red_single f 0 h t" by auto show ?thesis proof from red_single_0_lt[OF rs] have "lt h adds⇩_{t}lt f" by (simp add: term_simps) also from rs have "h ≠ 0" by (simp add: red_single_def) ultimately show "h ≠ 0 ∧ lt h adds⇩_{t}lt f" by simp qed (rule ‹h ∈ F›) next case False show ?thesis proof (cases "lt g = lt f") case True with False step.hyps show ?thesis by simp next case False from red_setE[OF ‹red F f g›] obtain h t where "h ∈ F" and rs: "red_single f g h t" by auto show ?thesis proof from red_single_lt_distinct_lt[OF rs ‹g ≠ 0› False] have "lt h adds⇩_{t}lt f" by (simp add: term_simps) also from rs have "h ≠ 0" by (simp add: red_single_def) ultimately show "h ≠ 0 ∧ lt h adds⇩_{t}lt f" by simp qed (rule ‹h ∈ F›) qed qed qed lemma zero_reducibility_implies_lt_divisibility: assumes "(red F)⇧^{*}⇧^{*}f 0" and "f ≠ 0" obtains h where "h ∈ F" and "h ≠ 0" and "lt h adds⇩_{t}lt f" using zero_reducibility_implies_lt_divisibility'[OF assms] by auto lemma is_red_addsI: assumes "f ∈ F" and "f ≠ 0" and "v ∈ keys p" and "lt f adds⇩_{t}v" shows "is_red F p" using assms proof (induction p rule: poly_mapping_tail_induct) case 0 from ‹v ∈ keys 0› show ?case by auto next case (tail p) from "tail.IH"[OF ‹f ∈ F› ‹f ≠ 0› _ ‹lt f adds⇩_{t}v›] have imp: "v ∈ keys (tail p) ⟹ is_red F (tail p)" . show ?case proof (cases "v = lt p") case True show ?thesis proof (rule is_red_indI1[OF ‹f ∈ F› ‹f ≠ 0› ‹p ≠ 0›]) from ‹lt f adds⇩_{t}v› True show "lt f adds⇩_{t}lt p" by simp qed next case False with ‹v ∈ keys p› ‹p ≠ 0› have "v ∈ keys (tail p)" by (simp add: lookup_tail_2 in_keys_iff) from is_red_indI2[OF ‹p ≠ 0› imp[OF this]] show ?thesis . qed qed lemma is_red_addsE': assumes "is_red F p" shows "∃f∈F. ∃v∈keys p. f ≠ 0 ∧ lt f adds⇩_{t}v" using assms proof (induction p rule: poly_mapping_tail_induct) case 0 with irred_0[of F] show ?case by simp next case (tail p) from is_red_indE[OF ‹is_red F p›] show ?case proof assume "∃f∈F. f ≠ 0 ∧ lt f adds⇩_{t}lt p" then obtain f where "f ∈ F" and "f ≠ 0" and "lt f adds⇩_{t}lt p" by auto show ?case proof show "∃v∈keys p. f ≠ 0 ∧ lt f adds⇩_{t}v" proof (intro bexI, intro conjI) from ‹p ≠ 0› show "lt p ∈ keys p" by (metis in_keys_iff lc_def lc_not_0) qed (rule ‹f ≠ 0›, rule ‹lt f adds⇩_{t}lt p›) qed (rule ‹f ∈ F›) next assume "is_red F (tail p)" from "tail.IH"[OF this] obtain f v where "f ∈ F" and "f ≠ 0" and v_in_keys_tail: "v ∈ keys (tail p)" and "lt f adds⇩_{t}v" by auto from "tail.hyps" v_in_keys_tail have v_in_keys: "v ∈ keys p" by (metis lookup_tail in_keys_iff) show ?case proof show "∃v∈keys p. f ≠ 0 ∧ lt f adds⇩_{t}v" by (intro bexI, intro conjI, rule ‹f ≠ 0›, rule ‹lt f adds⇩_{t}v›, rule v_in_keys) qed (rule ‹f ∈ F›) qed qed lemma is_red_addsE: assumes "is_red F p" obtains f v where "f ∈ F" and "v ∈ keys p" and "f ≠ 0" and "lt f adds⇩_{t}v" using is_red_addsE'[OF assms] by auto lemma is_red_adds_iff: shows "(is_red F p) ⟷ (∃f∈F. ∃v∈keys p. f ≠ 0 ∧ lt f adds⇩_{t}v)" using is_red_addsE' is_red_addsI by auto lemma is_red_subset: assumes red: "is_red A p" and sub: "A ⊆ B" shows "is_red B p" proof - from red obtain f v where "f ∈ A" and "v ∈ keys p" and "f ≠ 0" and "lt f adds⇩_{t}v" by (rule is_red_addsE) show ?thesis by (rule is_red_addsI, rule, fact+) qed lemma not_is_red_empty: "¬ is_red {} f" by (simp add: is_red_adds_iff) lemma red_single_mult_const: assumes "red_single p q f t" and "c ≠ 0" shows "red_single p q (monom_mult c 0 f) t" proof - let ?s = "t ⊕ lt f" let ?f = "monom_mult c 0 f" from assms(1) have "f ≠ 0" and "lookup p ?s ≠ 0" and "q = p - monom_mult ((lookup p ?s) / lc f) t f" by (simp_all add: red_single_def) from this(1) assms(2) have lt: "lt ?f = lt f" and lc: "lc ?f = c * lc f" by (simp add: lt_monom_mult term_simps, simp) show ?thesis unfolding red_single_def proof (intro conjI) from ‹f ≠ 0› assms(2) show "?f ≠ 0" by (simp add: monom_mult_eq_zero_iff) next from ‹lookup p ?s ≠ 0› show "lookup p (t ⊕ lt ?f) ≠ 0" by (simp add: lt) next show "q = p - monom_mult (lookup p (t ⊕ lt ?f) / lc ?f) t ?f" by (simp add: lt monom_mult_assoc lc assms(2), fact) qed qed lemma red_rtrancl_plus_higher: assumes "(red F)⇧^{*}⇧^{*}p q" and "⋀u v. u ∈ keys p ⟹ v ∈ keys r ⟹ u ≺⇩_{t}v" shows "(red F)⇧^{*}⇧^{*}(p + r) (q + r)" using assms(1) proof induct case base show ?case .. next case (step y z) from step(1) have "y ≼⇩_{p}p" by (rule red_rtrancl_ord) hence "lt y ≼⇩_{t}lt p" by (rule ord_p_lt) from step(2) have "red F (y + r) (z + r)" proof (rule red_plus_keys_disjoint) show "keys y ∩ keys r = {}" proof (rule ccontr) assume "keys y ∩ keys r ≠ {}" then obtain v where "v ∈ keys y" and "v ∈ keys r" by auto from this(1) have "v ≼⇩_{t}lt y" and "y ≠ 0" using lt_max by (auto simp: in_keys_iff) with ‹y ≼⇩_{p}p› have "p ≠ 0" using ord_p_zero_min[of y] by auto hence "lt p ∈ keys p" by (rule lt_in_keys) from this ‹v ∈ keys r› have "lt p ≺⇩_{t}v" by (rule assms(2)) with ‹lt y ≼⇩_{t}lt p› have "lt y ≺⇩_{t}v" by simp with ‹v ≼⇩_{t}lt y› show False by simp qed qed with step(3) show ?case .. qed lemma red_mult_scalar_leading_monomial: "(red {f})⇧^{*}⇧^{*}(p ⊙ monomial (lc f) (lt f)) (- p ⊙ tail f)" proof (cases "f = 0") case True show ?thesis by (simp add: True lc_def) next case False show ?thesis proof (induct p rule: punit.poly_mapping_tail_induct) case 0 show ?case by simp next case (tail p) from False have "lc f ≠ 0" by (rule lc_not_0) from tail(1) have "punit.lc p ≠ 0" by (rule punit.lc_not_0) let ?t = "punit.tail p ⊙ monomial (lc f) (lt f)" let ?m = "monom_mult (punit.lc p) (punit.lt p) (monomial (lc f) (lt f))" from ‹lc f ≠ 0› have kt: "keys ?t = (λt. t ⊕ lt f) ` keys (punit.tail p)" by (rule keys_mult_scalar_monomial_right) have km: "keys ?m = {punit.lt p ⊕ lt f}" by (simp add: keys_monom_mult[OF ‹punit.lc p ≠ 0›] ‹lc f ≠ 0›) from tail(2) have "(red {f})⇧^{*}⇧^{*}(?t + ?m) (- punit.tail p ⊙ tail f + ?m)" proof (rule red_rtrancl_plus_higher) fix u v assume "u ∈ keys ?t" and "v ∈ keys ?m" from this(1) obtain s where "s ∈ keys (punit.tail p)" and u: "u = s ⊕ lt f" unfolding kt .. from this(1) have "punit.tail p ≠ 0" and "s ≼ punit.lt (punit.tail p)" using punit.lt_max by (auto simp: in_keys_iff) moreover from ‹punit.tail p ≠ 0› have "punit.lt (punit.tail p) ≺ punit.lt p" by (rule punit.lt_tail) ultimately have "s ≺ punit.lt p" by simp moreover from ‹v ∈ keys ?m› have "v = punit.lt p ⊕ lt f" by (simp only: km, simp) ultimately show "u ≺⇩_{t}v" by (simp add: u splus_mono_strict_left) qed hence *: "(red {f})⇧^{*}⇧^{*}(p ⊙ monomial (lc f) (lt f)) (?m - punit.tail p ⊙ tail f)" by (simp add: punit.leading_monomial_tail[symmetric, of p] mult_scalar_monomial[symmetric] mult_scalar_distrib_right[symmetric] add.commute[of "punit.tail p"]) have "red {f} ?m (- (monomial (punit.lc p) (punit.lt p)) ⊙ tail f)" unfolding red_singleton proof show "red_single ?m (- (monomial (punit.lc p) (punit.lt p)) ⊙ tail f) f (punit.lt p)" proof (simp add: red_single_def ‹f ≠ 0› km lookup_monom_mult ‹lc f ≠ 0› ‹punit.lc p ≠ 0› term_simps, simp add: monom_mult_dist_right_minus[symmetric] mult_scalar_monomial) have "monom_mult (punit.lc p) (punit.lt p) (monomial (lc f) (lt f) - f) = - monom_mult (punit.lc p) (punit.lt p) (f - monomial (lc f) (lt f))" by (metis minus_diff_eq monom_mult_uminus_right) also have "... = - monom_mult (punit.lc p) (punit.lt p) (tail f)" by (simp only: tail_alt_2) finally show "- monom_mult (punit.lc p) (punit.lt p) (tail f) = monom_mult (punit.lc p) (punit.lt p) (monomial (lc f) (lt f) - f)" by simp qed qed hence "red {f} (?m + (- punit.tail p ⊙ tail f)) (- (monomial (punit.lc p) (punit.lt p)) ⊙ tail f + (- punit.tail p ⊙ tail f))" proof (rule red_plus_keys_disjoint) show "keys ?m ∩ keys (- punit.tail p ⊙ tail f) = {}" proof (cases "punit.tail p = 0") case True show ?thesis by (simp add: True) next case False from tail(2) have "- punit.tail p ⊙ tail f ≼⇩_{p}?t" by (rule red_rtrancl_ord) hence "lt (- punit.tail p ⊙ tail f) ≼⇩_{t}lt ?t" by (rule ord_p_lt) also from ‹lc f ≠ 0› False have "... = punit.lt (punit.tail p) ⊕ lt f" by (rule lt_mult_scalar_monomial_right) also from punit.lt_tail[OF False] have "... ≺⇩_{t}punit.lt p ⊕ lt f" by (rule splus_mono_strict_left) finally have "punit.lt p ⊕ lt f ∉ keys (- punit.tail p ⊙ tail f)" using lt_gr_keys by blast thus ?thesis by (simp add: km) qed qed hence "red {f} (?m - punit.tail p ⊙ tail f) (- (monomial (punit.lc p) (punit.lt p)) ⊙ tail f - punit.tail p ⊙ tail f)" by (simp add: term_simps) also have "... = - p ⊙ tail f" using punit.leading_monomial_tail[symmetric, of p] by (metis (mono_tags, lifting) add_uminus_conv_diff minus_add_distrib mult_scalar_distrib_right mult_scalar_minus_mult_left) finally have "red {f} (?m - punit.tail p ⊙ tail f) (- p ⊙ tail f)" . with * show ?case .. qed qed corollary red_mult_scalar_lt: assumes "f ≠ 0" shows "(red {f})⇧^{*}⇧^{*}(p ⊙ monomial c (lt f)) (monom_mult (- c / lc f) 0 (p ⊙ tail f))" proof - from assms have "lc f ≠ 0" by (rule lc_not_0) hence 1: "p ⊙ monomial c (lt f) = punit.monom_mult (c / lc f) 0 p ⊙ monomial (lc f) (lt f)" by (simp add: punit.mult_scalar_monomial[symmetric] mult.commute mult_scalar_assoc mult_scalar_monomial_monomial term_simps) have 2: "monom_mult (- c / lc f) 0 (p ⊙ tail f) = - punit.monom_mult (c / lc f) 0 p ⊙ tail f" by (simp add: times_monomial_left[symmetric] mult_scalar_assoc monom_mult_uminus_left mult_scalar_monomial) show ?thesis unfolding 1 2 by (fact red_mult_scalar_leading_monomial) qed lemma is_red_monomial_iff: "is_red F (monomial c v) ⟷ (c ≠ 0 ∧ (∃f∈F. f ≠ 0 ∧ lt f adds⇩_{t}v))" by (simp add: is_red_adds_iff) lemma is_red_monomialI: assumes "c ≠ 0" and "f ∈ F" and "f ≠ 0" and "lt f adds⇩_{t}v" shows "is_red F (monomial c v)" unfolding is_red_monomial_iff using assms by blast lemma is_red_monomialD: assumes "is_red F (monomial c v)" shows "c ≠ 0" using assms unfolding is_red_monomial_iff .. lemma is_red_monomialE: assumes "is_red F (monomial c v)" obtains f where "f ∈ F" and "f ≠ 0" and "lt f adds⇩_{t}v" using assms unfolding is_red_monomial_iff by blast lemma replace_lt_adds_stable_is_red: assumes red: "is_red F f" and "q ≠ 0" and "lt q adds⇩_{t}lt p" shows "is_red (insert q (F - {p})) f" proof - from red obtain g v where "g ∈ F" and "g ≠ 0" and "v ∈ keys f" and "lt g adds⇩_{t}v" by (rule is_red_addsE) show ?thesis proof (cases "g = p") case True show ?thesis proof (rule is_red_addsI) show "q ∈ insert q (F - {p})" by simp next have "lt q adds⇩_{t}lt p" by fact also have "... adds⇩_{t}v" using ‹lt g adds⇩_{t}v› unfolding True . finally show "lt q adds⇩_{t}v" . qed (fact+) next case False with ‹g ∈ F› have "g ∈ insert q (F - {p})" by blast from this ‹g ≠ 0› ‹v ∈ keys f› ‹lt g adds⇩_{t}v› show ?thesis by (rule is_red_addsI) qed qed lemma conversion_property: assumes "is_red {p} f" and "red {r} p q" shows "is_red {q} f ∨ is_red {r} f" proof - let ?s = "lp p - lp r" from ‹is_red {p} f› obtain v where "v ∈ keys f" and "lt p adds⇩_{t}v" and "p ≠ 0" by (rule is_red_addsE, simp) from red_indE[OF ‹red {r} p q›] have "(r ≠ 0 ∧ lt r adds⇩_{t}lt p ∧ q = p - monom_mult (lc p / lc r) ?s r) ∨ red {r} (tail p) (q - monomial (lc p) (lt p))" by simp thus ?thesis proof assume "r ≠ 0 ∧ lt r adds⇩_{t}lt p ∧ q = p - monom_mult (lc p / lc r) ?s r" hence "r ≠ 0" and "lt r adds⇩_{t}lt p" by simp_all show ?thesis by (intro disjI2, rule is_red_singleton_trans, rule ‹is_red {p} f›, fact+) next assume "red {r} (tail p) (q - monomial (lc p) (lt p))" (is "red _ ?p' ?q'") with red_ord have "?q' ≺⇩_{p}?p'" . hence "?p' ≠ 0" and assm: "(?q' = 0 ∨ ((lt ?q') ≺⇩_{t}<