src/HOL/Tools/function_package/size.ML
author wenzelm
Tue Sep 25 15:34:35 2007 +0200 (2007-09-25)
changeset 24711 e8bba7723858
parent 24710 141df8b68f63
child 24714 1618c2ac1b74
permissions -rw-r--r--
simplified interpretation setup;
     1 (*  Title:      HOL/Tools/function_package/size.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
     4 
     5 Size functions for datatypes.
     6 *)
     7 
     8 signature SIZE =
     9 sig
    10   val size_thms: theory -> string -> thm list
    11   val setup: theory -> theory
    12 end;
    13 
    14 structure Size: SIZE =
    15 struct
    16 
    17 open DatatypeAux;
    18 
    19 structure SizeData = TheoryDataFun(
    20 struct
    21   type T = thm list Symtab.table;
    22   val empty = Symtab.empty;
    23   val copy = I
    24   val extend = I
    25   fun merge _ = Symtab.merge (K true);
    26 end);
    27 
    28 fun specify_consts args thy =
    29   let
    30     val specs = map (fn (c, T, mx) =>
    31       Const (Sign.full_name thy (Syntax.const_name c mx), T)) args;
    32   in
    33     thy
    34     |> Sign.add_consts_authentic args
    35     |> Theory.add_finals_i false specs
    36   end;
    37 
    38 fun add_axioms label ts atts thy =
    39   thy
    40   |> PureThy.add_axiomss_i [((label, ts), atts)];
    41 
    42 val Const (size_name, _) = HOLogic.size_const dummyT;
    43 val size_name_base = NameSpace.base size_name;
    44 val size_suffix = "_" ^ size_name_base;
    45 
    46 fun instance_size_class tyco thy =
    47   let
    48     val n = Sign.arity_number thy tyco;
    49   in
    50     thy
    51     |> Class.prove_instance (Class.intro_classes_tac [])
    52         [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
    53     |> snd
    54   end
    55 
    56 fun plus (t1, t2) = Const ("HOL.plus_class.plus",
    57   HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
    58 
    59 fun indexify_names names =
    60   let
    61     fun index (x :: xs) tab =
    62       (case AList.lookup (op =) tab x of
    63         NONE => if member (op =) xs x then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab
    64       | SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab))
    65     | index [] _ = [];
    66   in index names [] end;
    67 
    68 fun make_size head_len descr' sorts recTs thy =
    69   let
    70     val size_names = replicate head_len size_name @
    71       map (Sign.intern_const thy) (indexify_names
    72         (map (fn T => name_of_typ T ^ size_suffix) (Library.drop (head_len, recTs))));
    73     val size_consts = map2 (fn s => fn T => Const (s, T --> HOLogic.natT))
    74       size_names recTs;
    75 
    76     fun make_tnames Ts =
    77       let
    78         fun type_name (TFree (name, _)) = implode (tl (explode name))
    79           | type_name (Type (name, _)) = 
    80               let val name' = Sign.base_name name
    81               in if Syntax.is_identifier name' then name' else "x" end;
    82       in indexify_names (map type_name Ts) end;
    83 
    84     fun make_size_eqn size_const T (cname, cargs) =
    85       let
    86         val recs = filter is_rec_type cargs;
    87         val Ts = map (typ_of_dtyp descr' sorts) cargs;
    88         val recTs = map (typ_of_dtyp descr' sorts) recs;
    89         val tnames = make_tnames Ts;
    90         val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
    91         val ts = map2 (fn (r, s) => fn T => nth size_consts (dest_DtRec r) $
    92           Free (s, T)) (recs ~~ rec_tnames) recTs;
    93         val t = if null ts then HOLogic.zero else
    94           Library.foldl plus (hd ts, tl ts @ [HOLogic.Suc_zero]);
    95       in
    96         HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
    97           list_comb (Const (cname, Ts ---> T), map2 (curry Free) tnames Ts), t))
    98       end
    99 
   100   in
   101     maps (fn (((_, (_, _, constrs)), size_const), T) =>
   102       map (make_size_eqn size_const T) constrs) (descr' ~~ size_consts ~~ recTs)
   103   end;
   104 
   105 fun prove_size_thms (info : datatype_info) head_len thy =
   106   let
   107     val descr' = #descr info;
   108     val sorts = #sorts info;
   109     val reccomb_names = #rec_names info;
   110     val primrec_thms = #rec_rewrites info;
   111     val recTs = get_rec_types descr' sorts;
   112 
   113     val size_names = replicate head_len size_name @
   114       map (Sign.full_name thy) (DatatypeProp.indexify_names
   115         (map (fn T => name_of_typ T ^ size_suffix) (Library.drop (head_len, recTs))));
   116     val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
   117       (map (fn T => name_of_typ T ^ size_suffix) recTs));
   118 
   119     fun make_sizefun (_, cargs) =
   120       let
   121         val Ts = map (typ_of_dtyp descr' sorts) cargs;
   122         val k = length (filter is_rec_type cargs);
   123         val ts = map Bound (k - 1 downto 0);
   124         val t = if null ts then HOLogic.zero else
   125           Library.foldl plus (hd ts, tl ts @ [HOLogic.Suc_zero]);
   126 
   127       in
   128         foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
   129       end;
   130 
   131     val fs = maps (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr';
   132     val fTs = map fastype_of fs;
   133 
   134     val (size_def_thms, thy') =
   135       thy
   136       |> Theory.add_consts_i (map (fn (s, T) =>
   137            (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   138            (Library.drop (head_len, size_names ~~ recTs)))
   139       |> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
   140       |> PureThy.add_defs_i true (map (Thm.no_attributes o (fn (((s, T), def_name), rec_name) =>
   141            (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
   142             list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs)))))
   143             (size_names ~~ recTs ~~ def_names ~~ reccomb_names));
   144 
   145     val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
   146 
   147     val size_thms = map (fn t => Goal.prove_global thy' [] [] t
   148       (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))
   149         (make_size head_len descr' sorts recTs thy')
   150 
   151   in
   152     thy'
   153     |> PureThy.add_thmss [((size_name_base, size_thms), [])]
   154     |>> flat
   155   end;
   156 
   157 fun axiomatize_size_thms (info : datatype_info) head_len thy =
   158   let
   159     val descr' = #descr info;
   160     val sorts = #sorts info;
   161     val recTs = get_rec_types descr' sorts;
   162 
   163     val used = map fst (fold Term.add_tfreesT recTs []);
   164 
   165     val size_names = DatatypeProp.indexify_names
   166       (map (fn T => name_of_typ T ^ size_suffix) (Library.drop (head_len, recTs)));
   167 
   168     val thy' = thy
   169       |> specify_consts (map (fn (s, T) =>
   170         (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   171           (size_names ~~ Library.drop (head_len, recTs)))
   172     val size_axs = make_size head_len descr' sorts recTs thy';
   173   in
   174     thy'
   175     |> add_axioms size_name_base size_axs []
   176     ||> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
   177     |>> flat
   178   end;
   179 
   180 fun add_size_thms (name :: _) thy =
   181   let
   182     val info = DatatypePackage.the_datatype thy name;
   183     val descr' = #descr info;
   184     val head_len = #head_len info;
   185     val typnames = map (#1 o snd) (curry Library.take head_len descr');
   186     val prefix = space_implode "_" (map NameSpace.base typnames);
   187     val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
   188       is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs)
   189         (#descr info)
   190   in if no_size then thy
   191     else
   192       thy
   193       |> Theory.add_path prefix
   194       |> (if ! quick_and_dirty
   195         then axiomatize_size_thms info head_len
   196         else prove_size_thms info head_len)
   197       ||> Theory.parent_path
   198       |-> (fn thms => PureThy.add_thmss [(("", thms),
   199             [Simplifier.simp_add, Thm.declaration_attribute
   200               (fn thm => Context.mapping (Code.add_default_func thm) I)])])
   201       |-> (fn thms => SizeData.map (fold (fn typname => Symtab.update_new
   202             (typname, flat thms)) typnames))
   203   end;
   204 
   205 fun size_thms thy = the o Symtab.lookup (SizeData.get thy);
   206 
   207 val setup = DatatypePackage.interpretation add_size_thms;
   208 
   209 end;