# 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
(*>*)