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