theory ExPS6+ −
imports "../NewParser"+ −
begin+ −
+ −
(* example 6 from Peter Sewell's bestiary *)+ −
+ −
atom_decl name+ −
+ −
(* Is this binding structure supported - I think not + −
because e1 occurs twice as body *)+ −
+ −
nominal_datatype exp =+ −
Var name+ −
| Pair exp exp+ −
| LetRec x::name p::pat e1::exp e2::exp bind x in e1 e2, bind "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.fv+ −
thm exp_pat.eq_iff+ −
thm exp_pat.bn+ −
thm exp_pat.perm+ −
thm exp_pat.induct+ −
thm exp_pat.distinct+ −
thm exp_pat.supp+ −
+ −
+ −
+ −
+ −
end+ −
+ −
+ −
+ −