Theory TAO_6_Identifiable

(*<*)
theory TAO_6_Identifiable
imports TAO_5_MetaSolver
begin
(*>*)

section‹General Identity›
text‹\label{TAO_Identifiable}›

text‹
\begin{remark}
  In order to define a general identity symbol that can act
  on all types of terms a type class is introduced
  which assumes the substitution property which
  is needed to derive the corresponding axiom.
  This type class is instantiated for all relation types, individual terms
  and individuals.
\end{remark}
›

subsection‹Type Classes›
text‹\label{TAO_Identifiable_Class}›

class identifiable =
fixes identity :: "'a⇒'a⇒𝗈" (infixl ‹❙=› 63)
assumes l_identity:
  "w ⊨ x ❙= y ⟹ w ⊨ φ x ⟹ w ⊨ φ y"
begin
  abbreviation notequal (infixl ‹❙≠› 63) where
    "notequal ≡ λ x y . ❙¬(x ❙= y)"
end

class quantifiable_and_identifiable = quantifiable + identifiable
begin
  definition exists_unique::"('a⇒𝗈)⇒𝗈" (binder ‹❙∃!› [8] 9) where
    "exists_unique ≡ λ φ . ❙∃ α . φ α ❙& (❙∀β. φ β ❙→ β ❙= α)"
  
  declare exists_unique_def[conn_defs]
end

subsection‹Instantiations›
text‹\label{TAO_Identifiable_Instantiation}›

instantiation κ :: identifiable
begin
  definition identity_κ where "identity_κ ≡ basic_identity⇩κ"
  instance proof
    fix x y :: κ and w φ
    show "[x ❙= y in w] ⟹ [φ x in w] ⟹ [φ y in w]"
      unfolding identity_κ_def
      using MetaSolver.Eqκ_prop ..
  qed
end

instantiation ν :: identifiable
begin
  definition identity_ν where "identity_ν ≡ λ x y . x⇧P ❙= y⇧P"
  instance proof
    fix α :: ν and β :: ν and v φ
    assume "v ⊨ α ❙= β"
    hence "v ⊨ α⇧P ❙= β⇧P"
      unfolding identity_ν_def by auto
    hence "⋀φ.(v ⊨ φ (α⇧P)) ⟹ (v ⊨ φ (β⇧P))"
      using l_identity by auto
    hence "(v ⊨ φ (rep (α⇧P))) ⟹ (v ⊨ φ (rep (β⇧P)))"
      by meson
    thus "(v ⊨ φ α) ⟹ (v ⊨ φ β)"
      by (simp only: rep_proper_id)
  qed
end

instantiation Π⇩1 :: identifiable
begin
  definition identity_Π⇩1 where "identity_Π⇩1 ≡ basic_identity⇩1"
  instance proof
    fix F G :: Π⇩1 and w φ
    show "(w ⊨ F ❙= G) ⟹ (w ⊨ φ F) ⟹ (w ⊨ φ G)"
      unfolding identity_Π⇩1_def using MetaSolver.Eq⇩1_prop ..
  qed
end

instantiation Π⇩2 :: identifiable
begin
  definition identity_Π⇩2 where "identity_Π⇩2 ≡ basic_identity⇩2"
  instance proof
    fix F G :: Π⇩2 and w φ
    show "(w ⊨ F ❙= G) ⟹ (w ⊨ φ F) ⟹ (w ⊨ φ G)"
      unfolding identity_Π⇩2_def using MetaSolver.Eq⇩2_prop ..
  qed
end

instantiation Π⇩3 :: identifiable
begin
  definition identity_Π⇩3 where "identity_Π⇩3 ≡ basic_identity⇩3"
  instance proof
    fix F G :: Π⇩3 and w φ
    show "(w ⊨ F ❙= G) ⟹ (w ⊨ φ F) ⟹ (w ⊨ φ G)"
      unfolding identity_Π⇩3_def using MetaSolver.Eq⇩3_prop ..
  qed
end

instantiation 𝗈 :: identifiable
begin
  definition identity_𝗈 where "identity_𝗈 ≡ basic_identity⇩0"
  instance proof
    fix F G :: 𝗈 and w φ
    show "(w ⊨ F ❙= G) ⟹ (w ⊨ φ F) ⟹ (w ⊨ φ G)"
      unfolding identity_𝗈_def using MetaSolver.Eq⇩0_prop ..
  qed
end

instance ν :: quantifiable_and_identifiable ..
instance Π⇩1 :: quantifiable_and_identifiable ..
instance Π⇩2 :: quantifiable_and_identifiable ..
instance Π⇩3 :: quantifiable_and_identifiable ..
instance 𝗈 :: quantifiable_and_identifiable ..

subsection‹New Identity Definitions›
text‹\label{TAO_Identifiable_Definitions}›

text‹
\begin{remark}
  The basic definitions of identity use type specific quantifiers
  and identity symbols. Equivalent definitions that
  use the general identity symbol and general quantifiers are provided.
\end{remark}
›

named_theorems identity_defs
lemma identity⇩E_def[identity_defs]:
  "basic_identity⇩E ≡ ❙λ⇧2 (λx y. ⦇O!,x⇧P⦈ ❙& ⦇O!,y⇧P⦈ ❙& ❙□(❙∀F. ⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈))"
  unfolding basic_identity⇩E_def forall_Π⇩1_def by simp
lemma identity⇩E_infix_def[identity_defs]:
  "x ❙=⇩E y ≡ ⦇basic_identity⇩E,x,y⦈" using basic_identity⇩E_infix_def .
lemma identity⇩κ_def[identity_defs]:
  "(❙=) ≡ λx y. x ❙=⇩E y ❙∨ ⦇A!,x⦈ ❙& ⦇A!,y⦈ ❙& ❙□(❙∀ F. ⦃x,F⦄ ❙≡ ⦃y,F⦄)"
  unfolding identity_κ_def basic_identity⇩κ_def forall_Π⇩1_def by simp
lemma identity⇩ν_def[identity_defs]:
  "(❙=) ≡ λx y. (x⇧P) ❙=⇩E (y⇧P) ❙∨ ⦇A!,x⇧P⦈ ❙& ⦇A!,y⇧P⦈ ❙& ❙□(❙∀ F. ⦃x⇧P,F⦄ ❙≡ ⦃y⇧P,F⦄)"
  unfolding identity_ν_def identity⇩κ_def by simp
lemma identity⇩1_def[identity_defs]:
  "(❙=) ≡ λF G. ❙□(❙∀ x . ⦃x⇧P,F⦄ ❙≡ ⦃x⇧P,G⦄)"
  unfolding identity_Π⇩1_def basic_identity⇩1_def forall_ν_def by simp
lemma identity⇩2_def[identity_defs]:
  "(❙=) ≡ λF G. ❙∀ x. (❙λy. ⦇F,x⇧P,y⇧P⦈) ❙= (❙λy. ⦇G,x⇧P,y⇧P⦈)
                    ❙& (❙λy. ⦇F,y⇧P,x⇧P⦈) ❙= (❙λy. ⦇G,y⇧P,x⇧P⦈)"
  unfolding identity_Π⇩2_def identity_Π⇩1_def basic_identity⇩2_def forall_ν_def by simp
lemma identity⇩3_def[identity_defs]:
  "(❙=) ≡ λF G. ❙∀ x y. (❙λz. ⦇F,z⇧P,x⇧P,y⇧P⦈) ❙= (❙λz. ⦇G,z⇧P,x⇧P,y⇧P⦈)
                      ❙& (❙λz. ⦇F,x⇧P,z⇧P,y⇧P⦈) ❙= (❙λz. ⦇G,x⇧P,z⇧P,y⇧P⦈)
                      ❙& (❙λz. ⦇F,x⇧P,y⇧P,z⇧P⦈) ❙= (❙λz. ⦇G,x⇧P,y⇧P,z⇧P⦈)"
  unfolding identity_Π⇩3_def identity_Π⇩1_def basic_identity⇩3_def forall_ν_def by simp
lemma identity⇩𝗈_def[identity_defs]: "(❙=) ≡ λF G. (❙λy. F) ❙= (❙λy. G)"
  unfolding identity_𝗈_def identity_Π⇩1_def basic_identity⇩0_def by simp

(*<*)
end
(*>*)