Theory Groebner_Bases.General

section ‹General Utilities›

theory General
  imports Polynomials.Utils
begin

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

subsection ‹Lists›

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

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

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

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

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

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

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

lemma UN_upt: "(⋃i∈{0..<length xs}. f (xs ! i)) = (⋃x∈set xs. f x)"
  by (metis image_image map_nth set_map set_upt)

lemma sum_list_zeroI':
  assumes "⋀i. i < length xs ⟹ xs ! i = 0"
  shows "sum_list xs = 0"
proof (rule sum_list_zeroI, rule, simp)
  fix x
  assume "x ∈ set xs"
  then obtain i where "i < length xs" and "x = xs ! i" by (metis in_set_conv_nth)
  from this(1) show "x = 0" unfolding ‹x = xs ! i› by (rule assms)
qed

lemma sum_list_map2_plus:
  assumes "length xs = length ys"
  shows "sum_list (map2 (+) xs ys) = sum_list xs + sum_list (ys::'a::comm_monoid_add list)"
  using assms
proof (induct rule: list_induct2)
  case Nil
  show ?case by simp
next
  case (Cons x xs y ys)
  show ?case by (simp add: Cons(2) ac_simps)
qed

lemma sum_list_eq_nthI:
  assumes "i < length xs" and "⋀j. j < length xs ⟹ j ≠ i ⟹ xs ! j = 0"
  shows "sum_list xs = xs ! i"
  using assms
proof (induct xs arbitrary: i)
  case Nil
  from Nil(1) show ?case by simp
next
  case (Cons x xs)
  have *: "xs ! j = 0" if "j < length xs" and "Suc j ≠ i" for j
  proof -
    have "xs ! j = (x # xs) ! (Suc j)" by simp
    also have "... = 0" by (rule Cons(3), simp add: ‹j < length xs›, fact)
    finally show ?thesis .
  qed
  show ?case
  proof (cases i)
    case 0
    have "sum_list xs = 0" by (rule sum_list_zeroI', erule *, simp add: 0)
    with 0 show ?thesis by simp
  next
    case (Suc k)
    with Cons(2) have "k < length xs" by simp
    hence "sum_list xs = xs ! k"
    proof (rule Cons(1))
      fix j
      assume "j < length xs"
      assume "j ≠ k"
      hence "Suc j ≠ i" by (simp add: Suc)
      with ‹j < length xs› show "xs ! j = 0" by (rule *)
    qed
    moreover have "x = 0"
    proof -
      have "x = (x # xs) ! 0" by simp
      also have "... = 0" by (rule Cons(3), simp_all add: Suc)
      finally show ?thesis .
    qed
    ultimately show ?thesis by (simp add: Suc)
  qed
qed

subsubsection ‹‹max_list››

fun (in ord) max_list :: "'a list ⇒ 'a" where
  "max_list (x # xs) = (case xs of [] ⇒ x | _ ⇒ max x (max_list xs))"

context linorder
begin

lemma max_list_Max: "xs ≠ [] ⟹ max_list xs = Max (set xs)"
  by (induct xs rule: induct_list012, auto)

lemma max_list_ge:
  assumes "x ∈ set xs"
  shows "x ≤ max_list xs"
proof -
  from assms have "xs ≠ []" by auto
  from finite_set assms have "x ≤ Max (set xs)" by (rule Max_ge)
  also from ‹xs ≠ []› have "Max (set xs) = max_list xs" by (rule max_list_Max[symmetric])
  finally show ?thesis .
qed

lemma max_list_boundedI:
  assumes "xs ≠ []" and "⋀x. x ∈ set xs ⟹ x ≤ a"
  shows "max_list xs ≤ a"
proof -
  from assms(1) have "set xs ≠ {}" by simp
  from assms(1) have "max_list xs = Max (set xs)" by (rule max_list_Max)
  also from finite_set ‹set xs ≠ {}› assms(2) have "… ≤ a" by (rule Max.boundedI)
  finally show ?thesis .
qed

end

subsubsection ‹‹insort_wrt››

primrec insort_wrt :: "('c ⇒ 'c ⇒ bool) ⇒ 'c ⇒ 'c list ⇒ 'c list" where
  "insort_wrt _ x [] = [x]" |
  "insort_wrt r x (y # ys) =
    (if r x y then (x # y # ys) else y # (insort_wrt r x ys))"

lemma insort_wrt_not_Nil [simp]: "insort_wrt r x xs ≠ []"
  by (induct xs, simp_all)

lemma length_insort_wrt [simp]: "length (insort_wrt r x xs) = Suc (length xs)"
  by (induct xs, simp_all)

lemma set_insort_wrt [simp]: "set (insort_wrt r x xs) = insert x (set xs)"
  by (induct xs, auto)

lemma sorted_wrt_insort_wrt_imp_sorted_wrt:
  assumes "sorted_wrt r (insort_wrt s x xs)"
  shows "sorted_wrt r xs"
  using assms
proof (induct xs)
  case Nil
  show ?case by simp
next
  case (Cons a xs)
  show ?case
  proof (cases "s x a")
    case True
    with Cons.prems have "sorted_wrt r (x # a # xs)" by simp
    thus ?thesis by simp
  next
    case False
    with Cons(2) have "sorted_wrt r (a # (insort_wrt s x xs))" by simp
    hence *: "(∀y∈set xs. r a y)" and "sorted_wrt r (insort_wrt s x xs)"
      by (simp_all)
    from this(2) have "sorted_wrt r xs" by (rule Cons(1))
    with * show ?thesis by (simp)
  qed
qed

lemma sorted_wrt_imp_sorted_wrt_insort_wrt:
  assumes "transp r" and "⋀a. r a x ∨ r x a" and "sorted_wrt r xs"
  shows "sorted_wrt r (insort_wrt r x xs)"
  using assms(3)
proof (induct xs)
  case Nil
  show ?case by simp
next
  case (Cons a xs)
  show ?case
  proof (cases "r x a")
    case True
    with Cons(2) assms(1) show ?thesis by (auto dest: transpD)
  next
    case False
    with assms(2) have "r a x" by blast
    from Cons(2) have *: "(∀y∈set xs. r a y)" and "sorted_wrt r xs"
      by (simp_all)
    from this(2) have "sorted_wrt r (insort_wrt r x xs)" by (rule Cons(1))
    with ‹r a x› * show ?thesis by (simp add: False)
  qed
qed

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

subsubsection ‹‹diff_list› and ‹insert_list››

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

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

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

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

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

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

subsubsection ‹‹remdups_wrt››

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

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

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

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

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

subsubsection ‹‹map_idx››

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

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

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

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

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

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

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

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

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

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

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

subsubsection ‹‹map_dup››

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

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

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

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

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

subsubsection ‹Filtering Minimal Elements›

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

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

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

definition filter_min_append :: "'a list ⇒ 'a list ⇒ 'a list"
  where "filter_min_append xs ys =
                  (let P = (λzs. λx. ¬ (∃z∈set zs. rel z x)); ys1 = filter (P xs) ys in
                    (filter (P ys1) xs) @ ys1)"
  
lemma filter_min_aux_supset: "set ys ⊆ set (filter_min_aux xs ys)"
proof (induct xs arbitrary: ys)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  have "set ys ⊆ set (x # ys)" by auto
  also have "set (x # ys) ⊆ set (filter_min_aux xs (x # ys))" by (rule Cons.hyps)
  finally have "set ys ⊆ set (filter_min_aux xs (x # ys))" .
  moreover have "set ys ⊆ set (filter_min_aux xs ys)" by (rule Cons.hyps)
  ultimately show ?case by simp
qed
    
lemma filter_min_aux_subset: "set (filter_min_aux xs ys) ⊆ set xs ∪ set ys"
proof (induct xs arbitrary: ys)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  note Cons.hyps
  also have "set xs ∪ set ys ⊆ set (x # xs) ∪ set ys" by fastforce
  finally have c1: "set (filter_min_aux xs ys) ⊆ set (x # xs) ∪ set ys" .
  
  note Cons.hyps
  also have "set xs ∪ set (x # ys) = set (x # xs) ∪ set ys" by simp
  finally have "set (filter_min_aux xs (x # ys)) ⊆ set (x # xs) ∪ set ys" .
  with c1 show ?case by simp
qed

lemma filter_min_aux_relE:
  assumes "transp rel" and "x ∈ set xs" and "x ∉ set (filter_min_aux xs ys)"
  obtains y where "y ∈ set (filter_min_aux xs ys)" and "rel y x"
  using assms(2, 3)
proof (induct xs arbitrary: x ys thesis)
  case Nil
  from Nil(2) show ?case by simp
next
  case (Cons x0 xs)
  from Cons(3) have "x = x0 ∨ x ∈ set xs" by simp
  thus ?case
  proof
    assume "x = x0"
    from Cons(4) have *: "∃y∈set xs ∪ set ys. rel y x0"
    proof (simp add: ‹x = x0› split: if_splits)
      assume "x0 ∉ set (filter_min_aux xs (x0 # ys))"
      moreover from filter_min_aux_supset have "x0 ∈ set (filter_min_aux xs (x0 # ys))"
        by (rule subsetD) simp
      ultimately show False ..
    qed
    hence eq: "filter_min_aux (x0 # xs) ys = filter_min_aux xs ys" by simp
    from * obtain x1 where "x1 ∈ set xs ∪ set ys" and "rel x1 x" unfolding ‹x = x0› ..
    from this(1) show ?thesis
    proof
      assume "x1 ∈ set xs"
      show ?thesis
      proof (cases "x1 ∈ set (filter_min_aux xs ys)")
        case True
        hence "x1 ∈ set (filter_min_aux (x0 # xs) ys)" by (simp only: eq)
        thus ?thesis using ‹rel x1 x› by (rule Cons(2))
      next
        case False
        with ‹x1 ∈ set xs› obtain y where "y ∈ set (filter_min_aux xs ys)" and "rel y x1"
          using Cons.hyps by blast
        from this(1) have "y ∈ set (filter_min_aux (x0 # xs) ys)" by (simp only: eq)
        moreover from assms(1) ‹rel y x1› ‹rel x1 x› have "rel y x" by (rule transpD)
        ultimately show ?thesis by (rule Cons(2))
      qed
    next
      assume "x1 ∈ set ys"
      hence "x1 ∈ set (filter_min_aux (x0 # xs) ys)" using filter_min_aux_supset ..
      thus ?thesis using ‹rel x1 x› by (rule Cons(2))
    qed
  next
    assume "x ∈ set xs"
    show ?thesis
    proof (cases "∃y∈set xs ∪ set ys. rel y x0")
      case True
      hence eq: "filter_min_aux (x0 # xs) ys = filter_min_aux xs ys" by simp
      with Cons(4) have "x ∉ set (filter_min_aux xs ys)" by simp
      with ‹x ∈ set xs› obtain y where "y ∈ set (filter_min_aux xs ys)" and "rel y x"
        using Cons.hyps by blast
      from this(1) have "y ∈ set (filter_min_aux (x0 # xs) ys)" by (simp only: eq)
      thus ?thesis using ‹rel y x› by (rule Cons(2))
    next
      case False
      hence eq: "filter_min_aux (x0 # xs) ys = filter_min_aux xs (x0 # ys)" by simp
      with Cons(4) have "x ∉ set (filter_min_aux xs (x0 # ys))" by simp
      with ‹x ∈ set xs› obtain y where "y ∈ set (filter_min_aux xs (x0 # ys))" and "rel y x"
        using Cons.hyps by blast
      from this(1) have "y ∈ set (filter_min_aux (x0 # xs) ys)" by (simp only: eq)
      thus ?thesis using ‹rel y x› by (rule Cons(2))
    qed
  qed
qed

lemma filter_min_aux_minimal:
  assumes "transp rel" and "x ∈ set (filter_min_aux xs ys)" and "y ∈ set (filter_min_aux xs ys)"
    and "rel x y"
  assumes "⋀a b. a ∈ set xs ∪ set ys ⟹ b ∈ set ys ⟹ rel a b ⟹ a = b"
  shows "x = y"
  using assms(2-5)
proof (induct xs arbitrary: x y ys)
  case Nil
  from Nil(1) have "x ∈ set [] ∪ set ys" by simp
  moreover from Nil(2) have "y ∈ set ys" by simp
  ultimately show ?case using Nil(3) by (rule Nil(4))
next
  case (Cons x0 xs)
  show ?case
  proof (cases "∃y∈set xs ∪ set ys. rel y x0")
    case True
    hence eq: "filter_min_aux (x0 # xs) ys = filter_min_aux xs ys" by simp
    with Cons(2, 3) have "x ∈ set (filter_min_aux xs ys)" and "y ∈ set (filter_min_aux xs ys)"
      by simp_all
    thus ?thesis using Cons(4)
    proof (rule Cons.hyps)
      fix a b
      assume "a ∈ set xs ∪ set ys"
      hence "a ∈ set (x0 # xs) ∪ set ys" by simp
      moreover assume "b ∈ set ys" and "rel a b"
      ultimately show "a = b" by (rule Cons(5))
    qed
  next
    case False
    hence eq: "filter_min_aux (x0 # xs) ys = filter_min_aux xs (x0 # ys)" by simp
    with Cons(2, 3) have "x ∈ set (filter_min_aux xs (x0 # ys))" and "y ∈ set (filter_min_aux xs (x0 # ys))"
      by simp_all
    thus ?thesis using Cons(4)
    proof (rule Cons.hyps)
      fix a b
      assume a: "a ∈ set xs ∪ set (x0 # ys)" and "b ∈ set (x0 # ys)" and "rel a b"
      from this(2) have "b = x0 ∨ b ∈ set ys" by simp
      thus "a = b"
      proof
        assume "b = x0"
        from a have "a = x0 ∨ a ∈ set xs ∪ set ys" by simp
        thus ?thesis
        proof
          assume "a = x0"
          with ‹b = x0› show ?thesis by simp
        next
          assume "a ∈ set xs ∪ set ys"
          hence "∃y∈set xs ∪ set ys. rel y x0" using ‹rel a b› unfolding ‹b = x0› ..
          with False show ?thesis ..
        qed
      next
        from a have "a ∈ set (x0 # xs) ∪ set ys" by simp
        moreover assume "b ∈ set ys"
        ultimately show ?thesis using ‹rel a b› by (rule Cons(5))
      qed
    qed
  qed
qed
  
lemma filter_min_aux_distinct:
  assumes "reflp rel" and "distinct ys"
  shows "distinct (filter_min_aux xs ys)"
  using assms(2)
proof (induct xs arbitrary: ys)
  case Nil
  thus ?case by simp
next
  case (Cons x xs)
  show ?case
  proof (simp split: if_split, intro conjI impI)
    from Cons(2) show "distinct (filter_min_aux xs ys)" by (rule Cons.hyps)
  next
    assume a: "∀y∈set xs ∪ set ys. ¬ rel y x"
    show "distinct (filter_min_aux xs (x # ys))"
    proof (rule Cons.hyps)
      have "x ∉ set ys"
      proof
        assume "x ∈ set ys"
        hence "x ∈ set xs ∪ set ys" by simp
        with a have "¬ rel x x" ..
        moreover from assms(1) have "rel x x" by (rule reflpD)
        ultimately show False ..
      qed
      with Cons(2) show "distinct (x # ys)" by simp
    qed
  qed
qed

lemma filter_min_subset: "set (filter_min xs) ⊆ set xs"
  using filter_min_aux_subset[of xs "[]"] by (simp add: filter_min_def)

lemma filter_min_cases:
  assumes "transp rel" and "x ∈ set xs"
  assumes "x ∈ set (filter_min xs) ⟹ thesis"
  assumes "⋀y. y ∈ set (filter_min xs) ⟹ x ∉ set (filter_min xs) ⟹ rel y x ⟹ thesis"
  shows thesis
proof (cases "x ∈ set (filter_min xs)")
  case True
  thus ?thesis by (rule assms(3))
next
  case False
  with assms(1, 2) obtain y where "y ∈ set (filter_min xs)" and "rel y x"
    unfolding filter_min_def by (rule filter_min_aux_relE)
  from this(1) False this(2) show ?thesis by (rule assms(4))
qed

corollary filter_min_relE:
  assumes "transp rel" and "reflp rel" and "x ∈ set xs"
  obtains y where "y ∈ set (filter_min xs)" and "rel y x"
  using assms(1, 3)
proof (rule filter_min_cases)
  assume "x ∈ set (filter_min xs)"
  moreover from assms(2) have "rel x x" by (rule reflpD)
  ultimately show ?thesis ..
qed

lemma filter_min_minimal:
  assumes "transp rel" and "x ∈ set (filter_min xs)" and "y ∈ set (filter_min xs)" and "rel x y"
  shows "x = y"
  using assms unfolding filter_min_def by (rule filter_min_aux_minimal) simp

lemma filter_min_distinct:
  assumes "reflp rel"
  shows "distinct (filter_min xs)"
  unfolding filter_min_def by (rule filter_min_aux_distinct, fact, simp)

lemma filter_min_append_subset: "set (filter_min_append xs ys) ⊆ set xs ∪ set ys"
  by (auto simp: filter_min_append_def)

lemma filter_min_append_cases:
  assumes "transp rel" and "x ∈ set xs ∪ set ys"
  assumes "x ∈ set (filter_min_append xs ys) ⟹ thesis"
  assumes "⋀y. y ∈ set (filter_min_append xs ys) ⟹ x ∉ set (filter_min_append xs ys) ⟹ rel y x ⟹ thesis"
  shows thesis
proof (cases "x ∈ set (filter_min_append xs ys)")
  case True
  thus ?thesis by (rule assms(3))
next
  case False
  define P where "P = (λzs. λa. ¬ (∃z∈set zs. rel z a))"
  from assms(2) obtain y where "y ∈ set (filter_min_append xs ys)" and "rel y x"
  proof
    assume "x ∈ set xs"
    with False obtain y where "y ∈ set (filter_min_append xs ys)" and "rel y x"
      by (auto simp: filter_min_append_def P_def)
    thus ?thesis ..
  next
    assume "x ∈ set ys"
    with False obtain y where "y ∈ set xs" and "rel y x"
      by (auto simp: filter_min_append_def P_def)
    show ?thesis
    proof (cases "y ∈ set (filter_min_append xs ys)")
      case True
      thus ?thesis using ‹rel y x› ..
    next
      case False
      with ‹y ∈ set xs› obtain y' where y': "y' ∈ set (filter_min_append xs ys)" and "rel y' y"
        by (auto simp: filter_min_append_def P_def)
      from assms(1) this(2) ‹rel y x› have "rel y' x" by (rule transpD)
      with y' show ?thesis ..
    qed
  qed
  from this(1) False this(2) show ?thesis by (rule assms(4))
qed

corollary filter_min_append_relE:
  assumes "transp rel" and "reflp rel" and "x ∈ set xs ∪ set ys"
  obtains y where "y ∈ set (filter_min_append xs ys)" and "rel y x"
  using assms(1, 3)
proof (rule filter_min_append_cases)
  assume "x ∈ set (filter_min_append xs ys)"
  moreover from assms(2) have "rel x x" by (rule reflpD)
  ultimately show ?thesis ..
qed

lemma filter_min_append_minimal:
  assumes "⋀x' y'. x' ∈ set xs ⟹ y' ∈ set xs ⟹ rel x' y' ⟹ x' = y'"
    and "⋀x' y'. x' ∈ set ys ⟹ y' ∈ set ys ⟹ rel x' y' ⟹ x' = y'"
    and "x ∈ set (filter_min_append xs ys)" and "y ∈ set (filter_min_append xs ys)" and "rel x y"
  shows "x = y"
proof -
  define P where "P = (λzs. λa. ¬ (∃z∈set zs. rel z a))"
  define ys1 where "ys1 = filter (P xs) ys"
  from assms(3) have "x ∈ set xs ∪ set ys1"
    by (auto simp: filter_min_append_def P_def ys1_def)
  moreover from assms(4) have "y ∈ set (filter (P ys1) xs) ∪ set ys1"
    by (simp add: filter_min_append_def P_def ys1_def)
  ultimately show ?thesis
  proof (elim UnE)
    assume "x ∈ set xs"
    assume "y ∈ set (filter (P ys1) xs)"
    hence "y ∈ set xs" by simp
    with ‹x ∈ set xs› show ?thesis using assms(5) by (rule assms(1))
  next
    assume "y ∈ set ys1"
    hence "⋀z. z ∈ set xs ⟹ ¬ rel z y" by (simp add: ys1_def P_def)
    moreover assume "x ∈ set xs"
    ultimately have "¬ rel x y" by blast
    thus ?thesis using ‹rel x y› ..
  next
    assume "y ∈ set (filter (P ys1) xs)"
    hence "⋀z. z ∈ set ys1 ⟹ ¬ rel z y" by (simp add: P_def)
    moreover assume "x ∈ set ys1"
    ultimately have "¬ rel x y" by blast
    thus ?thesis using ‹rel x y› ..
  next
    assume "x ∈ set ys1" and "y ∈ set ys1"
    hence "x ∈ set ys" and "y ∈ set ys" by (simp_all add: ys1_def)
    thus ?thesis using assms(5) by (rule assms(2))
  qed
qed

lemma filter_min_append_distinct:
  assumes "reflp rel" and "distinct xs" and "distinct ys"
  shows "distinct (filter_min_append xs ys)"
proof -
  define P where "P = (λzs. λa. ¬ (∃z∈set zs. rel z a))"
  define ys1 where "ys1 = filter (P xs) ys"
  from assms(2) have "distinct (filter (P ys1) xs)" by simp
  moreover from assms(3) have "distinct ys1" by (simp add: ys1_def)
  moreover have "set (filter (P ys1) xs) ∩ set ys1 = {}"
  proof (simp add: set_eq_iff, intro allI impI notI)
    fix x
    assume "P ys1 x"
    hence "⋀z. z ∈ set ys1 ⟹ ¬ rel z x" by (simp add: P_def)
    moreover assume "x ∈ set ys1"
    ultimately have "¬ rel x x" by blast
    moreover from assms(1) have "rel x x" by (rule reflpD)
    ultimately show False ..
  qed
  ultimately show ?thesis by (simp add: filter_min_append_def ys1_def P_def)
qed

end

end (* theory *)