theory NoneExamples

imports "../NewParser"

begin

atom_decl name

(* this example binds bound names and

   so is not respectful *)

(*

nominal_datatype trm =

  Vr "name"

| Lm x::"name" t::"trm"         bind x in t

| Lt left::"trm" right::"trm"   bind "bv left" in right

binder

  bv

where

  "bv (Vr n) = {}"

| "bv (Lm n t) = {atom n} \<union> bv t"

| "bv (Lt l r) = bv l \<union> bv r"

*)

(* this example uses "-" in the binding function; 

   at the moment this is unsupported *)

(*

nominal_datatype trm' =

  Vr' "name"

| Lm' l::"name" r::"trm'"   bind l in r

| Lt' l::"trm'" r::"trm'"   bind "bv' l" in r

binder

  bv'

where

  "bv' (Vr' n) = {atom n}"

| "bv' (Lm' n t) = bv' t - {atom n}"

| "bv' (Lt' l r) = bv' l \<union> bv' r"

*)

(* this example again binds bound names  *)

(*

nominal_datatype trm'' =

  Va'' "name"

| Lm'' n::"name" l::"trm''" bind n in l

and bla'' =

  Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s

binder

  bv''

where

  "bv'' (Vm'' x) = {}"

| "bv'' (Lm'' x b) = {atom x}"

*)

end