(*
  Forwards 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.

credential A R (^ B) => 
{!ismem (role A R) B}. 

credential A R0 (role B R1), 
ismem (role B R1) D => 
{!ismem (role A R0) D}. 

credential A R0 (linked_role B R1 R2), 
ismem (role B R1) D, 
ismem (role D R2) E => 
{!ismem (role A R0) E}. 

credential A R (inter Res), 
ismems Res B => 
{!ismem (role A R) B}.


ismems nil B. 

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


(*** Example Credential Assumptions ***)

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'}. 

***)