339 (*thm bv_raw.simps*)

   340 

   341 (* example 3 from Peter Sewell's bestiary *)

   342 nominal_datatype exp =

   343   Var name

   344 | App exp exp

   345 | Lam x::name e::exp bind x in e

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

   347 and pat =

   348   PVar name

   349 | PUnit

   350 | PPair pat pat

   351 binder

   352   bp :: "pat \<Rightarrow> atom set"

   353 where

   354   "bp (PVar x) = {atom x}"

   355 | "bp (PUnit) = {}"

   356 | "bp (PPair p1 p2) = bp p1 \<union> bp p2"

   357 

   358 (* example 6 from Peter Sewell's bestiary *)

   359 nominal_datatype exp6 =

   360   EVar name

   361 | EPair exp6 exp6

   362 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1

   363 and pat6 =

   364   PVar name

   365 | PUnit

   366 | PPair pat6 pat6

   367 binder

   368   bp6 :: "pat6 \<Rightarrow> atom set"

   369 where

   370   "bp6 (PVar x) = {atom x}"

   371 | "bp6 (PUnit) = {}"

   372 | "bp6 (PPair p1 p2) = bp6 p1 \<union> bp6 p2"

   373 

   374 (* example 7 from Peter Sewell's bestiary *)

   375 nominal_datatype exp7 =

   376   EVar name

   377 | EUnit

   378 | EPair exp7 exp7

   379 | ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l

   380 and lrb =

   381   Assign name exp7

   382 and lrbs =

   383   Single lrb

   384 | More lrb lrbs

   385 binder

   386   b7 :: "lrb \<Rightarrow> atom set" and

   387   b7s :: "lrbs \<Rightarrow> atom set"

   388 where

   389   "b7 (Assign x e) = {atom x}"

   390 | "b7s (Single a) = b7 a"

   391 | "b7s (More a as) = (b7 a) \<union> (b7s as)"

   392 

   393 (* example 8 from Peter Sewell's bestiary *)

   394 nominal_datatype exp8 =

   395   EVar name

   396 | EUnit

   397 | EPair exp8 exp8

   398 | ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l

   399 and fnclause =

   400   K x::name p::pat8 e::exp8 bind "b_pat p" in e

   401 and fnclauses =

   402   S fnclause

   403 | ORs fnclause fnclauses

   404 and lrb8 =

   405   Clause fnclauses

   406 and lrbs8 =

   407   Single lrb8

   408 | More lrb8 lrbs8

   409 and pat8 =

   410   PVar name

   411 | PUnit

   412 | PPair pat8 pat8

   413 binder

   414   b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and

   415   b_pat :: "pat8 \<Rightarrow> atom set" and

   416   b_fnclauses :: "fnclauses \<Rightarrow> atom set" and

   417   b_fnclause :: "fnclause \<Rightarrow> atom set" and

   418   b_lrb8 :: "lrb8 \<Rightarrow> atom set"

   419 where

   420   "b_lrbs8 (Single l) = b_lrb8 l"

   421 | "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"

   422 | "b_pat (PVar x) = {atom x}"

   423 | "b_pat (PUnit) = {}"

   424 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"

   425 | "b_fnclauses (S fc) = (b_fnclause fc)"

   426 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"

   427 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"

   428 | "b_fnclause (K x pat exp8) = {atom x}"

   429 

   430 

   431 

   432 

   433 (* example 9 from Peter Sewell's bestiary *)

   434 (* run out of steam at the moment *)

   435