src/HOL/Tools/Function/size.ML
author haftmann
Tue Jun 23 16:27:12 2009 +0200 (2009-06-23)
changeset 31784 bd3486c57ba3
parent 31775 2b04504fcb69
child 31902 862ae16a799d
permissions -rw-r--r--
tuned interfaces of datatype module
haftmann@31775
     1
(*  Title:      HOL/Tools/Function/size.ML
haftmann@29495
     2
    Author:     Stefan Berghofer, Florian Haftmann & Alexander Krauss, TU Muenchen
haftmann@24710
     3
haftmann@24710
     4
Size functions for datatypes.
haftmann@24710
     5
*)
haftmann@24710
     6
haftmann@24710
     7
signature SIZE =
haftmann@24710
     8
sig
haftmann@24710
     9
  val size_thms: theory -> string -> thm list
haftmann@24710
    10
  val setup: theory -> theory
haftmann@24710
    11
end;
haftmann@24710
    12
haftmann@24710
    13
structure Size: SIZE =
haftmann@24710
    14
struct
haftmann@24710
    15
haftmann@24710
    16
open DatatypeAux;
haftmann@24710
    17
wenzelm@24714
    18
structure SizeData = TheoryDataFun
wenzelm@24714
    19
(
berghofe@25679
    20
  type T = (string * thm list) Symtab.table;
haftmann@24710
    21
  val empty = Symtab.empty;
haftmann@24710
    22
  val copy = I
haftmann@24710
    23
  val extend = I
haftmann@24710
    24
  fun merge _ = Symtab.merge (K true);
wenzelm@24714
    25
);
haftmann@24710
    26
berghofe@25679
    27
val lookup_size = SizeData.get #> Symtab.lookup;
haftmann@24710
    28
haftmann@24710
    29
fun plus (t1, t2) = Const ("HOL.plus_class.plus",
haftmann@24710
    30
  HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
haftmann@24710
    31
berghofe@25679
    32
fun size_of_type f g h (T as Type (s, Ts)) =
berghofe@25679
    33
      (case f s of
berghofe@25679
    34
         SOME t => SOME t
berghofe@25679
    35
       | NONE => (case g s of
berghofe@25679
    36
           SOME size_name =>
berghofe@25679
    37
             SOME (list_comb (Const (size_name,
berghofe@25679
    38
               map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT),
berghofe@25679
    39
                 map (size_of_type' f g h) Ts))
berghofe@25679
    40
         | NONE => NONE))
berghofe@25679
    41
  | size_of_type f g h (TFree (s, _)) = h s
berghofe@25679
    42
and size_of_type' f g h T = (case size_of_type f g h T of
berghofe@25679
    43
      NONE => Abs ("x", T, HOLogic.zero)
berghofe@25679
    44
    | SOME t => t);
berghofe@25679
    45
berghofe@25679
    46
fun is_poly thy (DtType (name, dts)) =
haftmann@31784
    47
      (case Datatype.get_info thy name of
berghofe@25679
    48
         NONE => false
berghofe@25679
    49
       | SOME _ => exists (is_poly thy) dts)
berghofe@25679
    50
  | is_poly _ _ = true;
berghofe@25679
    51
berghofe@25679
    52
fun constrs_of thy name =
haftmann@24710
    53
  let
haftmann@31784
    54
    val {descr, index, ...} = Datatype.the_info thy name
berghofe@25679
    55
    val SOME (_, _, constrs) = AList.lookup op = descr index
berghofe@25679
    56
  in constrs end;
berghofe@25679
    57
berghofe@25679
    58
val app = curry (list_comb o swap);
haftmann@24710
    59
haftmann@31737
    60
fun prove_size_thms (info : info) new_type_names thy =
berghofe@25679
    61
  let
berghofe@25890
    62
    val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info;
berghofe@25679
    63
    val l = length new_type_names;
berghofe@25679
    64
    val alt_names' = (case alt_names of
berghofe@25679
    65
      NONE => replicate l NONE | SOME names => map SOME names);
berghofe@25679
    66
    val descr' = List.take (descr, l);
berghofe@25679
    67
    val (rec_names1, rec_names2) = chop l rec_names;
haftmann@25864
    68
    val recTs = get_rec_types descr sorts;
berghofe@25679
    69
    val (recTs1, recTs2) = chop l recTs;
berghofe@25679
    70
    val (_, (_, paramdts, _)) :: _ = descr;
haftmann@25864
    71
    val paramTs = map (typ_of_dtyp descr sorts) paramdts;
berghofe@25679
    72
    val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
berghofe@25679
    73
      map (fn T as TFree (s, _) =>
berghofe@25679
    74
        let
berghofe@25679
    75
          val name = "f" ^ implode (tl (explode s));
berghofe@25679
    76
          val U = T --> HOLogic.natT
berghofe@25679
    77
        in
berghofe@25679
    78
          (((s, Free (name, U)), U), name)
berghofe@25679
    79
        end) |> split_list |>> split_list;
berghofe@25679
    80
    val param_size = AList.lookup op = param_size_fs;
haftmann@24710
    81
berghofe@25679
    82
    val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
haftmann@29495
    83
      map_filter (Option.map snd o lookup_size thy) |> flat;
berghofe@25679
    84
    val extra_size = Option.map fst o lookup_size thy;
berghofe@25679
    85
berghofe@25679
    86
    val (((size_names, size_fns), def_names), def_names') =
berghofe@25679
    87
      recTs1 ~~ alt_names' |>
berghofe@25679
    88
      map (fn (T as Type (s, _), optname) =>
berghofe@25679
    89
        let
wenzelm@30364
    90
          val s' = the_default (Long_Name.base_name s) optname ^ "_size";
haftmann@28965
    91
          val s'' = Sign.full_bname thy s'
berghofe@25679
    92
        in
berghofe@25679
    93
          (s'',
berghofe@25679
    94
           (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
berghofe@25679
    95
              map snd param_size_fs),
berghofe@25679
    96
            (s' ^ "_def", s' ^ "_overloaded_def")))
berghofe@25679
    97
        end) |> split_list ||>> split_list ||>> split_list;
berghofe@25679
    98
    val overloaded_size_fns = map HOLogic.size_const recTs1;
berghofe@25679
    99
berghofe@25679
   100
    (* instantiation for primrec combinator *)
berghofe@25679
   101
    fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
haftmann@24710
   102
      let
haftmann@25864
   103
        val Ts = map (typ_of_dtyp descr sorts) cargs;
haftmann@24710
   104
        val k = length (filter is_rec_type cargs);
berghofe@25679
   105
        val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
berghofe@25679
   106
          if is_rec_type dt then (Bound i :: us, i + 1, j + 1)
berghofe@25679
   107
          else
berghofe@25679
   108
            (if b andalso is_poly thy dt' then
berghofe@25679
   109
               case size_of_type (K NONE) extra_size size_ofp T of
berghofe@25679
   110
                 NONE => us | SOME sz => sz $ Bound j :: us
berghofe@25679
   111
             else us, i, j + 1))
berghofe@25679
   112
              (cargs ~~ cargs' ~~ Ts) ([], 0, k);
berghofe@25679
   113
        val t =
berghofe@25679
   114
          if null ts andalso (not b orelse not (exists (is_poly thy) cargs'))
berghofe@25679
   115
          then HOLogic.zero
berghofe@25679
   116
          else foldl1 plus (ts @ [HOLogic.Suc_zero])
haftmann@24710
   117
      in
wenzelm@30190
   118
        List.foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
haftmann@24710
   119
      end;
haftmann@24710
   120
berghofe@25679
   121
    val fs = maps (fn (_, (name, _, constrs)) =>
berghofe@25679
   122
      map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr;
berghofe@25679
   123
    val fs' = maps (fn (n, (name, _, constrs)) =>
berghofe@25679
   124
      map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr;
haftmann@24710
   125
    val fTs = map fastype_of fs;
haftmann@24710
   126
berghofe@25679
   127
    val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) =>
berghofe@25679
   128
      Const (rec_name, fTs @ [T] ---> HOLogic.natT))
berghofe@25679
   129
        (recTs ~~ rec_names));
berghofe@25679
   130
haftmann@25835
   131
    fun define_overloaded (def_name, eq) lthy =
haftmann@25835
   132
      let
haftmann@25835
   133
        val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
wenzelm@28083
   134
        val ((_, (_, thm)), lthy') = lthy |> LocalTheory.define Thm.definitionK
haftmann@28965
   135
          ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
haftmann@25835
   136
        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
haftmann@25864
   137
        val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
haftmann@25835
   138
      in (thm', lthy') end;
haftmann@25835
   139
berghofe@25679
   140
    val ((size_def_thms, size_def_thms'), thy') =
haftmann@24710
   141
      thy
wenzelm@24714
   142
      |> Sign.add_consts_i (map (fn (s, T) =>
wenzelm@30364
   143
           (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
berghofe@25679
   144
           (size_names ~~ recTs1))
haftmann@27691
   145
      |> PureThy.add_defs false
berghofe@25679
   146
        (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
haftmann@29579
   147
           (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
haftmann@25835
   148
      ||> TheoryTarget.instantiation
berghofe@25890
   149
           (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
haftmann@25835
   150
      ||>> fold_map define_overloaded
haftmann@25835
   151
        (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
haftmann@25835
   152
      ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
wenzelm@28394
   153
      ||> LocalTheory.exit_global;
berghofe@25679
   154
berghofe@25679
   155
    val ctxt = ProofContext.init thy';
berghofe@25679
   156
berghofe@25679
   157
    val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm add_0_right} ::
berghofe@25679
   158
      size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
berghofe@25679
   159
    val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
berghofe@25679
   160
berghofe@25679
   161
    fun mk_unfolded_size_eq tab size_ofp fs (p as (x, T), r) =
berghofe@25679
   162
      HOLogic.mk_eq (app fs r $ Free p,
berghofe@25679
   163
        the (size_of_type tab extra_size size_ofp T) $ Free p);
berghofe@25679
   164
berghofe@25679
   165
    fun prove_unfolded_size_eqs size_ofp fs =
berghofe@25679
   166
      if null recTs2 then []
berghofe@25890
   167
      else split_conj_thm (SkipProof.prove ctxt xs []
berghofe@25679
   168
        (HOLogic.mk_Trueprop (mk_conj (replicate l HOLogic.true_const @
berghofe@25679
   169
           map (mk_unfolded_size_eq (AList.lookup op =
berghofe@25679
   170
               (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
berghofe@25679
   171
             (xs ~~ recTs2 ~~ rec_combs2))))
berghofe@25890
   172
        (fn _ => (indtac induction xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
berghofe@25679
   173
berghofe@25890
   174
    val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
berghofe@25890
   175
    val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';
haftmann@24710
   176
berghofe@25679
   177
    (* characteristic equations for size functions *)
berghofe@25679
   178
    fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
berghofe@25679
   179
      let
haftmann@25864
   180
        val Ts = map (typ_of_dtyp descr sorts) cargs;
berghofe@25679
   181
        val tnames = Name.variant_list f_names (DatatypeProp.make_tnames Ts);
haftmann@29495
   182
        val ts = map_filter (fn (sT as (s, T), dt) =>
berghofe@25679
   183
          Option.map (fn sz => sz $ Free sT)
berghofe@25679
   184
            (if p dt then size_of_type size_of extra_size size_ofp T
berghofe@25679
   185
             else NONE)) (tnames ~~ Ts ~~ cargs)
berghofe@25679
   186
      in
berghofe@25679
   187
        HOLogic.mk_Trueprop (HOLogic.mk_eq
berghofe@25679
   188
          (size_const $ list_comb (Const (cname, Ts ---> T),
berghofe@25679
   189
             map2 (curry Free) tnames Ts),
berghofe@25679
   190
           if null ts then HOLogic.zero
berghofe@25679
   191
           else foldl1 plus (ts @ [HOLogic.Suc_zero])))
berghofe@25679
   192
      end;
haftmann@24710
   193
berghofe@25679
   194
    val simpset2 = HOL_basic_ss addsimps
berghofe@25890
   195
      rec_rewrites @ size_def_thms @ unfolded_size_eqs1;
berghofe@25890
   196
    val simpset3 = HOL_basic_ss addsimps
berghofe@25890
   197
      rec_rewrites @ size_def_thms' @ unfolded_size_eqs2;
berghofe@25679
   198
berghofe@25890
   199
    fun prove_size_eqs p size_fns size_ofp simpset =
berghofe@25679
   200
      maps (fn (((_, (_, _, constrs)), size_const), T) =>
berghofe@25679
   201
        map (fn constr => standard (SkipProof.prove ctxt [] []
berghofe@25679
   202
          (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
berghofe@25679
   203
             size_ofp size_const T constr)
berghofe@25890
   204
          (fn _ => simp_tac simpset 1))) constrs)
berghofe@25679
   205
        (descr' ~~ size_fns ~~ recTs1);
berghofe@25679
   206
berghofe@25890
   207
    val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
berghofe@25890
   208
      prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3;
berghofe@25679
   209
berghofe@25679
   210
    val ([size_thms], thy'') =  PureThy.add_thmss
haftmann@29579
   211
      [((Binding.name "size", size_eqns),
blanchet@29866
   212
        [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
blanchet@29863
   213
         Thm.declaration_attribute
blanchet@29863
   214
             (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
haftmann@24710
   215
haftmann@24710
   216
  in
berghofe@25679
   217
    SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
berghofe@25679
   218
      (new_type_names ~~ size_names)) thy''
haftmann@24710
   219
  end;
haftmann@24710
   220
haftmann@31668
   221
fun add_size_thms config (new_type_names as name :: _) thy =
haftmann@24710
   222
  let
haftmann@31784
   223
    val info as {descr, alt_names, ...} = Datatype.the_info thy name;
wenzelm@30364
   224
    val prefix = Long_Name.map_base_name (K (space_implode "_"
wenzelm@30364
   225
      (the_default (map Long_Name.base_name new_type_names) alt_names))) name;
haftmann@24710
   226
    val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
berghofe@25679
   227
      is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr
haftmann@24710
   228
  in if no_size then thy
haftmann@24710
   229
    else
haftmann@24710
   230
      thy
berghofe@25679
   231
      |> Sign.root_path
wenzelm@24714
   232
      |> Sign.add_path prefix
wenzelm@28361
   233
      |> Theory.checkpoint
berghofe@25679
   234
      |> prove_size_thms info new_type_names
berghofe@25679
   235
      |> Sign.restore_naming thy
haftmann@24710
   236
  end;
haftmann@24710
   237
berghofe@25679
   238
val size_thms = snd oo (the oo lookup_size);
haftmann@24710
   239
haftmann@31723
   240
val setup = Datatype.interpretation add_size_thms;
haftmann@24710
   241
blanchet@29866
   242
end;