theory ExPS8+
−
imports "../Parser"+
−
begin+
−
+
−
(* example 8 from Peter Sewell's bestiary *)+
−
+
−
atom_decl name+
−
+
−
(* One function is recursive and the other one is not,+
−
   and as the parser cannot handle this we cannot set+
−
   the reference.  *)+
−
ML {* val _ = recursive := false  *}+
−
+
−
nominal_datatype exp =+
−
  EVar name+
−
| EUnit+
−
| EPair exp exp+
−
| ELetRec l::lrbs e::exp bind "b_lrbs l" in e (* rec *)+
−
and fnclause =+
−
  K x::name p::pat f::exp bind "b_pat p" in f (* non-rec *)+
−
and fnclauses =+
−
  S fnclause+
−
| ORs fnclause fnclauses+
−
and lrb =+
−
  Clause fnclauses+
−
and lrbs =+
−
  Single lrb+
−
| More lrb lrbs+
−
and pat =+
−
  PVar name+
−
| PUnit+
−
| PPair pat pat+
−
binder+
−
  b_lrbs :: "lrbs \<Rightarrow> atom set" and+
−
  b_pat :: "pat \<Rightarrow> atom set" and+
−
  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and+
−
  b_fnclause :: "fnclause \<Rightarrow> atom set" and+
−
  b_lrb :: "lrb \<Rightarrow> atom set"+
−
where+
−
  "b_lrbs (Single l) = b_lrb l"+
−
| "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"+
−
| "b_pat (PVar x) = {atom x}"+
−
| "b_pat (PUnit) = {}"+
−
| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"+
−
| "b_fnclauses (S fc) = (b_fnclause fc)"+
−
| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"+
−
| "b_lrb (Clause fcs) = (b_fnclauses fcs)"+
−
| "b_fnclause (K x pat exp) = {atom x}"+
−
+
−
thm exp7_lrb_lrbs.eq_iff+
−
thm exp7_lrb_lrbs.supp+
−
+
−
end+
−
+
−
+
−
+
−