335 thm bv_raw.simps

   335 (*thm bv_raw.simps*)

   336 

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

   338 nominal_datatype exp =

   339   Var name

   340 | App exp exp

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

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

   343 and pat =

   344   PVar name

   345 | PUnit

   346 | PPair pat pat

   347 binder

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

   349 where

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

   351 | "bp (PUnit) = {}"

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

   353 

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

   355 nominal_datatype exp6 =

   356   EVar name

   357 | EPair exp6 exp6

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

   359 and pat6 =

   360   PVar name

   361 | PUnit

   362 | PPair pat6 pat6

   363 binder

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

   365 where

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

   367 | "bp6 (PUnit) = {}"

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

   369 

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

   371 nominal_datatype exp7 =

   372   EVar name

   373 | EUnit

   374 | EPair exp7 exp7

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

   376 and lrb =

   377   Assign name exp7

   378 and lrbs =

   379   Single lrb

   380 | More lrb lrbs

   381 binder

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

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

   384 where

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

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

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

   388 

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

   390 nominal_datatype exp8 =

   391   EVar name

   392 | EUnit

   393 | EPair exp8 exp8

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

   395 and fnclause =

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

   397 and fnclauses =

   398   S fnclause

   399 | ORs fnclause fnclauses

   400 and lrb8 =

   401   Clause fnclauses

   402 and lrbs8 =

   403   Single lrb8

   404 | More lrb8 lrbs8

   405 and pat8 =

   406   PVar name

   407 | PUnit

   408 | PPair pat8 pat8

   409 binder

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

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

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

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

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

   415 where

   416   "b_lrbs8 (Single l) = b_lrb8 l"

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

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

   419 | "b_pat (PUnit) = {}"

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

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

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

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

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

   425 

   426 

   427 

   428 

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

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