some small tunings (incompleted work in Lambda.thy)
theory ExPS8imports "../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 exp8 = EVar name| EUnit| EPair exp8 exp8| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *)and fnclause = K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *)and fnclauses = S fnclause| ORs fnclause fnclausesand lrb8 = Clause fnclausesand lrbs8 = Single lrb8| More lrb8 lrbs8and pat8 = PVar name| PUnit| PPair pat8 pat8binder b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and b_pat :: "pat8 \<Rightarrow> atom set" and b_fnclauses :: "fnclauses \<Rightarrow> atom set" and b_fnclause :: "fnclause \<Rightarrow> atom set" and b_lrb8 :: "lrb8 \<Rightarrow> atom set"where "b_lrbs8 (Single l) = b_lrb8 l"| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 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_lrb8 (Clause fcs) = (b_fnclauses fcs)"| "b_fnclause (K x pat exp8) = {atom x}"thm exp7_lrb_lrbs.eq_iffthm exp7_lrb_lrbs.suppend