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"

    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 is 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 (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"  bind "bv f" in s1 f,  bind "bv f" in s2 f

| Bla2 f::"trm" s1::"trm" s2::"trm"  bind "bv f" in s1,  bind "bv f" in s2 f

| Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" bind "bv f" x in s1 f, bind y x in s2 

binder

  bv :: "trm \<Rightarrow> atom list"

where

  "bv (Var a) = [atom a]"

*)

end