Theory TAO_6_Identifiable

theory TAO_6_Identifiable
imports TAO_5_MetaSolver
(*<*)
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 . xP = yP"
  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_identity1"
  instance proof
    fix F G :: Π1 and w φ
    show "(w ⊨ F = G) ⟹ (w ⊨ φ F) ⟹ (w ⊨ φ G)"
      unfolding identity_Π1_def using MetaSolver.Eq1_prop ..
  qed
end

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

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

instantiation 𝗈 :: identifiable
begin
  definition identity_𝗈 where "identity_𝗈 ≡ basic_identity0"
  instance proof
    fix F G :: 𝗈 and w φ
    show "(w ⊨ F = G) ⟹ (w ⊨ φ F) ⟹ (w ⊨ φ G)"
      unfolding identity_𝗈_def using MetaSolver.Eq0_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 identityE_def[identity_defs]:
  "basic_identityEλ2 (λx y. ⦇O!,xP& ⦇O!,yP& (F. ⦇F,xP ⦇F,yP⦈))"
  unfolding basic_identityE_def forall_Π1_def by simp
lemma identityE_infix_def[identity_defs]:
  "x =E y ≡ ⦇basic_identityE,x,y⦈" using basic_identityE_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. (xP) =E (yP)  ⦇A!,xP& ⦇A!,yP& ( F. ⦃xP,F⦄  ⦃yP,F⦄)"
  unfolding identity_ν_def identityκ_def by simp
lemma identity1_def[identity_defs]:
  "(=) ≡ λF G. ( x . ⦃xP,F⦄  ⦃xP,G⦄)"
  unfolding identity_Π1_def basic_identity1_def forall_ν_def by simp
lemma identity2_def[identity_defs]:
  "(=) ≡ λF G.  x. (λy. ⦇F,xP,yP⦈) = (λy. ⦇G,xP,yP⦈)
                    & (λy. ⦇F,yP,xP⦈) = (λy. ⦇G,yP,xP⦈)"
  unfolding identity_Π2_def identity_Π1_def basic_identity2_def forall_ν_def by simp
lemma identity3_def[identity_defs]:
  "(=) ≡ λF G.  x y. (λz. ⦇F,zP,xP,yP⦈) = (λz. ⦇G,zP,xP,yP⦈)
                      & (λz. ⦇F,xP,zP,yP⦈) = (λz. ⦇G,xP,zP,yP⦈)
                      & (λz. ⦇F,xP,yP,zP⦈) = (λz. ⦇G,xP,yP,zP⦈)"
  unfolding identity_Π3_def identity_Π1_def basic_identity3_def forall_ν_def by simp
lemma identity𝗈_def[identity_defs]: "(=) ≡ λF G. (λy. F) = (λy. G)"
  unfolding identity_𝗈_def identity_Π1_def basic_identity0_def by simp

(*<*)
end
(*>*)