theory TypeVarsTest
imports "../Nominal2" 
begin

(* a nominal datatype with type variables and sorts *)


(* the sort constraints need to be attached to the  *)
(* first occurence of the type variables on the     *)
(* right-hand side                                  *)

atom_decl name

class s1
class s2

instance nat :: s1 ..
instance int :: s2 .. 

nominal_datatype ('a, 'b, 'c) lam =
  Var "name"
| App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam"
| Lam x::"name" l::"('a, 'b, 'c) lam"  bind x in l
| Foo "'a" "'b"
| Bar x::"'c" l::"('a, 'b, 'c) lam"  bind x in l   (* Bar binds a polymorphic atom *)

term Foo
term Bar

thm lam.distinct
thm lam.induct
thm lam.exhaust 
thm lam.strong_exhaust
thm lam.fv_defs
thm lam.bn_defs
thm lam.perm_simps
thm lam.eq_iff
thm lam.fv_bn_eqvt
thm lam.size_eqvt

(* FIXME: only works for type variables 'a 'b 'c *)

nominal_datatype ('a, 'b, 'c) psi =
  PsiNil
| Output "'a" "'a" "('a, 'b, 'c) psi" 


end