Quelle  TAO_1_Embedding.thy

(*<*)
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 o = "UNIV::(j==>i==>bool) set"
  morphisms evalo makeo .. ― ‹truth values›

type_synonym Π₀ = o ― ‹zero place relations›
typedef Π₁ = "UNIV::(υ==>j==>i==>bool) set"
  morphisms evalΠ₁ makeΠ₁ .. ― ‹one place relations›
typedef Π₂ = "UNIV::(υ==>υ==>j==>i==>bool) set"
  morphisms evalΠ₂ makeΠ₂ .. ― ‹two place relations›
typedef Π₃ = "UNIV::(υ==>υ==>υ==>j==>i==>bool) set"
  morphisms evalΠ₃ makeΠ₃ .. ― ‹three place relations›

type_synonym α = "Π₁ set" ― ‹abstract objects›

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

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

setup_lifting type_definition_o
setup_lifting type_definition_κ
setup_lifting type_definition_Π₁
setup_lifting type_definition_Π₂
setup_lifting type_definition_Π₃

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::"(ν==>o)==>κ" (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::"Π₀==>o" (‹(_)›) is id .
lift_definition exe1::"Π₁==>κ==>o" (‹(_,_)›) is
  "λ F x s w . (proper x) ∧ F (νυ (rep x)) s w" .
lift_definition exe2::"Π₂==>κ==>κ==>o" (‹(_,_,_)›) is
  "λ F x y s w . (proper x) ∧ (proper y) ∧
     F (νυ (rep x)) (νυ (rep y)) s w" .
lift_definition exe3::"Π₃==>κ==>κ==>κ==>o" (‹(_,_,_,_)›) 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 :: "κ==>Π₁==>o" (‹{_,_}›) 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 :: "o==>o" (‹\¬_› [54] 70) is
  "λ p s w . s = dj ∧ ¬p dj w ∨ s ≠ dj ∧ (I_NOT s (p s) w)" .
lift_definition impl :: "o==>o==>o" (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_\<nu> :: "(ν==>o)==>o" (binder ‹\∀_\ν› [8] 9) is
  "λ φ s w . ∀ x :: ν . (φ x) s w" .
lift_definition forall₀ :: "(Π₀==>o)==>o" (binder ‹\∀₀› [8] 9) is
  "λ φ s w . ∀ x :: Π₀ . (φ x) s w" .
lift_definition forall₁ :: "(Π₁==>o)==>o" (binder ‹\∀₁› [8] 9) is
  "λ φ s w . ∀ x :: Π₁ . (φ x) s w" .
lift_definition forall₂ :: "(Π₂==>o)==>o" (binder ‹\∀₂› [8] 9) is
  "λ φ s w . ∀ x :: Π₂ . (φ x) s w" .
lift_definition forall₃ :: "(Π₃==>o)==>o" (binder ‹\∀₃› [8] 9) is
  "λ φ s w . ∀ x :: Π₃ . (φ x) s w" .
lift_definition forall_\<o> :: "(o==>o)==>o" (binder ‹\∀_\o› [8] 9) is
  "λ φ s w . ∀ x :: o . (φ x) s w" .
lift_definition box :: "o==>o" (‹\◻_› [62] 63) is
  "λ p s w . ∀ v . p s v" .
lift_definition actual :: "o==>o" (‹\A_› [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 :: "o==>Π₀" (‹\λ⁰›) is id .
lift_definition lambdabinder1 :: "(ν==>o)==>Π₁" (binder ‹\λ› [8] 9) is
  "λ φ u s w . ∃ x . νυ x = u ∧ φ x s w" .
lift_definition lambdabinder2 :: "(ν==>ν==>o)==>Π₂" (‹\λ²›) is
  "λ φ u v s w . ∃ x y . νυ x = u ∧ νυ y = v ∧ φ x y s w" .
lift_definition lambdabinder3 :: "(ν==>ν==>ν==>o)==>Π₃" (‹\λ³›) 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 :: "(κ==>o)==>bool" is
  "λ φ . ∀ x v . (∃ a . νυ a = νυ x ∧ (φ (a^P) dj v)) = (φ (x^P) dj v)" .
lift_definition IsProperInXY :: "(κ==>κ==>o)==>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 :: "(κ==>κ==>κ==>o)==>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==>o==>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::"Π₁" (‹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_\<nu>_def[meta_defs]
        forall₀_def[meta_defs] forall₁_def[meta_defs]
        forall₂_def[meta_defs] forall₃_def[meta_defs] forall_\<o>_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]

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

declare makeκ_inverse[meta_aux] evalκ_inverse[meta_aux]
        makeo_inverse[meta_aux] evalo_inverse[meta_aux]
        makeΠ₁_inverse[meta_aux] evalΠ₁_inverse[meta_aux]
        makeΠ₂_inverse[meta_aux] evalΠ₂_inverse[meta_aux]
        makeΠ₃_inverse[meta_aux] evalΠ₃_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Π₁_aux[meta_aux]:
  "makeΠ₁ (λu s w. ∃x. νυ x = u ∧ evalΠ₁ 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Π₂_aux[meta_aux]:
  "makeΠ₂ (λu v s w. ∃x . νυ x = u ∧ (∃ y . νυ y = v ∧ evalΠ₂ 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Π₃_aux[meta_aux]:
  "makeΠ₃ (λu v r s w. ∃x. νυ x = u ∧ (∃y. νυ y = v ∧
   (∃z. νυ z = r ∧ evalΠ₃ 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
(*>*)