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

module OWL2.Examples.Family.Lemmas where

open import OWL2.Prelude
open import OWL2.Syntax
open import OWL2.DirectSemantics
open import OWL2.DirectSemantics.Lemmas
open import OWL2.Examples.Family

johnHasSpouseMary :
  evalObjectProperty familyInterpretation HasSpouse johnObject maryObject
johnHasSpouseMary =
  objectSubProperty
    {I = familyInterpretation}
    {p = subObjectProperty HasWife}
    {q = HasSpouse}
    {x = johnObject}
    {y = maryObject}
    wifeImpliesSpouse
    johnHasWifeMary

johnIsManFromHasWife :
  evalClass familyInterpretation ManC johnObject
johnIsManFromHasWife =
  objectDomainInfer
    {I = familyInterpretation}
    {p = HasWife}
    {c = ManC}
    {x = johnObject}
    {y = maryObject}
    hasWifeDomain
    johnHasWifeMary

maryIsWomanFromHasWife :
  evalClass familyInterpretation WomanC maryObject
maryIsWomanFromHasWife =
  objectRangeInfer
    {I = familyInterpretation}
    {p = HasWife}
    {c = WomanC}
    {x = johnObject}
    {y = maryObject}
    hasWifeRange
    johnHasWifeMary

johnIsPersonFromHasWife :
  evalClass familyInterpretation PersonC johnObject
johnIsPersonFromHasWife =
  classSubsumption
    {I = familyInterpretation}
    {c = ManC}
    {d = PersonC}
    {x = johnObject}
    manSubPerson
    johnIsManFromHasWife

maryIsPersonFromHasWife :
  evalClass familyInterpretation PersonC maryObject
maryIsPersonFromHasWife =
  classSubsumption
    {I = familyInterpretation}
    {c = WomanC}
    {d = PersonC}
    {x = maryObject}
    womanSubPerson
    maryIsWomanFromHasWife

johnHasSomeWife :
  evalClass familyInterpretation
    (objectSomeValuesFrom HasWife WomanC)
    johnObject
johnHasSomeWife =
  objectSomeIntro
    {I = familyInterpretation}
    {p = HasWife}
    {c = WomanC}
    {x = johnObject}
    {y = maryObject}
    johnHasWifeMary
    maryIsWomanFromHasWife

johnHasSomeSpouseWhoIsWoman :
  evalClass familyInterpretation
    (objectSomeValuesFrom HasSpouse WomanC)
    johnObject
johnHasSomeSpouseWhoIsWoman =
  objectSomeIntro
    {I = familyInterpretation}
    {p = HasSpouse}
    {c = WomanC}
    {x = johnObject}
    {y = maryObject}
    johnHasSpouseMary
    maryIsWomanFromHasWife

johnOnlyHasWomanWives :
  evalClass familyInterpretation
    (objectAllValuesFrom HasWife WomanC)
    johnObject
johnOnlyHasWomanWives maryObject johnMaryWife =
  maryWoman

maryIsWomanByUniversalRestriction :
  evalClass familyInterpretation WomanC maryObject
maryIsWomanByUniversalRestriction =
  objectAllApply
    {I = familyInterpretation}
    {p = HasWife}
    {c = WomanC}
    {x = johnObject}
    {y = maryObject}
    johnOnlyHasWomanWives
    johnHasWifeMary

johnIsManAndPerson :
  evalClass familyInterpretation
    (objectIntersectionOf (ManC ∷ PersonC ∷ []))
    johnObject
johnIsManAndPerson =
  objectIntersectionIntro
    {I = familyInterpretation}
    {c = ManC}
    {cs = PersonC ∷ []}
    {x = johnObject}
    johnIsManFromHasWife
    (objectIntersectionIntro
      {I = familyInterpretation}
      {c = PersonC}
      {cs = []}
      {x = johnObject}
      johnIsPersonFromHasWife
      (lift tt))

johnIsManOrWoman :
  evalClass familyInterpretation
    (objectUnionOf (ManC ∷ WomanC ∷ []))
    johnObject
johnIsManOrWoman =
  objectUnionLeft
    {I = familyInterpretation}
    {c = ManC}
    {cs = WomanC ∷ []}
    {x = johnObject}
    johnIsManFromHasWife

johnAgeInIntegerRange :
  evalDataRange familyInterpretation IntegerRange number42
johnAgeInIntegerRange =
  dataRangeInfer
    {I = familyInterpretation}
    {p = Age}
    {d = IntegerRange}
    {x = johnObject}
    {y = number42}
    ageRangeInteger
    johnAge42

johnHasIntegerAge :
  evalClass familyInterpretation
    (dataSomeValuesFrom Age IntegerRange)
    johnObject
johnHasIntegerAge =
  dataSomeIntro
    {I = familyInterpretation}
    {p = Age}
    {d = IntegerRange}
    {x = johnObject}
    {y = number42}
    johnAge42
    johnAgeInIntegerRange

johnOnlyHasIntegerAges :
  evalClass familyInterpretation
    (dataAllValuesFrom Age IntegerRange)
    johnObject
johnOnlyHasIntegerAges number42 johnAge42 =
  tt

johnAgeIntegerByUniversalRestriction :
  evalDataRange familyInterpretation IntegerRange number42
johnAgeIntegerByUniversalRestriction =
  dataAllApply
    {I = familyInterpretation}
    {p = Age}
    {d = IntegerRange}
    {x = johnObject}
    {y = number42}
    johnOnlyHasIntegerAges
    johnAge42