1 theory ExPS6

     2 imports "../NewParser"

     3 begin

     4 

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

     6 

     7 atom_decl name

     8 

     9 (* Is this binding structure supported - I think not 

    10    because e1 occurs twice as body *)

    11 

    12 nominal_datatype exp =

    13   Var name

    14 | Pair exp exp

    15 | LetRec x::name p::pat e1::exp e2::exp  bind x in e1 e2, bind "bp p" in e1

    16 and pat =

    17   PVar name

    18 | PUnit

    19 | PPair pat pat

    20 binder

    21   bp :: "pat \<Rightarrow> atom list"

    22 where

    23   "bp (PVar x) = [atom x]"

    24 | "bp (PUnit) = []"

    25 | "bp (PPair p1 p2) = bp p1 @ bp p2"

    26 

    27 thm exp_pat.fv

    28 thm exp_pat.eq_iff

    29 thm exp_pat.bn

    30 thm exp_pat.perm

    31 thm exp_pat.induct

    32 thm exp_pat.distinct

    33 thm exp_pat.supp

    34 

    35 

    36 

    37 

    38 end

    39 

    40 

    41