+ −
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+ −
+ −
+ −
end+ −
+ −
+ −
+ −