Theory Bounded_Definite_Description

✐‹creator "Kevin Kappelmann"›
subsection ‹Bounded Definite Description›
theory Bounded_Definite_Description
  imports
    Bounded_Quantifiers
begin

consts bthe :: "'a ⇒ ('b ⇒ bool) ⇒ 'b"

open_bundle bounded_the_syntax
begin
syntax "_bthe" :: "[idt, 'a, bool] ⇒ 'b" (‹(3THE _ : _./ _)› [0, 0, 10] 10)
end

syntax_consts "_bthe" ⇌ bthe
translations "THE x : P. Q" ⇌ "CONST bthe P (λx. Q)"

definition "bthe_pred P Q ≡ The (P ⊓ Q)"
adhoc_overloading bthe ⇌ bthe_pred

lemma bthe_eqI [intro]:
  assumes "Q a"
  and "P a"
  and "⋀x. ⟦P x; Q x⟧ ⟹ x = a"
  shows "(THE x : P. Q x) = a"
  unfolding bthe_pred_def by (auto intro: assms)

lemma pred_bthe_if_ex1E:
  assumes "∃!x : P. Q x"
  obtains "P (THE x : P. Q x)" "Q (THE x : P. Q x)"
  unfolding bthe_pred_def inf_fun_def using theI'[OF assms[unfolded bex1_pred_def]]
  by auto

lemma pred_btheI:
  assumes "∃!x : P. Q x"
  shows "P (THE x : P. Q x)"
  using assms by (elim pred_bthe_if_ex1E)

lemma pred_btheI':
  assumes "∃!x : P. Q x"
  shows "Q (THE x : P. Q x)"
  using assms by (elim pred_bthe_if_ex1E)


end