(*<*)
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→o)→o" (binder ‹\∀› [8] 9)
  assumes quantifiable_T8: "(w ⊨ (\<forall> x . ψ x)) = (∀ x . (w ⊨ (ψ x)))"
begin
end

lemma (in Semantics) T8: shows "(w ⊨ \<forall> x . ψ x) = (∀ x . (w ⊨ ψ x))"
  using quantifiable_T8 .

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

instantiation ν :: quantifiable
begin
  definition forall_ν :: "(ν→o)→o" where "forall_ν ≡ forall_\<nu>"
  instance proof
    fix w :: i and ψ :: "ν→o"
    show "(w ⊨ \<forall>x. ψ x) = (∀x. (w ⊨ ψ x))"
      unfolding forall_ν_def using Semantics.T8_ν .
  qed
end

instantiation o :: quantifiable
begin
  definition forall_o :: "(o→o)→o" where "forall_o ≡ forall_\<o>"
  instance proof
    fix w :: i and ψ :: "o→o"
    show "(w ⊨ \<forall>x. ψ x) = (∀x. (w ⊨ ψ x))"
      unfolding forall_o_def using Semantics.T8_o .
  qed
end

instantiation Π₁ :: quantifiable
begin
  definition forall_Π₁ :: "(Π₁→o)→o" where "forall_Π₁ ≡ forall₁"
  instance proof
    fix w :: i and ψ :: "Π₁→o"
    show "(w ⊨ \<forall>x. ψ x) = (∀x. (w ⊨ ψ x))"
      unfolding forall_Π₁_def using Semantics.T8_1 .
  qed
end

instantiation Π₂ :: quantifiable
begin
  definition forall_Π₂ :: "(Π₂→o)→o" where "forall_Π₂ ≡ forall₂"
  instance proof
    fix w :: i and ψ :: "Π₂→o"
    show "(w ⊨ \<forall>x. ψ x) = (∀x. (w ⊨ ψ x))"
      unfolding forall_Π₂_def using Semantics.T8_2 .
  qed
end

instantiation Π₃ :: quantifiable
begin
  definition forall_Π₃ :: "(Π₃→o)→o" where "forall_Π₃ ≡ forall₃"
  instance proof
    fix w :: i and ψ :: "Π₃→o"
    show "(w ⊨ \<forall>x. ψ x) = (∀x. (w ⊨ ψ x))"
      unfolding forall_Π₃_def using Semantics.T8_3 .
  qed
end

(*<*)
end
(*>*)