(*<*)
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→o" (infixl ‹=› 63)
assumes l_identity:
  "w ⊨ x = y ==> w ⊨ φ x ==> w ⊨ φ y"
begin
  abbreviation notequal (infixl ‹\≠› 63) where
    "notequal ≡ λ x y . \<not>(x = y)"
end

class quantifiable_and_identifiable = quantifiable + identifiable
begin
  definition exists_unique::"('a→o)→o" (binder ‹\∃!› [8] 9) where
    "exists_unique ≡ λ φ . \<exists> α . φ α & (\<forall>β. φ β \<rightarrow> β = α)"
  
  declare exists_unique_def[conn_defs]
end

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

instantiation κ :: identifiable
begin
  definition identity_κ where "identity_κ ≡ basic_identity_\<kappa>"
  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 Π₁ :: identifiable
begin
  definition identity_Π₁ where "identity_Π₁ ≡ basic_identity₁"
  instance proof
    fix F G :: Π₁ and w φ
    show "(w ⊨ F = G) ==> (w ⊨ φ F) ==> (w ⊨ φ G)"
      unfolding identity_Π₁_def using MetaSolver.Eq₁_prop ..
  qed
end

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

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

instantiation o :: identifiable
begin
  definition identity_o where "identity_o ≡ basic_identity₀"
  instance proof
    fix F G :: o and w φ
    show "(w ⊨ F = G) ==> (w ⊨ φ F) ==> (w ⊨ φ G)"
      unfolding identity_o_def using MetaSolver.Eq₀_prop ..
  qed
end

instance ν :: quantifiable_and_identifiable ..
instance Π₁ :: quantifiable_and_identifiable ..
instance Π₂ :: quantifiable_and_identifiable ..
instance Π₃ :: quantifiable_and_identifiable ..
instance o :: 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 ≡ \<lambda>² (λx y. (O!,x^P) & (O!,y^P) & \<box>(\<forall>F. (F,x^P) \<equiv> (F,y^P)))"
  unfolding basic_identity_{E_def} forall_Π₁_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 \<or> (A!,x) & (A!,y) & \<box>(\<forall> F. {x,F} \<equiv> {y,F})"
  unfolding identity_κ_def basic_identity_\κ_def forall_Π₁_def by simp
lemma identity_\ν_def[identity_defs]:
  "(=) ≡ λx y. (x^P) =_E (y^P) \<or> (A!,x^P) & (A!,y^P) & \<box>(\<forall> F. {x^P,F} \<equiv> {y^P,F})"
  unfolding identity_ν_def identity_\κ_def by simp
lemma identity₁_def[identity_defs]:
  "(=) ≡ λF G. \<box>(\<forall> x . {x^P,F} \<equiv> {x^P,G})"
  unfolding identity_Π₁_def basic_identity₁_def forall_ν_def by simp
lemma identity₂_def[identity_defs]:
  "(=) ≡ λF G. \<forall> x. (\<lambda>y. (F,x^P,y^P)) = (\<lambda>y. (G,x^P,y^P))
                    & (\<lambda>y. (F,y^P,x^P)) = (\<lambda>y. (G,y^P,x^P))"
  unfolding identity_Π₂_def identity_Π₁_def basic_identity₂_def forall_ν_def by simp
lemma identity₃_def[identity_defs]:
  "(=) ≡ λF G. \<forall> x y. (\<lambda>z. (F,z^P,x^P,y^P)) = (\<lambda>z. (G,z^P,x^P,y^P))
                      & (\<lambda>z. (F,x^P,z^P,y^P)) = (\<lambda>z. (G,x^P,z^P,y^P))
                      & (\<lambda>z. (F,x^P,y^P,z^P)) = (\<lambda>z. (G,x^P,y^P,z^P))"
  unfolding identity_Π₃_def identity_Π₁_def basic_identity₃_def forall_ν_def by simp
lemma identity_\o_def[identity_defs]: "(=) ≡ λF G. (\<lambda>y. F) = (\<lambda>y. G)"
  unfolding identity_o_def identity_Π₁_def basic_identity₀_def by simp

(*<*)
end
(*>*)