1 theory ExPS8

     2 imports "Parser"

     3 begin

     4 

     5 (* example 8 from Peter Sewell's bestiary *)

     6 

     7 atom_decl name

     8 

     9 (* One function is recursive and the other one is not,

    10    and as the parser cannot handle this we cannot set

    11    the reference.  *)

    12 ML {* val _ = recursive := false  *}

    13 

    14 nominal_datatype exp8 =

    15   EVar name

    16 | EUnit

    17 | EPair exp8 exp8

    18 | ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *)

    19 and fnclause =

    20   K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *)

    21 and fnclauses =

    22   S fnclause

    23 | ORs fnclause fnclauses

    24 and lrb8 =

    25   Clause fnclauses

    26 and lrbs8 =

    27   Single lrb8

    28 | More lrb8 lrbs8

    29 and pat8 =

    30   PVar name

    31 | PUnit

    32 | PPair pat8 pat8

    33 binder

    34   b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and

    35   b_pat :: "pat8 \<Rightarrow> atom set" and

    36   b_fnclauses :: "fnclauses \<Rightarrow> atom set" and

    37   b_fnclause :: "fnclause \<Rightarrow> atom set" and

    38   b_lrb8 :: "lrb8 \<Rightarrow> atom set"

    39 where

    40   "b_lrbs8 (Single l) = b_lrb8 l"

    41 | "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"

    42 | "b_pat (PVar x) = {atom x}"

    43 | "b_pat (PUnit) = {}"

    44 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"

    45 | "b_fnclauses (S fc) = (b_fnclause fc)"

    46 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"

    47 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"

    48 | "b_fnclause (K x pat exp8) = {atom x}"

    49 

    50 thm exp7_lrb_lrbs.eq_iff

    51 thm exp7_lrb_lrbs.supp

    52 

    53 end

    54 

    55 

    56