Theory First_Order_Clause.Uprod_Extra

theory Uprod_Extra
  imports
    "HOL-Library.Uprod"
    Multiset_Extra
    Abstract_Substitution.Natural_Functor
begin

setup natural_functor_setups

abbreviation upair where
  "upair ≡ λ(x, y). Upair x y"

lemma Upair_sym: "Upair x y = Upair y x"
  by (metis Upair_inject)

lemma upair_in_sym [simp]:
  assumes "sym I"
  shows "Upair a b ∈ upair ` I ⟷ (a, b) ∈ I ∧ (b, a) ∈ I"
  using assms
  by (auto dest: symD)

lemma ex_ordered_Upair:
  assumes tot: "totalp_on (set_uprod p) R"
  shows "∃x y. p = Upair x y ∧ R⇧=⇧= x y"
proof -
  obtain x y where "p = Upair x y"
    by (metis uprod_exhaust)

  show ?thesis
  proof (cases "R⇧=⇧= x y")
    case True
    show ?thesis
    proof (intro exI conjI)
      show "p = Upair x y"
        using ‹p = Upair x y› .
    next
      show "R⇧=⇧= x y"
        using True by simp
    qed
  next
    case False
    then show ?thesis
    proof (intro exI conjI)
      show "p = Upair y x"
        using ‹p = Upair x y› by simp
    next
      from tot have "R y x"
        using False
        by (simp add: ‹p = Upair x y› totalp_on_def)
      thus "R⇧=⇧= y x"
        by simp
    qed
  qed
qed

definition mset_uprod :: "'a uprod ⇒ 'a multiset" where
  "mset_uprod = case_uprod (Abs_commute (λx y. {#x, y#}))"

lemma Abs_commute_inverse_mset [simp]:
  "apply_commute (Abs_commute (λx y. {#x, y#})) = (λx y. {#x, y#})"
  by (simp add: Abs_commute_inverse)

lemma set_mset_mset_uprod [simp]: "set_mset (mset_uprod up) = set_uprod up"
  by (simp add: mset_uprod_def case_uprod.rep_eq set_uprod.rep_eq case_prod_beta)

lemma mset_uprod_Upair [simp]: "mset_uprod (Upair x y) = {#x, y#}"
  by (simp add: mset_uprod_def)

lemma mset_uprod_not_empty [simp]: "mset_uprod up ≠ {#}"
  by (cases up) simp

lemma map_uprod_inverse: "(⋀x. f (g x) = x) ⟹ (⋀y. map_uprod f (map_uprod g y) = y)"
  by (simp add: uprod.map_comp)

lemma mset_uprod_image_mset: "mset_uprod (map_uprod f p) = image_mset f (mset_uprod p)"
proof-
  obtain x y where [simp]: "p = Upair x y"
    using uprod_exhaust by blast

  have "mset_uprod (map_uprod f p) = {# f x, f y #}"
    by simp

  then show "mset_uprod (map_uprod f p) = image_mset f (mset_uprod p)"
    by simp
qed

lemma ball_set_uprod [simp]: "(∀t∈set_uprod (Upair t⇩1 t⇩2). P t) ⟷ P t⇩1 ∧ P t⇩2"
  by auto

lemma inj_mset_uprod: "inj mset_uprod"
proof(unfold inj_def, intro allI impI)
  fix a b :: "'a uprod"
  assume "mset_uprod a = mset_uprod b"

  then show "a = b"
    by (cases a; cases b) (auto simp: add_mset_eq_add_mset)
qed

lemma mset_uprod_plus_neq: "mset_uprod a ≠ mset_uprod b + mset_uprod b"
  by( cases a; cases b) (auto simp: add_mset_eq_add_mset)

lemma set_uprod_not_empty [iff]: "set_uprod a ≠ {}"
  by (cases a) simp

global_interpretation uprod_functor: non_empty_finite_natural_functor where
  map = map_uprod and to_set = set_uprod
  by unfold_locales simp

global_interpretation uprod_functor: natural_functor_conversion where
  map = map_uprod and to_set = set_uprod and map_to = map_uprod and map_from = map_uprod and
  map' = map_uprod and to_set' = set_uprod
  by unfold_locales (auto simp: uprod.set_map uprod.map_comp)

lemma uprod_mem_image_iff_prod_mem [simp]:
  assumes "sym I"
  shows "Upair t t' ∈ upair ` I ⟷ (t, t') ∈ I"
  using assms[THEN symD]
  by auto

(* TODO: Report this as nitpick error *)
lemma rep_uprod_UpairI: "P (a, b) ⟹ P (b, a) ⟹ P (rep_uprod (Upair a b))"
  using Quotient3_uprod eq_upair_simps 
  unfolding Upair.abs_eq Quotient3_def
  by (smt (verit, ccfv_threshold) split_pairs2)

lemma rep_uprod_UpairE: "P (rep_uprod (Upair a b)) ⟹ P (a, b) ∨ P (b, a)"
  using Quotient3_uprod eq_upair_simps
  unfolding Upair.abs_eq Quotient3_def
  by (smt (verit, ccfv_threshold) split_pairs2)  

end