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