Theory HOL_Extra_Extra

theory HOL_Extra_Extra
  imports First_Order_Clause.HOL_Extra
begin

no_notation restrict_map (infixl "|`"  110)

lemma
  assumes "∃⇩≤⇩1x. P x"
  shows "finite {x. P x}"
  using assms Collect_eq_if_Uniq by fastforce

lemma finite_if_Uniq_Uniq:
  assumes
    "∃⇩≤⇩1x. P x"
    "∀x. ∃⇩≤⇩1y. Q x y"
  shows "finite {y. ∃x. P x ∧ Q x y}"
  using assms
  by (smt (verit, best) Collect_eq_if_Uniq UniqI Uniq_D finite.emptyI finite_insert)

lemma finite_if_finite_finite:
  assumes
    "finite {x. P x}"
    "∀x. finite {y. Q x y}"
  shows "finite {y. ∃x. P x ∧ Q x y}"
  using assms by auto

lemma (in order) greater_wfp_on_finite_set: "finite 𝒳 ⟹ Wellfounded.wfp_on 𝒳 (>)"
  using strict_partial_order_wfp_on_finite_set[OF transp_on_greater asymp_on_greater] .

lemma (in order) less_wfp_on_finite_set: "finite 𝒳 ⟹ Wellfounded.wfp_on 𝒳 (<)"
  using strict_partial_order_wfp_on_finite_set[OF transp_on_less asymp_on_less] .

lemma distinct_if_sorted_wrt_asymp:
  assumes "asymp_on (set xs) R" and "sorted_wrt R xs"
  shows "distinct xs"
  using assms
proof (induction xs)
  case Nil
  show ?case
    unfolding distinct.simps ..
next
  case (Cons x xs)

  have R_x_asym: "∀y ∈ set xs. R x y ⟶ ¬ R y x" and "asymp_on (set xs) R"
    using Cons.prems(1)
    unfolding atomize_conj
    by (metis asymp_on_def list.set_intros(1) list.set_intros(2))

  have R_x: "∀y ∈ set xs. R x y" and "sorted_wrt R xs"
    using Cons.prems(2)
    unfolding atomize_conj sorted_wrt.simps
    by argo

  have "x ∉ set xs"
  proof (intro notI)
    assume x_in: "x ∈ set xs"

    have "R x x"
      using R_x x_in by metis

    moreover hence "¬ R x x"
      using R_x_asym x_in by metis

    ultimately show False
      by contradiction
  qed

  moreover have "distinct xs"
    using Cons.IH ‹asymp_on (set xs) R› ‹sorted_wrt R xs› by argo

  ultimately show ?case
    unfolding distinct.simps by argo
qed

lemma dropWhile_append_eq_rhs:
  fixes xs ys :: "'a list" and P :: "'a ⇒ bool"
  assumes
    "⋀x. x ∈ set xs ⟹ P x" and
    "⋀y. y ∈ set ys ⟹ ¬ P y"
  shows "dropWhile P (xs @ ys) = ys"
  using assms by simp

lemma mem_set_dropWhile_conv_if_list_sorted_and_pred_monotone:
  fixes R :: "'a ⇒ 'a ⇒ bool" and xs :: "'a list" and P :: "'a ⇒ bool"
  assumes "sorted_wrt R xs" and "monotone_on (set xs) R (≥) P"
  shows "x ∈ set (dropWhile P xs) ⟷ ¬ P x ∧ x ∈ set xs"
  using assms
proof (induction xs)
  case Nil
  show ?case
    by simp
next
  case (Cons y xs)
  have "∀z ∈ set xs. R y z" and "sorted_wrt R xs"
    using ‹sorted_wrt R (y # xs)› by simp_all

  moreover have "monotone_on (set xs) R (≥) P"
    using ‹monotone_on (set (y # xs)) R (≥) P›
    by (metis monotone_on_subset set_subset_Cons)

  ultimately have IH: "(x ∈ set (dropWhile P xs)) = (¬ P x ∧ x ∈ set xs)"
    using Cons.IH ‹sorted_wrt R xs› by metis

  show ?case
  proof (cases "P y")
    case True
    thus ?thesis
      unfolding dropWhile.simps
      unfolding if_P[OF True]
      using IH by auto
  next
    case False
    then show ?thesis
      unfolding dropWhile.simps
      unfolding if_not_P[OF False]
      by (metis (full_types) Cons.prems(1) Cons.prems(2) le_boolD list.set_intros(1) monotone_on_def
          set_ConsD sorted_wrt.simps(2))
  qed
qed

lemma ball_set_dropWhile_if_sorted_wrt_and_monotone_on:
  fixes R :: "'a ⇒ 'a ⇒ bool" and xs :: "'a list" and P :: "'a ⇒ bool"
  assumes "sorted_wrt R xs" and "monotone_on (set xs) R (≥) P"
  shows "∀x ∈ set (dropWhile P xs). ¬ P x"
  using mem_set_dropWhile_conv_if_list_sorted_and_pred_monotone[OF assms] by metis

lemma filter_set_eq_filter_set_minus_singleton:
  assumes "¬ P y"
  shows "{x ∈ X. P x} = {x ∈ X - {y}. P x}"
  using assms by blast

lemma ex1_subset_eq_image_if_bij_betw:
  fixes f :: "'a ⇒ 'b" and X :: "'a set" and Y :: "'b set"
  assumes "bij_betw f X Y" and "Y' ⊆ Y"
  shows "∃!X'. X' ⊆ X ∧ Y' = f ` X'"
  using assms
  by (metis bij_betw_def inv_into_image_cancel subset_image_iff)

lemma Collect_eq_image_filter_Collect_if_bij_betw:
  fixes f :: "'a ⇒ 'b" and X :: "'a set" and Y :: "'b set"
  assumes bij: "bij_betw f X Y" and sub: "{y. P y} ⊆ Y"
  shows "{y. P y} = f ` {x. x ∈ X ∧ P (f x)}"
  using ex1_subset_eq_image_if_bij_betw[OF bij sub]
  by (smt (verit, best) Collect_cong image_def in_mono mem_Collect_eq)

lemma restrict_map_ident_if_dom_subset: "dom ℳ ⊆ A ⟹ restrict_map ℳ A = ℳ"
  by (metis domIff ext in_mono restrict_map_def)


subsection ‹Move to \<^theory>‹HOL.Transitive_Closure››

lemma relpowp_right_unique:
  fixes R :: "'a ⇒ 'a ⇒ bool" and n :: nat and x y z :: 'a
  assumes runique: "⋀x y z. R x y ⟹ R x z ⟹ y = z"
  shows "(R ^^ n) x y ⟹ (R ^^ n) x z ⟹ y = z"
proof (induction n arbitrary: x y z)
  case 0
  thus ?case
    by simp
next
  case (Suc n')
  then obtain x' :: 'a where
    "(R ^^ n') x x'" and "R x' y" and "R x' z"
    by auto
  thus "y = z"
    using runique by simp
qed

lemma Uniq_relpowp:
  fixes n :: nat and R :: "'a ⇒ 'a ⇒ bool"
  assumes runiq: "∀x. ∃⇩≤⇩1y. R x y"
  shows "∃⇩≤⇩1y. (R ^^ n) x y"
proof (rule Uniq_I)
  fix y z
  assume "(R ^^ n) x y" and "(R ^^ n) x z"
  show "y = z"
  proof (rule relpowp_right_unique)
    show "⋀x y z. R x y ⟹ R x z ⟹ y = z"
      using runiq by (auto dest: Uniq_D)
  next
    show "(R ^^ n) x y"
      using ‹(R ^^ n) x y› .
  next
    show "(R ^^ n) x z"
      using ‹(R ^^ n) x z› .
  qed
qed

lemma relpowp_plus_of_right_unique:
  assumes
    "right_unique R"
    "(R ^^ m) x y" and
    "(R ^^ (m + n)) x z"
  shows "(R ^^ n) y z"
  using assms(2,3)
proof (induction m arbitrary: x)
  case 0
  thus ?case
    by simp
next
  case (Suc m)
  then show ?case
    by (metis add_Suc assms(1) relpowp_Suc_E2 right_uniqueD)
qed

lemma relpowp_plusD:
  assumes "(R ^^ (m + n)) x z"
  shows "∃y. (R ^^ m) x y ∧ (R ^^ n) y z"
  using assms
proof (induction m arbitrary: x)
  case 0
  thus ?case
    by simp
next
  case (Suc m)

  obtain y where "R x y" and "(R ^^ (m + n)) y z"
    using Suc.prems by (metis add_Suc relpowp_Suc_D2)

  obtain y' where "(R ^^ m) y y'" and "(R ^^ n) y' z"
    using Suc.IH[OF ‹(R ^^ (m + n)) y z›] by metis

  show ?case
  proof (intro exI conjI)
    show "(R ^^ Suc m) x y'"
      using ‹R x y› ‹(R ^^ m) y y'› by (metis relpowp_Suc_I2)
  next
    show "(R ^^ n) y' z"
      using ‹(R ^^ n) y' z› .
  qed
qed

lemma relpowp_Suc_of_right_unique:
  assumes
    "right_unique R"
    "R x y" and
    "(R ^^ Suc n) x z"
  shows "(R ^^ n) y z"
  using assms
  by (metis relpowp_Suc_D2 right_uniqueD)

lemma tranclp_if_relpowp: "n ≠ 0 ⟹ (R ^^ n) x y ⟹ R⇧+⇧+ x y"
  by (meson bot_nat_0.not_eq_extremum tranclp_power)

lemma transp_on_singleton[simp]: "transp_on {x} R"
  by (simp add: transp_on_def)

lemma rtranclp_rtranclp_compose_if_right_unique:
  assumes runique: "right_unique R" and "R⇧*⇧* a b" and "R⇧*⇧* a c"
  shows "R⇧*⇧* a b ∧ R⇧*⇧* b c ∨ R⇧*⇧* a c ∧ R⇧*⇧* c b"
  using assms(2,3)
proof (induction b arbitrary: c rule: rtranclp_induct)
  case base
  thus ?case
    by simp
next
  case (step a' b)
  with runique show ?case
    by (metis converse_rtranclpE right_uniqueD rtranclp.rtrancl_into_rtrancl)
qed

lemma right_unique_terminating_rtranclp:
  assumes "right_unique R"
  shows "right_unique (λx y. R⇧*⇧* x y ∧ (∄z. R y z))"
  unfolding right_unique_def
  using rtranclp_rtranclp_compose_if_right_unique[OF ‹right_unique R›]
  by (metis converse_rtranclpE)

end