diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExPS8.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/ExPS8.thy Sat Apr 03 22:31:11 2010 +0200 @@ -0,0 +1,56 @@ +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 \ atom set" and + b_pat :: "pat8 \ atom set" and + b_fnclauses :: "fnclauses \ atom set" and + b_fnclause :: "fnclause \ atom set" and + b_lrb8 :: "lrb8 \ atom set" +where + "b_lrbs8 (Single l) = b_lrb8 l" +| "b_lrbs8 (More l ls) = b_lrb8 l \ b_lrbs8 ls" +| "b_pat (PVar x) = {atom x}" +| "b_pat (PUnit) = {}" +| "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" +| "b_fnclauses (S fc) = (b_fnclause fc)" +| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \ (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 + + +