theory ExNotRsp

imports "Parser"

begin

atom_decl name

(* example 6 from Terms.thy *)

nominal_datatype trm6 =

  Vr6 "name"

| Lm6 x::"name" t::"trm6"         bind x in t

| Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right

binder

  bv6

where

  "bv6 (Vr6 n) = {}"

| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"

| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"

(* example 7 from Terms.thy *)

nominal_datatype trm7 =

  Vr7 "name"

| Lm7 l::"name" r::"trm7"   bind l in r

| Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r

binder

  bv7

where

  "bv7 (Vr7 n) = {atom n}"

| "bv7 (Lm7 n t) = bv7 t - {atom n}"

| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"

*)

(* example 9 from Terms.thy *)

nominal_datatype lam9 =

  Var9 "name"

| Lam9 n::"name" l::"lam9" bind n in l

and bla9 =

  Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s

binder

  bv9

where

  "bv9 (Var9 x) = {}"

| "bv9 (Lam9 x b) = {atom x}"

end