theory LetFunimports "../Nominal2"beginatom_decl name(* x is bound in both e1 and e2; bp-names in p are bound only in e1 *)nominal_datatype exp = Var name| Pair exp exp| LetRec x::name p::pat e1::exp e2::exp binds x in e2, binds x "bp p" in e1and pat = PVar name| PUnit| PPair pat patbinder bp :: "pat \<Rightarrow> atom list"where "bp (PVar x) = [atom x]"| "bp (PUnit) = []"| "bp (PPair p1 p2) = bp p1 @ bp p2"thm exp_pat.distinctthm exp_pat.inductthm exp_pat.inductsthm exp_pat.exhaustthm exp_pat.fv_defsthm exp_pat.bn_defsthm exp_pat.perm_simpsthm exp_pat.eq_iffthm exp_pat.fv_bn_eqvtthm exp_pat.size_eqvtthm exp_pat.sizethm exp_pat.supportsthm exp_pat.fsuppthm exp_pat.suppend