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::s1, 'b::s2, 'c::at) lam =
  Var "name"
| App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"
| Lam x::"name" l::"('a, 'b, 'c) lam"  binds x in l
| Foo "'a" "'b"
| Bar x::"'c" l::"('a, 'b, 'c) lam"  binds 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


nominal_datatype ('alpha, 'beta, 'gamma) psi =
  PsiNil
| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 


nominal_datatype 'a foo = 
  Node x::"name" f::"'a foo" binds x in f
| Leaf "'a"

term "Leaf"




end