# 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)"
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)"

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

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)]"
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"

lemma map_idx_append: "map_idx f (xs @ ys) n = (map_idx f xs n) @ (map_idx f ys (n + length xs))"

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"

lemma map_idx_map: "map_idx f (map g xs) n = map_idx (f ∘ g) xs n"

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)]"
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}"

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"

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"
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"
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"
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"
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"
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
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"
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
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
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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)"
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"
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)"
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"
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"
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)"
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"
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

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)"
from is_red_indI2[OF ‹p ≠ 0› imp[OF this]] show ?thesis .
qed
qed

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

assumes "is_red F p"
obtains f v where "f ∈ F" and "v ∈ keys p" and "f ≠ 0" and "lt f adds⇩t v"

shows "(is_red F p) ⟷ (∃f∈F. ∃v∈keys p. f ≠ 0 ∧ lt f adds⇩t v)"

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"

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)"
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,
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)"
also have "... = - p ⊙ tail f" using punit.leading_monomial_tail[symmetric, of p]
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)"
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"
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))"

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

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"
show ?thesis
proof (cases "g = p")
case True
show ?thesis
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"
and assm: "(?q' = 0 ∨ ((lt ?q') ≺⇩t<