src/HOL/Tools/Function/size.ML
author berghofe
Tue, 24 Jan 2012 16:00:51 +0100
changeset 46328 fd21bbcbe61b
parent 45901 cea7cd0c7e99
child 49964 4d84fe96d5cb
permissions -rw-r--r--
Use lookup_size rather than Datatype.get_info in is_poly to avoid incorrect results for datatypes on which no size function is defined
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31775
2b04504fcb69 uniformly capitialized names for subdirectories
haftmann
parents: 31737
diff changeset
     1
(*  Title:      HOL/Tools/Function/size.ML
43084
946c8e171ffd more precise authorship, reflecting my own ignorance and hg annotate
krauss
parents: 42361
diff changeset
     2
    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
     3
141df8b68f63 size hook
haftmann
parents:
diff changeset
     4
Size functions for datatypes.
141df8b68f63 size hook
haftmann
parents:
diff changeset
     5
*)
141df8b68f63 size hook
haftmann
parents:
diff changeset
     6
141df8b68f63 size hook
haftmann
parents:
diff changeset
     7
signature SIZE =
141df8b68f63 size hook
haftmann
parents:
diff changeset
     8
sig
141df8b68f63 size hook
haftmann
parents:
diff changeset
     9
  val size_thms: theory -> string -> thm list
141df8b68f63 size hook
haftmann
parents:
diff changeset
    10
  val setup: theory -> theory
141df8b68f63 size hook
haftmann
parents:
diff changeset
    11
end;
141df8b68f63 size hook
haftmann
parents:
diff changeset
    12
141df8b68f63 size hook
haftmann
parents:
diff changeset
    13
structure Size: SIZE =
141df8b68f63 size hook
haftmann
parents:
diff changeset
    14
struct
141df8b68f63 size hook
haftmann
parents:
diff changeset
    15
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33339
diff changeset
    16
structure SizeData = Theory_Data
24714
1618c2ac1b74 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24711
diff changeset
    17
(
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    18
  type T = (string * thm list) Symtab.table;
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
    19
  val empty = Symtab.empty;
141df8b68f63 size hook
haftmann
parents:
diff changeset
    20
  val extend = I
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33339
diff changeset
    21
  fun merge data = Symtab.merge (K true) data;
24714
1618c2ac1b74 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24711
diff changeset
    22
);
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
    23
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    24
val lookup_size = SizeData.get #> Symtab.lookup;
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
    25
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35064
diff changeset
    26
fun plus (t1, t2) = Const (@{const_name Groups.plus},
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
    27
  HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
141df8b68f63 size hook
haftmann
parents:
diff changeset
    28
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    29
fun size_of_type f g h (T as Type (s, Ts)) =
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    30
      (case f s of
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    31
         SOME t => SOME t
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    32
       | NONE => (case g s of
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    33
           SOME size_name =>
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    34
             SOME (list_comb (Const (size_name,
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    35
               map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT),
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    36
                 map (size_of_type' f g h) Ts))
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    37
         | NONE => NONE))
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    38
  | size_of_type f g h (TFree (s, _)) = h s
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    39
and size_of_type' f g h T = (case size_of_type f g h T of
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    40
      NONE => Abs ("x", T, HOLogic.zero)
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    41
    | SOME t => t);
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    42
45896
100fb1f33e3e tuned signature;
wenzelm
parents: 45822
diff changeset
    43
fun is_poly thy (Datatype.DtType (name, dts)) =
46328
fd21bbcbe61b Use lookup_size rather than Datatype.get_info in is_poly to avoid
berghofe
parents: 45901
diff changeset
    44
      (case lookup_size thy name of
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    45
         NONE => false
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    46
       | SOME _ => exists (is_poly thy) dts)
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    47
  | is_poly _ _ = true;
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    48
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    49
fun constrs_of thy name =
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
    50
  let
31784
bd3486c57ba3 tuned interfaces of datatype module
haftmann
parents: 31775
diff changeset
    51
    val {descr, index, ...} = Datatype.the_info thy name
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    52
    val SOME (_, _, constrs) = AList.lookup op = descr index
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    53
  in constrs end;
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    54
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    55
val app = curry (list_comb o swap);
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
    56
45736
2888e076ac17 do not open ML structures;
wenzelm
parents: 45735
diff changeset
    57
fun prove_size_thms (info : Datatype.info) new_type_names thy =
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    58
  let
45822
843dc212f69e datatype dtyp with explicit sort information;
wenzelm
parents: 45740
diff changeset
    59
    val {descr, rec_names, rec_rewrites, induct, ...} = info;
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    60
    val l = length new_type_names;
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    61
    val descr' = List.take (descr, l);
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    62
    val (rec_names1, rec_names2) = chop l rec_names;
45822
843dc212f69e datatype dtyp with explicit sort information;
wenzelm
parents: 45740
diff changeset
    63
    val recTs = Datatype_Aux.get_rec_types descr;
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    64
    val (recTs1, recTs2) = chop l recTs;
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    65
    val (_, (_, paramdts, _)) :: _ = descr;
45822
843dc212f69e datatype dtyp with explicit sort information;
wenzelm
parents: 45740
diff changeset
    66
    val paramTs = map (Datatype_Aux.typ_of_dtyp descr) paramdts;
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    67
    val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    68
      map (fn T as TFree (s, _) =>
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    69
        let
40720
b770df486e5c explicit use of unprefix;
wenzelm
parents: 40627
diff changeset
    70
          val name = "f" ^ unprefix "'" s;
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    71
          val U = T --> HOLogic.natT
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    72
        in
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    73
          (((s, Free (name, U)), U), name)
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    74
        end) |> split_list |>> split_list;
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    75
    val param_size = AList.lookup op = param_size_fs;
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
    76
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    77
    val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
29495
haftmann
parents: 28965
diff changeset
    78
      map_filter (Option.map snd o lookup_size thy) |> flat;
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    79
    val extra_size = Option.map fst o lookup_size thy;
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    80
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    81
    val (((size_names, size_fns), def_names), def_names') =
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 43084
diff changeset
    82
      recTs1 |> map (fn T as Type (s, _) =>
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    83
        let
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 43084
diff changeset
    84
          val s' = Long_Name.base_name s ^ "_size";
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 43084
diff changeset
    85
          val s'' = Sign.full_bname thy s';
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    86
        in
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    87
          (s'',
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    88
           (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    89
              map snd param_size_fs),
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    90
            (s' ^ "_def", s' ^ "_overloaded_def")))
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    91
        end) |> split_list ||>> split_list ||>> split_list;
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    92
    val overloaded_size_fns = map HOLogic.size_const recTs1;
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    93
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    94
    (* instantiation for primrec combinator *)
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    95
    fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
    96
      let
45822
843dc212f69e datatype dtyp with explicit sort information;
wenzelm
parents: 45740
diff changeset
    97
        val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
45736
2888e076ac17 do not open ML structures;
wenzelm
parents: 45735
diff changeset
    98
        val k = length (filter Datatype_Aux.is_rec_type cargs);
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
    99
        val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
45736
2888e076ac17 do not open ML structures;
wenzelm
parents: 45735
diff changeset
   100
          if Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   101
          else
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   102
            (if b andalso is_poly thy dt' then
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   103
               case size_of_type (K NONE) extra_size size_ofp T of
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   104
                 NONE => us | SOME sz => sz $ Bound j :: us
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   105
             else us, i, j + 1))
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   106
              (cargs ~~ cargs' ~~ Ts) ([], 0, k);
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   107
        val t =
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   108
          if null ts andalso (not b orelse not (exists (is_poly thy) cargs'))
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   109
          then HOLogic.zero
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   110
          else foldl1 plus (ts @ [HOLogic.Suc_zero])
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   111
      in
33339
d41f77196338 eliminated some old folds;
wenzelm
parents: 33056
diff changeset
   112
        fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   113
      end;
141df8b68f63 size hook
haftmann
parents:
diff changeset
   114
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   115
    val fs = maps (fn (_, (name, _, constrs)) =>
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   116
      map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr;
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   117
    val fs' = maps (fn (n, (name, _, constrs)) =>
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   118
      map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr;
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   119
    val fTs = map fastype_of fs;
141df8b68f63 size hook
haftmann
parents:
diff changeset
   120
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   121
    val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) =>
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   122
      Const (rec_name, fTs @ [T] ---> HOLogic.natT))
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   123
        (recTs ~~ rec_names));
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   124
25835
5dac4855a080 adhering to instantiation policy
haftmann
parents: 25769
diff changeset
   125
    fun define_overloaded (def_name, eq) lthy =
5dac4855a080 adhering to instantiation policy
haftmann
parents: 25769
diff changeset
   126
      let
5dac4855a080 adhering to instantiation policy
haftmann
parents: 25769
diff changeset
   127
        val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
35756
cfde251d03a5 refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
bulwahn
parents: 35267
diff changeset
   128
        val (thm, lthy') = lthy
cfde251d03a5 refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
bulwahn
parents: 35267
diff changeset
   129
          |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
cfde251d03a5 refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
bulwahn
parents: 35267
diff changeset
   130
          |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41423
diff changeset
   131
        val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41423
diff changeset
   132
        val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
25835
5dac4855a080 adhering to instantiation policy
haftmann
parents: 25769
diff changeset
   133
      in (thm', lthy') end;
5dac4855a080 adhering to instantiation policy
haftmann
parents: 25769
diff changeset
   134
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   135
    val ((size_def_thms, size_def_thms'), thy') =
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   136
      thy
24714
1618c2ac1b74 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24711
diff changeset
   137
      |> Sign.add_consts_i (map (fn (s, T) =>
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   138
           (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   139
           (size_names ~~ recTs1))
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38348
diff changeset
   140
      |> Global_Theory.add_defs false
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   141
        (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29495
diff changeset
   142
           (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
38348
cf7b2121ad9d moved instantiation target formally to class_target.ML
haftmann
parents: 36610
diff changeset
   143
      ||> Class.instantiation
25890
0ba401ddbaed Now uses more carefully designed simpsets to prevent proofs from
berghofe
parents: 25864
diff changeset
   144
           (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
25835
5dac4855a080 adhering to instantiation policy
haftmann
parents: 25769
diff changeset
   145
      ||>> fold_map define_overloaded
5dac4855a080 adhering to instantiation policy
haftmann
parents: 25769
diff changeset
   146
        (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
5dac4855a080 adhering to instantiation policy
haftmann
parents: 25769
diff changeset
   147
      ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33553
diff changeset
   148
      ||> Local_Theory.exit_global;
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   149
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41423
diff changeset
   150
    val ctxt = Proof_Context.init_global thy';
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   151
35064
1bdef0c013d3 hide fact names clashing with fact names from Group.thy
haftmann
parents: 35047
diff changeset
   152
    val simpset1 = HOL_basic_ss addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   153
      size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   154
    val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   155
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   156
    fun mk_unfolded_size_eq tab size_ofp fs (p as (x, T), r) =
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   157
      HOLogic.mk_eq (app fs r $ Free p,
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   158
        the (size_of_type tab extra_size size_ofp T) $ Free p);
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   159
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   160
    fun prove_unfolded_size_eqs size_ofp fs =
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   161
      if null recTs2 then []
45736
2888e076ac17 do not open ML structures;
wenzelm
parents: 45735
diff changeset
   162
      else Datatype_Aux.split_conj_thm (Skip_Proof.prove ctxt xs []
45740
132a3e1c0fe5 more antiquotations;
wenzelm
parents: 45736
diff changeset
   163
        (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l @{term True} @
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   164
           map (mk_unfolded_size_eq (AList.lookup op =
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   165
               (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   166
             (xs ~~ recTs2 ~~ rec_combs2))))
45735
7d7d7af647a9 tuned signature;
wenzelm
parents: 45701
diff changeset
   167
        (fn _ => (Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   168
25890
0ba401ddbaed Now uses more carefully designed simpsets to prevent proofs from
berghofe
parents: 25864
diff changeset
   169
    val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
0ba401ddbaed Now uses more carefully designed simpsets to prevent proofs from
berghofe
parents: 25864
diff changeset
   170
    val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   171
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   172
    (* characteristic equations for size functions *)
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   173
    fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   174
      let
45822
843dc212f69e datatype dtyp with explicit sort information;
wenzelm
parents: 45740
diff changeset
   175
        val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
33968
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33766
diff changeset
   176
        val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts);
29495
haftmann
parents: 28965
diff changeset
   177
        val ts = map_filter (fn (sT as (s, T), dt) =>
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   178
          Option.map (fn sz => sz $ Free sT)
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   179
            (if p dt then size_of_type size_of extra_size size_ofp T
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   180
             else NONE)) (tnames ~~ Ts ~~ cargs)
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   181
      in
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   182
        HOLogic.mk_Trueprop (HOLogic.mk_eq
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   183
          (size_const $ list_comb (Const (cname, Ts ---> T),
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   184
             map2 (curry Free) tnames Ts),
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   185
           if null ts then HOLogic.zero
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   186
           else foldl1 plus (ts @ [HOLogic.Suc_zero])))
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   187
      end;
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   188
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   189
    val simpset2 = HOL_basic_ss addsimps
25890
0ba401ddbaed Now uses more carefully designed simpsets to prevent proofs from
berghofe
parents: 25864
diff changeset
   190
      rec_rewrites @ size_def_thms @ unfolded_size_eqs1;
0ba401ddbaed Now uses more carefully designed simpsets to prevent proofs from
berghofe
parents: 25864
diff changeset
   191
    val simpset3 = HOL_basic_ss addsimps
0ba401ddbaed Now uses more carefully designed simpsets to prevent proofs from
berghofe
parents: 25864
diff changeset
   192
      rec_rewrites @ size_def_thms' @ unfolded_size_eqs2;
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   193
25890
0ba401ddbaed Now uses more carefully designed simpsets to prevent proofs from
berghofe
parents: 25864
diff changeset
   194
    fun prove_size_eqs p size_fns size_ofp simpset =
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   195
      maps (fn (((_, (_, _, constrs)), size_const), T) =>
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 34974
diff changeset
   196
        map (fn constr => Drule.export_without_context (Skip_Proof.prove ctxt [] []
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   197
          (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   198
             size_ofp size_const T constr)
25890
0ba401ddbaed Now uses more carefully designed simpsets to prevent proofs from
berghofe
parents: 25864
diff changeset
   199
          (fn _ => simp_tac simpset 1))) constrs)
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   200
        (descr' ~~ size_fns ~~ recTs1);
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   201
25890
0ba401ddbaed Now uses more carefully designed simpsets to prevent proofs from
berghofe
parents: 25864
diff changeset
   202
    val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
45736
2888e076ac17 do not open ML structures;
wenzelm
parents: 45735
diff changeset
   203
      prove_size_eqs Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   204
45901
cea7cd0c7e99 eliminated old-fashioned Global_Theory.add_thms(s);
wenzelm
parents: 45896
diff changeset
   205
    val ([(_, size_thms)], thy'') = thy'
cea7cd0c7e99 eliminated old-fashioned Global_Theory.add_thms(s);
wenzelm
parents: 45896
diff changeset
   206
      |> Global_Theory.note_thmss ""
cea7cd0c7e99 eliminated old-fashioned Global_Theory.add_thms(s);
wenzelm
parents: 45896
diff changeset
   207
        [((Binding.name "size",
cea7cd0c7e99 eliminated old-fashioned Global_Theory.add_thms(s);
wenzelm
parents: 45896
diff changeset
   208
            [Simplifier.simp_add, Nitpick_Simps.add,
cea7cd0c7e99 eliminated old-fashioned Global_Theory.add_thms(s);
wenzelm
parents: 45896
diff changeset
   209
             Thm.declaration_attribute (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
cea7cd0c7e99 eliminated old-fashioned Global_Theory.add_thms(s);
wenzelm
parents: 45896
diff changeset
   210
          [(size_eqns, [])])];
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   211
141df8b68f63 size hook
haftmann
parents:
diff changeset
   212
  in
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   213
    SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   214
      (new_type_names ~~ size_names)) thy''
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   215
  end;
141df8b68f63 size hook
haftmann
parents:
diff changeset
   216
31668
a616e56a5ec8 datatype packages: record datatype_config for configuration flags; less verbose signatures
haftmann
parents: 30364
diff changeset
   217
fun add_size_thms config (new_type_names as name :: _) thy =
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   218
  let
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 43084
diff changeset
   219
    val info as {descr, ...} = Datatype.the_info thy name;
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 43084
diff changeset
   220
    val prefix =
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 43084
diff changeset
   221
      Long_Name.map_base_name (K (space_implode "_" (map Long_Name.base_name new_type_names))) name;
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   222
    val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
45736
2888e076ac17 do not open ML structures;
wenzelm
parents: 45735
diff changeset
   223
      Datatype_Aux.is_rec_type dt andalso
2888e076ac17 do not open ML structures;
wenzelm
parents: 45735
diff changeset
   224
        not (null (fst (Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 43084
diff changeset
   225
  in
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 43084
diff changeset
   226
    if no_size then thy
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   227
    else
141df8b68f63 size hook
haftmann
parents:
diff changeset
   228
      thy
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   229
      |> Sign.root_path
24714
1618c2ac1b74 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24711
diff changeset
   230
      |> Sign.add_path prefix
28361
232fcbba2e4e explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;
wenzelm
parents: 28083
diff changeset
   231
      |> Theory.checkpoint
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   232
      |> prove_size_thms info new_type_names
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   233
      |> Sign.restore_naming thy
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   234
  end;
141df8b68f63 size hook
haftmann
parents:
diff changeset
   235
25679
b77f797b528a size functions for nested datatypes are now expressed using
berghofe
parents: 25569
diff changeset
   236
val size_thms = snd oo (the oo lookup_size);
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   237
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31668
diff changeset
   238
val setup = Datatype.interpretation add_size_thms;
24710
141df8b68f63 size hook
haftmann
parents:
diff changeset
   239
29866
6e93ae65c678 Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute.
blanchet
parents: 29863
diff changeset
   240
end;