Session Groebner_Bases

Theory General

section ‹General Utilities›

theory General
  imports Polynomials.Utils
begin

text ‹A couple of general-purpose functions and lemmas, mainly related to lists.›

subsection ‹Lists›

lemma distinct_reorder: "distinct (xs @ (y # ys)) = distinct (y # (xs @ ys))" by auto
    
lemma set_reorder: "set (xs @ (y # ys)) = set (y # (xs @ ys))" by simp

lemma distinctI:
  assumes "i j. i < j  i < length xs  j < length xs  xs ! i  xs ! j"
  shows "distinct xs"
  using assms
proof (induct xs)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  show ?case
  proof (simp, intro conjI, rule)
    assume "x  set xs"
    then obtain j where "j < length xs" and "x = xs ! j" by (metis in_set_conv_nth)
    hence "Suc j < length (x # xs)" by simp
    have "(x # xs) ! 0  (x # xs) ! (Suc j)" by (rule Cons(2), simp, simp, fact)
    thus False by (simp add: x = xs ! j)
  next
    show "distinct xs"
    proof (rule Cons(1))
      fix i j
      assume "i < j" and "i < length xs" and "j < length xs"
      hence "Suc i < Suc j" and "Suc i < length (x # xs)" and "Suc j < length (x # xs)" by simp_all
      hence "(x # xs) ! (Suc i)  (x # xs) ! (Suc j)" by (rule Cons(2))
      thus "xs ! i  xs ! j" by simp
    qed
  qed
qed

lemma filter_nth_pairE:
  assumes "i < j" and "i < length (filter P xs)" and "j < length (filter P xs)"
  obtains i' j' where "i' < j'" and "i' < length xs" and "j' < length xs"
    and "(filter P xs) ! i = xs ! i'" and "(filter P xs) ! j = xs ! j'"
  using assms
proof (induct xs arbitrary: i j thesis)
  case Nil
  from Nil(3) show ?case by simp
next
  case (Cons x xs)
  let ?ys = "filter P (x # xs)"
  show ?case
  proof (cases "P x")
    case True
    hence *: "?ys = x # (filter P xs)" by simp
    from i < j obtain j0 where j: "j = Suc j0" using lessE by blast
    have len_ys: "length ?ys = Suc (length (filter P xs))" and ys_j: "?ys ! j = (filter P xs) ! j0"
      by (simp only: * length_Cons, simp only: j * nth_Cons_Suc)
    from Cons(5) have "j0 < length (filter P xs)" unfolding len_ys j by auto
    show ?thesis
    proof (cases "i = 0")
      case True
      from j0 < length (filter P xs) obtain j' where "j' < length xs" and **: "(filter P xs) ! j0 = xs ! j'"
        by (metis (no_types, lifting) in_set_conv_nth mem_Collect_eq nth_mem set_filter)
      have "0 < Suc j'" by simp
      thus ?thesis
        by (rule Cons(2), simp, simp add: j' < length xs, simp only: True * nth_Cons_0,
            simp only: ys_j nth_Cons_Suc **)
    next
      case False
      then obtain i0 where i: "i = Suc i0" using lessE by blast
      have ys_i: "?ys ! i = (filter P xs) ! i0" by (simp only: i * nth_Cons_Suc)
      from Cons(3) have "i0 < j0" by (simp add: i j)
      from Cons(4) have "i0 < length (filter P xs)" unfolding len_ys i by auto
      from _ i0 < j0 this j0 < length (filter P xs) obtain i' j'
        where "i' < j'" and "i' < length xs" and "j' < length xs"
          and i': "filter P xs ! i0 = xs ! i'" and j': "filter P xs ! j0 = xs ! j'"
        by (rule Cons(1))
      from i' < j' have "Suc i' < Suc j'" by simp
      thus ?thesis
        by (rule Cons(2), simp add: i' < length xs, simp add: j' < length xs,
            simp only: ys_i nth_Cons_Suc i', simp only: ys_j nth_Cons_Suc j')
    qed
  next
    case False
    hence *: "?ys = filter P xs" by simp
    with Cons(4) Cons(5) have "i < length (filter P xs)" and "j < length (filter P xs)" by simp_all
    with _ i < j obtain i' j' where "i' < j'" and "i' < length xs" and "j' < length xs"
      and i': "filter P xs ! i = xs ! i'" and j': "filter P xs ! j = xs ! j'"
      by (rule Cons(1))
    from i' < j' have "Suc i' < Suc j'" by simp
    thus ?thesis
      by (rule Cons(2), simp add: i' < length xs, simp add: j' < length xs,
          simp only: * nth_Cons_Suc i', simp only: * nth_Cons_Suc j')
  qed
qed

lemma distinct_filterI:
  assumes "i j. i < j  i < length xs  j < length xs  P (xs ! i)  P (xs ! j)  xs ! i  xs ! j"
  shows "distinct (filter P xs)"
proof (rule distinctI)
  fix i j::nat
  assume "i < j" and "i < length (filter P xs)" and "j < length (filter P xs)"
  then obtain i' j' where "i' < j'" and "i' < length xs" and "j' < length xs"
    and i: "(filter P xs) ! i = xs ! i'" and j: "(filter P xs) ! j = xs ! j'" by (rule filter_nth_pairE)
  from i' < j' i' < length xs j' < length xs show "(filter P xs) ! i  (filter P xs) ! j" unfolding i j
  proof (rule assms)
    from i < length (filter P xs) show "P (xs ! i')" unfolding i[symmetric] using nth_mem by force
  next
    from j < length (filter P xs) show "P (xs ! j')" unfolding j[symmetric] using nth_mem by force
  qed
qed

lemma set_zip_map: "set (zip (map f xs) (map g xs)) = (λx. (f x, g x)) ` (set xs)"
proof -
  have "{(map f xs ! i, map g xs ! i) |i. i < length xs} = {(f (xs ! i), g (xs ! i)) |i. i < length xs}"
  proof (rule Collect_eqI, rule, elim exE conjE, intro exI conjI, simp add: map_nth, assumption,
      elim exE conjE, intro exI)
    fix x i
    assume "x = (f (xs ! i), g (xs ! i))" and "i < length xs"
    thus "x = (map f xs ! i, map g xs ! i)  i < length xs" by (simp add: map_nth)
  qed
  also have "... = (λx. (f x, g x)) ` {xs ! i | i. i < length xs}" by blast
  finally show "set (zip (map f xs) (map g xs)) = (λx. (f x, g x)) ` (set xs)"
    by (simp add: set_zip set_conv_nth[symmetric])
qed

lemma set_zip_map1: "set (zip (map f xs) xs) = (λx. (f x, x)) ` (set xs)"
proof -
  have "set (zip (map f xs) (map id xs)) = (λx. (f x, id x)) ` (set xs)" by (rule set_zip_map)
  thus ?thesis by simp
qed

lemma set_zip_map2: "set (zip xs (map f xs)) = (λx. (x, f x)) ` (set xs)"
proof -
  have "set (zip (map id xs) (map f xs)) = (λx. (id x, f x)) ` (set xs)" by (rule set_zip_map)
  thus ?thesis by simp
qed

lemma UN_upt: "(i{0..<length xs}. f (xs ! i)) = (xset 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 *: "(yset 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 *: "(yset xs. r a y)" and "sorted_wrt r xs"
      by (simp_all)
    from this(2) have "sorted_wrt r (insort_wrt r x xs)" by (rule Cons(1))
    with r a x * show ?thesis by (simp add: False)
  qed
qed

corollary sorted_wrt_insort_wrt:
  assumes "transp r" and "a. r a x  r x a"
  shows "sorted_wrt r (insort_wrt r x xs)  sorted_wrt r xs" (is "?l  ?r")
proof
  assume ?l
  then show ?r by (rule sorted_wrt_insort_wrt_imp_sorted_wrt)
next
  assume ?r
  with assms show ?l by (rule sorted_wrt_imp_sorted_wrt_insort_wrt)
qed

subsubsection diff_list› and insert_list›

definition diff_list :: "'a list  'a list  'a list" (infixl "--" 65)
  where "diff_list xs ys = fold removeAll ys xs"

lemma set_diff_list: "set (xs -- ys) = set xs - set ys"
  by (simp only: diff_list_def, induct ys arbitrary: xs, auto)

lemma diff_list_disjoint: "set ys  set (xs -- ys) = {}"
  unfolding set_diff_list by (rule Diff_disjoint)

lemma subset_append_diff_cancel:
  assumes "set ys  set xs"
  shows "set (ys @ (xs -- ys)) = set xs"
  by (simp only: set_append set_diff_list Un_Diff_cancel, rule Un_absorb1, fact)

definition insert_list :: "'a  'a list  'a list"
  where "insert_list x xs = (if x  set xs then xs else x # xs)"

lemma set_insert_list: "set (insert_list x xs) = insert x (set xs)"
  by (auto simp add: insert_list_def)

subsubsection remdups_wrt›

primrec remdups_wrt :: "('a  'b)  'a list  'a list" where
  remdups_wrt_base: "remdups_wrt _ [] = []" |
  remdups_wrt_rec: "remdups_wrt f (x # xs) = (if f x  f ` set xs then remdups_wrt f xs else x # remdups_wrt f xs)"
    
lemma set_remdups_wrt: "f ` set (remdups_wrt f xs) = f ` set xs"
proof (induct xs)
  case Nil
  show ?case unfolding remdups_wrt_base ..
next
  case (Cons a xs)
  show ?case unfolding remdups_wrt_rec
  proof (simp only: split: if_splits, intro conjI, intro impI)
    assume "f a  f ` set xs"
      have "f ` set (a # xs) = insert (f a) (f ` set xs)" by simp
    have "f ` set (remdups_wrt f xs) = f ` set xs" by fact
    also from f a  f ` set xs have "... = insert (f a) (f ` set xs)" by (simp add: insert_absorb)
    also have "... = f ` set (a # xs)" by simp
    finally show "f ` set (remdups_wrt f xs) = f ` set (a # xs)" .
  qed (simp add: Cons.hyps)
qed

lemma subset_remdups_wrt: "set (remdups_wrt f xs)  set xs"
  by (induct xs, auto)

lemma remdups_wrt_distinct_wrt:
  assumes "x  set (remdups_wrt f xs)" and "y  set (remdups_wrt f xs)" and "x  y"
  shows "f x  f y"
  using assms(1) assms(2)
proof (induct xs)
  case Nil
  thus ?case unfolding remdups_wrt_base by simp
next
  case (Cons a xs)
  from Cons(2) Cons(3) show ?case unfolding remdups_wrt_rec
  proof (simp only: split: if_splits)
    assume "x  set (remdups_wrt f xs)" and "y  set (remdups_wrt f xs)"
    thus "f x  f y" by (rule Cons.hyps)
  next
    assume "¬ True"
    thus "f x  f y" by simp
  next
    assume "f a  f ` set xs" and xin: "x  set (a # remdups_wrt f xs)" and yin: "y  set (a # remdups_wrt f xs)"
    from yin have y: "y = a  y  set (remdups_wrt f xs)" by simp
    from xin have "x = a  x  set (remdups_wrt f xs)" by simp
    thus "f x  f y"
    proof
      assume "x = a"
      from y show ?thesis
      proof
        assume "y = a"
        with x  y show ?thesis unfolding x = a by simp
      next
        assume "y  set (remdups_wrt f xs)"
        have "y  set xs" by (rule, fact, rule subset_remdups_wrt)
        hence "f y  f ` set xs" by simp
        with f a  f ` set xs show ?thesis unfolding x = a by auto
      qed
    next
      assume "x  set (remdups_wrt f xs)"
      from y show ?thesis
      proof
        assume "y = a"
        have "x  set xs" by (rule, fact, rule subset_remdups_wrt)
        hence "f x  f ` set xs" by simp
        with f a  f ` set xs show ?thesis unfolding y = a by auto
      next
        assume "y  set (remdups_wrt f xs)"
        with x  set (remdups_wrt f xs) show ?thesis by (rule Cons.hyps)
      qed
    qed
  qed
qed
  
lemma distinct_remdups_wrt: "distinct (remdups_wrt f xs)"
proof (induct xs)
  case Nil
  show ?case unfolding remdups_wrt_base by simp
next
  case (Cons a xs)
  show ?case unfolding remdups_wrt_rec
  proof (split if_split, intro conjI impI, rule Cons.hyps)
    assume "f a  f ` set xs"
    hence "a  set xs" by auto
    hence "a  set (remdups_wrt f xs)" using subset_remdups_wrt[of f xs] by auto
    with Cons.hyps show "distinct (a # remdups_wrt f xs)" by simp
  qed
qed

lemma map_remdups_wrt: "map f (remdups_wrt f xs) = remdups (map f xs)"
  by (induct xs, auto)

lemma remdups_wrt_append:
  "remdups_wrt f (xs @ ys) = (filter (λa. f a  f ` set ys) (remdups_wrt f xs)) @ (remdups_wrt f ys)"
  by (induct xs, auto)

subsubsection map_idx›

primrec map_idx :: "('a  nat  'b)  'a list  nat  'b list" where
  "map_idx f [] n = []"|
  "map_idx f (x # xs) n = (f x n) # (map_idx f xs (Suc n))"

lemma map_idx_eq_map2: "map_idx f xs n = map2 f xs [n..<n + length xs]"
proof (induct xs arbitrary: n)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  have eq: "[n..<n + length (x # xs)] = n # [Suc n..<Suc (n + length xs)]"
    by (metis add_Suc_right length_Cons less_add_Suc1 upt_conv_Cons)
  show ?case unfolding eq by (simp add: Cons del: upt_Suc)
qed

lemma length_map_idx [simp]: "length (map_idx f xs n) = length xs"
  by (simp add: map_idx_eq_map2)

lemma map_idx_append: "map_idx f (xs @ ys) n = (map_idx f xs n) @ (map_idx f ys (n + length xs))"
  by (simp add: map_idx_eq_map2 ab_semigroup_add_class.add_ac(1) zip_append1)

lemma map_idx_nth:
  assumes "i < length xs"
  shows "(map_idx f xs n) ! i = f (xs ! i) (n + i)"
  using assms by (simp add: map_idx_eq_map2)

lemma map_map_idx: "map f (map_idx g xs n) = map_idx (λx i. f (g x i)) xs n"
  by (auto simp add: map_idx_eq_map2)

lemma map_idx_map: "map_idx f (map g xs) n = map_idx (f  g) xs n"
  by (simp add: map_idx_eq_map2 map_zip_map)

lemma map_idx_no_idx: "map_idx (λx _. f x) xs n = map f xs"
  by (induct xs arbitrary: n, simp_all)

lemma map_idx_no_elem: "map_idx (λ_. f) xs n = map f [n..<n + length xs]"
proof (induct xs arbitrary: n)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  have eq: "[n..<n + length (x # xs)] = n # [Suc n..<Suc (n + length xs)]"
    by (metis add_Suc_right length_Cons less_add_Suc1 upt_conv_Cons)
  show ?case unfolding eq by (simp add: Cons del: upt_Suc)
qed

lemma map_idx_eq_map: "map_idx f xs n = map (λi. f (xs ! i) (i + n)) [0..<length xs]"
proof (induct xs arbitrary: n)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  have eq: "[0..<length (x # xs)] = 0 # [Suc 0..<Suc (length xs)]"
    by (metis length_Cons upt_conv_Cons zero_less_Suc)
  have "map (λi. f ((x # xs) ! i) (i + n)) [Suc 0..<Suc (length xs)] =
        map ((λi. f ((x # xs) ! i) (i + n))  Suc) [0..<length xs]"
    by (metis map_Suc_upt map_map)
  also have "... = map (λi. f (xs ! i) (Suc (i + n))) [0..<length xs]"
    by (rule map_cong, fact refl, simp)
  finally show ?case unfolding eq by (simp add: Cons del: upt_Suc)
qed

lemma set_map_idx: "set (map_idx f xs n) = (λi. f (xs ! i) (i + n)) ` {0..<length xs}"
  by (simp add: map_idx_eq_map)

subsubsection map_dup›

primrec map_dup :: "('a  'b)  ('a  'b)  'a list  'b list" where
  "map_dup _ _ [] = []"|
  "map_dup f g (x # xs) = (if x  set xs then g x else f x) # (map_dup f g xs)"

lemma length_map_dup[simp]: "length (map_dup f g xs) = length xs"
  by (induct xs, simp_all)

lemma map_dup_distinct:
  assumes "distinct xs"
  shows "map_dup f g xs = map f xs"
  using assms by (induct xs, simp_all)

lemma filter_map_dup_const:
  "filter (λx. x  c) (map_dup f (λ_. c) xs) = filter (λx. x  c) (map f (remdups xs))"
  by (induct xs, simp_all)

lemma filter_zip_map_dup_const:
  "filter (λ(a, b). a  c) (zip (map_dup f (λ_. c) xs) xs) =
    filter (λ(a, b). a  c) (zip (map f (remdups xs)) (remdups xs))"
  by (induct xs, simp_all)

subsubsection ‹Filtering Minimal Elements›

context
  fixes rel :: "'a  'a  bool"
begin

primrec filter_min_aux :: "'a list  'a list  'a list" where
  "filter_min_aux [] ys = ys"|
  "filter_min_aux (x # xs) ys =
    (if (y(set xs  set ys). rel y x) then (filter_min_aux xs ys)
    else (filter_min_aux xs (x # ys)))"

definition filter_min :: "'a list  'a list"
  where "filter_min xs = filter_min_aux xs []"

definition filter_min_append :: "'a list  'a list  'a list"
  where "filter_min_append xs ys =
                  (let P = (λzs. λx. ¬ (zset 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 *: "yset 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 "yset 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 "yset 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 "yset 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: "yset 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. ¬ (zset 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. ¬ (zset 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. ¬ (zset 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  zQ. yA. 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 "zQ. yA. 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 "zQ. y. r y z  y  Q"
  proof (intro bexI allI impI)
    fix y
    assume "r y z"
    show "y  Q"
    proof (cases "y  A")
      case True
      thus ?thesis using r y z by (rule 1)
    next
      case False
      with Q  A show ?thesis by blast
    qed
  qed fact
qed

lemma wfp_onE_min:
  assumes "wfp_on r A" and "x  Q" and "Q  A"
  obtains z where "z  Q" and "y. r y z  y  Q"
  using wfp_on_imp_minimal[OF assms(1)] assms(2, 3) by blast

lemma wfp_onI_chain: "¬ (f. i. f i  A  r (f (Suc i)) (f i))  wfp_on r A"
  by (simp add: wfp_on_def)

lemma finite_minimalE:
  assumes "finite A" and "A  {}" and "irreflp rel" and "transp rel"
  obtains a where "a  A" and "b. rel b a  b  A"
  using assms(1, 2)
proof (induct arbitrary: thesis)
  case empty
  from empty(2) show ?case by simp
next
  case (insert a A)
  show ?case
  proof (cases "A = {}")
    case True
    show ?thesis
    proof (rule insert(4))
      fix b
      assume "rel b a"
      with assms(3) show "b  insert a A" by (auto simp: True irreflp_def)
    qed simp
  next
    case False
    with insert(3) obtain z where "z  A" and *: "b. rel b z  b  A" by blast
    show ?thesis
    proof (cases "rel a z")
      case True
      show ?thesis
      proof (rule insert(4))
        fix b
        assume "rel b a"
        with assms(4) have "rel b z" using rel a z by (rule transpD)
        hence "b  A" by (rule *)
        moreover from rel b a assms(3) have "b  a" by (auto simp: irreflp_def)
        ultimately show "b  insert a A" by simp
      qed simp
    next
      case False
      show ?thesis
      proof (rule insert(4))
        fix b
        assume "rel b z"
        hence "b  A" by (rule *)
        moreover from rel b z False have "b  a" by blast
        ultimately show "b  insert a A" by simp
      next
        from z  A show "z  insert a A" by simp
      qed
    qed
  qed
qed

lemma wfp_on_finite:
  assumes "irreflp rel" and "transp rel" and "finite A"
  shows "wfp_on rel A"
proof (rule wfp_onI_min)
  fix x Q
  assume "x  Q" and "Q  A"
  from this(2) assms(3) have "finite Q" by (rule finite_subset)
  moreover from x  Q have "Q  {}" by blast
  ultimately obtain z where "z  Q" and "y. rel y z  y  Q" using assms(1, 2)
    by (rule finite_minimalE) blast
  thus "zQ. yA. 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  (aA. 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  (aA. 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 = "{bA. 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  (aA. 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 xa b)
    fix b
    assume "relbelow_on A ord z rel a b"
    hence "rel a b" and "a  A" and "b  A" and "ord a z" and "ord b z"
      by (simp_all add: relbelow_on_def)
    hence "cbelow_on A ord z rel a a" by (simp add: cbelow_on_def)
    from this rel a b b  A ord b z base[OF a  A ord a z] show "P b" by (rule ind)
  next
    fix b c
    assume IH: "(relbelow_on A ord z rel)++ a b" and "P b" and "relbelow_on A ord z rel b c"
    hence "rel b c" and "b  A" and "c  A" and "ord b z" and "ord c z"
      by (simp_all add: relbelow_on_def)
    from IH have "cbelow_on A ord z rel a b" by (simp add: cbelow_on_def cbelow_on_1_def)
    from this rel b c c  A ord c z P b show "P c" by (rule ind)
  qed
qed

lemma cbelow_on_symmetric:
  assumes main: "cbelow_on A ord z rel a b" and "symp rel"
  shows "cbelow_on A ord z rel b a"
  using main unfolding cbelow_on_def
proof
  assume a1: "a = b  b  A  ord b z"
  show "b = a  a  A  ord a z  cbelow_on_1 A ord z rel b a"
  proof
    from a1 show "b = a  a  A  ord a z" by simp
  qed
next
  assume a2: "cbelow_on_1 A ord z rel a b"
  show "b = a  a  A  ord a z  cbelow_on_1 A ord z rel b a"
  proof (rule disjI2)
    from ‹symp rel have "symp (relbelow_on A ord z rel)" unfolding symp_def
    proof (intro allI impI)
      fix x y
      assume rel_sym: "x y. rel x y  rel y x"
      assume "relbelow_on A ord z rel x y"
      hence "rel x y" and "x  A" and "y  A" and "ord x z" and "ord y z"
        by (simp_all add: relbelow_on_def)
      show "relbelow_on A ord z rel y x" unfolding relbelow_on_def
      proof (intro conjI)
        from rel_sym rel x y show "rel y x" by simp
      qed fact+
    qed
    from sym_trancl[to_pred, OF this] a2 show "cbelow_on_1 A ord z rel b a"
      by (simp add: symp_def cbelow_on_1_def)
  qed
qed

lemma cbelow_on_transitive:
  assumes "cbelow_on A ord z rel a b" and "cbelow_on A ord z rel b c"
  shows "cbelow_on A ord z rel a c"
proof (induct rule: cbelow_on_induct[OF ‹cbelow_on A ord z rel b c])
  from ‹cbelow_on A ord z rel a b show "cbelow_on A ord z rel a b" .
next
  fix c0 c
  assume "cbelow_on A ord z rel b c0" and "rel c0 c" and "c  A" and "ord c z" and "cbelow_on A ord z rel a c0"
  show "cbelow_on A ord z rel a c" by (rule, fact+)
qed

lemma cbelow_on_mono:
  assumes "cbelow_on A ord z rel a b" and "A  B"
  shows "cbelow_on B ord z rel a b"
  using assms(1)
proof (induct rule: cbelow_on_induct)
  case base
  show ?case by (simp add: cbelow_on_def, intro disjI1 conjI, rule, fact+)
next
  case (step b c)
  from step(3) assms(2) have "c  B" ..
  from step(5) this step(2) step (4) show ?case ..
qed

locale relation_order = relation +
  fixes ord::"'a  'a  bool"
  fixes A::"'a set"
  assumes trans: "ord x y  ord y z  ord x z"
  assumes wf: "wfp_on ord A"
  assumes refines: "(→)  ord¯¯"
begin

lemma relation_refines:
  assumes "a  b"
  shows "ord b a"
  using refines assms by auto

lemma relation_wf: "wfp_on (→)¯¯ A"
  using subset_refl _ wf
proof (rule wfp_on_mono)
  fix x y
  assume "(→)¯¯ x y"
  hence "y  x" by simp
  with refines have "(ord)¯¯ y x" ..
  thus "ord x y" by simp
qed

lemma rtc_implies_cbelow_on:
  assumes "dw_closed A" and main: "a * b" and "a  A" and "ord a c"
  shows "cbelow_on A ord c (↔) a b"
  using main
proof (induct rule: rtranclp_induct)
  from assms(3) assms(4) show "cbelow_on A ord c (↔) a a" by (simp add: cbelow_on_def)
next
  fix b0 b
  assume "a * b0" and "b0  b" and IH: "cbelow_on A ord c (↔) a b0"
  from assms(1) assms(3) a * b0 have "b0  A" by (rule dw_closed_rtrancl)
  from assms(1) this b0  b have "b  A" by (rule dw_closedD)
  show "cbelow_on A ord c (↔) a b"
  proof
    from b0  b show "b0  b" by simp
  next
    from relation_refines[OF b0  b] cbelow_on_second_below[OF IH] show "ord b c" by (rule trans)
  qed fact+
qed

lemma cs_implies_cbelow_on:
  assumes "dw_closed A" and "a * b" and "a  A" and "b  A" and "ord a c" and "ord b c"
  shows "cbelow_on A ord c (↔) a b"
proof -
  from a * b obtain s where "a * s" and "b * s" unfolding cs_def by auto
  have sym: "symp (↔)" unfolding symp_def
  proof (intro allI, intro impI)
    fix x y
    assume "x  y"
    thus "y  x" by auto
  qed
  from assms(1) a * s assms(3) assms(5) have "cbelow_on A ord c (↔) a s"
    by (rule rtc_implies_cbelow_on)
  also have "cbelow_on A ord c (↔) s b"
  proof (rule cbelow_on_symmetric)
    from assms(1) b * s assms(4) assms(6) show "cbelow_on A ord c (↔) b s"
      by (rule rtc_implies_cbelow_on)
  qed fact
  finally(cbelow_on_transitive) show ?thesis .
qed

text ‹The generalized Newman lemma, taken from @{cite Winkler1983}:›

lemma loc_connectivity_implies_confluence:
  assumes "is_loc_connective_on A ord (→)" and "dw_closed A"
  shows "is_confluent_on A"
  using assms(1) unfolding is_loc_connective_on_def is_confluent_on_def
proof (intro ballI allI impI)
  fix z x y::'a
  assume "aA. 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  (fF. t. red_single p q f t)"

definition is_red :: "('t 0 'b::field) set  ('t 0 'b)  bool"
  where "is_red F a  ¬ relation.is_final (red F) a"

subsection ‹Basic Properties of Reduction›

lemma red_setI:
  assumes "f  F" and a: "red_single p q f t"
  shows "red F p q"
  unfolding red_def
proof
  from f  F show "f  F" .
next
  from a show "t. red_single p q f t" ..
qed

lemma red_setE:
  assumes "red F p q"
  obtains f and t where "f  F" and "red_single p q f t"
proof -
  from assms obtain f where "f  F" and t: "t. red_single p q f t" unfolding red_def by auto
  from t obtain t where "red_single p q f t" ..
  from f  F this show "?thesis" ..
qed

lemma red_empty: "¬ red {} p q"
  by (rule, elim red_setE, simp)

lemma red_singleton_zero: "¬ red {0} p q"
  by (rule, elim red_setE, simp add: red_single_def)

lemma red_union: "red (F  G) p q = (red F p q  red G p q)"
proof
  assume "red (F  G) p q"
  from red_setE[OF this] obtain f t where "f  F  G" and r: "red_single p q f t" .
  from f  F  G have "f  F  f  G" by simp
  thus "red F p q  red G p q"
  proof
    assume "f  F" 
    show ?thesis by (intro disjI1, rule red_setI[OF f  F r])
  next
    assume "f  G" 
    show ?thesis by (intro disjI2, rule red_setI[OF f  G r])
  qed
next
  assume "red F p q  red G p q"
  thus "red (F  G) p q"
  proof
    assume "red F p q"
    from red_setE[OF this] obtain f t where "f  F" and "red_single p q f t" .
    show ?thesis by (intro red_setI[of f _ _ _ t], rule UnI1, rule f  F, fact)
  next
    assume "red G p q"
    from red_setE[OF this] obtain f t where "f  G" and "red_single p q f t" .
    show ?thesis by (intro red_setI[of f _ _ _ t], rule UnI2, rule f  G, fact)
  qed
qed

lemma red_unionI1:
  assumes "red F p q"
  shows "red (F  G) p q"
  unfolding red_union by (rule disjI1, fact)

lemma red_unionI2:
  assumes "red G p q"
  shows "red (F  G) p q"
  unfolding red_union by (rule disjI2, fact)

lemma red_subset:
  assumes "red G p q" and "G  F"
  shows "red F p q"
proof -
  from G  F obtain H where "F = G  H" by auto
  show ?thesis unfolding F = G  H by (rule red_unionI1, fact)
qed

lemma red_union_singleton_zero: "red (F  {0}) = red F"
  by (intro ext, simp only: red_union red_singleton_zero, simp)

lemma red_minus_singleton_zero: "red (F - {0}) = red F"
  by (metis Un_Diff_cancel2 red_union_singleton_zero)

lemma red_rtrancl_subset:
  assumes major: "(red G)** p q" and "G  F"
  shows "(red F)** p q"
  using major
proof (induct rule: rtranclp_induct)
  show "(red F)** p p" ..
next
  fix r q
  assume "red G r q" and "(red F)** p r"
  show "(red F)** p q"
  proof
    show "(red F)** p r" by fact
  next
    from red_subset[OF ‹red G r q G  F] show "red F r q" .
  qed
qed

lemma red_singleton: "red {f} p q  (t. red_single p q f t)"
  unfolding red_def
proof
  assume "f{f}. t. red_single p q f t"
  from this obtain f0 where "f0  {f}" and a: "t. red_single p q f0 t" ..
  from f0  {f} have "f0 = f" by simp
  from this a show "t. red_single p q f t" by simp
next
  assume a: "t. red_single p q f t"
  show "f{f}. t. red_single p q f t"
  proof (rule, simp)
    from a show "t. red_single p q f t" .
  qed
qed

lemma red_single_lookup:
  assumes "red_single p q f t"
  shows "lookup q (t  lt f) = 0"
  using assms unfolding red_single_def
proof
  assume "f  0" and "lookup p (t  lt f)  0  q = p - monom_mult (lookup p (t  lt f) / lc f) t f"
  hence "lookup p (t  lt f)  0" and q_def: "q = p - monom_mult (lookup p (t  lt f) / lc f) t f"
    by auto
  from lookup_minus[of p "monom_mult (lookup p (t  lt f) / lc f) t f" "t  lt f"]
       lookup_monom_mult_plus[of "lookup p (t  lt f) / lc f" t f "lt f"]
       lc_not_0[OF f  0]
    show ?thesis unfolding q_def lc_def by simp
qed

lemma red_single_higher:
  assumes "red_single p q f t"
  shows "higher q (t  lt f) = higher p (t  lt f)"
  using assms unfolding higher_eq_iff red_single_def
proof (intro allI, intro impI)
  fix u
  assume a: "t  lt f t u"
    and "f  0  lookup p (t  lt f)  0  q = p - monom_mult (lookup p (t  lt f) / lc f) t f"
  hence "f  0"
    and "lookup p (t  lt f)  0"
    and q_def: "q = p - monom_mult (lookup p (t  lt f) / lc f) t f"
    by simp_all
  from ‹lookup p (t  lt f)  0 lc_not_0[OF f  0] have c_not_0: "lookup p (t  lt f) / lc f  0"
    by (simp add: field_simps)
  from q_def lookup_minus[of p "monom_mult (lookup p (t  lt f) / lc f) t f"]
    have q_lookup: "s. lookup q s = lookup p s - lookup (monom_mult (lookup p (t  lt f) / lc f) t f) s"
    by simp
  from a lt_monom_mult[OF c_not_0 f  0, of t]
    have "¬ u t lt (monom_mult (lookup p (t  lt f) / lc f) t f)" by simp
  with lt_max[of "monom_mult (lookup p (t  lt f) / lc f) t f" u]
  have "lookup (monom_mult (lookup p (t  lt f) / lc f) t f) u = 0" by auto
  thus "lookup q u = lookup p u" using q_lookup[of u] by simp
qed

lemma red_single_ord:
  assumes "red_single p q f t"
  shows "q p p"
  unfolding ord_strict_higher
proof (intro exI, intro conjI)
  from red_single_lookup[OF assms] show "lookup q (t  lt f) = 0" .
next
  from assms show "lookup p (t  lt f)  0" unfolding red_single_def by simp
next
  from red_single_higher[OF assms] show "higher q (t  lt f) = higher p (t  lt f)" .
qed

lemma red_single_nonzero1:
  assumes "red_single p q f t"
  shows "p  0"
proof
  assume "p = 0"
  from this red_single_ord[OF assms] ord_p_zero_min[of q] show False by simp
qed

lemma red_single_nonzero2:
  assumes "red_single p q f t"
  shows "f  0"
proof
  assume "f = 0"
  from assms monom_mult_zero_right have "f  0" by (simp add: red_single_def)
  from this f = 0 show False by simp
qed

lemma red_single_self:
  assumes "p  0"
  shows "red_single p 0 p 0"
proof -
  from lc_not_0[OF assms] have lc: "lc p  0" .
  show ?thesis unfolding red_single_def
  proof (intro conjI)
    show "p  0" by fact
  next
    from lc show "lookup p (0  lt p)  0" unfolding lc_def by (simp add: term_simps)
  next
    from lc have "(lookup p (0  lt p)) / lc p = 1" unfolding lc_def by (simp add: term_simps)
    from this monom_mult_one_left[of p] show "0 = p - monom_mult (lookup p (0  lt p) / lc p) 0 p"
      by simp
  qed
qed

lemma red_single_trans:
  assumes "red_single p p0 f t" and "lt g addst 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 addst lt p"
  shows "red F p (p - monom_mult (lc p / lc f) (lp p - lp f) f)"
proof (intro red_setI[OF f  F])
  let ?s = "lp p - lp f"
  have c: "lookup p (?s  lt f) = lc p" unfolding lc_def
    by (metis add_diff_cancel_right' adds adds_termE pp_of_term_splus)
  show "red_single p (p - monom_mult (lc p / lc f) ?s f) f ?s" unfolding red_single_def
  proof (intro conjI, fact)
    from c lc_not_0[OF p  0] show "lookup p (?s  lt f)  0" by simp
  next
    from c show "p - monom_mult (lc p / lc f) ?s f = p - monom_mult (lookup p (?s  lt f) / lc f) ?s f"
      by simp
  qed
qed

lemma red_indI2:
  assumes "p  0" and r: "red F (tail p) q"
  shows "red F p (q + monomial (lc p) (lt p))"
proof -
  from red_setE[OF r] obtain f t where "f  F" and rs: "red_single (tail p) q f t" by auto
  from rs have "f  0" and ct: "lookup (tail p) (t  lt f)  0"
    and q: "q = tail p - monom_mult (lookup (tail p) (t  lt f) / lc f) t f"
    unfolding red_single_def by simp_all
  from ct lookup_tail[of p "t  lt f"] have "t  lt f t lt p" by (auto split: if_splits)
  hence c: "lookup (tail p) (t  lt f) = lookup p (t  lt f)" using lookup_tail[of p] by simp
  show ?thesis
  proof (intro red_setI[OF f  F])
    show "red_single p (q + Poly_Mapping.single (lt p) (lc p)) f t" unfolding red_single_def
    proof (intro conjI, fact)
      from ct c show "lookup p (t  lt f)  0" by simp
    next
      from q have "q + monomial (lc p) (lt p) =
                  (monomial (lc p) (lt p) + tail p) - monom_mult (lookup (tail p) (t  lt f) / lc f) t f"
        by simp
      also have " = p - monom_mult (lookup (tail p) (t  lt f) / lc f) t f"
        using leading_monomial_tail[of p] by auto
      finally show "q + monomial (lc p) (lt p) = p - monom_mult (lookup p (t  lt f) / lc f) t f"
        by (simp only: c)
    qed
  qed
qed

lemma red_indE:
  assumes "red F p q"
  shows "(fF. f  0  lt f addst lt p 
            (q = p - monom_mult (lc p / lc f) (lp p - lp f) f)) 
            red F (tail p) (q - monomial (lc p) (lt p))"
proof -
  from red_nonzero[OF assms] have "p  0" .
  from red_setE[OF assms] obtain f t where "f  F" and rs: "red_single p q f t" by auto
  from rs have "f  0"
    and cn0: "lookup p (t  lt f)  0"
    and q: "q = p - monom_mult ((lookup p (t  lt f)) / lc f) t f"
    unfolding red_single_def by simp_all
  show ?thesis
  proof (cases "lt p = t  lt f")
    case True
    hence "lt f addst lt p" by (simp add: term_simps)
    from True have eq1: "lp p - lp f = t" by (simp add: term_simps)
    from True have eq2: "lc p = lookup p (t  lt f)" unfolding lc_def by simp
    show ?thesis
    proof (intro disjI1, rule bexI[of _ f], intro conjI, fact+)
      from q eq1 eq2 show "q = p - monom_mult (lc p / lc f) (lp p - lp f) f"
        by simp
    qed (fact)
  next
    case False
    from this lookup_tail_2[of p "t  lt f"]
      have ct: "lookup (tail p) (t  lt f) = lookup p (t  lt f)" by simp
    show ?thesis
    proof (intro disjI2, intro red_setI[of f], fact)
      show "red_single (tail p) (q - monomial (lc p) (lt p)) f t" unfolding red_single_def
      proof (intro conjI, fact)
        from cn0 ct show "lookup (tail p) (t  lt f)  0" by simp
      next
        from leading_monomial_tail[of p]
          have "p - monomial (lc p) (lt p) = (monomial (lc p) (lt p) + tail p) - monomial (lc p) (lt p)"
          by simp
        also have " = tail p" by simp
        finally have eq: "p - monomial (lc p) (lt p) = tail p" .
        from q have "q - monomial (lc p) (lt p) =
                    (p - monomial (lc p) (lt p)) - monom_mult ((lookup p (t  lt f)) / lc f) t f" by simp
        also from eq have " = tail p - monom_mult ((lookup p (t  lt f)) / lc f) t f" by simp
        finally show "q - monomial (lc p) (lt p) = tail p - monom_mult (lookup (tail p) (t  lt f) / lc f) t f"
          using ct by simp
      qed
    qed
  qed
qed

lemma is_redI:
  assumes "red F a b"
  shows "is_red F a"
  unfolding is_red_def relation.is_final_def by (simp, intro exI[of _ b], fact)

lemma is_redE:
  assumes "is_red F a"
  obtains b where "red F a b"
  using assms unfolding is_red_def relation.is_final_def
proof simp
  assume r: "b. red F a b  thesis" and b: "x. red F a x"
  from b obtain b where "red F a b" ..
  show thesis by (rule r[of b], fact)
qed

lemma is_red_alt:
  shows "is_red F a  (b. red F a b)"
proof
  assume "is_red F a"
  from is_redE[OF this] obtain b where "red F a b" .
  show "b. red F a b" by (intro exI[of _ b], fact)
next
  assume "b. red F a b"
  from this obtain b where "red F a b" ..
  show "is_red F a" by (rule is_redI, fact)
qed

lemma is_red_singletonI:
  assumes "is_red F q"
  obtains p where "p  F" and "is_red {p} q"
proof -
  from assms obtain q0 where "red F q q0" unfolding is_red_alt ..
  from this red_def[of F q q0] obtain p where "p  F" and t: "t. red_single q q0 p t" by auto
  have "is_red {p} q" unfolding is_red_alt
  proof
    from red_singleton[of p q q0] t show "red {p} q q0" by simp
  qed
  from p  F this show ?thesis ..
qed

lemma is_red_singletonD:
  assumes "is_red {p} q" and "p  F"
  shows "is_red F q"
proof -
  from assms(1) obtain q0 where "red {p} q q0" unfolding is_red_alt ..
  from red_singleton[of p q q0] this have "t. red_single q q0 p t" ..
  from this obtain t where "red_single q q0 p t" ..
  show ?thesis unfolding is_red_alt
    by (intro exI[of _ q0], intro red_setI[OF assms(2), of q q0 t], fact)
qed

lemma is_red_singleton_trans:
  assumes "is_red {f} p" and "lt g addst 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 addst 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 "(fF. f  0  lt f addst 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 "fF. f  0  lt f addst 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 addst lt p" by auto
    show ?thesis by (intro disjI1, rule bexI[of _ f], intro conjI, fact+)
  next
    assume "red F (tail p) (q - monomial (lc p) (lt p))"
    show ?thesis by (intro disjI2, intro is_redI, fact)
  qed
qed

lemma rtrancl_0:
  assumes "(red F)** 0 x"
  shows "x = 0"
proof -
  from irred_0[of F] have "relation.is_final (red F) 0" unfolding is_red_def by simp
  from relation.rtrancl_is_final[OF (red F)** 0 x this] show ?thesis by simp
qed

lemma red_rtrancl_ord:
  assumes "(red F)** p q"
  shows "q p p"
  using assms
proof induct
  case base
  show ?case ..
next
  case (step y z)
  from step(2) have "z p y" by (rule red_ord)
  hence "z p y" by simp
  also note step(3)
  finally show ?case .
qed

lemma components_red_subset:
  assumes "red F p q"
  shows "component_of_term ` keys q  component_of_term ` keys p  component_of_term ` Keys F"
proof -
  from assms obtain f t where "f  F" and "red_single p q f t" by (rule red_setE)
  from this(2) have q: "q = p - monom_mult ((lookup p (t  lt f)) / lc f) t f"
    by (simp add: red_single_def)
  have "component_of_term ` keys q 
        component_of_term ` (keys p  keys (monom_mult ((lookup p (t  lt f)) / lc f) t f))"
    by (rule image_mono, simp add: q keys_minus)
  also have "...  component_of_term ` keys p  component_of_term ` Keys F"
  proof (simp add: image_Un, rule)
    fix k
    assume "k  component_of_term ` keys (monom_mult (lookup p (t  lt f) / lc f) t f)"
    then obtain v where "v  keys (monom_mult (lookup p (t  lt f) / lc f) t f)"
      and "k = component_of_term v" ..
    from this(1) keys_monom_mult_subset have "v  (⊕) t ` keys f" ..
    then obtain u where "u  keys f" and "v = t  u" ..
    have "k = component_of_term u" by (simp add: k = component_of_term v v = t  u term_simps)
    with u  keys f have "k  component_of_term ` keys f" by fastforce
    also have "...  component_of_term ` Keys F" by (rule image_mono, rule keys_subset_Keys, fact)
    finally show "k  component_of_term ` keys p  component_of_term ` Keys F" by simp
  qed
  finally show ?thesis .
qed

corollary components_red_rtrancl_subset:
  assumes "(red F)** p q"
  shows "component_of_term ` keys q  component_of_term ` keys p  component_of_term ` Keys F"
  using assms
proof (induct)
  case base
  show ?case by simp
next
  case (step q r)
  from step(2) have "component_of_term ` keys r  component_of_term ` keys q  component_of_term ` Keys F"
    by (rule components_red_subset)
  also from step(3) have "...  component_of_term ` keys p  component_of_term ` Keys F" by blast
  finally show ?case .
qed

subsection ‹Reducibility and Addition \& Multiplication›

lemma red_single_monom_mult:
  assumes "red_single p q f t" and "c  0"
  shows "red_single (monom_mult c s p) (monom_mult c s q) f (s + t)"
proof -
  from assms(1) have "f  0"
    and "lookup p (t  lt f)  0"
    and q_def: "q = p - monom_mult ((lookup p (t  lt f)) / lc f) t f"
    unfolding red_single_def by auto
  have assoc: "(s + t)  lt f = s  (t  lt f)" by (simp add: ac_simps)
  have g2: "lookup (monom_mult c s p) ((s + t)  lt f)  0"
  proof
    assume "lookup (monom_mult c s p) ((s + t)  lt f) = 0"
    hence "c * lookup p (t  lt f) = 0" using assoc by (simp add: lookup_monom_mult_plus)
    thus False using c  0 ‹lookup p (t  lt f)  0 by simp
  qed
  have g3: "monom_mult c s q =
    (monom_mult c s p) - monom_mult ((lookup (monom_mult c s p) ((s + t)  lt f)) / lc f) (s + t) f"
  proof -
    from q_def monom_mult_dist_right_minus[of c s p]
      have "monom_mult c s q =
            monom_mult c s p - monom_mult c s (monom_mult (lookup p (t  lt f) / lc f) t f)" by simp
    also from monom_mult_assoc[of c s "lookup p (t  lt f) / lc f" t f] assoc
      have "monom_mult c s (monom_mult (lookup p (t  lt f) / lc f) t f) =
            monom_mult ((lookup (monom_mult c s p) ((s + t)  lt f)) / lc f) (s + t) f"
        by (simp add: lookup_monom_mult_plus)
    finally show ?thesis .
  qed
  from f  0 g2 g3 show ?thesis unfolding red_single_def by auto
qed

lemma red_single_plus_1:
  assumes "red_single p q f t" and "t  lt f  keys (p + r)"
  shows "red_single (q + r) (p + r) f t"
proof -
  from assms have "f  0" and "lookup p (t  lt f)  0"
    and q: "q = p - monom_mult ((lookup p (t  lt f)) / lc f) t f"
    by (simp_all add: red_single_def)
  from assms(1) have cq_0: "lookup q (t  lt f) = 0" by (rule red_single_lookup)
  from assms(2) have "lookup (p + r) (t  lt f) = 0"
    by (simp add: in_keys_iff)
  with neg_eq_iff_add_eq_0[of "lookup p (t  lt f)" "lookup r (t  lt f)"]
    have cr: "lookup r (t  lt f) = - (lookup p (t  lt f))" by (simp add: lookup_add)
  hence cr_not_0: "lookup r (t  lt f)  0" using ‹lookup p (t  lt f)  0 by simp
  from f  0 show ?thesis unfolding red_single_def
  proof (intro conjI)
    from cr_not_0 show "lookup (q + r) (t  lt f)  0" by (simp add: lookup_add cq_0)
  next
    from lc_not_0[OF f  0]
      have "monom_mult ((lookup (q + r) (t  lt f)) / lc f) t f =
                  monom_mult ((lookup r (t  lt f)) / lc f) t f"
        by (simp add: field_simps lookup_add cq_0)
    thus "p + r = q + r - monom_mult (lookup (q + r) (t  lt f) / lc f) t f"
      by (simp add: cr q monom_mult_uminus_left)
  qed
qed

lemma red_single_plus_2:
  assumes "red_single p q f t" and "t  lt f  keys (q + r)"
  shows "red_single (p + r) (q + r) f t"
proof -
  from assms have "f  0" and cp: "lookup p (t  lt f)  0"
    and q: "q = p - monom_mult ((lookup p (t  lt f)) / lc f) t f"
    by (simp_all add: red_single_def)
  from assms(1) have cq_0: "lookup q (t  lt f) = 0" by (rule red_single_lookup)
  with assms(2) have cr_0: "lookup r (t  lt f) = 0"
    by (simp add: lookup_add in_keys_iff)
  from f  0 show ?thesis unfolding red_single_def
  proof (intro conjI)
    from cp show "lookup (p + r) (t  lt f)  0" by (simp add: lookup_add cr_0)
  next
    show "q + r = p + r - monom_mult (lookup (p + r) (t  lt f) / lc f) t f"
      by (simp add: cr_0 q lookup_add)
  qed
qed

lemma red_single_plus_3:
  assumes "red_single p q f t" and "t  lt f  keys (p + r)" and "t  lt f  keys (q + r)"
  shows "s. red_single (p + r) s f t  red_single (q + r) s f t"
proof -
  let ?t = "t  lt f"
  from assms have "f  0" and "lookup p ?t  0"
    and q: "q = p - monom_mult ((lookup p ?t) / lc f) t f"
    by (simp_all add: red_single_def)
  from assms(2) have cpr: "lookup (p + r) ?t  0" by (simp add: in_keys_iff)
  from assms(3) have cqr: "lookup (q + r) ?t  0" by (simp add: in_keys_iff)
  from assms(1) have cq_0: "lookup q ?t = 0" by (rule red_single_lookup)
  let ?s = "(p + r) - monom_mult ((lookup (p + r) ?t) / lc f) t f"
  from f  0 cpr have "red_single (p + r) ?s f t" by (simp add: red_single_def)
  moreover from f  0 have "red_single (q + r) ?s f t" unfolding red_single_def
  proof (intro conjI)
    from cqr show "lookup (q + r) ?t  0" .
  next
    from lc_not_0[OF f  0]
      monom_mult_dist_left[of "(lookup p ?t) / lc f" "(lookup r ?t) / lc f" t f]
      have "monom_mult ((lookup (p + r) ?t) / lc f) t f =
                (monom_mult ((lookup p ?t) / lc f) t f) +
                  (monom_mult ((lookup r ?t) / lc f) t f)"
        by (simp add: field_simps lookup_add)
    moreover from lc_not_0[OF f  0]
      monom_mult_dist_left[of "(lookup q ?t) / lc f" "(lookup r ?t) / lc f" t f]
      have "monom_mult ((lookup (q + r) ?t) / lc f) t f =
                monom_mult ((lookup r ?t) / lc f) t f"
        by (simp add: field_simps lookup_add cq_0)
    ultimately show "p + r - monom_mult (lookup (p + r) ?t / lc f) t f =
                     q + r - monom_mult (lookup (q + r) ?t / lc f) t f" by (simp add: q)
  qed
  ultimately show ?thesis by auto
qed

lemma red_single_plus:
  assumes "red_single p q f t"
  shows "red_single (p + r) (q + r) f t 
          red_single (q + r) (p + r) f t 
          (s. red_single (p + r) s f t  red_single (q + r) s f t)" (is "?A  ?B  ?C")
proof (cases "t  lt f  keys (p + r)")
  case True
  show ?thesis
  proof (cases "t  lt f  keys (q + r)")
    case True
    with assms t  lt f  keys (p + r) have ?C by (rule red_single_plus_3)
    thus ?thesis by simp
  next
    case False
    with assms have ?A by (rule red_single_plus_2)
    thus ?thesis ..
  qed
next
  case False
  with assms have ?B by (rule red_single_plus_1)
  thus ?thesis by simp
qed

lemma red_single_diff:
  assumes "red_single (p - q) r f t"
  shows "red_single p (r + q) f t  red_single q (p - r) f t 
          (p' q'. red_single p p' f t  red_single q q' f t  r = p' - q')" (is "?A  ?B  ?C")
proof -
  let ?s = "t  lt f"
  from assms have "f  0"
    and "lookup (p - q) ?s  0"
    and r: "r = p - q - monom_mult ((lookup (p - q) ?s) / lc f) t f"
    unfolding red_single_def by auto
  from this(2) have diff: "lookup p ?s  lookup q ?s" by (simp add: lookup_minus)
  show ?thesis
  proof (cases "lookup p ?s = 0")
    case True
    with diff have "?s  keys q" by (simp add: in_keys_iff)
    moreover have "lookup (p - q) ?s = - lookup q ?s" by (simp add: lookup_minus True)
    ultimately have ?B using f  0 by (simp add: in_keys_iff red_single_def r monom_mult_uminus_left)
    thus ?thesis by simp
  next
    case False
    hence "?s  keys p" by (simp add: in_keys_iff)
    show ?thesis
    proof (cases "lookup q ?s = 0")
      case True
      hence "lookup (p - q) ?s = lookup p ?s" by (simp add: lookup_minus)
      hence ?A using f  0 ?s  keys p by (simp add: in_keys_iff red_single_def r monom_mult_uminus_left)
      thus ?thesis ..
    next
      case False
      hence "?s  keys q" by (simp add: in_keys_iff)
      let ?p = "p - monom_mult ((lookup p ?s) / lc f) t f"
      let ?q = "q - monom_mult ((lookup q ?s) / lc f) t f"
      have ?C
      proof (intro exI conjI)
        from f  0 ?s  keys p show "red_single p ?p f t" by (simp add: in_keys_iff red_single_def)
      next
        from f  0 ?s  keys q show "red_single q ?q f t" by (simp add: in_keys_iff red_single_def)
      next
        from f  0 have "lc f  0" by (rule lc_not_0)
        hence eq: "(lookup p ?s - lookup q ?s) / lc f =
                   lookup p ?s / lc f - lookup q ?s / lc f" by (simp add: field_simps)
        show "r = ?p - ?q" by (simp add: r lookup_minus eq monom_mult_dist_left_minus)
      qed
      thus ?thesis by simp
    qed
  qed
qed

lemma red_monom_mult:
  assumes a: "red F p q" and "c  0"
  shows "red F (monom_mult c s p) (monom_mult c s q)"
proof -
  from red_setE[OF a] obtain f and t where "f  F" and rs: "red_single p q f t" by auto
  from red_single_monom_mult[OF rs c  0, of s] show ?thesis by (intro red_setI[OF f  F])
qed

lemma red_plus_keys_disjoint:
  assumes "red F p q" and "keys p  keys r = {}"
  shows "red F (p + r) (q + r)"
proof -
  from assms(1) obtain f t where "f  F" and *: "red_single p q f t" by (rule red_setE)
  from this(2) have "red_single (p + r) (q + r) f t"
  proof (rule red_single_plus_2)
    from * have "lookup q (t  lt f) = 0"
      by (simp add: red_single_def lookup_minus lookup_monom_mult lc_def[symmetric] lc_not_0 term_simps)
    hence "t  lt f  keys q" by (simp add: in_keys_iff)
    moreover have "t  lt f  keys r"
    proof
      assume "t  lt f  keys r"
      moreover from * have "t  lt f  keys p" by (simp add: in_keys_iff red_single_def)
      ultimately have "t  lt f  keys p  keys r" by simp
      with assms(2) show False by simp
    qed
    ultimately have "t  lt f  keys q  keys r" by simp
    thus "t  lt f  keys (q + r)"
      by (meson Poly_Mapping.keys_add subsetD)
  qed
  with f  F show ?thesis by (rule red_setI)
qed

lemma red_plus:
  assumes "red F p q"
  obtains s where "(red F)** (p + r) s" and "(red F)** (q + r) s"
proof -
  from red_setE[OF assms] obtain f and t where "f  F" and rs: "red_single p q f t" by auto
  from red_single_plus[OF rs, of r] show ?thesis
  proof
    assume c1: "red_single (p + r) (q + r) f t"
    show ?thesis
    proof
      from c1 show "(red F)** (p + r) (q + r)" by (intro r_into_rtranclp, intro red_setI[OF f  F])
    next
      show "(red F)** (q + r) (q + r)" ..
    qed
  next
    assume "red_single (q + r) (p + r) f t  (s. red_single (p + r) s f t  red_single (q + r) s f t)"
    thus ?thesis
    proof
      assume c2: "red_single (q + r) (p + r) f t"
      show ?thesis
      proof
        show "(red F)** (p + r) (p + r)" ..
      next
        from c2 show "(red F)** (q + r) (p + r)" by (intro r_into_rtranclp, intro red_setI[OF f  F])
      qed
    next
      assume "s. red_single (p + r) s f t  red_single (q + r) s f t"
      then obtain s where s1: "red_single (p + r) s f t" and s2: "red_single (q + r) s f t" by auto
      show ?thesis
      proof
        from s1 show "(red F)** (p + r) s" by (intro r_into_rtranclp, intro red_setI[OF f  F])
      next
        from s2 show "(red F)** (q + r) s" by (intro r_into_rtranclp, intro red_setI[OF f  F])
      qed
    qed
  qed
qed

corollary red_plus_cs:
  assumes "red F p q"
  shows "relation.cs (red F) (p + r) (q + r)"
  unfolding relation.cs_def
proof -
  from assms obtain s where "(red F)** (p + r) s" and "(red F)** (q + r) s" by (rule red_plus)
  show "s. (red F)** (p + r) s  (red F)** (q + r) s" by (intro exI, intro conjI, fact, fact)
qed

lemma red_uminus:
  assumes "red F p q"
  shows "red F (-p) (-q)"
  using red_monom_mult[OF assms, of "-1" 0] by (simp add: uminus_monom_mult)

lemma red_diff:
  assumes "red F (p - q) r"
  obtains p' q' where "(red F)** p p'" and "(red F)** q q'" and "r = p' - q'"
proof -
  from assms obtain f t where "f  F" and "red_single (p - q) r f t" by (rule red_setE)
  from red_single_diff[OF this(2)] show ?thesis
  proof (elim disjE)
    assume "red_single p (r + q) f t"
    with f  F have *: "red F p (r + q)" by (rule red_setI)
    show ?thesis
    proof
      from * show "(red F)** p (r + q)" ..
    next
      show "(red F)** q q" ..
    qed simp
  next
    assume "red_single q (p - r) f t"
    with f  F have *: "red F q (p - r)" by (rule red_setI)
    show ?thesis
    proof
      show "(red F)** p p" ..
    next
      from * show "(red F)** q (p - r)" ..
    qed simp
  next
    assume "p' q'. red_single p p' f t  red_single q q' f t  r = p' - q'"
    then obtain p' q' where 1: "red_single p p' f t" and 2: "red_single q q' f t" and "r = p' - q'"
      by blast
    from f  F 2 have "red F q q'" by (rule red_setI)
    from f  F 1 have "red F p p'" by (rule red_setI)
    hence "(red F)** p p'" ..
    moreover from ‹red F q q' have "(red F)** q q'" ..
    moreover note r = p' - q'
    ultimately show ?thesis ..
  qed
qed

lemma red_diff_rtrancl':
  assumes "(red F)** (p - q) r"
  obtains p' q' where "(red F)** p p'" and "(red F)** q q'" and "r = p' - q'"
  using assms
proof (induct arbitrary: thesis rule: rtranclp_induct)
  case base
  show ?case by (rule base, fact rtrancl_refl[to_pred], fact rtrancl_refl[to_pred], fact refl)
next
  case (step y z)
  obtain p1 q1 where p1: "(red F)** p p1" and q1: "(red F)** q q1" and y: "y = p1 - q1" by (rule step(3))
  from step(2) obtain p' q' where p': "(red F)** p1 p'" and q': "(red F)** q1 q'" and z: "z = p' - q'"
    unfolding y by (rule red_diff)
  show ?case
  proof (rule step(4))
    from p1 p' show "(red F)** p p'" by simp
  next
    from q1 q' show "(red F)** q q'" by simp
  qed fact
qed

lemma red_diff_rtrancl:
  assumes "(red F)** (p - q) 0"
  obtains s where "(red F)** p s" and "(red F)** q s"
proof -
  from assms obtain p' q' where p': "(red F)** p p'" and q': "(red F)** q q'" and "0 = p' - q'"
    by (rule red_diff_rtrancl')
  from this(3) have "q' = p'" by simp
  from p' q' show ?thesis unfolding q' = p' ..
qed

corollary red_diff_rtrancl_cs:
  assumes "(red F)** (p - q) 0"
  shows "relation.cs (red F) p q"
  unfolding relation.cs_def
proof -
  from assms obtain s where "(red F)** p s" and "(red F)** q s" by (rule red_diff_rtrancl)
  show "s. (red F)** p s  (red F)** q s" by (intro exI, intro conjI, fact, fact)
qed

subsection ‹Confluence of Reducibility›

lemma confluent_distinct_aux:
  assumes r1: "red_single p q1 f1 t1" and r2: "red_single p q2 f2 t2"
    and "t1  lt f1 t t2  lt f2" and "f1  F" and "f2  F"
  obtains s where "(red F)** q1 s" and "(red F)** q2 s"
proof -
  from r1 have "f1  0" and c1: "lookup p (t1  lt f1)  0"
    and q1_def: "q1 = p - monom_mult (lookup p (t1  lt f1) / lc f1) t1 f1"
    unfolding red_single_def by auto
  from r2 have "f2  0" and c2: "lookup p (t2  lt f2)  0"
    and q2_def: "q2 = p - monom_mult (lookup p (t2  lt f2) / lc f2) t2 f2"
    unfolding red_single_def by auto
  from t1  lt f1 t t2  lt f2
  have "lookup (monom_mult (lookup p (t1  lt f1) / lc f1) t1 f1) (t2  lt f2) = 0"
    by (simp add: lookup_monom_mult_eq_zero)
  from lookup_minus[of p _ "t2  lt f2"] this have c: "lookup q1 (t2  lt f2) = lookup p (t2  lt f2)"
    unfolding q1_def by simp
  define q3 where "q3  q1 - monom_mult ((lookup q1 (t2  lt f2)) / lc f2) t2 f2"
  have "red_single q1 q3 f2 t2" unfolding red_single_def
  proof (rule, fact, rule)
    from c c2 show "lookup q1 (t2  lt f2)  0" by simp
  next
    show "q3 = q1 - monom_mult (lookup q1 (t2  lt f2) / lc f2) t2 f2" unfolding q3_def ..
  qed
  hence "red F q1 q3" by (intro red_setI[OF f2  F])
  hence q1q3: "(red F)** q1 q3" by (intro r_into_rtranclp)
  from r1 have "red F p q1" by (intro red_setI[OF f1  F])
  from red_plus[OF this, of "- monom_mult ((lookup p (t2  lt f2)) / lc f2) t2 f2"] obtain s
    where r3: "(red F)** (p - monom_mult (lookup p (t2  lt f2) / lc f2) t2 f2) s"
    and r4: "(red F)** (q1 - monom_mult (lookup p (t2  lt f2) / lc f2) t2 f2) s" by auto
  from r3 have q2s: "(red F)** q2 s" unfolding q2_def by simp
  from r4 c have q3s: "(red F)** q3 s" unfolding q3_def by simp
  show ?thesis
  proof
    from rtranclp_trans[OF q1q3 q3s] show "(red F)** q1 s" .
  next
    from q2s show "(red F)** q2 s" .
  qed
qed

lemma confluent_distinct:
  assumes r1: "red_single p q1 f1 t1" and r2: "red_single p q2 f2 t2"
    and ne: "t1  lt f1  t2  lt f2" and "f1  F" and "f2  F"
  obtains s where "(red F)** q1 s" and "(red F)** q2 s"
proof -
  from ne have "t1  lt f1 t t2  lt f2  t2  lt f2 t t1  lt f1" by auto
  thus ?thesis
  proof
    assume a1: "t1  lt f1 t t2  lt f2"
    from confluent_distinct_aux[OF r1 r2 a1 f1  F f2  F] obtain s where
      "(red F)** q1 s" and "(red F)** q2 s" .
    thus ?thesis ..
  next
    assume a2: "t2  lt f2 t t1  lt f1"
    from confluent_distinct_aux[OF r2 r1 a2 f2  F f1  F] obtain s where
      "(red F)** q1 s" and "(red F)** q2 s" .
    thus ?thesis ..
  qed
qed

corollary confluent_same:
  assumes r1: "red_single p q1 f t1" and r2: "red_single p q2 f t2" and "f  F"
  obtains s where "(red F)** q1 s" and "(red F)** q2 s"
proof (cases "t1 = t2")
  case True
  with r1 r2 have "q1 = q2" by (simp add: red_single_def)
  show ?thesis
  proof
    show "(red F)** q1 q2" unfolding q1 = q2 ..
  next
    show "(red F)** q2 q2" ..
  qed
next
  case False
  hence "t1  lt f  t2  lt f" by (simp add: term_simps)
  from r1 r2 this f  F f  F obtain s where "(red F)** q1 s" and "(red F)** q2 s"
    by (rule confluent_distinct)
  thus ?thesis ..
qed

subsection ‹Reducibility and Module Membership›

lemma srtc_in_pmdl:
  assumes "relation.srtc (red F) p q"
  shows "p - q  pmdl F"
  using assms unfolding relation.srtc_def
proof (induct rule: rtranclp.induct)
  fix p
  show "p - p  pmdl F" by (simp add: pmdl.span_zero)
next
  fix p r q
  assume pr_in: "p - r  pmdl F" and red: "red F r q  red F q r"
  from red obtain f c t where "f  F" and "q = r - monom_mult c t f"
  proof
    assume "red F r q"
    from red_setE[OF this] obtain f t where "f  F" and "red_single r q f t" .
    hence "q = r - monom_mult (lookup r (t  lt f) / lc f) t f" by (simp add: red_single_def)
    show thesis by (rule, fact, fact)
  next
    assume "red F q r"
    from red_setE[OF this] obtain f t where "f  F" and "red_single q r f t" .
    hence "r = q - monom_mult (lookup q (t  lt f) / lc f) t f" by (simp add: red_single_def)
    hence "q = r + monom_mult (lookup q (t  lt f) / lc f) t f" by simp
    hence "q = r - monom_mult (-(lookup q (t  lt f) / lc f)) t f"
      using monom_mult_uminus_left[of _ t f] by simp
    show thesis by (rule, fact, fact)
  qed
  hence eq: "p - q = (p - r) + monom_mult c t f" by simp
  show "p - q  pmdl F" unfolding eq
    by (rule pmdl.span_add, fact, rule monom_mult_in_pmdl, fact)
qed

lemma in_pmdl_srtc:
  assumes "p  pmdl F"
  shows "relation.srtc (red F) p 0"
  using assms
proof (induct p rule: pmdl_induct)
  show "relation.srtc (red F) 0 0" unfolding relation.srtc_def ..
next
  fix a f c t
  assume a_in: "a  pmdl F" and IH: "relation.srtc (red F) a 0" and "f  F"
  show "relation.srtc (red F) (a + monom_mult c t f) 0"
  proof (cases "c = 0")
    assume "c = 0"
    hence "a + monom_mult c t f = a" by simp
    thus ?thesis using IH by simp
  next
    assume "c  0"
    show ?thesis
    proof (cases "f = 0")
      assume "f = 0"
      hence "a + monom_mult c t f = a" by simp
      thus ?thesis using IH by simp
    next
      assume "f  0"
      from lc_not_0[OF this] have "lc f  0" .
      have "red F (monom_mult c t f) 0"
      proof (intro red_setI[OF f  F])
        from lookup_monom_mult_plus[of c t f "lt f"]
          have eq: "lookup (monom_mult c t f) (t  lt f) = c * lc f" unfolding lc_def .
        show "red_single (monom_mult c t f) 0 f t" unfolding red_single_def eq
        proof (intro conjI, fact)
          from c  0 ‹lc f  0 show "c * lc f  0" by simp
        next
          from ‹lc f  0 show "0 = monom_mult c t f - monom_mult (c * lc f / lc f) t f" by simp
        qed
      qed
      from red_plus[OF this, of a] obtain s where
        s1: "(red F)** (monom_mult c t f + a) s" and s2: "(red F)** (0 + a) s" .
      have "relation.cs (red F) (a + monom_mult c t f) a" unfolding relation.cs_def
      proof (intro exI[of _ s], intro conjI)
        from s1 show "(red F)** (a + monom_mult c t f) s" by (simp only: add.commute)
      next
        from s2 show "(red F)** a s" by simp
      qed
      from relation.srtc_transitive[OF relation.cs_implies_srtc[OF this] IH] show ?thesis .
    qed
  qed
qed

lemma red_rtranclp_diff_in_pmdl:
  assumes "(red F)** p q"
  shows "p - q  pmdl F"
proof -
  from assms have "relation.srtc (red F) p q"
    by (simp add: r_into_rtranclp relation.rtc_implies_srtc)
  thus ?thesis by (rule srtc_in_pmdl)
qed

corollary red_diff_in_pmdl:
  assumes "red F p q"
  shows "p - q  pmdl F"
  by (rule red_rtranclp_diff_in_pmdl, rule r_into_rtranclp, fact)
  
corollary red_rtranclp_0_in_pmdl:
  assumes "(red F)** p 0"
  shows "p  pmdl F"
  using assms red_rtranclp_diff_in_pmdl by fastforce

lemma pmdl_closed_red:
  assumes "pmdl B  pmdl A" and "p  pmdl A" and "red B p q"
  shows "q  pmdl A"
proof -
  have "q - p  pmdl A"
  proof
    have "p - q  pmdl B" by (rule red_diff_in_pmdl, fact)
    hence "- (p - q)  pmdl B" by (rule pmdl.span_neg)
    thus "q - p  pmdl B" by simp
  qed fact
  from pmdl.span_add[OF this p  pmdl A] show ?thesis by simp
qed

subsection ‹More Properties of @{const red}, @{const red_single} and @{const is_red}

lemma red_rtrancl_mult:
  assumes "(red F)** p q"
  shows "(red F)** (monom_mult c t p) (monom_mult c t q)"
proof (cases "c = 0")
  case True
  have "(red F)** 0 0" by simp
  thus ?thesis by (simp only: True monom_mult_zero_left)
next
  case False
  from assms show ?thesis
  proof (induct rule: rtranclp_induct)
    show "(red F)** (monom_mult c t p) (monom_mult c t p)" by simp
  next
    fix q0 q
    assume "(red F)** p q0" and "red F q0 q" and "(red F)** (monom_mult c t p) (monom_mult c t q0)"
    show "(red F)** (monom_mult c t p) (monom_mult c t q)"
    proof (rule rtranclp.intros(2)[OF (red F)** (monom_mult c t p) (monom_mult c t q0)])
      from red_monom_mult[OF ‹red F q0 q False, of t] show "red F (monom_mult c t q0) (monom_mult c t q)" .
    qed
  qed
qed

corollary red_rtrancl_uminus:
  assumes "(red F)** p q"
  shows "(red F)** (-p) (-q)"
  using red_rtrancl_mult[OF assms, of "-1" 0] by (simp add: uminus_monom_mult)

lemma red_rtrancl_diff_induct [consumes 1, case_names base step]:
  assumes a: "(red F)** (p - q) r"
    and cases: "P p p" "!!y z. [| (red F)** (p - q) z; red F z y; P p (q + z)|] ==> P p (q + y)"
  shows "P p (q + r)"
  using a
proof (induct rule: rtranclp_induct)
  from cases(1) show "P p (q + (p - q))" by simp
next
  fix y z
  assume "(red F)** (p - q) z" "red F z y" "P p (q + z)"
  thus "P p (q + y)" using cases(2) by simp
qed

lemma red_rtrancl_diff_0_induct [consumes 1, case_names base step]:
  assumes a: "(red F)** (p - q) 0"
    and base: "P p p" and ind: "y z. [| (red F)** (p - q) y; red F y z; P p (y + q)|] ==> P p (z + q)"
  shows "P p q"
proof -
  from ind red_rtrancl_diff_induct[of F p q 0 P, OF a base] have "P p (0 + q)"
    by (simp add: ac_simps)
  thus ?thesis by simp
qed

lemma is_red_union: "is_red (A  B) p  (is_red A p  is_red B p)"
  unfolding is_red_alt red_union by auto

lemma red_single_0_lt:
  assumes "red_single f 0 h t"
  shows "lt f = t  lt h"
proof -
  from red_single_nonzero1[OF assms] have "f  0" .
  {
    assume "h  0" and neq: "lookup f (t  lt h)  0" and
      eq: "f = monom_mult (lookup f (t  lt h) / lc h) t h"
    from lc_not_0[OF h  0] have "lc h  0" .
    with neq have "(lookup f (t  lt h) / lc h)  0" by simp
    from eq lt_monom_mult[OF this h  0, of t] have "lt f = t  lt h" by simp
    hence "lt f = t  lt h" by (simp add: ac_simps)
  }
  with assms show ?thesis unfolding red_single_def by auto
qed

lemma red_single_lt_distinct_lt:
  assumes rs: "red_single f g h t" and "g  0" and "lt g  lt f"
  shows "lt f = t  lt h"
proof -
  from red_single_nonzero1[OF rs] have "f  0" .
  from red_single_ord[OF rs] have "g p f" by simp
  from ord_p_lt[OF this] ‹lt g  lt f have "lt g t lt f" by simp
  {
    assume "h  0" and neq: "lookup f (t  lt h)  0" and
      eq: "f = g + monom_mult (lookup f (t  lt h) / lc h) t h" (is "f = g + ?R")
    from lc_not_0[OF h  0] have "lc h  0" .
    with neq have "(lookup f (t  lt h) / lc h)  0" (is "?c  0") by simp
    from eq lt_monom_mult[OF this h  0, of t] have ltR: "lt ?R = t  lt h" by simp
    from monom_mult_eq_zero_iff[of ?c t h] ?c  0 h  0 have "?R  0" by auto
    from lt_plus_lessE[of g] eq ‹lt g t lt f have "lt g t lt ?R" by auto
    from lt_plus_eqI[OF this] eq ltR have "lt f = t  lt h" by (simp add: ac_simps)
  }
  with assms show ?thesis unfolding red_single_def by auto
qed

lemma zero_reducibility_implies_lt_divisibility':
  assumes "(red F)** f 0" and "f  0"
  shows "hF. h  0  (lt h addst 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 addst 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 addst 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 addst 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 addst 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 addst lt f"
  using zero_reducibility_implies_lt_divisibility'[OF assms] by auto

lemma is_red_addsI:
  assumes "f  F" and "f  0" and "v  keys p" and "lt f addst 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 addst 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 addst v True show "lt f addst lt p" by simp
    qed
  next
    case False
    with v  keys p p  0 have "v  keys (tail p)"
      by (simp add: lookup_tail_2 in_keys_iff) 
    from is_red_indI2[OF p  0 imp[OF this]] show ?thesis .
  qed
qed

lemma is_red_addsE':
  assumes "is_red F p"
  shows "fF. vkeys p. f  0  lt f addst 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 "fF. f  0  lt f addst lt p"
    then obtain f where "f  F" and "f  0" and "lt f addst lt p" by auto
    show ?case
    proof
      show "vkeys p. f  0  lt f addst 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 addst 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 addst 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 "vkeys p. f  0  lt f addst v"
        by (intro bexI, intro conjI, rule f  0, rule ‹lt f addst v, rule v_in_keys)
    qed (rule f  F)
  qed
qed

lemma is_red_addsE:
  assumes "is_red F p"
  obtains f v where "f  F" and "v  keys p" and "f  0" and "lt f addst v"
  using is_red_addsE'[OF assms] by auto

lemma is_red_adds_iff:
  shows "(is_red F p)  (fF. vkeys p. f  0  lt f addst v)"
  using is_red_addsE' is_red_addsI by auto
    
lemma is_red_subset:
  assumes red: "is_red A p" and sub: "A  B"
  shows "is_red B p"
proof -
  from red obtain f v where "f  A" and "v  keys p" and "f  0" and "lt f addst v" by (rule is_red_addsE)
  show ?thesis by (rule is_red_addsI, rule, fact+)
qed

lemma not_is_red_empty: "¬ is_red {} f"
  by (simp add: is_red_adds_iff)

lemma red_single_mult_const:
  assumes "red_single p q f t" and "c  0"
  shows "red_single p q (monom_mult c 0 f) t"
proof -
  let ?s = "t  lt f"
  let ?f = "monom_mult c 0 f"
  from assms(1) have "f  0" and "lookup p ?s  0"
    and "q = p - monom_mult ((lookup p ?s) / lc f) t f" by (simp_all add: red_single_def)
  from this(1) assms(2) have lt: "lt ?f = lt f" and lc: "lc ?f = c * lc f"
    by (simp add: lt_monom_mult term_simps, simp)
  show ?thesis unfolding red_single_def
  proof (intro conjI)
    from f  0 assms(2) show "?f  0" by (simp add: monom_mult_eq_zero_iff)
  next
    from ‹lookup p ?s  0 show "lookup p (t  lt ?f)  0" by (simp add: lt)
  next
    show "q = p - monom_mult (lookup p (t  lt ?f) / lc ?f) t ?f"
      by (simp add: lt monom_mult_assoc lc assms(2), fact)
  qed
qed

lemma red_rtrancl_plus_higher:
  assumes "(red F)** p q" and "u v. u  keys p  v  keys r  u t v"
  shows "(red F)** (p + r) (q + r)"
  using assms(1)
proof induct
  case base
  show ?case ..
next
  case (step y z)
  from step(1) have "y p p" by (rule red_rtrancl_ord)
  hence "lt y t lt p" by (rule ord_p_lt)
  from step(2) have "red F (y + r) (z + r)"
  proof (rule red_plus_keys_disjoint)
    show "keys y  keys r = {}"
    proof (rule ccontr)
      assume "keys y  keys r  {}"
      then obtain v where "v  keys y" and "v  keys r" by auto
      from this(1) have "v t lt y" and "y  0" using lt_max by (auto simp: in_keys_iff)
      with y p p have "p  0" using ord_p_zero_min[of y] by auto
      hence "lt p  keys p" by (rule lt_in_keys)
      from this v  keys r have "lt p t v" by (rule assms(2))
      with ‹lt y t lt p have "lt y t v" by simp
      with v t lt y  show False by simp
    qed
  qed
  with step(3) show ?case ..
qed

lemma red_mult_scalar_leading_monomial: "(red {f})** (p  monomial (lc f) (lt f)) (- p  tail f)"
proof (cases "f = 0")
  case True
  show ?thesis by (simp add: True lc_def)
next
  case False
  show ?thesis
  proof (induct p rule: punit.poly_mapping_tail_induct)
    case 0
    show ?case by simp
  next
    case (tail p)
    from False have "lc f  0" by (rule lc_not_0)
    from tail(1) have "punit.lc p  0" by (rule punit.lc_not_0)
    let ?t = "punit.tail p  monomial (lc f) (lt f)"
    let ?m = "monom_mult (punit.lc p) (punit.lt p) (monomial (lc f) (lt f))"
    from ‹lc f  0 have kt: "keys ?t = (λt. t  lt f) ` keys (punit.tail p)"
      by (rule keys_mult_scalar_monomial_right)
    have km: "keys ?m = {punit.lt p  lt f}"
      by (simp add: keys_monom_mult[OF ‹punit.lc p  0] ‹lc f  0)
    from tail(2) have "(red {f})** (?t + ?m) (- punit.tail p  tail f + ?m)"
    proof (rule red_rtrancl_plus_higher)
      fix u v
      assume "u  keys ?t" and "v  keys ?m"
      from this(1) obtain s where "s  keys (punit.tail p)" and u: "u = s  lt f" unfolding kt ..
      from this(1) have "punit.tail p  0" and "s  punit.lt (punit.tail p)" using punit.lt_max by (auto simp: in_keys_iff)
      moreover from ‹punit.tail p  0 have "punit.lt (punit.tail p)  punit.lt p" by (rule punit.lt_tail)
      ultimately have "s  punit.lt p" by simp
      moreover from v  keys ?m have "v = punit.lt p  lt f" by (simp only: km, simp)
      ultimately show "u t v" by (simp add: u splus_mono_strict_left)
    qed
    hence *: "(red {f})** (p  monomial (lc f) (lt f)) (?m - punit.tail p  tail f)"
      by (simp add: punit.leading_monomial_tail[symmetric, of p] mult_scalar_monomial[symmetric]
            mult_scalar_distrib_right[symmetric] add.commute[of "punit.tail p"])
    have "red {f} ?m (- (monomial (punit.lc p) (punit.lt p))  tail f)" unfolding red_singleton
    proof
      show "red_single ?m (- (monomial (punit.lc p) (punit.lt p))  tail f) f (punit.lt p)"
      proof (simp add: red_single_def f  0 km lookup_monom_mult ‹lc f  0 ‹punit.lc p  0 term_simps,
              simp add: monom_mult_dist_right_minus[symmetric] mult_scalar_monomial)
        have "monom_mult (punit.lc p) (punit.lt p) (monomial (lc f) (lt f) - f) =
              - monom_mult (punit.lc p) (punit.lt p) (f - monomial (lc f) (lt f))"
          by (metis minus_diff_eq monom_mult_uminus_right)
        also have "... = - monom_mult (punit.lc p) (punit.lt p) (tail f)" by (simp only: tail_alt_2)
        finally show "- monom_mult (punit.lc p) (punit.lt p) (tail f) =
                      monom_mult (punit.lc p) (punit.lt p) (monomial (lc f) (lt f) - f)" by simp
      qed
    qed
    hence "red {f} (?m + (- punit.tail p  tail f))
                    (- (monomial (punit.lc p) (punit.lt p))  tail f + (- punit.tail p  tail f))"
    proof (rule red_plus_keys_disjoint)
      show "keys ?m  keys (- punit.tail p  tail f) = {}"
      proof (cases "punit.tail p = 0")
        case True
        show ?thesis by (simp add: True)
      next
        case False
        from tail(2) have "- punit.tail p  tail f p ?t" by (rule red_rtrancl_ord)
        hence "lt (- punit.tail p  tail f) t lt ?t" by (rule ord_p_lt)
        also from ‹lc f  0 False have "... = punit.lt (punit.tail p)  lt f"
          by (rule lt_mult_scalar_monomial_right)
        also from punit.lt_tail[OF False] have "... t punit.lt p  lt f" by (rule splus_mono_strict_left)
        finally have "punit.lt p  lt f  keys (- punit.tail p  tail f)" using lt_gr_keys by blast
        thus ?thesis by (simp add: km)
      qed
    qed
    hence "red {f} (?m - punit.tail p  tail f)
            (- (monomial (punit.lc p) (punit.lt p))  tail f - punit.tail p  tail f)"
      by (simp add: term_simps)
    also have "... = - p  tail f" using punit.leading_monomial_tail[symmetric, of p]
      by (metis (mono_tags, lifting) add_uminus_conv_diff minus_add_distrib mult_scalar_distrib_right
          mult_scalar_minus_mult_left)
    finally have "red {f} (?m - punit.tail p  tail f) (- p  tail f)" .
    with * show ?case ..
  qed
qed

corollary red_mult_scalar_lt:
  assumes "f  0"
  shows "(red {f})** (p  monomial c (lt f)) (monom_mult (- c / lc f) 0 (p  tail f))"
proof -
  from assms have "lc f  0" by (rule lc_not_0)
  hence 1: "p  monomial c (lt f) = punit.monom_mult (c / lc f) 0 p  monomial (lc f) (lt f)"
    by (simp add: punit.mult_scalar_monomial[symmetric] mult.commute
        mult_scalar_assoc mult_scalar_monomial_monomial term_simps)
  have 2: "monom_mult (- c / lc f) 0 (p  tail f) = - punit.monom_mult (c / lc f) 0 p  tail f"
    by (simp add: times_monomial_left[symmetric] mult_scalar_assoc
        monom_mult_uminus_left mult_scalar_monomial)
  show ?thesis unfolding 1 2 by (fact red_mult_scalar_leading_monomial)
qed

lemma is_red_monomial_iff: "is_red F (monomial c v)  (c  0  (fF. f  0  lt f addst v))"
  by (simp add: is_red_adds_iff)

lemma is_red_monomialI:
  assumes "c  0" and "f  F" and "f  0" and "lt f addst 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 addst v"
  using assms unfolding is_red_monomial_iff by blast

lemma replace_lt_adds_stable_is_red:
  assumes red: "is_red F f" and "q  0" and "lt q addst 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 addst v"
    by (rule is_red_addsE)
  show ?thesis
  proof (cases "g = p")
    case True
    show ?thesis
    proof (rule is_red_addsI)
      show "q  insert q (F - {p})" by simp
    next
      have "lt q addst lt p" by fact
      also have "... addst v" using ‹lt g addst v unfolding True .
      finally show "lt q addst 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 addst 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 addst v" and "p  0"
    by (rule is_red_addsE, simp)
  from red_indE[OF ‹red {r} p q]
    have "(r  0  lt r addst lt p  q = p - monom_mult (lc p / lc r) ?s r) 
          red {r} (tail p) (q - monomial (lc p) (lt p))" by simp
  thus ?thesis
  proof
    assume "r  0  lt r addst lt p  q = p - monom_mult (lc p / lc r) ?s r"
    hence "r  0" and "lt r addst lt p" by simp_all
    show ?thesis by (intro disjI2, rule is_red_singleton_trans, rule ‹is_red {p} f, fact+)
  next
    assume "red {r} (tail p) (q - monomial (lc p) (lt p))" (is "red _ ?p' ?q'")
    with red_ord have "?q' p ?p'" .
    hence "?p'  0"
      and assm: "(?q' = 0  ((lt ?q') t<