(*
  Backwards chaining specification of ismem.
*)

entity : type.

role_name : type.

role_expr : type.
^ : entity -> role_expr.
role : entity -> role_name -> role_expr.
linked_role : entity -> role_name -> role_name -> role_expr.
inter : list role_expr -> role_expr.

credential : entity -> role_name -> role_expr -> o.


ismem : role_expr -> entity -> o.
ismems : list role_expr -> entity -> o.

ismem (role A R) B <= credential A R (^ B). 

ismem (role A R0) D <= 
  credential A R0 (role B R1), 
  ismem (role B R1) D. 

ismem (role A R0) E <= 
  credential A R0 (linked_role B R1 R2), 
  ismem (role B R1) D, 
  ismem (role D R2) E. 

ismem (role A R) E <= 
  credential A R (inter Res), 
  ismems Res E. 


ismems nil B. 

ismems ((role A R)::Res) B <= 
  ismem (role A R) B, 
  ismems Res B. 


(*** Examples ***)

a : entity.
b : entity.
ab : entity.
c : entity.
d : entity.
e : entity.

rab : role_name.
r1 : role_name.
r2 : role_name.
r3 : role_name.
r4 : role_name.

credential a r1 (inter (role ab rab :: role c r4 :: nil)).
credential ab rab (linked_role b r2 r3).
credential b r2 (^ e).
credential e r3 (^ d).
credential c r4 (role e r3). 


(*** Example Queries

ismem (role b r2) e.
ismem (role e r3) d.
ismem (role c r4) d.
ismem (role a r1) d.

***)


a' : entity.
c' : entity.
d' : entity.

r1' : role_name.
r2' : role_name.

credential c' r2' (^ d'). 
credential a' r1' (^ c'). 
credential a' r2' (role c' r2'). 
credential c' r2' (role a' r2').

(*** Example Queries

ismem (role a' r2') d'. 

***)