theory NoneExamples+
−
imports "../Nominal2"+
−
begin+
−
+
−
text {*+
−
  This example is 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"+
−
    bind x in p1 p2, +
−
    bind 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"         bind x in t+
−
| Let left::"trm" right::"trm"   bind (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'"   bind l in r+
−
| Let l::"trm'" r::"trm'"   bind (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 not respectful+
−
*}+
−
+
−
(*+
−
nominal_datatype trm =+
−
  Var "name"+
−
| Lam n::"name" l::"trm" bind n in l+
−
and bla =+
−
  Bla f::"trm" s::"trm" bind (set) "bv f" in s+
−
binder+
−
  bv :: "trm \<Rightarrow> atom set"+
−
where+
−
  "bv (Vam x) = {}"+
−
| "bv (Lam x b) = {atom x}"+
−
*)+
−
+
−
end+
−
+
−
+
−
+
−