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