1 theory ExPS3

     2 imports "Parser"

     3 begin

     4 

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

     6 

     7 atom_decl name

     8 

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

    10 nominal_datatype exp =

    11   VarP "name"

    12 | AppP "exp" "exp"

    13 | LamP x::"name" e::"exp" bind x in e

    14 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1

    15 and pat3 =

    16   PVar "name"

    17 | PUnit

    18 | PPair "pat3" "pat3"

    19 binder

    20   bp'' :: "pat3 \<Rightarrow> atom set"

    21 where

    22   "bp'' (PVar x) = {atom x}"

    23 | "bp'' (PUnit) = {}"

    24 | "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"

    25 

    26 thm exp_pat3.fv

    27 thm exp_pat3.eq_iff

    28 thm exp_pat3.bn

    29 thm exp_pat3.perm

    30 thm exp_pat3.induct

    31 thm exp_pat3.distinct

    32 thm exp_pat3.fv[simplified exp_pat3.supp]

    33 

    34 end

    35 

    36 

    37