{-# OPTIONS --safe --cubical #-}

module OWL2.Kernel.Semantics where

open import Cubical.Data.Sigma.Base using (Σ)
open import Cubical.Data.Nat.Base using (zero; suc)
open import OWL2.Prelude
open import OWL2.Foundation.List hiding (NonEmpty)
open import OWL2.Kernel.Syntax

record Interpretation (Sig : Signature) : Type₁ where
  constructor kernelInterpretation
  field
    ObjectDomain :
      Type₀
    DataDomain :
      Type₀
    classDenotation :
      ClassName Sig → ObjectDomain → Type₀
    objectPropertyDenotation :
      ObjectPropertyName Sig → ObjectDomain → ObjectDomain → Type₀
    dataPropertyDenotation :
      DataPropertyName Sig → ObjectDomain → DataDomain → Type₀
    individualDenotation :
      IndividualName Sig → ObjectDomain
    literalDenotation :
      Literal Sig → DataDomain
    datatypeDenotation :
      DatatypeName Sig → DataDomain → Type₀
    facetRestrictionDenotation :
      FacetRestriction Sig → DataDomain → Type₀

open Interpretation public

atLeastTwoToList :
  ∀ {ℓ} {A : Type ℓ} →
  AtLeastTwo A →
  List A
atLeastTwoToList (atLeastTwo first second rest) =
  first ∷ second ∷ rest

atLeastTwoToNonEmpty :
  ∀ {ℓ} {A : Type ℓ} →
  AtLeastTwo A →
  NonEmpty A
atLeastTwoToNonEmpty (atLeastTwo first second rest) =
  nonEmpty first (second ∷ rest)

SatisfiesAll :
  {A : Type₀} →
  (A → Type₀) →
  NonEmpty A →
  Type₀
SatisfiesAll P (nonEmpty head tail) =
  P head × All P tail

SatisfiesAny :
  {A : Type₀} →
  (A → Type₀) →
  NonEmpty A →
  Type₀
SatisfiesAny P (nonEmpty head tail) =
  P head ⊎ Any P tail

PairwiseFrom :
  {A : Type₀} →
  (A → A → Type₀) →
  A →
  List A →
  Type₀
PairwiseFrom R x [] =
  Unit
PairwiseFrom R x (y ∷ ys) =
  R x y × PairwiseFrom R x ys

Pairwise :
  {A : Type₀} →
  (A → A → Type₀) →
  List A →
  Type₀
Pairwise R [] =
  Unit
Pairwise R (x ∷ xs) =
  PairwiseFrom R x xs × Pairwise R xs

HasAtLeastObjects :
  ∀ {Sig} →
  (I : Interpretation Sig) →
  ℕ →
  (ObjectDomain I → Type₀) →
  Type₀
HasAtLeastObjects I zero P =
  Unit
HasAtLeastObjects I (suc n) P =
  Σ (ObjectDomain I)
    (λ x → P x × HasAtLeastObjects I n (λ y → P y × (¬ (y ≡ x))))

HasAtMostObjects :
  ∀ {Sig} →
  (I : Interpretation Sig) →
  ℕ →
  (ObjectDomain I → Type₀) →
  Type₀
HasAtMostObjects I n P =
  ¬ HasAtLeastObjects I (suc n) P

HasExactlyObjects :
  ∀ {Sig} →
  (I : Interpretation Sig) →
  ℕ →
  (ObjectDomain I → Type₀) →
  Type₀
HasExactlyObjects I n P =
  HasAtLeastObjects I n P × HasAtMostObjects I n P

HasAtLeastData :
  ∀ {Sig} →
  (I : Interpretation Sig) →
  ℕ →
  (DataDomain I → Type₀) →
  Type₀
HasAtLeastData I zero P =
  Unit
HasAtLeastData I (suc n) P =
  Σ (DataDomain I)
    (λ x → P x × HasAtLeastData I n (λ y → P y × (¬ (y ≡ x))))

HasAtMostData :
  ∀ {Sig} →
  (I : Interpretation Sig) →
  ℕ →
  (DataDomain I → Type₀) →
  Type₀
HasAtMostData I n P =
  ¬ HasAtLeastData I (suc n) P

HasExactlyData :
  ∀ {Sig} →
  (I : Interpretation Sig) →
  ℕ →
  (DataDomain I → Type₀) →
  Type₀
HasExactlyData I n P =
  HasAtLeastData I n P × HasAtMostData I n P

SatisfiesFacetRestrictions :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  List (FacetRestriction Sig) →
  DataDomain I →
  Type₀
SatisfiesFacetRestrictions I [] value =
  Unit
SatisfiesFacetRestrictions I (restriction ∷ restrictions) value =
  facetRestrictionDenotation I restriction value ×
  SatisfiesFacetRestrictions I restrictions value

mutual
  SatisfiesDataRange :
    {Sig : Signature} →
    (I : Interpretation Sig) →
    DataRange Sig →
    DataDomain I →
    Type₀
  SatisfiesDataRange I (datatype name support) value =
    datatypeDenotation I name value
  SatisfiesDataRange I dataTop value =
    Unit
  SatisfiesDataRange I dataBottom value =
    ⊥
  SatisfiesDataRange I (dataComplementOf range) value =
    ¬ SatisfiesDataRange I range value
  SatisfiesDataRange I (dataIntersectionOf (nonEmpty head tail)) value =
    SatisfiesDataRange I head value × SatisfiesDataRangeAll I tail value
  SatisfiesDataRange I (dataUnionOf (nonEmpty head tail)) value =
    SatisfiesDataRange I head value ⊎ SatisfiesDataRangeAny I tail value
  SatisfiesDataRange I (dataOneOf literals) value =
    SatisfiesAny (λ lit → value ≡ literalDenotation I lit) literals
  SatisfiesDataRange I (datatypeRestriction name support facets) value =
    datatypeDenotation I name value × SatisfiesFacetRestrictions I facets value

  SatisfiesDataRangeAll :
    {Sig : Signature} →
    (I : Interpretation Sig) →
    List (DataRange Sig) →
    DataDomain I →
    Type₀
  SatisfiesDataRangeAll I [] value =
    Unit
  SatisfiesDataRangeAll I (range ∷ ranges) value =
    SatisfiesDataRange I range value × SatisfiesDataRangeAll I ranges value

  SatisfiesDataRangeAny :
    {Sig : Signature} →
    (I : Interpretation Sig) →
    List (DataRange Sig) →
    DataDomain I →
    Type₀
  SatisfiesDataRangeAny I [] value =
    ⊥
  SatisfiesDataRangeAny I (range ∷ ranges) value =
    SatisfiesDataRange I range value ⊎ SatisfiesDataRangeAny I ranges value

SatisfiesObjectPropertyExpression :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  ObjectPropertyExpression Sig →
  ObjectDomain I →
  ObjectDomain I →
  Type₀
SatisfiesObjectPropertyExpression I (objectProperty property) x y =
  objectPropertyDenotation I property x y
SatisfiesObjectPropertyExpression I topObjectProperty x y =
  Unit
SatisfiesObjectPropertyExpression I bottomObjectProperty x y =
  ⊥
SatisfiesObjectPropertyExpression I (objectInverseOf property) x y =
  SatisfiesObjectPropertyExpression I property y x

SatisfiesSimpleObjectProperty :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  SimpleObjectPropertyName Sig →
  ObjectDomain I →
  ObjectDomain I →
  Type₀
SatisfiesSimpleObjectProperty I property x y =
  SatisfiesObjectPropertyExpression I (objectProperty (SimpleObjectPropertyName.property property)) x y

SatisfiesObjectPropertyExpressionList :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  List (ObjectPropertyExpression Sig) →
  ObjectDomain I →
  ObjectDomain I →
  Type₀
SatisfiesObjectPropertyExpressionList I [] x y =
  x ≡ y
SatisfiesObjectPropertyExpressionList I (property ∷ properties) x z =
  Σ (ObjectDomain I)
    (λ y →
      SatisfiesObjectPropertyExpression I property x y ×
      SatisfiesObjectPropertyExpressionList I properties y z)

SatisfiesObjectPropertyChain :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  ObjectPropertyChain Sig →
  ObjectDomain I →
  ObjectDomain I →
  Type₀
SatisfiesObjectPropertyChain I chain =
  SatisfiesObjectPropertyExpressionList I (atLeastTwoToList (links chain))

SatisfiesSubObjectPropertyExpression :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  SubObjectPropertyExpression Sig →
  ObjectDomain I →
  ObjectDomain I →
  Type₀
SatisfiesSubObjectPropertyExpression I (subObjectProperty property) x y =
  SatisfiesObjectPropertyExpression I property x y
SatisfiesSubObjectPropertyExpression I (subObjectPropertyChain chain) x y =
  SatisfiesObjectPropertyChain I chain x y

SatisfiesDataPropertyExpression :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  DataPropertyExpression Sig →
  ObjectDomain I →
  DataDomain I →
  Type₀
SatisfiesDataPropertyExpression I (dataProperty property) x value =
  dataPropertyDenotation I property x value
SatisfiesDataPropertyExpression I topDataProperty x value =
  Unit
SatisfiesDataPropertyExpression I bottomDataProperty x value =
  ⊥

individualValue :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  Individual Sig →
  ObjectDomain I
individualValue I (namedIndividual individual) =
  individualDenotation I individual

SatisfiesIndividual :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  Individual Sig →
  ObjectDomain I →
  Type₀
SatisfiesIndividual I individual x =
  x ≡ individualValue I individual

mutual
  SatisfiesOptionalClassExpression :
    {Sig : Signature} →
    (I : Interpretation Sig) →
    Optional (ClassExpression Sig) →
    ObjectDomain I →
    Type₀
  SatisfiesOptionalClassExpression I absent x =
    Unit
  SatisfiesOptionalClassExpression I (present class) x =
    SatisfiesClassExpression I class x

  SatisfiesOptionalDataRange :
    {Sig : Signature} →
    (I : Interpretation Sig) →
    Optional (DataRange Sig) →
    DataDomain I →
    Type₀
  SatisfiesOptionalDataRange I absent value =
    Unit
  SatisfiesOptionalDataRange I (present range) value =
    SatisfiesDataRange I range value

  SatisfiesClassExpressionAll :
    {Sig : Signature} →
    (I : Interpretation Sig) →
    List (ClassExpression Sig) →
    ObjectDomain I →
    Type₀
  SatisfiesClassExpressionAll I [] x =
    Unit
  SatisfiesClassExpressionAll I (class ∷ classes) x =
    SatisfiesClassExpression I class x × SatisfiesClassExpressionAll I classes x

  SatisfiesClassExpressionAny :
    {Sig : Signature} →
    (I : Interpretation Sig) →
    List (ClassExpression Sig) →
    ObjectDomain I →
    Type₀
  SatisfiesClassExpressionAny I [] x =
    ⊥
  SatisfiesClassExpressionAny I (class ∷ classes) x =
    SatisfiesClassExpression I class x ⊎ SatisfiesClassExpressionAny I classes x

  SatisfiesClassExpression :
    {Sig : Signature} →
    (I : Interpretation Sig) →
    ClassExpression Sig →
    ObjectDomain I →
    Type₀
  SatisfiesClassExpression I (namedClass c) x =
    classDenotation I c x
  SatisfiesClassExpression I owlThing x =
    Unit
  SatisfiesClassExpression I owlNothing x =
    ⊥
  SatisfiesClassExpression I (objectIntersectionOf (nonEmpty head tail)) x =
    SatisfiesClassExpression I head x × SatisfiesClassExpressionAll I tail x
  SatisfiesClassExpression I (objectUnionOf (nonEmpty head tail)) x =
    SatisfiesClassExpression I head x ⊎ SatisfiesClassExpressionAny I tail x
  SatisfiesClassExpression I (objectComplementOf c) x =
    ¬ SatisfiesClassExpression I c x
  SatisfiesClassExpression I (objectOneOf xs) x =
    SatisfiesAny (λ individual → SatisfiesIndividual I individual x) xs
  SatisfiesClassExpression I (objectSomeValuesFrom p c) x =
    Σ (ObjectDomain I)
      (λ y →
        SatisfiesObjectPropertyExpression I p x y ×
        SatisfiesClassExpression I c y)
  SatisfiesClassExpression I (objectAllValuesFrom p c) x =
    (y : ObjectDomain I) →
    SatisfiesObjectPropertyExpression I p x y →
    SatisfiesClassExpression I c y
  SatisfiesClassExpression I (objectHasValue p y) x =
    SatisfiesObjectPropertyExpression I p x (individualValue I y)
  SatisfiesClassExpression I (objectHasSelf p) x =
    SatisfiesSimpleObjectProperty I p x x
  SatisfiesClassExpression I (objectMinCardinality n p c) x =
    HasAtLeastObjects I n
      (λ y →
        SatisfiesSimpleObjectProperty I p x y ×
        SatisfiesOptionalClassExpression I c y)
  SatisfiesClassExpression I (objectMaxCardinality n p c) x =
    HasAtMostObjects I n
      (λ y →
        SatisfiesSimpleObjectProperty I p x y ×
        SatisfiesOptionalClassExpression I c y)
  SatisfiesClassExpression I (objectExactCardinality n p c) x =
    HasExactlyObjects I n
      (λ y →
        SatisfiesSimpleObjectProperty I p x y ×
        SatisfiesOptionalClassExpression I c y)
  SatisfiesClassExpression I (dataSomeValuesFrom p d) x =
    Σ (DataDomain I)
      (λ value →
        SatisfiesDataPropertyExpression I p x value ×
        SatisfiesDataRange I d value)
  SatisfiesClassExpression I (dataAllValuesFrom p d) x =
    (value : DataDomain I) →
    SatisfiesDataPropertyExpression I p x value →
    SatisfiesDataRange I d value
  SatisfiesClassExpression I (dataHasValue p lit) x =
    SatisfiesDataPropertyExpression I p x (literalDenotation I lit)
  SatisfiesClassExpression I (dataMinCardinality n p d) x =
    HasAtLeastData I n
      (λ value →
        SatisfiesDataPropertyExpression I p x value ×
        SatisfiesOptionalDataRange I d value)
  SatisfiesClassExpression I (dataMaxCardinality n p d) x =
    HasAtMostData I n
      (λ value →
        SatisfiesDataPropertyExpression I p x value ×
        SatisfiesOptionalDataRange I d value)
  SatisfiesClassExpression I (dataExactCardinality n p d) x =
    HasExactlyData I n
      (λ value →
        SatisfiesDataPropertyExpression I p x value ×
        SatisfiesOptionalDataRange I d value)

ClassSubsumes :
  {Sig : Signature} →
  Interpretation Sig →
  ClassExpression Sig →
  ClassExpression Sig →
  Type₀
ClassSubsumes I sub sup =
  (x : ObjectDomain I) →
  SatisfiesClassExpression I sub x →
  SatisfiesClassExpression I sup x

EquivalentClassExpressions :
  {Sig : Signature} →
  Interpretation Sig →
  ClassExpression Sig →
  ClassExpression Sig →
  Type₀
EquivalentClassExpressions I left right =
  ClassSubsumes I left right × ClassSubsumes I right left

DisjointClassExpressions :
  {Sig : Signature} →
  Interpretation Sig →
  ClassExpression Sig →
  ClassExpression Sig →
  Type₀
DisjointClassExpressions I left right =
  (x : ObjectDomain I) →
  SatisfiesClassExpression I left x →
  SatisfiesClassExpression I right x →
  ⊥

EquivalentObjectProperties :
  {Sig : Signature} →
  Interpretation Sig →
  ObjectPropertyExpression Sig →
  ObjectPropertyExpression Sig →
  Type₀
EquivalentObjectProperties I left right =
  ((x y : ObjectDomain I) →
   SatisfiesObjectPropertyExpression I left x y →
   SatisfiesObjectPropertyExpression I right x y)
  ×
  ((x y : ObjectDomain I) →
   SatisfiesObjectPropertyExpression I right x y →
   SatisfiesObjectPropertyExpression I left x y)

DisjointObjectProperties :
  {Sig : Signature} →
  Interpretation Sig →
  SimpleObjectPropertyName Sig →
  SimpleObjectPropertyName Sig →
  Type₀
DisjointObjectProperties I left right =
  (x y : ObjectDomain I) →
  SatisfiesSimpleObjectProperty I left x y →
  SatisfiesSimpleObjectProperty I right x y →
  ⊥

EquivalentDataProperties :
  {Sig : Signature} →
  Interpretation Sig →
  DataPropertyExpression Sig →
  DataPropertyExpression Sig →
  Type₀
EquivalentDataProperties I left right =
  ((x : ObjectDomain I) → (value : DataDomain I) →
   SatisfiesDataPropertyExpression I left x value →
   SatisfiesDataPropertyExpression I right x value)
  ×
  ((x : ObjectDomain I) → (value : DataDomain I) →
   SatisfiesDataPropertyExpression I right x value →
   SatisfiesDataPropertyExpression I left x value)

DisjointDataProperties :
  {Sig : Signature} →
  Interpretation Sig →
  DataPropertyExpression Sig →
  DataPropertyExpression Sig →
  Type₀
DisjointDataProperties I left right =
  (x : ObjectDomain I) → (value : DataDomain I) →
  SatisfiesDataPropertyExpression I left x value →
  SatisfiesDataPropertyExpression I right x value →
  ⊥

DataRangeEquivalentToDatatype :
  {Sig : Signature} →
  Interpretation Sig →
  DatatypeName Sig →
  DataRange Sig →
  Type₀
DataRangeEquivalentToDatatype I name range =
  ((value : DataDomain I) →
   datatypeDenotation I name value →
   SatisfiesDataRange I range value)
  ×
  ((value : DataDomain I) →
   SatisfiesDataRange I range value →
   datatypeDenotation I name value)

SharedSimpleObjectPropertyValue :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  SimpleObjectPropertyName Sig →
  ObjectDomain I →
  ObjectDomain I →
  Type₀
SharedSimpleObjectPropertyValue I property x y =
  Σ (ObjectDomain I)
    (λ value →
      SatisfiesSimpleObjectProperty I property x value ×
      SatisfiesSimpleObjectProperty I property y value)

SharedDataPropertyValue :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  DataPropertyExpression Sig →
  ObjectDomain I →
  ObjectDomain I →
  Type₀
SharedDataPropertyValue I property x y =
  Σ (DataDomain I)
    (λ value →
      SatisfiesDataPropertyExpression I property x value ×
      SatisfiesDataPropertyExpression I property y value)

SharedKey :
  {Sig : Signature} →
  (I : Interpretation Sig) →
  PropertyKey Sig →
  ObjectDomain I →
  ObjectDomain I →
  Type₀
SharedKey I key x y =
  All
    (λ property → SharedSimpleObjectPropertyValue I property x y)
    (objectProperties key)
  ×
  All (λ property → SharedDataPropertyValue I property x y) (dataProperties key)

SatisfiesPropertyKey :
  {Sig : Signature} →
  Interpretation Sig →
  ClassExpression Sig →
  PropertyKey Sig →
  Type₀
SatisfiesPropertyKey I class key =
  (x y : ObjectDomain I) →
  SatisfiesClassExpression I class x →
  SatisfiesClassExpression I class y →
  SharedKey I key x y →
  x ≡ y

SatisfiesAxiom :
  {Sig : Signature} →
  Interpretation Sig →
  Axiom Sig →
  Type₀
SatisfiesAxiom I (declaration entity) =
  Unit
SatisfiesAxiom I (subClassOf sub sup) =
  ClassSubsumes I sub sup
SatisfiesAxiom I (equivalentClasses classes) =
  Pairwise (EquivalentClassExpressions I) (atLeastTwoToList classes)
SatisfiesAxiom I (disjointClasses classes) =
  Pairwise (DisjointClassExpressions I) (atLeastTwoToList classes)
SatisfiesAxiom I (disjointUnion class classes) =
  EquivalentClassExpressions I
    (namedClass class)
    (objectUnionOf (atLeastTwoToNonEmpty classes))
  ×
  Pairwise (DisjointClassExpressions I) (atLeastTwoToList classes)
SatisfiesAxiom I (subObjectPropertyOf sub sup) =
  (x y : ObjectDomain I) →
  SatisfiesSubObjectPropertyExpression I sub x y →
  SatisfiesObjectPropertyExpression I sup x y
SatisfiesAxiom I (equivalentObjectProperties properties) =
  Pairwise (EquivalentObjectProperties I) (atLeastTwoToList properties)
SatisfiesAxiom I (disjointObjectProperties properties) =
  Pairwise (DisjointObjectProperties I) (atLeastTwoToList properties)
SatisfiesAxiom I (inverseObjectProperties left right) =
  ((x y : ObjectDomain I) →
   SatisfiesObjectPropertyExpression I left x y →
   SatisfiesObjectPropertyExpression I right y x)
  ×
  ((x y : ObjectDomain I) →
   SatisfiesObjectPropertyExpression I right x y →
   SatisfiesObjectPropertyExpression I left y x)
SatisfiesAxiom I (objectPropertyDomain property class) =
  (x y : ObjectDomain I) →
  SatisfiesObjectPropertyExpression I property x y →
  SatisfiesClassExpression I class x
SatisfiesAxiom I (objectPropertyRange property class) =
  (x y : ObjectDomain I) →
  SatisfiesObjectPropertyExpression I property x y →
  SatisfiesClassExpression I class y
SatisfiesAxiom I (functionalObjectProperty property) =
  (x y z : ObjectDomain I) →
  SatisfiesSimpleObjectProperty I property x y →
  SatisfiesSimpleObjectProperty I property x z →
  y ≡ z
SatisfiesAxiom I (inverseFunctionalObjectProperty property) =
  (x y z : ObjectDomain I) →
  SatisfiesSimpleObjectProperty I property y x →
  SatisfiesSimpleObjectProperty I property z x →
  y ≡ z
SatisfiesAxiom I (reflexiveObjectProperty property) =
  (x : ObjectDomain I) →
  SatisfiesObjectPropertyExpression I property x x
SatisfiesAxiom I (irreflexiveObjectProperty property) =
  (x : ObjectDomain I) →
  ¬ SatisfiesSimpleObjectProperty I property x x
SatisfiesAxiom I (symmetricObjectProperty property) =
  (x y : ObjectDomain I) →
  SatisfiesObjectPropertyExpression I property x y →
  SatisfiesObjectPropertyExpression I property y x
SatisfiesAxiom I (asymmetricObjectProperty property) =
  (x y : ObjectDomain I) →
  SatisfiesSimpleObjectProperty I property x y →
  ¬ SatisfiesSimpleObjectProperty I property y x
SatisfiesAxiom I (transitiveObjectProperty property) =
  (x y z : ObjectDomain I) →
  SatisfiesObjectPropertyExpression I property x y →
  SatisfiesObjectPropertyExpression I property y z →
  SatisfiesObjectPropertyExpression I property x z
SatisfiesAxiom I (subDataPropertyOf sub sup) =
  (x : ObjectDomain I) → (value : DataDomain I) →
  SatisfiesDataPropertyExpression I sub x value →
  SatisfiesDataPropertyExpression I sup x value
SatisfiesAxiom I (equivalentDataProperties properties) =
  Pairwise (EquivalentDataProperties I) (atLeastTwoToList properties)
SatisfiesAxiom I (disjointDataProperties properties) =
  Pairwise (DisjointDataProperties I) (atLeastTwoToList properties)
SatisfiesAxiom I (dataPropertyDomain property class) =
  (x : ObjectDomain I) → (value : DataDomain I) →
  SatisfiesDataPropertyExpression I property x value →
  SatisfiesClassExpression I class x
SatisfiesAxiom I (dataPropertyRange property range) =
  (x : ObjectDomain I) → (value : DataDomain I) →
  SatisfiesDataPropertyExpression I property x value →
  SatisfiesDataRange I range value
SatisfiesAxiom I (functionalDataProperty property) =
  (x : ObjectDomain I) → (left right : DataDomain I) →
  SatisfiesDataPropertyExpression I property x left →
  SatisfiesDataPropertyExpression I property x right →
  left ≡ right
SatisfiesAxiom I (datatypeDefinition name support range) =
  DataRangeEquivalentToDatatype I name range
SatisfiesAxiom I (hasKey class key) =
  SatisfiesPropertyKey I class key
SatisfiesAxiom I (sameIndividual individuals) =
  Pairwise
    (λ left right →
      individualValue I left ≡ individualValue I right)
    (atLeastTwoToList individuals)
SatisfiesAxiom I (differentIndividuals individuals) =
  Pairwise
    (λ left right →
      ¬ (individualValue I left ≡ individualValue I right))
    (atLeastTwoToList individuals)
SatisfiesAxiom I (classAssertion class individual) =
  SatisfiesClassExpression I class (individualValue I individual)
SatisfiesAxiom I (objectPropertyAssertion property subject object) =
  SatisfiesObjectPropertyExpression I property
    (individualValue I subject)
    (individualValue I object)
SatisfiesAxiom I (negativeObjectPropertyAssertion property subject object) =
  ¬ SatisfiesObjectPropertyExpression I property
      (individualValue I subject)
      (individualValue I object)
SatisfiesAxiom I (dataPropertyAssertion property subject literal) =
  SatisfiesDataPropertyExpression I property
    (individualValue I subject)
    (literalDenotation I literal)
SatisfiesAxiom I (negativeDataPropertyAssertion property subject literal) =
  ¬ SatisfiesDataPropertyExpression I property
      (individualValue I subject)
      (literalDenotation I literal)
SatisfiesAxiom I (annotationAssertion property subject value) =
  Unit
SatisfiesAxiom I (subAnnotationPropertyOf sub sup) =
  Unit
SatisfiesAxiom I (annotationPropertyDomain property iri) =
  Unit
SatisfiesAxiom I (annotationPropertyRange property iri) =
  Unit

SatisfiesAxioms :
  {Sig : Signature} →
  Interpretation Sig →
  List (Axiom Sig) →
  Type₀
SatisfiesAxioms I axioms =
  All (SatisfiesAxiom I) axioms

SatisfiesOntology :
  {Sig : Signature} →
  Interpretation Sig →
  Ontology Sig →
  Type₀
SatisfiesOntology I ont =
  SatisfiesAxioms I (axioms ont)

record Model (Sig : Signature) (ont : Ontology Sig) : Type₁ where
  constructor model
  field
    interpretation :
      Interpretation Sig
    satisfies :
      SatisfiesOntology interpretation ont

open Model public