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

module OWL2.Examples.WellFormed where

open import OWL2.Prelude
open import OWL2.Syntax
open import OWL2.Syntax.Declarations
open import OWL2.Syntax.WellFormed
import OWL2.Examples.Cardinality as C

cardinalityFullEnvironment :
  DeclarationEnvironment C.CardinalitySignature
cardinalityFullEnvironment =
  fullDeclarationEnvironment

cardinalityOntologyWellFormed :
  OntologyWellFormed cardinalityFullEnvironment C.cardinalityOntology
cardinalityOntologyWellFormed =
  lift tt ,
  lift tt ,
  lift tt ,
  lift tt ,
  (lift tt , lift tt) ,
  (lift tt , lift tt) ,
  (lift tt , (lift tt , lift tt)) ,
  ((lift tt , lift tt) , lift tt) ,
  (lift tt , lift tt) ,
  ((lift tt , lift tt) , lift tt) ,
  lift tt

cardinalitySelfEnvironment :
  DeclarationEnvironment C.CardinalitySignature
cardinalitySelfEnvironment =
  ontologyDeclarationEnvironment C.cardinalityOntology

personDeclaredInCardinalityOntology :
  EntityDeclared cardinalitySelfEnvironment (classEntity C.Person)
personDeclaredInCardinalityOntology =
  declaredAtHead

spouseDeclaredInCardinalityOntology :
  EntityDeclared cardinalitySelfEnvironment (objectPropertyEntity C.hasSpouse)
spouseDeclaredInCardinalityOntology =
  declaredLater declaredAtHead

ageDeclaredInCardinalityOntology :
  EntityDeclared cardinalitySelfEnvironment (dataPropertyEntity C.hasAge)
ageDeclaredInCardinalityOntology =
  declaredLater (declaredLater declaredAtHead)

integerDeclaredInCardinalityOntology :
  EntityDeclared cardinalitySelfEnvironment (datatypeEntity C.integerDatatype)
integerDeclaredInCardinalityOntology =
  declaredLater (declaredLater (declaredLater declaredAtHead))

exactlyOneSpouseClassWellFormed :
  ClassExpressionWellFormed
    cardinalitySelfEnvironment
    C.ExactlyOneSpouse
exactlyOneSpouseClassWellFormed =
  spouseDeclaredInCardinalityOntology ,
  personDeclaredInCardinalityOntology

exactlyOneAgeClassWellFormed :
  ClassExpressionWellFormed
    cardinalitySelfEnvironment
    C.ExactlyOneAge
exactlyOneAgeClassWellFormed =
  ageDeclaredInCardinalityOntology ,
  integerDeclaredInCardinalityOntology