Theory TAO_1_Embedding

(*<*)
theory TAO_1_Embedding
imports Main
begin
(*>*)

section‹Representation Layer›
text‹\label{TAO_Embedding}›

subsection‹Primitives›
text‹\label{TAO_Embedding_Primitives}›

typedecl i ― ‹possible worlds›
typedecl j ― ‹states›

consts dw :: i ― ‹actual world›
consts dj :: j ― ‹actual state›

typedecl ω ― ‹ordinary objects›
typedecl σ ― ‹special urelements›
datatype υ = ωυ ω | συ σ ― ‹urelements›

subsection‹Derived Types›
text‹\label{TAO_Embedding_Derived_Types}›

typedef 𝗈 = "UNIV::(j⇒i⇒bool) set"
  morphisms eval𝗈 make𝗈 .. ― ‹truth values›

type_synonym Π⇩0 = 𝗈 ― ‹zero place relations›
typedef Π⇩1 = "UNIV::(υ⇒j⇒i⇒bool) set"
  morphisms evalΠ⇩1 makeΠ⇩1 .. ― ‹one place relations›
typedef Π⇩2 = "UNIV::(υ⇒υ⇒j⇒i⇒bool) set"
  morphisms evalΠ⇩2 makeΠ⇩2 .. ― ‹two place relations›
typedef Π⇩3 = "UNIV::(υ⇒υ⇒υ⇒j⇒i⇒bool) set"
  morphisms evalΠ⇩3 makeΠ⇩3 .. ― ‹three place relations›

type_synonym α = "Π⇩1 set" ― ‹abstract objects›

datatype ν = ων ω | αν α ― ‹individuals›

typedef κ = "UNIV::(ν option) set"
  morphisms evalκ makeκ .. ― ‹individual terms›

setup_lifting type_definition_𝗈
setup_lifting type_definition_κ
setup_lifting type_definition_Π⇩1
setup_lifting type_definition_Π⇩2
setup_lifting type_definition_Π⇩3

subsection‹Individual Terms and Definite Descriptions›
text‹\label{TAO_Embedding_IndividualTerms}›

lift_definition νκ :: "ν⇒κ" ("_⇧P" [90] 90) is Some .
lift_definition proper :: "κ⇒bool" is "(≠) None" .
lift_definition rep :: "κ⇒ν" is the .

lift_definition that::"(ν⇒𝗈)⇒κ" (binder "❙ι" [8] 9) is
  "λ φ . if (∃! x . (φ x) dj dw)
         then Some (THE x . (φ x) dj dw)
         else None" .

subsection‹Mapping from Individuals to Urelements›
text‹\label{TAO_Embedding_AbstractObjectsToSpecialUrelements}›

consts ασ :: "α⇒σ"
axiomatization where ασ_surj: "surj ασ"
definition νυ :: "ν⇒υ" where "νυ ≡ case_ν ωυ (συ ∘ ασ)"

subsection‹Exemplification of n-place-Relations.›
text‹\label{TAO_Embedding_Exemplification}›

lift_definition exe0::"Π⇩0⇒𝗈" ("⦇_⦈") is id .
lift_definition exe1::"Π⇩1⇒κ⇒𝗈" ("⦇_,_⦈") is
  "λ F x s w . (proper x) ∧ F (νυ (rep x)) s w" .
lift_definition exe2::"Π⇩2⇒κ⇒κ⇒𝗈" ("⦇_,_,_⦈") is
  "λ F x y s w . (proper x) ∧ (proper y) ∧
     F (νυ (rep x)) (νυ (rep y)) s w" .
lift_definition exe3::"Π⇩3⇒κ⇒κ⇒κ⇒𝗈" ("⦇_,_,_,_⦈") is
"λ F x y z s w . (proper x) ∧ (proper y) ∧ (proper z) ∧
   F (νυ (rep x)) (νυ (rep y)) (νυ (rep z)) s w" .

subsection‹Encoding›
text‹\label{TAO_Embedding_Encoding}›

lift_definition enc :: "κ⇒Π⇩1⇒𝗈" ("⦃_,_⦄") is
  "λ x F s w . (proper x) ∧ case_ν (λ ω . False) (λ α . F ∈ α) (rep x)" .

subsection‹Connectives and Quantifiers›
text‹\label{TAO_Embedding_Connectives}›

consts I_NOT :: "j⇒(i⇒bool)⇒i⇒bool"
consts I_IMPL :: "j⇒(i⇒bool)⇒(i⇒bool)⇒(i⇒bool)"

lift_definition not :: "𝗈⇒𝗈" ("❙¬_" [54] 70) is
  "λ p s w . s = dj ∧ ¬p dj w ∨ s ≠ dj ∧ (I_NOT s (p s) w)" .
lift_definition impl :: "𝗈⇒𝗈⇒𝗈" (infixl "❙→" 51) is
  "λ p q s w . s = dj ∧ (p dj w ⟶ q dj w) ∨ s ≠ dj ∧ (I_IMPL s (p s) (q s) w)" .
lift_definition forall⇩ν :: "(ν⇒𝗈)⇒𝗈" (binder "❙∀⇩ν" [8] 9) is
  "λ φ s w . ∀ x :: ν . (φ x) s w" .
lift_definition forall⇩0 :: "(Π⇩0⇒𝗈)⇒𝗈" (binder "❙∀⇩0" [8] 9) is
  "λ φ s w . ∀ x :: Π⇩0 . (φ x) s w" .
lift_definition forall⇩1 :: "(Π⇩1⇒𝗈)⇒𝗈" (binder "❙∀⇩1" [8] 9) is
  "λ φ s w . ∀ x :: Π⇩1  . (φ x) s w" .
lift_definition forall⇩2 :: "(Π⇩2⇒𝗈)⇒𝗈" (binder "❙∀⇩2" [8] 9) is
  "λ φ s w . ∀ x :: Π⇩2  . (φ x) s w" .
lift_definition forall⇩3 :: "(Π⇩3⇒𝗈)⇒𝗈" (binder "❙∀⇩3" [8] 9) is
  "λ φ s w . ∀ x :: Π⇩3  . (φ x) s w" .
lift_definition forall⇩𝗈 :: "(𝗈⇒𝗈)⇒𝗈" (binder "❙∀⇩𝗈" [8] 9) is
  "λ φ s w . ∀ x :: 𝗈  . (φ x) s w" .
lift_definition box :: "𝗈⇒𝗈" ("❙□_" [62] 63) is
  "λ p s w . ∀ v . p s v" .
lift_definition actual :: "𝗈⇒𝗈" ("❙𝒜_" [64] 65) is
  "λ p s w . p s dw" .

text‹
\begin{remark}
  The connectives behave classically if evaluated for the actual state @{term "dj"},
  whereas their behavior is governed by uninterpreted constants for any
  other state.
\end{remark}
›

subsection‹Lambda Expressions›
text‹\label{TAO_Embedding_Lambda}›

text‹
\begin{remark}
  Lambda expressions have to convert maps from individuals to propositions to
  relations that are represented by maps from urelements to truth values.
\end{remark}
›

lift_definition lambdabinder0 :: "𝗈⇒Π⇩0" ("❙λ⇧0") is id .
lift_definition lambdabinder1 :: "(ν⇒𝗈)⇒Π⇩1" (binder "❙λ" [8] 9) is
  "λ φ u s w . ∃ x . νυ x = u ∧ φ x s w" .
lift_definition lambdabinder2 :: "(ν⇒ν⇒𝗈)⇒Π⇩2" ("❙λ⇧2") is
  "λ φ u v s w . ∃ x y . νυ x = u ∧ νυ y = v ∧ φ x y s w" .
lift_definition lambdabinder3 :: "(ν⇒ν⇒ν⇒𝗈)⇒Π⇩3" ("❙λ⇧3") is
  "λ φ u v r s w . ∃ x y z . νυ x = u ∧ νυ y = v ∧ νυ z = r ∧ φ x y z s w" .

subsection‹Proper Maps›
text‹\label{TAO_Embedding_Proper}›

text‹
\begin{remark}
  The embedding introduces the notion of \emph{proper} maps from
  individual terms to propositions.

  Such a map is proper if and only if for all proper individual terms its truth evaluation in the
  actual state only depends on the urelements corresponding to the individuals the terms denote.

  Proper maps are exactly those maps that - when used as matrix of a lambda-expression - unconditionally
  allow beta-reduction.
\end{remark}
›

lift_definition IsProperInX :: "(κ⇒𝗈)⇒bool" is
  "λ φ . ∀ x v . (∃ a . νυ a = νυ x ∧ (φ (a⇧P) dj v)) = (φ (x⇧P) dj v)" .
lift_definition IsProperInXY :: "(κ⇒κ⇒𝗈)⇒bool" is
  "λ φ . ∀ x y v . (∃ a b . νυ a = νυ x ∧ νυ b = νυ y
                    ∧ (φ (a⇧P) (b⇧P) dj v)) = (φ (x⇧P) (y⇧P) dj v)" .
lift_definition IsProperInXYZ :: "(κ⇒κ⇒κ⇒𝗈)⇒bool" is
  "λ φ . ∀ x y z v . (∃ a b c . νυ a = νυ x ∧ νυ b = νυ y ∧ νυ c = νυ z
                      ∧ (φ (a⇧P) (b⇧P) (c⇧P) dj v)) = (φ (x⇧P) (y⇧P) (z⇧P) dj v)" .


subsection‹Validity› 
text‹\label{TAO_Embedding_Validity}›

lift_definition valid_in :: "i⇒𝗈⇒bool" (infixl "⊨" 5) is
  "λ v φ . φ dj v" .

text‹
\begin{remark}
  A formula is considered semantically valid for a possible world,
  if it evaluates to @{term "True"} for the actual state @{term "dj"}
  and the given possible world.
\end{remark}
›

subsection‹Concreteness›
text‹\label{TAO_Embedding_Concreteness}›

consts ConcreteInWorld :: "ω⇒i⇒bool"

abbreviation (input) OrdinaryObjectsPossiblyConcrete where
  "OrdinaryObjectsPossiblyConcrete ≡ ∀ x . ∃ v . ConcreteInWorld x v"
abbreviation (input) PossiblyContingentObjectExists where
  "PossiblyContingentObjectExists ≡ ∃ x v . ConcreteInWorld x v
                                        ∧ (∃ w . ¬ ConcreteInWorld x w)"
abbreviation (input) PossiblyNoContingentObjectExists where
  "PossiblyNoContingentObjectExists ≡ ∃ w . ∀ x . ConcreteInWorld x w
                                        ⟶ (∀ v . ConcreteInWorld x v)"
axiomatization where
  OrdinaryObjectsPossiblyConcreteAxiom:
    "OrdinaryObjectsPossiblyConcrete"
  and PossiblyContingentObjectExistsAxiom:
    "PossiblyContingentObjectExists"
  and PossiblyNoContingentObjectExistsAxiom:
    "PossiblyNoContingentObjectExists"

text‹
\begin{remark}
  Care has to be taken that the defined notion of concreteness
  coincides with the meta-logical distinction between
  abstract objects and ordinary objects. Furthermore the axioms about
  concreteness have to be satisfied. This is achieved by introducing an
  uninterpreted constant @{term "ConcreteInWorld"} that determines whether
  an ordinary object is concrete in a given possible world. This constant is
  axiomatized, such that all ordinary objects are possibly concrete, contingent
  objects possibly exist and possibly no contingent objects exist.
\end{remark}
›


lift_definition Concrete::"Π⇩1" ("E!") is
  "λ u s w . case u of ωυ x ⇒ ConcreteInWorld x w | _ ⇒ False" .

text‹
\begin{remark}
  Concreteness of ordinary objects is now defined using this
  axiomatized uninterpreted constant. Abstract objects on the other
  hand are never concrete.
\end{remark}
›

subsection‹Collection of Meta-Definitions›
text‹\label{TAO_Embedding_meta_defs}›

named_theorems meta_defs

declare not_def[meta_defs] impl_def[meta_defs] forall⇩ν_def[meta_defs]
        forall⇩0_def[meta_defs] forall⇩1_def[meta_defs]
        forall⇩2_def[meta_defs] forall⇩3_def[meta_defs] forall⇩𝗈_def[meta_defs]
        box_def[meta_defs] actual_def[meta_defs] that_def[meta_defs]
        lambdabinder0_def[meta_defs] lambdabinder1_def[meta_defs]
        lambdabinder2_def[meta_defs] lambdabinder3_def[meta_defs]
        exe0_def[meta_defs] exe1_def[meta_defs] exe2_def[meta_defs]
        exe3_def[meta_defs] enc_def[meta_defs] inv_def[meta_defs]
        that_def[meta_defs] valid_in_def[meta_defs] Concrete_def[meta_defs]

declare [[smt_solver = cvc4]]
declare [[simp_depth_limit = 10]] (* prevent the simplifier from running forever *)
declare [[unify_search_bound = 40]] (* prevent unification bound errors *)

subsection‹Auxiliary Lemmata›
text‹\label{TAO_Embedding_Aux}›
  
named_theorems meta_aux

declare makeκ_inverse[meta_aux] evalκ_inverse[meta_aux]
        make𝗈_inverse[meta_aux] eval𝗈_inverse[meta_aux]
        makeΠ⇩1_inverse[meta_aux] evalΠ⇩1_inverse[meta_aux]
        makeΠ⇩2_inverse[meta_aux] evalΠ⇩2_inverse[meta_aux]
        makeΠ⇩3_inverse[meta_aux] evalΠ⇩3_inverse[meta_aux]
lemma νυ_ων_is_ωυ[meta_aux]: "νυ (ων x) = ωυ x" by (simp add: νυ_def)
lemma rep_proper_id[meta_aux]: "rep (x⇧P) = x"
  by (simp add: meta_aux νκ_def rep_def)
lemma νκ_proper[meta_aux]: "proper (x⇧P)"
  by (simp add: meta_aux νκ_def proper_def)
lemma no_αω[meta_aux]: "¬(νυ (αν x) = ωυ y)" by (simp add: νυ_def)
lemma no_σω[meta_aux]: "¬(συ x = ωυ y)" by blast
lemma νυ_surj[meta_aux]: "surj νυ"
  using ασ_surj unfolding νυ_def surj_def
  by (metis ν.simps(5) ν.simps(6) υ.exhaust comp_apply)
lemma lambdaΠ⇩1_aux[meta_aux]:
  "makeΠ⇩1 (λu s w. ∃x. νυ x = u ∧ evalΠ⇩1 F (νυ x) s w) = F"
  proof -
    have "⋀ u s w φ . (∃ x . νυ x = u ∧ φ (νυ x) (s::j) (w::i)) ⟷ φ u s w"
      using νυ_surj unfolding surj_def by metis
    thus ?thesis apply transfer by simp
  qed
lemma lambdaΠ⇩2_aux[meta_aux]:
  "makeΠ⇩2 (λu v s w. ∃x . νυ x = u ∧ (∃ y . νυ y = v ∧ evalΠ⇩2 F (νυ x) (νυ y) s w)) = F"
  proof -
    have "⋀ u v (s ::j) (w::i) φ .
      (∃ x . νυ x = u ∧ (∃ y . νυ y = v ∧ φ (νυ x) (νυ y) s w))
      ⟷ φ u v s w"
      using νυ_surj unfolding surj_def by metis
    thus ?thesis apply transfer by simp
  qed
lemma lambdaΠ⇩3_aux[meta_aux]:
  "makeΠ⇩3 (λu v r s w. ∃x. νυ x = u ∧ (∃y. νυ y = v ∧
   (∃z. νυ z = r ∧ evalΠ⇩3 F (νυ x) (νυ y) (νυ z) s w))) = F"
  proof -
    have "⋀ u v r (s::j) (w::i) φ . ∃x. νυ x = u ∧ (∃y. νυ y = v
          ∧ (∃z. νυ z = r ∧ φ (νυ x) (νυ y) (νυ z) s w)) = φ u v r s w"
      using νυ_surj unfolding surj_def by metis
    thus ?thesis apply transfer apply (rule ext)+ by metis
  qed
(*<*)
end
(*>*)