Theory TAO_3_Quantifiable

theory TAO_3_Quantifiable
imports TAO_2_Semantics
(*<*)
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 ≡ forall1"
  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 ≡ forall2"
  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 ≡ forall3"
  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
(*>*)