{-# OPTIONS --safe --cubical #-}
module OWL2.Examples.Portable.RegularityRank where
open import OWL2.Prelude
import OWL2.Portable.RegularityRank as Rank
import OWL2.Portable.RegularityRankProof as RankProof
import OWL2.Portable.Semantics as Sem
import OWL2.Portable.Syntax as P
import OWL2.Syntax as S
import OWL2.Syntax.Regularity as Reg
name : String → P.Name
name text =
P.named (P.iri text)
objectPropertyName : String → P.ObjectPropertyName
objectPropertyName =
name
axiom : P.Axiom → P.Annotated P.Axiom
axiom body =
P.annotated [] body
document : List (P.Annotated P.Axiom) → P.OntologyDocument
document axioms =
P.ontologyDocument [] (P.ontology P.anonymousOntology [] [] axioms)
optionalValueOr : ∀ {A : Type₀} → Optional A → A → A
optionalValueOr (present value) fallback =
value
optionalValueOr absent fallback =
fallback
hasParent hasGrandparent hasAncestor : P.ObjectPropertyName
hasParent =
objectPropertyName "https://example.org/portable-regularity-rank#hasParent"
hasGrandparent =
objectPropertyName
"https://example.org/portable-regularity-rank#hasGrandparent"
hasAncestor =
objectPropertyName "https://example.org/portable-regularity-rank#hasAncestor"
HasParent HasGrandparent HasAncestor : P.ObjectPropertyExpression
HasParent =
P.objectProperty hasParent
HasGrandparent =
P.objectProperty hasGrandparent
HasAncestor =
P.objectProperty hasAncestor
parentParentChain ancestorAncestorChain ancestorInverseChain : P.ObjectPropertyChain
parentParentChain =
P.objectPropertyChain (P.twoOrMore HasParent HasParent [])
ancestorAncestorChain =
P.objectPropertyChain (P.twoOrMore HasAncestor HasAncestor [])
ancestorInverseChain =
P.objectPropertyChain
(P.twoOrMore HasAncestor (P.objectInverseOf HasAncestor) [])
strictChainDocument : P.OntologyDocument
strictChainDocument =
document
( axiom
(P.subObjectPropertyOf
(P.subObjectPropertyChain parentParentChain)
HasGrandparent)
∷ [] )
strictChainRanks : List Rank.PropertyRank
strictChainRanks =
Rank.propertyRankForExpression HasParent 0
∷ Rank.propertyRankForExpression HasGrandparent 1
∷ []
strictChainReport : Rank.RegularityRankReport
strictChainReport =
Rank.reportRegularityRank strictChainRanks strictChainDocument
strictChainAxiomCount :
Rank.regularityRankReportPropertyChainAxiomCount strictChainReport ≡ 1
strictChainAxiomCount =
refl
strictChainIssueCount :
Rank.regularityRankReportPropertyChainIssueCount strictChainReport ≡ 0
strictChainIssueCount =
refl
strictChainAccepted :
Rank.PortableRegularityRankRestrictions
strictChainRanks
strictChainDocument
strictChainAccepted =
tt*
translatedStrictChainAxiomShape :
Sem.translateAxiom
(P.subObjectPropertyOf
(P.subObjectPropertyChain parentParentChain)
HasGrandparent)
≡
present
( S.subObjectPropertyOf
(S.subObjectPropertyChain
(Sem.translateObjectPropertyExpression HasParent)
(Sem.translateObjectPropertyExpression HasParent)
[])
(Sem.translateObjectPropertyExpression HasGrandparent)
∷ [] )
translatedStrictChainAxiomShape =
refl
strictChainCompleteSemanticTranslation :
Sem.CompleteSemanticTranslation strictChainDocument
strictChainCompleteSemanticTranslation =
refl
parentRankBelowGrandparentRank :
RankProof.RankedObjectPropertyLess
strictChainRanks
(Sem.translateObjectPropertyExpression HasParent)
(Sem.translateObjectPropertyExpression HasGrandparent)
parentRankBelowGrandparentRank =
RankProof.rankedObjectPropertyLess
0
1
refl
refl
(0 , refl)
strictChainPortableRegular :
RankProof.PortableRegularPropertyChainByRank
strictChainRanks
parentParentChain
HasGrandparent
strictChainPortableRegular =
RankProof.portableRegularStrictPropertyChain
parentRankBelowGrandparentRank
parentRankBelowGrandparentRank
tt*
strictChainSynthesizedPortableRegular :
RankProof.portableStrictRankedPropertyChainCertificate
strictChainRanks
parentParentChain
HasGrandparent
≡
present strictChainPortableRegular
strictChainSynthesizedPortableRegular =
refl
strictChainSynthesizedFactCertificates :
RankProof.strictOntologyDocumentPropertyChainAxiomFactsCertificates
strictChainRanks
strictChainDocument
≡
present (strictChainPortableRegular , tt*)
strictChainSynthesizedFactCertificates =
refl
strictChainTranslatedRegular :
Reg.RegularPropertyChain
(RankProof.RankedObjectPropertyLess strictChainRanks)
(Sem.translateObjectPropertyExpression HasParent)
(Sem.translateObjectPropertyExpression HasParent)
[]
(Sem.translateObjectPropertyExpression HasGrandparent)
strictChainTranslatedRegular =
RankProof.portableRegularPropertyChainByRank
strictChainPortableRegular
strictChainTranslatedAxiomRegular :
Reg.AxiomPropertyChainRegular
(RankProof.RankedObjectPropertyLess strictChainRanks)
(S.subObjectPropertyOf
(Sem.translateObjectPropertyChain parentParentChain)
(Sem.translateObjectPropertyExpression HasGrandparent))
strictChainTranslatedAxiomRegular =
RankProof.portableRegularPropertyChainAxiomByRank
strictChainPortableRegular
strictChainTranslatedAxiomsRegular :
Reg.AxiomsPropertyChainsRegular
(RankProof.RankedObjectPropertyLess strictChainRanks)
(S.axioms
(Sem.semanticOntology
(Sem.partialTranslateOntologyDocument strictChainDocument)))
strictChainTranslatedAxiomsRegular =
strictChainTranslatedAxiomRegular ,
tt*
strictChainTranslatedStrictOrder :
Reg.StrictChainOrder
Sem.PortableSignature
(S.axioms
(Sem.semanticOntology
(Sem.partialTranslateOntologyDocument strictChainDocument)))
strictChainTranslatedStrictOrder =
RankProof.rankedOntologyStrictChainOrder
strictChainRanks
(Sem.semanticOntology
(Sem.partialTranslateOntologyDocument strictChainDocument))
strictChainTranslatedAxiomsRegular
strictChainTranslatedStrictOrderFromDocumentCertificate :
Reg.StrictChainOrder
Sem.PortableSignature
(S.axioms
(Sem.semanticOntology
(Sem.partialTranslateOntologyDocument strictChainDocument)))
strictChainTranslatedStrictOrderFromDocumentCertificate =
RankProof.ontologyDocumentStrictChainOrderByRank
strictChainRanks
strictChainDocument
(strictChainPortableRegular , tt*)
strictChainTranslatedStrictOrderCertificatePresent :
RankProof.ontologyDocumentStrictChainOrderCertificateByRank
strictChainRanks
strictChainDocument
≡
present strictChainTranslatedStrictOrderFromDocumentCertificate
strictChainTranslatedStrictOrderCertificatePresent =
refl
topChainDocument : P.OntologyDocument
topChainDocument =
document
( axiom
(P.subObjectPropertyOf
(P.subObjectPropertyChain parentParentChain)
P.topObjectProperty)
∷ [] )
topChainReport : Rank.RegularityRankReport
topChainReport =
Rank.reportRegularityRank [] topChainDocument
topChainIssueCount :
Rank.regularityRankReportPropertyChainIssueCount topChainReport ≡ 0
topChainIssueCount =
refl
topChainAcceptedWithoutRanks :
Rank.PortableRegularityRankRestrictions [] topChainDocument
topChainAcceptedWithoutRanks =
tt*
topChainPortableRegular :
RankProof.PortableRegularPropertyChainByRank
[]
parentParentChain
P.topObjectProperty
topChainPortableRegular =
RankProof.portableRegularPropertyChainToTop
topChainSynthesizedPortableRegular :
RankProof.portableRankedPropertyChainCertificate
[]
parentParentChain
P.topObjectProperty
≡
present topChainPortableRegular
topChainSynthesizedPortableRegular =
refl
topChainSynthesizedFactCertificates :
RankProof.ontologyDocumentPropertyChainAxiomFactsCertificatesByRank
[]
topChainDocument
≡
present (topChainPortableRegular , tt*)
topChainSynthesizedFactCertificates =
refl
topChainStrictFactCertificateRejected :
RankProof.strictOntologyDocumentPropertyChainAxiomFactsCertificates
[]
topChainDocument
≡
absent
topChainStrictFactCertificateRejected =
refl
topChainPortableRegularWithStrictRanks :
RankProof.PortableRegularPropertyChainByRank
strictChainRanks
parentParentChain
P.topObjectProperty
topChainPortableRegularWithStrictRanks =
RankProof.portableRegularPropertyChainToTop
topChainTranslatedAxiomRegularWithStrictRanks :
Reg.AxiomPropertyChainRegular
(RankProof.RankedObjectPropertyLess strictChainRanks)
(S.subObjectPropertyOf
(Sem.translateObjectPropertyChain parentParentChain)
(Sem.translateObjectPropertyExpression P.topObjectProperty))
topChainTranslatedAxiomRegularWithStrictRanks =
RankProof.portableRegularPropertyChainAxiomByRank
topChainPortableRegularWithStrictRanks
topChainTranslatedAxiomsRegularWithStrictRanks :
Reg.AxiomsPropertyChainsRegular
(RankProof.RankedObjectPropertyLess strictChainRanks)
(S.axioms
(Sem.semanticOntology
(Sem.partialTranslateOntologyDocument topChainDocument)))
topChainTranslatedAxiomsRegularWithStrictRanks =
topChainTranslatedAxiomRegularWithStrictRanks ,
tt*
strictThenTopTranslatedAxiomsRegular :
Reg.AxiomsPropertyChainsRegular
(RankProof.RankedObjectPropertyLess strictChainRanks)
( S.axioms
(Sem.semanticOntology
(Sem.partialTranslateOntologyDocument strictChainDocument))
++
S.axioms
(Sem.semanticOntology
(Sem.partialTranslateOntologyDocument topChainDocument)) )
strictThenTopTranslatedAxiomsRegular =
RankProof.rankedAxiomsPropertyChainsRegularAppend
strictChainRanks
strictChainTranslatedAxiomsRegular
topChainTranslatedAxiomsRegularWithStrictRanks
strictChainAnnotatedAxiomsPropertyChainsRegular :
RankProof.AnnotatedAxiomsPropertyChainsRegularByRank
strictChainRanks
(P.axioms (P.documentOntology strictChainDocument))
strictChainAnnotatedAxiomsPropertyChainsRegular =
( RankProof.portableRegularPropertyChainByRank strictChainPortableRegular ,
tt* ) ,
tt*
strictChainTranslatedAnnotatedAxiomsRegular :
Reg.AxiomsPropertyChainsRegular
(RankProof.RankedObjectPropertyLess strictChainRanks)
(Sem.semanticAxioms
(Sem.translateAnnotatedAxioms
(P.axioms (P.documentOntology strictChainDocument))))
strictChainTranslatedAnnotatedAxiomsRegular =
RankProof.translatedAnnotatedAxiomsPropertyChainsRegularByRank
strictChainRanks
(P.axioms (P.documentOntology strictChainDocument))
strictChainAnnotatedAxiomsPropertyChainsRegular
strictChainExtractedAnnotatedAxiomsRegular :
RankProof.AnnotatedAxiomsPropertyChainsRegularByRank
strictChainRanks
(P.axioms (P.documentOntology strictChainDocument))
strictChainExtractedAnnotatedAxiomsRegular =
RankProof.propertyChainAxiomFactsCertifiedByRankToAnnotatedAxioms
strictChainRanks
(P.axioms (P.documentOntology strictChainDocument))
(strictChainPortableRegular , tt*)
strictChainExtractedTranslatedAxiomsRegular :
Reg.AxiomsPropertyChainsRegular
(RankProof.RankedObjectPropertyLess strictChainRanks)
(Sem.semanticAxioms
(Sem.translateAnnotatedAxioms
(P.axioms (P.documentOntology strictChainDocument))))
strictChainExtractedTranslatedAxiomsRegular =
RankProof.ontologyDocumentPropertyChainAxiomFactsCertifiedByRankToTranslatedAxioms
strictChainRanks
strictChainDocument
(strictChainPortableRegular , tt*)
strictChainOntologyExtractedTranslatedAxiomsRegular :
Reg.AxiomsPropertyChainsRegular
(RankProof.RankedObjectPropertyLess strictChainRanks)
(Sem.semanticAxioms
(Sem.translateAnnotatedAxioms
(P.axioms (P.documentOntology strictChainDocument))))
strictChainOntologyExtractedTranslatedAxiomsRegular =
RankProof.ontologyPropertyChainAxiomFactsCertifiedByRankToTranslatedAxioms
strictChainRanks
(P.documentOntology strictChainDocument)
(strictChainPortableRegular , tt*)
missingSuperRankRanks : List Rank.PropertyRank
missingSuperRankRanks =
Rank.propertyRankForExpression HasParent 0
∷ []
missingSuperRankReport : Rank.RegularityRankReport
missingSuperRankReport =
Rank.reportRegularityRank missingSuperRankRanks strictChainDocument
missingSuperRankIssueCount :
Rank.regularityRankReportPropertyChainIssueCount
missingSuperRankReport
≡ 1
missingSuperRankIssueCount =
refl
missingSuperRankRejected :
¬
Rank.PortableRegularityRankRestrictions
missingSuperRankRanks
strictChainDocument
missingSuperRankRejected impossible =
impossible
missingSuperRankCertificateRejected :
RankProof.portableStrictRankedPropertyChainCertificate
missingSuperRankRanks
parentParentChain
HasGrandparent
≡
absent
missingSuperRankCertificateRejected =
refl
missingSuperRankFactCertificateRejected :
RankProof.strictOntologyDocumentPropertyChainAxiomFactsCertificates
missingSuperRankRanks
strictChainDocument
≡
absent
missingSuperRankFactCertificateRejected =
refl
insufficientRankRanks : List Rank.PropertyRank
insufficientRankRanks =
Rank.propertyRankForExpression HasParent 1
∷ Rank.propertyRankForExpression HasGrandparent 1
∷ []
insufficientRankReport : Rank.RegularityRankReport
insufficientRankReport =
Rank.reportRegularityRank insufficientRankRanks strictChainDocument
insufficientRankIssueCount :
Rank.regularityRankReportPropertyChainIssueCount
insufficientRankReport
≡ 2
insufficientRankIssueCount =
refl
insufficientRankRejected :
¬
Rank.PortableRegularityRankRestrictions
insufficientRankRanks
strictChainDocument
insufficientRankRejected impossible =
impossible
insufficientRankCertificateRejected :
RankProof.portableStrictRankedPropertyChainCertificate
insufficientRankRanks
parentParentChain
HasGrandparent
≡
absent
insufficientRankCertificateRejected =
refl
insufficientRankFactCertificateRejected :
RankProof.strictOntologyDocumentPropertyChainAxiomFactsCertificates
insufficientRankRanks
strictChainDocument
≡
absent
insufficientRankFactCertificateRejected =
refl
selfChainDocument : P.OntologyDocument
selfChainDocument =
document
( axiom
(P.subObjectPropertyOf
(P.subObjectPropertyChain ancestorAncestorChain)
HasAncestor)
∷ [] )
selfChainReport : Rank.RegularityRankReport
selfChainReport =
Rank.reportRegularityRank [] selfChainDocument
selfChainIssueCount :
Rank.regularityRankReportPropertyChainIssueCount selfChainReport ≡ 0
selfChainIssueCount =
refl
selfChainAcceptedWithoutRanks :
Rank.PortableRegularityRankRestrictions [] selfChainDocument
selfChainAcceptedWithoutRanks =
tt*
translatedSelfChainAxiomShape :
Sem.translateAxiom
(P.subObjectPropertyOf
(P.subObjectPropertyChain ancestorAncestorChain)
HasAncestor)
≡
present
( S.subObjectPropertyOf
(S.subObjectPropertyChain
(Sem.translateObjectPropertyExpression HasAncestor)
(Sem.translateObjectPropertyExpression HasAncestor)
[])
(Sem.translateObjectPropertyExpression HasAncestor)
∷ [] )
translatedSelfChainAxiomShape =
refl
selfChainCompleteSemanticTranslation :
Sem.CompleteSemanticTranslation selfChainDocument
selfChainCompleteSemanticTranslation =
refl
selfChainExactTransitive :
RankProof.ExactTransitiveSelfPropertyChain
ancestorAncestorChain
HasAncestor
selfChainExactTransitive =
RankProof.exactTransitiveSelf
selfChainPortableRegular :
RankProof.PortableRegularPropertyChainByRank
[]
ancestorAncestorChain
HasAncestor
selfChainPortableRegular =
RankProof.exactTransitiveSelfPropertyChainByRank
selfChainExactTransitive
selfChainPortableRegularByEquality :
RankProof.PortableRegularPropertyChainByRank
[]
ancestorAncestorChain
HasAncestor
selfChainPortableRegularByEquality =
RankProof.portableRegularTransitivePropertyChainByEquality
refl
refl
selfChainPortableRegularDirect :
RankProof.PortableRegularPropertyChainByRank
[]
ancestorAncestorChain
HasAncestor
selfChainPortableRegularDirect =
RankProof.portableRegularTransitivePropertyChain
selfChainPortableRegularByExactEvidence :
RankProof.PortableRegularPropertyChainByRank
[]
ancestorAncestorChain
HasAncestor
selfChainPortableRegularByExactEvidence =
RankProof.portableRegularTransitivePropertyChainByExactEvidence
(refl , refl , refl)
selfChainExactEvidenceFromShapeReflection :
RankProof.ExactTransitiveSelfChainEvidence
ancestorAncestorChain
HasAncestor
selfChainExactEvidenceFromShapeReflection =
RankProof.chainIsTransitiveSelfShapeReflectsExactEvidence
ancestorAncestorChain
HasAncestor
refl
selfChainPortableRegularFromShapeReflection :
RankProof.PortableRegularPropertyChainByRank
[]
ancestorAncestorChain
HasAncestor
selfChainPortableRegularFromShapeReflection =
RankProof.portableRegularTransitivePropertyChainByExactEvidence
selfChainExactEvidenceFromShapeReflection
selfChainExactEvidenceSynthesized :
RankProof.ExactTransitiveSelfChainEvidence
ancestorAncestorChain
HasAncestor
selfChainExactEvidenceSynthesized =
optionalValueOr
(RankProof.exactTransitiveSelfChainEvidence
ancestorAncestorChain
HasAncestor)
(refl , refl , refl)
selfChainRankedOrExactCertificate :
RankProof.PortableRegularPropertyChainByRank
[]
ancestorAncestorChain
HasAncestor
selfChainRankedOrExactCertificate =
optionalValueOr
(RankProof.portableRankedOrExactSelfPropertyChainCertificate
[]
ancestorAncestorChain
HasAncestor)
selfChainPortableRegularByExactEvidence
selfChainSynthesizedFactCertificates :
RankProof.OntologyDocumentPropertyChainAxiomFactsCertifiedByRank
[]
selfChainDocument
selfChainSynthesizedFactCertificates =
optionalValueOr
(RankProof.ontologyDocumentPropertyChainAxiomFactsCertificatesByRank
[]
selfChainDocument)
(selfChainPortableRegularByExactEvidence , tt*)
selfChainExactEvidenceDecisionPresent :
RankProof.exactTransitiveSelfChainEvidence
ancestorAncestorChain
HasAncestor
≡ present selfChainExactEvidenceSynthesized
selfChainExactEvidenceDecisionPresent =
refl
selfChainRankedOrExactCertificateDecisionPresent :
RankProof.portableRankedOrExactSelfPropertyChainCertificate
[]
ancestorAncestorChain
HasAncestor
≡ present selfChainRankedOrExactCertificate
selfChainRankedOrExactCertificateDecisionPresent =
refl
selfChainSynthesizedFactCertificatesDecisionPresent :
RankProof.ontologyDocumentPropertyChainAxiomFactsCertificatesByRank
[]
selfChainDocument
≡ present selfChainSynthesizedFactCertificates
selfChainSynthesizedFactCertificatesDecisionPresent =
refl
selfChainExactFactCertificate :
RankProof.OntologyDocumentPropertyChainAxiomFactsCertifiedByRank
[]
selfChainDocument
selfChainExactFactCertificate =
selfChainPortableRegularByExactEvidence ,
tt*
selfChainExactFactTranslatedAxiomsRegular :
Reg.AxiomsPropertyChainsRegular
(RankProof.RankedObjectPropertyLess [])
(Sem.semanticAxioms
(Sem.translateAnnotatedAxioms
(P.axioms (P.documentOntology selfChainDocument))))
selfChainExactFactTranslatedAxiomsRegular =
RankProof.ontologyDocumentPropertyChainAxiomFactsCertifiedByRankToTranslatedAxioms
[]
selfChainDocument
selfChainExactFactCertificate
selfChainStrictFactCertificateRejected :
RankProof.strictOntologyDocumentPropertyChainAxiomFactsCertificates
[]
selfChainDocument
≡
absent
selfChainStrictFactCertificateRejected =
refl
inverseSelfChainShapeRejected :
Rank.chainIsTransitiveSelfShape
ancestorInverseChain
HasAncestor
≡
false
inverseSelfChainShapeRejected =
refl
inverseSelfChainExactEvidenceRejected :
RankProof.exactTransitiveSelfChainEvidence
ancestorInverseChain
HasAncestor
≡
absent
inverseSelfChainExactEvidenceRejected =
refl
inverseSelfChainDocument : P.OntologyDocument
inverseSelfChainDocument =
document
( axiom
(P.subObjectPropertyOf
(P.subObjectPropertyChain ancestorInverseChain)
HasAncestor)
∷ [] )
inverseSelfChainReport : Rank.RegularityRankReport
inverseSelfChainReport =
Rank.reportRegularityRank [] inverseSelfChainDocument
inverseSelfChainIssueCount :
Rank.regularityRankReportPropertyChainIssueCount inverseSelfChainReport ≡ 3
inverseSelfChainIssueCount =
refl
inverseSelfChainRejectedWithoutRanks :
¬ Rank.PortableRegularityRankRestrictions [] inverseSelfChainDocument
inverseSelfChainRejectedWithoutRanks impossible =
impossible
selfChainTranslatedRegular :
Reg.RegularPropertyChain
(RankProof.RankedObjectPropertyLess [])
(Sem.translateObjectPropertyExpression HasAncestor)
(Sem.translateObjectPropertyExpression HasAncestor)
[]
(Sem.translateObjectPropertyExpression HasAncestor)
selfChainTranslatedRegular =
RankProof.portableRegularPropertyChainByRank
selfChainPortableRegular
selfChainTranslatedAxiomRegular :
Reg.AxiomPropertyChainRegular
(RankProof.RankedObjectPropertyLess [])
(S.subObjectPropertyOf
(Sem.translateObjectPropertyChain ancestorAncestorChain)
(Sem.translateObjectPropertyExpression HasAncestor))
selfChainTranslatedAxiomRegular =
RankProof.portableRegularPropertyChainAxiomByRank
selfChainPortableRegular
selfChainTranslatedAxiomsRegular :
Reg.AxiomsPropertyChainsRegular
(RankProof.RankedObjectPropertyLess [])
(S.axioms
(Sem.semanticOntology
(Sem.partialTranslateOntologyDocument selfChainDocument)))
selfChainTranslatedAxiomsRegular =
selfChainTranslatedAxiomRegular ,
tt*
selfChainTranslatedStrictOrder :
Reg.StrictChainOrder
Sem.PortableSignature
(S.axioms
(Sem.semanticOntology
(Sem.partialTranslateOntologyDocument selfChainDocument)))
selfChainTranslatedStrictOrder =
RankProof.rankedOntologyStrictChainOrder
[]
(Sem.semanticOntology
(Sem.partialTranslateOntologyDocument selfChainDocument))
selfChainTranslatedAxiomsRegular