src/HOL/Nominal/nominal_atoms.ML
changeset 28372 291e7a158e95
parent 28083 103d9282a946
child 28729 cfd169f1dae2
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Sep 26 14:51:27 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Sep 26 14:52:27 2008 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    type atom_info
     1.5    val get_atom_infos : theory -> atom_info Symtab.table
     1.6    val get_atom_info : theory -> string -> atom_info option
     1.7 +  val the_atom_info : theory -> string -> atom_info
     1.8    val atoms_of : theory -> string list
     1.9    val mk_permT : typ -> typ
    1.10  end
    1.11 @@ -29,7 +30,10 @@
    1.12  type atom_info =
    1.13    {pt_class : string,
    1.14     fs_class : string,
    1.15 -   cp_classes : (string * string) list};
    1.16 +   cp_classes : (string * string) list,
    1.17 +   at_inst : thm,
    1.18 +   pt_inst : thm,
    1.19 +   dj_thms : thm list};
    1.20  
    1.21  structure NominalData = TheoryDataFun
    1.22  (
    1.23 @@ -40,14 +44,21 @@
    1.24    fun merge _ x = Symtab.merge (K true) x;
    1.25  );
    1.26  
    1.27 -fun make_atom_info ((pt_class, fs_class), cp_classes) =
    1.28 +fun make_atom_info (((((pt_class, fs_class), cp_classes), at_inst), pt_inst), dj_thms) =
    1.29    {pt_class = pt_class,
    1.30     fs_class = fs_class,
    1.31 -   cp_classes = cp_classes};
    1.32 +   cp_classes = cp_classes,
    1.33 +   at_inst = at_inst,
    1.34 +   pt_inst = pt_inst,
    1.35 +   dj_thms = dj_thms};
    1.36  
    1.37  val get_atom_infos = NominalData.get;
    1.38  val get_atom_info = Symtab.lookup o NominalData.get;
    1.39  
    1.40 +fun the_atom_info thy name = (case get_atom_info thy name of
    1.41 +      SOME info => info
    1.42 +    | NONE => error ("Unknown atom type " ^ quote name));
    1.43 +
    1.44  fun atoms_of thy = map fst (Symtab.dest (NominalData.get thy));
    1.45  
    1.46  fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
    1.47 @@ -949,7 +960,9 @@
    1.48        NominalData.map (fold Symtab.update (full_ak_names ~~ map make_atom_info
    1.49          (pt_ax_classes ~~
    1.50           fs_ax_classes ~~
    1.51 -         map (fn cls => full_ak_names ~~ cls) cp_ax_classes))) thy33
    1.52 +         map (fn cls => full_ak_names ~~ cls) cp_ax_classes ~~
    1.53 +         prm_cons_thms ~~ prm_inst_thms ~~
    1.54 +         map flat dj_thms))) thy33
    1.55      end;
    1.56  
    1.57