Ex4 does work, and I don't see the difference between the alphas.
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+ −
+ −
+ −
+ −