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"

bundle bounded_the_syntax
begin
syntax "_bthe" :: "[idt, 'a, bool] ⇒ 'b" ("(3THE _ : _./ _)" [0, 0, 10] 10)
end
bundle no_bounded_the_syntax
begin
no_syntax "_bthe" :: "[idt, 'a, bool] ⇒ 'b" ("(3THE _ : _./ _)" [0, 0, 10] 10)
end
unbundle bounded_the_syntax
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