theory ExPS7+
−
imports "../NewParser"+
−
begin+
−
+
−
(* example 7 from Peter Sewell's bestiary *)+
−
+
−
atom_decl name+
−
+
−
nominal_datatype exp7 =+
−
  EVar name+
−
| EUnit+
−
| EPair exp7 exp7+
−
| ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l e+
−
and lrb =+
−
  Assign name exp7+
−
and lrbs =+
−
  Single lrb+
−
| More lrb lrbs+
−
binder+
−
  b7 :: "lrb \<Rightarrow> atom set" and+
−
  b7s :: "lrbs \<Rightarrow> atom set"+
−
where+
−
  "b7 (Assign x e) = {atom x}"+
−
| "b7s (Single a) = b7 a"+
−
| "b7s (More a as) = (b7 a) \<union> (b7s as)"+
−
thm exp7_lrb_lrbs.eq_iff+
−
thm exp7_lrb_lrbs.supp+
−
+
−
end+
−
+
−
+
−
+
−