Theory TAO_3_Quantifiable

(*<*)
theory TAO_3_Quantifiable
imports TAO_2_Semantics
begin
(*>*)

section‹General Quantification›
text‹\label{TAO_Quantifiable}›

text‹
\begin{remark}
  In order to define general quantifiers that can act
  on individuals as well as relations a type class
  is introduced which assumes the semantics of the all quantifier.
  This type class is then instantiated for individuals and
  relations.
\end{remark}
›

subsection‹Type Class›
text‹\label{TAO_Quantifiable_Class}›

class quantifiable = fixes forall :: "('a⇒𝗈)⇒𝗈" (binder "❙∀" [8] 9)
  assumes quantifiable_T8: "(w ⊨ (❙∀ x . ψ x)) = (∀ x . (w ⊨ (ψ x)))"
begin
end

lemma (in Semantics) T8: shows "(w ⊨ ❙∀ x . ψ x) = (∀ x . (w ⊨ ψ x))"
  using quantifiable_T8 .

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

instantiation ν :: quantifiable
begin
  definition forall_ν :: "(ν⇒𝗈)⇒𝗈" where "forall_ν ≡ forall⇩ν"
  instance proof
    fix w :: i and ψ :: "ν⇒𝗈"
    show "(w ⊨ ❙∀x. ψ x) = (∀x. (w ⊨ ψ x))"
      unfolding forall_ν_def using Semantics.T8_ν .
  qed
end

instantiation 𝗈 :: quantifiable
begin
  definition forall_𝗈 :: "(𝗈⇒𝗈)⇒𝗈" where "forall_𝗈 ≡ forall⇩𝗈"
  instance proof
    fix w :: i and ψ :: "𝗈⇒𝗈"
    show "(w ⊨ ❙∀x. ψ x) = (∀x. (w ⊨ ψ x))"
      unfolding forall_𝗈_def using Semantics.T8_𝗈 .
  qed
end

instantiation Π⇩1 :: quantifiable
begin
  definition forall_Π⇩1 :: "(Π⇩1⇒𝗈)⇒𝗈" where "forall_Π⇩1 ≡ forall⇩1"
  instance proof
    fix w :: i and ψ :: "Π⇩1⇒𝗈"
    show "(w ⊨ ❙∀x. ψ x) = (∀x. (w ⊨ ψ x))"
      unfolding forall_Π⇩1_def using Semantics.T8_1 .
  qed
end

instantiation Π⇩2 :: quantifiable
begin
  definition forall_Π⇩2 :: "(Π⇩2⇒𝗈)⇒𝗈" where "forall_Π⇩2 ≡ forall⇩2"
  instance proof
    fix w :: i and ψ :: "Π⇩2⇒𝗈"
    show "(w ⊨ ❙∀x. ψ x) = (∀x. (w ⊨ ψ x))"
      unfolding forall_Π⇩2_def using Semantics.T8_2 .
  qed
end

instantiation Π⇩3 :: quantifiable
begin
  definition forall_Π⇩3 :: "(Π⇩3⇒𝗈)⇒𝗈" where "forall_Π⇩3 ≡ forall⇩3"
  instance proof
    fix w :: i and ψ :: "Π⇩3⇒𝗈"
    show "(w ⊨ ❙∀x. ψ x) = (∀x. (w ⊨ ψ x))"
      unfolding forall_Π⇩3_def using Semantics.T8_3 .
  qed
end

(*<*)
end
(*>*)