Theory First_Order_Clause.HOL_Extra

theory HOL_Extra
  imports Main
begin

lemmas UniqI = Uniq_I

lemma Uniq_prodI:
  assumes "⋀x1 y1 x2 y2. P x1 y1 ⟹ P x2 y2 ⟹ (x1, y1) = (x2, y2)"
  shows "∃⇩≤⇩1(x, y). P x y"
  using assms
  by (metis UniqI case_prodE)

lemma Uniq_implies_ex1: "∃⇩≤⇩1x. P x ⟹ P y ⟹ ∃!x. P x"
  by (iprover intro: ex1I dest: Uniq_D)

lemma Uniq_antimono: "Q ≤ P ⟹ Uniq Q ≥ Uniq P"
  unfolding le_fun_def le_bool_def
  by (rule impI) (simp only: Uniq_I Uniq_D)

lemma Uniq_antimono': "(⋀x. Q x ⟹ P x) ⟹ Uniq P ⟹ Uniq Q"
  by (fact Uniq_antimono[unfolded le_fun_def le_bool_def, rule_format])

lemma Collect_eq_if_Uniq: "(∃⇩≤⇩1x. P x) ⟹ {x. P x} = {} ∨ (∃x. {x. P x} = {x})"
  using Uniq_D by fastforce

lemma Collect_eq_if_Uniq_prod:
  "(∃⇩≤⇩1(x, y). P x y) ⟹ {(x, y). P x y} = {} ∨ (∃x y. {(x, y). P x y} = {(x, y)})"
  using Collect_eq_if_Uniq by fastforce

lemma Ball_Ex_comm:
  "(∀x ∈ X. ∃f. P (f x) x) ⟹ (∃f. ∀x ∈ X. P (f x) x)"
  "(∃f. ∀x ∈ X. P (f x) x) ⟹ (∀x ∈ X. ∃f. P (f x) x)"
  by meson+

lemma set_map_id:
  assumes "x ∈ set X" "f x ∉ set X" "map f X = X"
  shows False
  using assms
  by(induction X) auto

lemma Ball_singleton: "(∀x ∈ {x}. P x) ⟷ P x"
  by simp

end