Nominal/Ex/ExPS7.thy
author Christian Urban <urbanc@in.tum.de>
Wed, 12 May 2010 16:33:25 +0100
changeset 2118 0e52851acac4
parent 2105 e25b0fff0dd2
child 2120 2786ff1df475
permissions -rw-r--r--
moved the data-transformation into the parser


theory ExPS7
imports "../NewParser"
begin

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

atom_decl name

nominal_datatype exp =
  Var name
| Unit
| Pair exp exp
| LetRec l::"lrbs" e::"exp"  bind_set "bs l" in l e
and lrb =
  Assign name exp
and lrbs =
  Single lrb
| More lrb lrbs
binder
  b :: "lrb \<Rightarrow> atom set" and
  bs :: "lrbs \<Rightarrow> atom set"
where
  "b (Assign x e) = {atom x}"
| "bs (Single a) = b a"
| "bs (More a as) = (b a) \<union> (bs as)"

thm exp_lrb_lrbs.eq_iff
thm exp_lrb_lrbs.supp

equivariance alpha_exp_raw

end