Nominal/Test.thy
changeset 1316 0577afdb1732
parent 1309 b395b902cf0d
child 1317 a8627c3bdd0c
equal deleted inserted replaced
1315:43d6e3730353 1316:0577afdb1732
     1 theory Test
     1 theory Test
     2 imports "Parser"
     2 imports "Parser"
     3 begin
     3 begin
     4 
     4 
     5 text {* example 1 *}
     5 text {* example 1 *}
       
     6 
       
     7 (* ML {* set show_hyps *} *)
     6 
     8 
     7 nominal_datatype lam =
     9 nominal_datatype lam =
     8   VAR "name"
    10   VAR "name"
     9 | APP "lam" "lam"
    11 | APP "lam" "lam"
    10 | LET bp::"bp" t::"lam"   bind "bi bp" in t
    12 | LET bp::"bp" t::"lam"   bind "bi bp" in t
    75 
    77 
    76 nominal_datatype tyS =
    78 nominal_datatype tyS =
    77   All xs::"name list" ty::"t_raw" bind xs in ty
    79   All xs::"name list" ty::"t_raw" bind xs in ty
    78 *)
    80 *)
    79 
    81 
       
    82 
       
    83 (* alpha_eqvt fails...
    80 nominal_datatype t = 
    84 nominal_datatype t = 
    81   Var "name" 
    85   Var "name" 
    82 | Fun "t" "t"
    86 | Fun "t" "t"
    83 and  tyS = 
    87 and  tyS = 
    84   All xs::"name set" ty::"t" bind xs in ty
    88   All xs::"name set" ty::"t" bind xs in ty *)
    85 
    89 
    86 (* example 1 from Terms.thy *)
    90 (* example 1 from Terms.thy *)
    87 
    91 
    88 nominal_datatype trm1 =
    92 nominal_datatype trm1 =
    89   Vr1 "name"
    93   Vr1 "name"
   133   "bv3 ANil = {}"
   137   "bv3 ANil = {}"
   134 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
   138 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
   135 
   139 
   136 (* example 4 from Terms.thy *)
   140 (* example 4 from Terms.thy *)
   137 
   141 
   138 
   142 (* fv_eqvt does not work, we need to repaire defined permute functions...
   139 nominal_datatype trm4 =
   143 nominal_datatype trm4 =
   140   Vr4 "name"
   144   Vr4 "name"
   141 | Ap4 "trm4" "trm4 list"
   145 | Ap4 "trm4" "trm4 list"
   142 | Lm4 x::"name" t::"trm4"  bind x in t
   146 | Lm4 x::"name" t::"trm4"  bind x in t
   143 
   147 *)
   144 
   148 
   145 (* example 5 from Terms.thy *)
   149 (* example 5 from Terms.thy *)
   146 
   150 
   147 nominal_datatype trm5 =
   151 nominal_datatype trm5 =
   148   Vr5 "name"
   152   Vr5 "name"