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