(defvar *class-addition-counter* 0)

(defun classes-same-size (a labela b labelb)
  "Make it such that a and b must have individuals in a ratio of 1:1"
  (let ((prop (make-uri nil (format nil "ex:~a,~a_1_1-~a" labela labelb (incf *class-addition-counter*))))
	(inv-prop (make-uri nil (format nil "ex:~a,~a_1_1-~a" labelb labela (incf *class-addition-counter*)))))
    (list 
     (object-property prop :inverse-functional)
     (object-property prop :functional)
     (object-property inv-prop :inverse-functional  (inverse-of prop))
     (object-property inv-prop :functional)
     (class a :partial (restriction prop (some-values-from b)))
     (class b :partial (restriction inv-prop (some-values-from a))))))

(defun add-classes (sum a b)
  "Make it such that individuals that are instances of sum are in 1:1 ratio an element of either a or b (which are to be disjoint).
If a and b is finite, then c must be finite and have the sum of distinct individuals in a and b"
  (list 
   (disjoint-classes a b)
   (class sum :complete (union-of a b))))

(defun class-of-size (name n)
  "Assert that class name is of size n by using a nominal with n different individuals"
  (let ((names (loop repeat n
		  for name = (format nil "ex:unique-~a" (incf *class-addition-counter*))
		  collect name)))
    (list*
     (class name :complete (apply 'one-of (loop for name in names collect (make-uri nil name))))
     (apply 'different-individuals (loop for name in names collect (make-uri nil name)))
     (loop for name in names collect
	  (individual (make-uri nil name)))
     )))

;; should be inconsistent because 3 isn't 4
(with-ontology notequal ()
    ((classes-same-size !a "a" !b  "b")
     (class-of-size !a 3)
     (class-of-size !b 4))
  (check foo))

;; play games with the reasoner. With (a) and not (b) or (c) it should be inconsistent, I think.  Pellet says consistent.
;; Given also the hint b you think it might get it. Not pellet.
;; If (a) (b) there, then any size given in (c) is inconsistent.
;; For a good time, remove (b). Now pellet is consistent if the value in (c) is even, and not if odd :)

(let ((*class-addition-counter* 0))
  (with-ontology one+one ()
      ((classes-same-size !a "a" !b  "b")
       (classes-same-size !b "b" !c  "c")
       (disjoint-classes !a !b !c)
       (add-classes !two !b !c)
       (classes-same-size !two "two" !a "a") ; a) 2 = 1 nope. But reasoner says OK if we don't assert b or c
;       (class-of-size !a 3) ; b) should still be nope, but reasoner still says ok
;       (class-of-size !two 3) ; c) if a and b are ok, then this should be ok, right? (nope says the reasoner). 
       )
    (prin1 (abstract-syntax one+one))
    (check one+one t)
    (print-db (unsatisfiable-classes one+one))
    (write-rdfxml one+one)))

#|

Namespace(ex = <http://example.com/>)
Ontology(<http://example.com/> ObjectProperty(<http://example.com/a,b_1_1-1> InverseFunctional )
ObjectProperty(<http://example.com/a,b_1_1-1> Functional )
ObjectProperty(<http://example.com/b,a_1_1-2> inverseOf(<http://example.com/a,b_1_1-1> )InverseFunctional )
ObjectProperty(<http://example.com/b,a_1_1-2> Functional )
Class(ex:a partial restriction(<http://example.com/a,b_1_1-1> someValuesFrom(ex:b )))
Class(ex:b partial restriction(<http://example.com/b,a_1_1-2> someValuesFrom(ex:a )))
ObjectProperty(<http://example.com/b,c_1_1-3> InverseFunctional )
ObjectProperty(<http://example.com/b,c_1_1-3> Functional )
ObjectProperty(<http://example.com/c,b_1_1-4> inverseOf(<http://example.com/b,c_1_1-3> )InverseFunctional )
ObjectProperty(<http://example.com/c,b_1_1-4> Functional )
Class(ex:b partial restriction(<http://example.com/b,c_1_1-3> someValuesFrom(ex:c )))
Class(ex:c partial restriction(<http://example.com/c,b_1_1-4> someValuesFrom(ex:b )))
DisjointClasses(ex:a ex:b ex:c )
DisjointClasses(ex:b ex:c )
Class(ex:two complete unionOf(ex:b ex:c ))

(a)

ObjectProperty(<http://example.com/two,a_1_1-5> InverseFunctional )
ObjectProperty(<http://example.com/two,a_1_1-5> Functional )
ObjectProperty(<http://example.com/a,two_1_1-6> inverseOf(<http://example.com/two,a_1_1-5> )InverseFunctional )
ObjectProperty(<http://example.com/a,two_1_1-6> Functional )
Class(ex:two partial restriction(<http://example.com/two,a_1_1-5> someValuesFrom(ex:a )))
Class(ex:a partial restriction(<http://example.com/a,two_1_1-6> someValuesFrom(ex:two )))

(b)
Class(ex:a complete oneOf(<http://example.com/unique-7> <http://example.com/unique-8> <http://example.com/unique-9> ))
DifferentIndividuals(<http://example.com/unique-7> <http://example.com/unique-8> <http://example.com/unique-9> )
Individual(<http://example.com/unique-7> )
Individual(<http://example.com/unique-8> )
Individual(<http://example.com/unique-9> )

(c)

Class(ex:two complete oneOf(<http://example.com/unique-10> <http://example.com/unique-11> <http://example.com/unique-12> ))
DifferentIndividuals(<http://example.com/unique-10> <http://example.com/unique-11> <http://example.com/unique-12> )
Individual(<http://example.com/unique-10> )
Individual(<http://example.com/unique-11> )
Individual(<http://example.com/unique-12> )
)

|#