theory NoneExamples+ −
imports "../Nominal2"+ −
begin+ −
+ −
text {*+ −
These examples are not covered by our binding + −
specification.+ −
*}+ −
+ −
atom_decl name+ −
+ −
text {* + −
"Weirdo" example from Peter Sewell's bestiary. + −
+ −
p2 occurs in two bodies+ −
*}+ −
+ −
(*+ −
nominal_datatype weird =+ −
Foo_var "name"+ −
| Foo_pair "weird" "weird" + −
| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"+ −
binds x in p1 p2, + −
binds y in p2 p3+ −
*)+ −
+ −
text {* + −
This example binds bound names and therefore the + −
fv-function is not respectful - the proof just fails.+ −
*}+ −
+ −
(*+ −
nominal_datatype trm =+ −
Var "name"+ −
| Lam x::"name" t::"trm" binds x in t+ −
| Let left::"trm" right::"trm" binds (set) "bv left" in right+ −
binder+ −
bv+ −
where+ −
"bv (Var n) = {}"+ −
| "bv (Lam n t) = {atom n} \<union> bv t"+ −
| "bv (Let l r) = bv l \<union> bv r"+ −
*)+ −
+ −
text {* + −
This example uses "-" in the binding function; + −
at the moment this is unsupported + −
*}+ −
+ −
(*+ −
nominal_datatype trm' =+ −
Var "name"+ −
| Lam l::"name" r::"trm'" binds l in r+ −
| Let l::"trm'" r::"trm'" binds (set) "bv' l" in r+ −
binder+ −
bv'+ −
where+ −
"bv' (Var n) = {atom n}"+ −
| "bv' (Lam n t) = bv' t - {atom n}"+ −
| "bv' (Let l r) = bv' l \<union> bv' r"+ −
*)+ −
+ −
text {* + −
Again this example binds bound names - so is not respectful+ −
*}+ −
+ −
(*+ −
nominal_datatype trm =+ −
Var "name"+ −
| Lam n::"name" l::"trm" binds n in l+ −
and bla =+ −
Bla f::"trm" s::"trm" binds (set) "bv f" in s+ −
binder+ −
bv :: "trm \<Rightarrow> atom set"+ −
where+ −
"bv (Var x) = {}"+ −
| "bv (Lam x b) = {atom x}"+ −
*)+ −
+ −
text {*+ −
This example has mal-formed deep recursive binders.+ −
+ −
- Bla1: recursive deep binder used twice+ −
- Bla2: deep binder used recursively and non-recursively+ −
- Bla3: x used in recursive deep binder and somewhere else+ −
*}+ −
+ −
(*+ −
nominal_datatype trm =+ −
Var "name"+ −
and bla =+ −
App "trm" "trm"+ −
| Bla1 f::"trm" s1::"trm" s2::"trm" binds "bv f" in s1 f, binds "bv f" in s2 f+ −
| Bla2 f::"trm" s1::"trm" s2::"trm" binds "bv f" in s1, binds "bv f" in s2 f+ −
| Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" binds "bv f" x in s1 f, binds y x in s2 + −
binder+ −
bv :: "trm \<Rightarrow> atom list"+ −
where+ −
"bv (Var a) = [atom a]"+ −
*)+ −
+ −
+ −
end+ −
+ −
+ −
+ −