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