Some more functions for accessing information about atoms.
authorberghofe
Mon Nov 10 17:34:26 2008 +0100 (2008-11-10 ago)
changeset 28729cfd169f1dae2
parent 28728 08314d96246b
child 28730 71c946ce7eb9
Some more functions for accessing information about atoms.
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon Nov 10 14:36:49 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Nov 10 17:34:26 2008 +0100
     1.3 @@ -12,6 +12,13 @@
     1.4    val get_atom_infos : theory -> atom_info Symtab.table
     1.5    val get_atom_info : theory -> string -> atom_info option
     1.6    val the_atom_info : theory -> string -> atom_info
     1.7 +  val fs_class_of : theory -> string -> string
     1.8 +  val pt_class_of : theory -> string -> string
     1.9 +  val cp_class_of : theory -> string -> string -> string
    1.10 +  val at_inst_of : theory -> string -> thm
    1.11 +  val pt_inst_of : theory -> string -> thm
    1.12 +  val cp_inst_of : theory -> string -> string -> thm
    1.13 +  val dj_thm_of : theory -> string -> string -> thm
    1.14    val atoms_of : theory -> string list
    1.15    val mk_permT : typ -> typ
    1.16  end
    1.17 @@ -30,10 +37,11 @@
    1.18  type atom_info =
    1.19    {pt_class : string,
    1.20     fs_class : string,
    1.21 -   cp_classes : (string * string) list,
    1.22 +   cp_classes : string Symtab.table,
    1.23     at_inst : thm,
    1.24     pt_inst : thm,
    1.25 -   dj_thms : thm list};
    1.26 +   cp_inst : thm Symtab.table,
    1.27 +   dj_thms : thm Symtab.table};
    1.28  
    1.29  structure NominalData = TheoryDataFun
    1.30  (
    1.31 @@ -44,20 +52,35 @@
    1.32    fun merge _ x = Symtab.merge (K true) x;
    1.33  );
    1.34  
    1.35 -fun make_atom_info (((((pt_class, fs_class), cp_classes), at_inst), pt_inst), dj_thms) =
    1.36 +fun make_atom_info ((((((pt_class, fs_class), cp_classes), at_inst), pt_inst), cp_inst), dj_thms) =
    1.37    {pt_class = pt_class,
    1.38     fs_class = fs_class,
    1.39     cp_classes = cp_classes,
    1.40     at_inst = at_inst,
    1.41     pt_inst = pt_inst,
    1.42 +   cp_inst = cp_inst,
    1.43     dj_thms = dj_thms};
    1.44  
    1.45  val get_atom_infos = NominalData.get;
    1.46  val get_atom_info = Symtab.lookup o NominalData.get;
    1.47  
    1.48 -fun the_atom_info thy name = (case get_atom_info thy name of
    1.49 -      SOME info => info
    1.50 -    | NONE => error ("Unknown atom type " ^ quote name));
    1.51 +fun gen_lookup lookup name = case lookup name of
    1.52 +    SOME info => info
    1.53 +  | NONE => error ("Unknown atom type " ^ quote name);
    1.54 +
    1.55 +fun the_atom_info thy = gen_lookup (get_atom_info thy);
    1.56 +
    1.57 +fun gen_lookup' f thy = the_atom_info thy #> f;
    1.58 +fun gen_lookup'' f thy =
    1.59 +  gen_lookup' (f #> Symtab.lookup #> gen_lookup) thy;
    1.60 +
    1.61 +val fs_class_of = gen_lookup' #fs_class;
    1.62 +val pt_class_of = gen_lookup' #pt_class;
    1.63 +val at_inst_of = gen_lookup' #at_inst;
    1.64 +val pt_inst_of = gen_lookup' #pt_inst;
    1.65 +val cp_class_of = gen_lookup'' #cp_classes;
    1.66 +val cp_inst_of = gen_lookup'' #cp_inst;
    1.67 +val dj_thm_of = gen_lookup'' #dj_thms;
    1.68  
    1.69  fun atoms_of thy = map fst (Symtab.dest (NominalData.get thy));
    1.70  
    1.71 @@ -405,7 +428,8 @@
    1.72                                          rtac allI 1, rtac allI 1, rtac allI 1,
    1.73                                          rtac cp1 1];
    1.74             in
    1.75 -             PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
    1.76 +             yield_singleton PureThy.add_thms ((name,
    1.77 +               Goal.prove_global thy' [] [] statement proof), []) thy'
    1.78             end) 
    1.79             ak_names_types thy) ak_names_types thy12b;
    1.80         
    1.81 @@ -960,9 +984,12 @@
    1.82        NominalData.map (fold Symtab.update (full_ak_names ~~ map make_atom_info
    1.83          (pt_ax_classes ~~
    1.84           fs_ax_classes ~~
    1.85 -         map (fn cls => full_ak_names ~~ cls) cp_ax_classes ~~
    1.86 +         map (fn cls => Symtab.make (full_ak_names ~~ cls)) cp_ax_classes ~~
    1.87           prm_cons_thms ~~ prm_inst_thms ~~
    1.88 -         map flat dj_thms))) thy33
    1.89 +         map (fn ths => Symtab.make (full_ak_names ~~ ths)) cp_thms ~~
    1.90 +         map (fn thss => Symtab.make
    1.91 +           (List.mapPartial (fn (s, [th]) => SOME (s, th) | _ => NONE)
    1.92 +              (full_ak_names ~~ thss))) dj_thms))) thy33
    1.93      end;
    1.94  
    1.95