Theory FNDS_Definite_Description

(* 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_syntaxThe_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 "yU. 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