Nominal/NewParser.thy
changeset 2035 3622cae9b10e
parent 2027 68b2d2d7b4ed
child 2037 205ac2d13339
equal deleted inserted replaced
2034:837b889fcf59 2035:3622cae9b10e
   372   val induct = #induct dtinfo;
   372   val induct = #induct dtinfo;
   373   val exhausts = map #exhaust dtinfos;
   373   val exhausts = map #exhaust dtinfos;
   374 
   374 
   375   (* definitions of raw permutations *)
   375   (* definitions of raw permutations *)
   376   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
   376   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
   377     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
   377     Local_Theory.theory_result (define_raw_perms dtinfo) lthy1;
   378 
   378 
   379   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
   379   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
   380   fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
   380   fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
   381   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
   381   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
   382   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
   382   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
   696 
   696 
   697 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
   697 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
   698   (main_parser >> nominal_datatype2_cmd)
   698   (main_parser >> nominal_datatype2_cmd)
   699 *}
   699 *}
   700 
   700 
   701 (*atom_decl name
   701 
       
   702 atom_decl name
   702 
   703 
   703 nominal_datatype lam =
   704 nominal_datatype lam =
   704   Var name
   705   Var name
   705 | App lam lam
   706 | App lam lam
   706 | Lam x::name t::lam  bind_set x in t
   707 | Lam x::name t::lam  bind_set x in t