theory Multi_Recs+ −
imports "../Nominal2"+ −
begin+ −
+ −
(* + −
multiple recursive binders+ −
+ −
example 7 from Peter Sewell's bestiary + −
+ −
*)+ −
+ −
atom_decl name+ −
+ −
nominal_datatype multi_recs: 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 multi_recs.distinct+ −
thm multi_recs.induct+ −
thm multi_recs.inducts+ −
thm multi_recs.exhaust+ −
thm multi_recs.fv_defs+ −
thm multi_recs.bn_defs+ −
thm multi_recs.perm_simps+ −
thm multi_recs.eq_iff+ −
thm multi_recs.fv_bn_eqvt+ −
thm multi_recs.size_eqvt+ −
thm multi_recs.supports+ −
thm multi_recs.fsupp+ −
thm multi_recs.supp+ −
+ −
end+ −
+ −
+ −
+ −