Theory FNDS_Definite_Description

```(* Title: Examples/TTS_Foundations/Foundations/FNDS_Definite_Description.thy
Author: Mihails Milehins
*)
section‹Definite description operator›
theory FNDS_Definite_Description
imports Main
begin

subsection‹Definition and common properties›

definition The_on
where "The_on U P =
(if ∃!x. x ∈ U ∧ P x then Some (THE x. x ∈ U ∧ P x) else None)"

syntax
"_The_on" :: "pttrn ⇒ 'a set ⇒ bool ⇒ 'a option"
("(THE _ on _./ _)" [0, 0, 10] 10)
translations "THE x on U. P" ⇌ "CONST The_on U (λx. P)"

print_translation ‹
[
(
\<^const_syntax>‹The_on›,
fn _ => fn [Ut, Abs abs] =>
let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
in Syntax.const \<^syntax_const>‹_The_on› \$ x \$ Ut \$ t end
)
]
›

lemma The_on_UNIV_eq_The:
assumes "∃!x. P x"
obtains x where "(THE x on UNIV. P x) = Some x" and "(THE x. P x) = x"
unfolding The_on_def by (simp add: assms)

lemma The_on_UNIV_None:
assumes "¬(∃!x. P x)"
shows "(THE x on UNIV. P x) = None"
unfolding The_on_def by (simp add: assms)

lemma The_on_eq_The:
assumes "∃!x. x ∈ U ∧ P x"
obtains x where "(THE x on U. P x) = Some x" and "(THE x. x ∈ U ∧ P x) = x"
unfolding The_on_def by (simp add: assms)

lemma The_on_None:
assumes "¬(∃!x. x ∈ U ∧ P x)"
shows "(THE x on U. P x) = None"
unfolding The_on_def by (auto simp: assms)

lemma The_on_Some_equality[intro]:
assumes "a ∈ U" and "P a" and "⋀x. x ∈ U ⟹ P x ⟹ x = a"
shows "(THE x on U. P x) = Some a"
proof-
from assms have "∃!x. x ∈ U ∧ P x" by auto
moreover have "(THE x. x ∈ U ∧ P x) = a"
apply standard using assms by blast+
ultimately show ?thesis unfolding The_on_def by auto
qed

lemma The_on_equality[intro]:
assumes "a ∈ U" and "P a" and "⋀x. x ∈ U ⟹ P x ⟹ x = a"
shows "the (THE x on U. P x) = a"
by (metis assms option.sel The_on_Some_equality)

lemma The_on_SomeI:
assumes "a ∈ U" and "P a" and "⋀x. x ∈ U ⟹ P x ⟹ x = a"
obtains x where "(THE x on U. P x) = Some x" and "P x"
using assms unfolding The_on_def by (meson that The_on_Some_equality)

lemma The_onI:
assumes "a ∈ U" and "P a" and "⋀x. x ∈ U ⟹ P x ⟹ x = a"
shows "P (the (THE x on U. P x))"
by (metis assms The_on_equality)

lemma The_on_SomeI':
assumes "∃!x. x ∈ U ∧ P x"
obtains x where "(THE x on U. P x) = Some x" and "P x"
by (metis assms The_on_SomeI)

lemma The_onI':
assumes "∃!x. x ∈ U ∧ P x"
shows "P (the (THE x on U. P x))"
by (metis assms The_onI)

lemma The_on_SomeI2:
assumes "a ∈ U"
and "P a"
and "⋀x. x ∈ U ⟹ P x ⟹ x = a"
and "⋀x. x ∈ U ⟹ P x ⟹ Q x"
obtains x where "(THE x on U. P x) = Some x" and "Q x"
using assms by blast

lemma The_on_I2:
assumes "a ∈ U"
and "P a"
and "⋀x. x ∈ U ⟹ P x ⟹ x = a"
and "⋀x. x ∈ U ⟹ P x ⟹ Q x"
shows "Q (the (THE x on U. P x))"
by (metis assms The_on_equality)

lemma The_on_Some1I2:
assumes "∃!x. x ∈ U ∧ P x" and "⋀x. x ∈ U ⟹ P x ⟹ Q x"
obtains x where "(THE x on U. P x) = Some x" and "Q x"
using assms by blast

lemma The_on1I2:
assumes "∃!x. x ∈ U ∧ P x" and "⋀x. x ∈ U ⟹ P x ⟹ Q x"
shows "Q (the (THE x on U. P x))"
by (metis (mono_tags, opaque_lifting) The_on_I2 assms)

lemma The_on1_equality [elim?]:
assumes "∃!x. P x" and "a ∈ U" and "P a"
shows "(THE x on U. P x) = Some a"
using assms by blast

lemma the_sym_eq_trivial:
assumes "x ∈ U"
shows "(THE y on U. x = y) = Some x"
using assms by blast

subsection‹Transfer rules›

lemma The_on_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows "(rel_set A ===> (A ===> (=)) ===> rel_option A) The_on The_on"
proof(intro rel_funI)
fix U and U' and P :: "'a ⇒ bool" and P' :: "'b ⇒ bool"
assume UU'[transfer_rule]: "rel_set A U U'"
and PP'[transfer_rule]: "(A ===> (=)) P P'"
show "rel_option A (THE x on U. P x) (THE x on U'. P' x)"
proof(cases ‹∃!x'. x' ∈ U' ∧ P' x'›)
case True show ?thesis
proof-
from True obtain x' where "x' ∈ U'" and "P' x'" by clarsimp
with True have The_on': "(THE x on U'. P' x) = Some x'"
unfolding The_on_def by auto
from assms(2) obtain x where [transfer_rule]: "A x x'"
unfolding right_total_def by auto
from True have "∀y'∈U'. x' ≠ y' ⟶ (¬P' y')"
by (auto simp: ‹x' ∈ U'› ‹P' x'›)
then have "∀y∈U. x ≠ y ⟶ (¬P y)" by transfer
moreover from ‹P' x'› have "P x" by transfer
ultimately have "∃!x. x ∈ U ∧ P x"
using UU' ‹A x x'› ‹x' ∈ U'› assms(1)
by (auto dest: bi_uniqueDl rel_setD2)
moreover from ‹x' ∈ U'› have "x ∈ U" by transfer
ultimately have The_on: "(THE x on U. P x) = Some x"
using ‹P x› unfolding The_on_def by auto
show ?thesis unfolding The_on The_on' by transfer_prover
qed
next
case nux: False show ?thesis
proof(cases ‹∃x'. x' ∈ U' ∧ P' x'›)
case True show ?thesis
proof-
from True obtain x' where "x' ∈ U'" and "P' x'" by clarsimp
with nux True obtain y' where "y' ∈ U'" and "P' y'" and "x' ≠ y'"
by auto
from assms(2) ‹P' x'› obtain x where [transfer_rule]: "A x x'"
unfolding right_total_def by auto
from assms(2) ‹P' y'› obtain y where [transfer_rule]: "A y y'"
unfolding right_total_def by auto
from ‹P' x'› have "P x" by transfer
moreover from ‹P' y'› have "P y" by transfer
moreover from ‹x' ≠ y'› have "x ≠ y" by transfer
ultimately have "∄!x. x ∈ U ∧ P x"
apply transfer
using UU' ‹A x x'› ‹A y y'› ‹x' ∈ U'› ‹y' ∈ U'› assms(1)
by (blast dest: bi_uniqueDl rel_setD2)
then show ?thesis unfolding The_on_def by (auto simp: nux)
qed
next
case False then show ?thesis
unfolding The_on_def
using PP' UU' by (fastforce dest: rel_funD rel_setD1)
qed
qed
qed

text‹\newpage›

end```