(in-package "ACL2")

(include-book "rdf")

(namespace "rdfs"
	   "http://www.w3.org/2000/01/rdf-schema#"
	   ("domain" "range"
	    "Resource"
	    "Literal" "Datatype"
	    "Class"
	    "subClassOf" "subPropertyOf"
	    "member" "Container" "ContainerMembershipProperty" ; ugh.
	    "comment" "seeAlso" "isDefinedBy"
	    "label"
	    ) )

(defaxiom subclass-gen ;; rdfs9 in http://www.w3.org/TR/rdf-mt/#RDFRules
  (implies (and (holds (rdf-type) x c1)
                (holds (rdfs-subclassof) c1 c2) )
           (holds (rdf-type) x c2) ) )

(defaxiom subproperty-gen ;; rdfs7 in http://www.w3.org/TR/rdf-mt/#RDFRules
  (implies (and (holds p s o)
                (holds (rdfs-subPropertyOf) p q) )
           (holds q s o) ) )

(defaxiom domain-defn ;; rdfs2
  (implies (and (holds (rdfs-domain) P C)
		(holds P S O) )
	   (holds (rdf-type) S C) ) )

(defaxiom range-defn ;; rdfs2
  (implies (and (holds (rdfs-range) P C)
		(holds P S O) )
	   (holds (rdf-type) O C) ) )

(defaxiom subClassOf-transitivity ;rdfs11
  ;; this is a little boring; if we define subClassOf extensionally,
  ;; as in OWL, then this falls out as a theorem.
  (implies (and (holds (rdfs-subClassOf) c1 c2)
		(holds (rdfs-subClassOf) c2 c3) )
	   (holds (rdfs-subClassOf) c1 c3) ) )


;; RDFS axiomatic triples. leaving out reification stuff. bleah.
(defaxiom rdfs-domain-range
  (and (holds (rdfs-domain) (rdf-type) (rdfs-Resource))
       (holds (rdfs-range) (rdf-type) (rdfs-Class))

       (holds (rdfs-domain) (rdfs-domain) (rdf-Property))
       (holds (rdfs-range) (rdfs-domain) (rdfs-Class))

       (holds (rdfs-domain) (rdfs-range) (rdf-Property))
       (holds (rdfs-range) (rdfs-range) (rdfs-Class))

       (holds (rdfs-domain) (rdfs-subClassOf) (rdfs-Class))
       (holds (rdfs-range) (rdfs-subClassOf) (rdfs-Class))

       (holds (rdfs-domain) (rdfs-subPropertyOf) (rdf-Property))
       (holds (rdfs-range) (rdfs-subPropertyOf) (rdf-Property))

       (holds (rdf-type) (rdf-nil) (rdf-List))
       (holds (rdfs-domain) (rdf-first) (rdf-List))
       (holds (rdfs-domain) (rdf-rest) (rdf-List))
       (holds (rdfs-range) (rdf-rest) (rdf-List))
       ) )

(defaxiom isdefinedby
  (holds (rdfs-subPropertyOf) (rdfs-isDefinedBy) (rdfs-seeAlso)))

;; leaving out datatypes stuff, and some stuff about Literals
;; and leaving out some "boring" stuff like "everything is a Resource"