OWL2.Examples.Regularity

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

module OWL2.Examples.Regularity where

open import OWL2.Prelude
open import OWL2.Syntax
open import OWL2.Syntax.Regularity
import OWL2.Examples.PropertyChain as Chain

chainAxioms : List (Axiom Chain.ChainSignature)
chainAxioms =
  subObjectPropertyOf Chain.ParentParentChain Chain.HasGrandparent ∷ []

regularityOntology :
  Ontology Chain.ChainSignature
regularityOntology =
  ontology [] [] chainAxioms

axiomRegularitySeesGrandparentComposite :
  Composite
    (axiomRegularityContext chainAxioms)
    Chain.HasGrandparent
axiomRegularitySeesGrandparentComposite =
  compositeChain here

ChainComposite :
  ObjectPropertyExpression Chain.ChainSignature → Type₀
ChainComposite (objectProperty Chain.hasParent) =
  ⊥
ChainComposite (objectProperty Chain.hasGrandparent) =
  Unit
ChainComposite topObjectProperty =
  Unit
ChainComposite bottomObjectProperty =
  Unit
ChainComposite (objectInverseOf (objectProperty Chain.hasParent)) =
  ⊥
ChainComposite (objectInverseOf (objectProperty Chain.hasGrandparent)) =
  Unit
ChainComposite (objectInverseOf _) =
  ⊥

ChainHierarchyStep :
  ObjectPropertyExpression Chain.ChainSignature →
  ObjectPropertyExpression Chain.ChainSignature →
  Type₀
ChainHierarchyStep p q =
  ⊥

chainRegularityContext :
  RegularityContext Chain.ChainSignature
chainRegularityContext .Composite =
  ChainComposite
chainRegularityContext .HierarchyStep =
  ChainHierarchyStep

hasParentSimple :
  SimpleObjectPropertyExpression
    chainRegularityContext
    Chain.HasParent
hasParentSimple =
  canonicalObjectProperty ,
  λ where
    q hierarchyRefl composite →
      composite
    q (hierarchyTrans step path) composite →
      step

hasGrandparentComposite :
  Composite chainRegularityContext Chain.HasGrandparent
hasGrandparentComposite =
  tt

hasGrandparentNonSimple :
  NonSimpleObjectPropertyExpression
    chainRegularityContext
    Chain.HasGrandparent
hasGrandparentNonSimple =
  Chain.HasGrandparent , hierarchyRefl , hasGrandparentComposite

AtLeastOneParent AtLeastOneGrandparent :
  ClassExpression Chain.ChainSignature
AtLeastOneParent =
  objectMinCardinality 1 Chain.HasParent absent
AtLeastOneGrandparent =
  objectMinCardinality 1 Chain.HasGrandparent absent

atLeastOneParentUsesOnlySimpleProperties :
  ClassExpressionUsesOnlySimpleObjectProperties
    chainRegularityContext
    AtLeastOneParent
atLeastOneParentUsesOnlySimpleProperties =
  hasParentSimple , tt*

atLeastOneGrandparentRejected :
  ¬ ClassExpressionUsesOnlySimpleObjectProperties
      chainRegularityContext
      AtLeastOneGrandparent
atLeastOneGrandparentRejected (simpleGrandparent , qualifier-ok) =
  nonSimpleContradictsSimple
    hasGrandparentNonSimple
    simpleGrandparent

DisjointParentAndGrandparent :
  Axiom Chain.ChainSignature
DisjointParentAndGrandparent =
  disjointObjectProperties
    (Chain.HasGrandparent ∷ Chain.HasParent ∷ [])

disjointParentAndGrandparentRejected :
  ¬ AxiomUsesOnlySimpleObjectProperties
      chainRegularityContext
      DisjointParentAndGrandparent
disjointParentAndGrandparentRejected (simpleGrandparent , rest) =
  nonSimpleContradictsSimple
    hasGrandparentNonSimple
    simpleGrandparent

data ChainOrder :
  ObjectPropertyExpression Chain.ChainSignature →
  ObjectPropertyExpression Chain.ChainSignature →
  Type₀ where
  parent<grandparent :
    ChainOrder Chain.HasParent Chain.HasGrandparent
  inverseParent<inverseGrandparent :
    ChainOrder
      (inverseObjectPropertyExpression Chain.HasParent)
      (inverseObjectPropertyExpression Chain.HasGrandparent)

chainOrderIrrefl :
  ∀ p → ¬ ChainOrder p p
chainOrderIrrefl p ()

chainOrderTrans :
  ∀ {p q r} →
  ChainOrder p q →
  ChainOrder q r →
  ChainOrder p r
chainOrderTrans parent<grandparent ()
chainOrderTrans inverseParent<inverseGrandparent ()

chainOrderInversePreserves :
  ∀ {p q} →
  ChainOrder p q →
  ChainOrder
    (inverseObjectPropertyExpression p)
    (inverseObjectPropertyExpression q)
chainOrderInversePreserves parent<grandparent =
  inverseParent<inverseGrandparent
chainOrderInversePreserves inverseParent<inverseGrandparent =
  parent<grandparent

chainOrderNoBackHierarchy :
  ∀ {p q} →
  ChainOrder p q →
  ¬ PropertyHierarchyPath chainRegularityContext q p
chainOrderNoBackHierarchy parent<grandparent (hierarchyTrans step path) =
  step
chainOrderNoBackHierarchy
  inverseParent<inverseGrandparent
  (hierarchyTrans step path) =
  step

chainOrderRegular :
  AxiomsPropertyChainsRegular ChainOrder chainAxioms
chainOrderRegular =
  regularStrictPropertyChain
    parent<grandparent
    parent<grandparent
    tt*
  ,
  tt*

chainStrictOrder :
  StrictChainOrder Chain.ChainSignature chainAxioms
chainStrictOrder ._<_ =
  ChainOrder
chainStrictOrder .irrefl =
  chainOrderIrrefl
chainStrictOrder .trans =
  chainOrderTrans
chainStrictOrder .inversePreserves =
  chainOrderInversePreserves
chainStrictOrder .chainsRegular =
  chainOrderRegular

chainHierarchyCompatibleOrder :
  HierarchyCompatibleChainOrder
    Chain.ChainSignature
    chainRegularityContext
    chainAxioms
chainHierarchyCompatibleOrder .strictChainOrder =
  chainStrictOrder
chainHierarchyCompatibleOrder .noBackHierarchy =
  chainOrderNoBackHierarchy

chainToTopRegular :
  RegularPropertyChain
    ChainOrder
    Chain.HasParent
    Chain.HasGrandparent
    []
    topObjectProperty
chainToTopRegular =
  regularPropertyChainToTop

transitiveSelfChainRegular :
  RegularPropertyChain
    ChainOrder
    Chain.HasParent
    Chain.HasParent
    []
    Chain.HasParent
transitiveSelfChainRegular =
  regularTransitivePropertyChain

strictChainRegular :
  RegularPropertyChain
    ChainOrder
    Chain.HasParent
    Chain.HasParent
    []
    Chain.HasGrandparent
strictChainRegular =
  regularStrictPropertyChain
    parent<grandparent
    parent<grandparent
    tt*

leftRecursiveChainRegular :
  RegularPropertyChain
    ChainOrder
    Chain.HasGrandparent
    Chain.HasParent
    []
    Chain.HasGrandparent
leftRecursiveChainRegular =
  regularLeftRecursivePropertyChain
    parent<grandparent
    tt*

rightRecursiveChainRegular :
  RegularPropertyChain
    ChainOrder
    Chain.HasParent
    Chain.HasGrandparent
    []
    Chain.HasGrandparent
rightRecursiveChainRegular =
  regularRightRecursivePropertyChain
    (rightRecursiveTwo parent<grandparent)

recursiveChainAxioms : List (Axiom Chain.ChainSignature)
recursiveChainAxioms =
  subObjectPropertyOf
    (subObjectPropertyChain Chain.HasParent Chain.HasGrandparent [])
    topObjectProperty
  ∷
  subObjectPropertyOf
    (subObjectPropertyChain Chain.HasParent Chain.HasParent [])
    Chain.HasParent
  ∷
  subObjectPropertyOf
    (subObjectPropertyChain Chain.HasParent Chain.HasParent [])
    Chain.HasGrandparent
  ∷
  subObjectPropertyOf
    (subObjectPropertyChain Chain.HasGrandparent Chain.HasParent [])
    Chain.HasGrandparent
  ∷
  subObjectPropertyOf
    (subObjectPropertyChain Chain.HasParent Chain.HasGrandparent [])
    Chain.HasGrandparent
  ∷ []

recursiveChainAxiomsRegular :
  AxiomsPropertyChainsRegular ChainOrder recursiveChainAxioms
recursiveChainAxiomsRegular =
  chainToTopRegular ,
  transitiveSelfChainRegular ,
  strictChainRegular ,
  leftRecursiveChainRegular ,
  rightRecursiveChainRegular ,
  tt*

recursiveRegularityOntology :
  Ontology Chain.ChainSignature
recursiveRegularityOntology =
  ontology [] [] recursiveChainAxioms

recursiveChainStrictOrder :
  StrictChainOrder Chain.ChainSignature recursiveChainAxioms
recursiveChainStrictOrder ._<_ =
  ChainOrder
recursiveChainStrictOrder .irrefl =
  chainOrderIrrefl
recursiveChainStrictOrder .trans =
  chainOrderTrans
recursiveChainStrictOrder .inversePreserves =
  chainOrderInversePreserves
recursiveChainStrictOrder .chainsRegular =
  recursiveChainAxiomsRegular

recursiveChainHierarchyCompatibleOrder :
  HierarchyCompatibleChainOrder
    Chain.ChainSignature
    chainRegularityContext
    recursiveChainAxioms
recursiveChainHierarchyCompatibleOrder .strictChainOrder =
  recursiveChainStrictOrder
recursiveChainHierarchyCompatibleOrder .noBackHierarchy =
  chainOrderNoBackHierarchy

recursiveRegularityOntologySimpleUses :
  OntologyUsesOnlySimpleObjectProperties recursiveRegularityOntology
recursiveRegularityOntologySimpleUses =
  tt* , tt* , tt* , tt* , tt* , tt*

recursiveRegularityOntologyRegular :
  OntologyRegular recursiveRegularityOntology
recursiveRegularityOntologyRegular .simpleObjectPropertyUses =
  recursiveRegularityOntologySimpleUses
recursiveRegularityOntologyRegular .strictChainOrder =
  recursiveChainStrictOrder

recursiveRegularityOntologyContextualRegular :
  ContextualOntologyRegular
    chainRegularityContext
    recursiveRegularityOntology
recursiveRegularityOntologyContextualRegular .simpleObjectPropertyUses =
  recursiveRegularityOntologySimpleUses
recursiveRegularityOntologyContextualRegular .hierarchyCompatibleChainOrder =
  recursiveChainHierarchyCompatibleOrder

regularityOntologySimpleUses :
  OntologyUsesOnlySimpleObjectProperties regularityOntology
regularityOntologySimpleUses =
  tt* , tt*

regularityOntologyRegular :
  OntologyRegular regularityOntology
regularityOntologyRegular .simpleObjectPropertyUses =
  regularityOntologySimpleUses
regularityOntologyRegular .strictChainOrder =
  chainStrictOrder

regularityOntologyContextualRegular :
  ContextualOntologyRegular
    chainRegularityContext
    regularityOntology
regularityOntologyContextualRegular .simpleObjectPropertyUses =
  regularityOntologySimpleUses
regularityOntologyContextualRegular .hierarchyCompatibleChainOrder =
  chainHierarchyCompatibleOrder