Nominal/Ex/ExLeroy.thy
changeset 2093 751d1349329b
parent 2092 c0ab7451b20d
parent 2091 1f38489f1cf0
child 2094 56b849d348ae
child 2095 ae94bae5bb93
equal deleted inserted replaced
2092:c0ab7451b20d 2093:751d1349329b
     1 theory ExLeroy
       
     2 imports "../NewParser"
       
     3 begin
       
     4 
       
     5 (* example form Leroy 96 about modules; OTT *)
       
     6 
       
     7 atom_decl name
       
     8 
       
     9 nominal_datatype mexp =
       
    10   Acc "path"
       
    11 | Stru "body"
       
    12 | Funct x::"name" "sexp" m::"mexp"    bind_set x in m
       
    13 | FApp "mexp" "path"
       
    14 | Ascr "mexp" "sexp"
       
    15 and body =
       
    16   Empty
       
    17 | Seq c::defn d::"body"     bind_set "cbinders c" in d
       
    18 and defn =
       
    19   Type "name" "tyty"
       
    20 | Dty "name"
       
    21 | DStru "name" "mexp"
       
    22 | Val "name" "trmtrm"
       
    23 and sexp =
       
    24   Sig sbody
       
    25 | SFunc "name" "sexp" "sexp"
       
    26 and sbody =
       
    27   SEmpty
       
    28 | SSeq C::spec D::sbody    bind_set "Cbinders C" in D
       
    29 and spec =
       
    30   Type1 "name"
       
    31 | Type2 "name" "tyty"
       
    32 | SStru "name" "sexp"
       
    33 | SVal "name" "tyty"
       
    34 and tyty =
       
    35   Tyref1 "name"
       
    36 | Tyref2 "path" "tyty"
       
    37 | Fun "tyty" "tyty"
       
    38 and path =
       
    39   Sref1 "name"
       
    40 | Sref2 "path" "name"
       
    41 and trmtrm =
       
    42   Tref1 "name"
       
    43 | Tref2 "path" "name"
       
    44 | Lam' v::"name" "tyty" M::"trmtrm"  bind_set v in M
       
    45 | App' "trmtrm" "trmtrm"
       
    46 | Let' "body" "trmtrm"
       
    47 binder
       
    48     cbinders :: "defn \<Rightarrow> atom set"
       
    49 and Cbinders :: "spec \<Rightarrow> atom set"
       
    50 where
       
    51   "cbinders (Type t T) = {atom t}"
       
    52 | "cbinders (Dty t) = {atom t}"
       
    53 | "cbinders (DStru x s) = {atom x}"
       
    54 | "cbinders (Val v M) = {atom v}"
       
    55 | "Cbinders (Type1 t) = {atom t}"
       
    56 | "Cbinders (Type2 t T) = {atom t}"
       
    57 | "Cbinders (SStru x S) = {atom x}"
       
    58 | "Cbinders (SVal v T) = {atom v}"
       
    59 
       
    60 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv
       
    61 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
       
    62 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn
       
    63 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm
       
    64 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
       
    65 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
       
    66 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
       
    67 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)
       
    68 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)]
       
    69 
       
    70 end
       
    71 
       
    72 
       
    73