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