theory LetFun+ −
imports "../Nominal2"+ −
begin+ −
+ −
atom_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 bind x in e2, bind x "bp p" in e1+ −
and pat =+ −
PVar name+ −
| PUnit+ −
| PPair pat pat+ −
binder+ −
bp :: "pat \<Rightarrow> atom list"+ −
where+ −
"bp (PVar x) = [atom x]"+ −
| "bp (PUnit) = []"+ −
| "bp (PPair p1 p2) = bp p1 @ bp p2"+ −
+ −
thm exp_pat.distinct+ −
thm exp_pat.induct+ −
thm exp_pat.inducts+ −
thm exp_pat.exhaust+ −
thm exp_pat.fv_defs+ −
thm exp_pat.bn_defs+ −
thm exp_pat.perm_simps+ −
thm exp_pat.eq_iff+ −
thm exp_pat.fv_bn_eqvt+ −
thm exp_pat.size_eqvt+ −
thm exp_pat.supports+ −
thm exp_pat.fsupp+ −
thm exp_pat.supp+ −
+ −
+ −
end+ −