theory NoneExamples

imports "../NewParser"

begin

atom_decl name

text {* 

  "Weirdo" example from Peter Sewell's bestiary. 

  This example is not covered by our binding 

  specification.

*}

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

(* e1 occurs in two bodies *)

nominal_datatype exp =

  Var name

| Pair exp exp

| LetRec x::name p::pat e1::exp e2::exp  bind x in e1 e2, bind "bp p" in e1

and pat =

  PVar name

| PUnit

| PPair pat pat

binder

  bp :: "pat \<Rightarrow> atom list"

where

  "bp (PVar x) = [atom x]"

| "bp (PUnit) = []"

| "bp (PPair p1 p2) = bp p1 @ bp p2"

(* this example binds bound names and

   so is not respectful *)

(*

nominal_datatype trm =

  Vr "name"

| Lm x::"name" t::"trm"         bind x in t

| Lt left::"trm" right::"trm"   bind "bv left" in right

binder

  bv

where

  "bv (Vr n) = {}"

| "bv (Lm n t) = {atom n} \<union> bv t"

| "bv (Lt l r) = bv l \<union> bv r"

*)

(* this example uses "-" in the binding function; 

   at the moment this is unsupported *)

(*

nominal_datatype trm' =

  Vr' "name"

| Lm' l::"name" r::"trm'"   bind l in r

| Lt' l::"trm'" r::"trm'"   bind "bv' l" in r

binder

  bv'

where

  "bv' (Vr' n) = {atom n}"

| "bv' (Lm' n t) = bv' t - {atom n}"

| "bv' (Lt' l r) = bv' l \<union> bv' r"

*)

(* this example again binds bound names  *)

(*

nominal_datatype trm'' =

  Va'' "name"

| Lm'' n::"name" l::"trm''" bind n in l

and bla'' =

  Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s

binder

  bv''

where

  "bv'' (Vm'' x) = {}"

| "bv'' (Lm'' x b) = {atom x}"

*)

end