@prefix dc: <http://purl.org/dc/elements/1.1/>.

<> dc:title "Infoset Utilites";
 dc:source <http://www.w3.org/TR/2001/WD-xml-infoset-20010316/>;
 dc:description """rules and such...""".

@prefix iu: <infosetUtil#>.
@prefix dl: <http://www.w3.org/2001/03swell/lists#>.
@prefix sws: <http://www.w3.org/2001/03swell/finiteSet#>.
@prefix dpo:  <http://www.daml.org/2001/03/daml+oil#> .
@prefix rdf:  <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix is: <http://www.w3.org/2001/05id/infoset#> . #@@ move this there.
@prefix : <#>. #variables

iu:AbsoluteURIref   rdfs:label "Abs. URIref";
  rdfs:subClassOf rdfs:Literal;
  rdfs:comment "@@hmm... before or after %xx-ing unicode chars?";
  rdfs:comment "@@connect with XML Schema data type and/or 03swell/URI stuff.".

iu:AbsoluteURI   rdfs:label "Absolute URI";
  rdfs:subClassOf iu:AbsoluteURIref;
  rdfs:comment "@@hmm... before or after %xx-ing unicode chars?".

iu:String  rdfs:label "String";
  rdfs:subClassOf rdfs:Literal;
  rdfs:comment "@@connect with XML Schema data type stuff".

iu:Boolean rdfs:label "Boolean";
  rdfs:subClassOf rdfs:Literal;
  dpo:oneOf ( iu:true iu:false );
  rdfs:comment "@@connect with XML Schema data type stuff".
iu:true rdfs:label "true".
iu:false rdfs:label "false".

rdfs:Literal rdfs:label "Literal".

iu:EncName rdfs:label "EncName";
  iu:pattern "[A-Za-z][A-Za-z0-9._-]*"; #@@ double-check this.
  rdfs:isDefinedBy <http://www.w3.org/TR/REC-xml#NT-EncName>;
  rdfs:subClassOf iu:Name;
  rdfs:comment"production [81] from the XML spec".

iu:Name rdfs:label "Name";
  iu:pattern "@@";
  rdfs:subClassOf iu:String;
  rdfs:comment"production [@@] from the XML spec".

iu:NCName rdfs:label "NCName";
  iu:pattern "@@";
  rdfs:subClassOf iu:Name;
  rdfs:comment"production [@@] from the Namespaces in XML spec".

#@@@iu:Prefix rdfs:label "Prefix";
#  dpo:disjointUnionOf (iu:NoValue iu:NCName).

iu:VersionNum rdfs:label "VersionNum";
  iu:pattern "[a-zA-Z0-9_.:-]+";
  rdfs:subClassOf iu:String;
  rdfs:isDefinedBy <http://www.w3.org/TR/REC-xml#NT-VersionNum>.

iu:pattern rdfs:label "pattern";
  rdfs:comment "@@xml schema datatype facet";
  rdfs:domain rdfs:Class.

iu:StandAloneType rdfs:label "Standalone Type";
  dpo:oneOf ( is:yes is:no ).
iu:NoValue rdfs:label "No Value";
  dpo:oneOf ( is:noValue ). #@@ cf bottom in KIF v3

## Logic utilities...
#@@{ :P log:means :Q } log:implies { :P log:implies :Q. :Q log:implies :P. }.
         
# explain a bit of daml...
dpo:toClass rdfs:range rdfs:Class.
dpo:toClass rdfs:domain rdfs:Class.

this log:forAll :C1, :s, :p, :o, :L, :C2.

{ :C1 dpo:disjointUnionOf :L.
  :L dl:member :C2 }
  log:implies { :C2 rdfs:subClassOf :C1 }.

{ :s a [ dpo:onProperty :p; dpo:hasValue :o ]. }
  log:implies { :s :p :o }.

dpo:oneOf rdfs:domain rdfs:Class.

#@@ { :C1 dpo:oneOf :L.
#  :L dl:member :x.
#}
#  log:implies { :x a :L }.

# some rdfs rules...
rdfs:domain rdfs:domain rdfs:Class.
rdfs:range rdfs:domain rdfs:Class.

this log:forAll :s, :p, :o, :C.

#subproperty
{ :s [ rdfs:subPropertyOf :p ] :o. }
log:implies { :s :p :o }.

#subclass
{ :s rdf:type [ rdfs:subClassOf :C ] }
log:implies { :s rdf:type :C. }.
rdfs:subClassOf rdfs:domain rdfs:Class.

# (part of?) the definition of rdfs:domain...
{ :s :p :o.
  :p rdfs:domain :C. } log:implies { :s a :C }.

# transitivity of subClassOf
{ :s rdfs:subClassOf [ rdfs:subClassOf :o ] }
  log:implies { :s rdfs:subClassOf :o }.