theory ExPS6+
−
imports "../Parser"+
−
begin+
−
+
−
(* example 6 from Peter Sewell's bestiary *)+
−
+
−
atom_decl name+
−
+
−
(* The binding structure is too complicated, so equivalence the+
−
   way we define it is not true *)+
−
+
−
ML {* val _ = recursive := false  *}+
−
nominal_datatype exp6 =+
−
  EVar name+
−
| EPair exp6 exp6+
−
| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1+
−
and pat6 =+
−
  PVar' name+
−
| PUnit'+
−
| PPair' pat6 pat6+
−
binder+
−
  bp6 :: "pat6 \<Rightarrow> atom set"+
−
where+
−
  "bp6 (PVar' x) = {atom x}"+
−
| "bp6 (PUnit') = {}"+
−
| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"+
−
+
−
thm exp6_pat6.fv+
−
thm exp6_pat6.eq_iff+
−
thm exp6_pat6.bn+
−
thm exp6_pat6.perm+
−
thm exp6_pat6.induct+
−
thm exp6_pat6.distinct+
−
thm exp6_pat6.supp+
−
+
−
end+
−
+
−
+
−
+
−