theory ExPS7imports "../NewParser"begin(* example 7 from Peter Sewell's bestiary *)atom_decl namenominal_datatype exp = Var name| Unit| Pair exp exp| LetRec l::"lrbs" e::"exp" bind_set "bs l" in l eand lrb = Assign name expand lrbs = Single lrb| More lrb lrbsbinder 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_iffthm exp_lrb_lrbs.suppequivariance alpha_exp_rawend