(* Title: Examples/TTS_Foundations/Foundations/FNDS_Definite_Description.thy Author: Mihails Milehins Copyright 2021 (C) 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