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 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 fnclauses+ −
and lrb8 =+ −
Clause fnclauses+ −
and lrbs8 =+ −
Single lrb8+ −
| More lrb8 lrbs8+ −
and pat8 =+ −
PVar name+ −
| PUnit+ −
| PPair pat8 pat8+ −
binder+ −
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_iff+ −
thm exp7_lrb_lrbs.supp+ −
+ −
end+ −
+ −
+ −
+ −