size hook
authorhaftmann
Tue Sep 25 13:42:59 2007 +0200 (2007-09-25)
changeset 24710141df8b68f63
parent 24709 ecfb9dcb6c4c
child 24711 e8bba7723858
size hook
src/HOL/Tools/function_package/size.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/function_package/size.ML	Tue Sep 25 13:42:59 2007 +0200
     1.3 @@ -0,0 +1,209 @@
     1.4 +(*  Title:      HOL/Tools/function_package/size.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
     1.7 +
     1.8 +Size functions for datatypes.
     1.9 +*)
    1.10 +
    1.11 +signature SIZE =
    1.12 +sig
    1.13 +  val size_thms: theory -> string -> thm list
    1.14 +  val setup: theory -> theory
    1.15 +end;
    1.16 +
    1.17 +structure Size: SIZE =
    1.18 +struct
    1.19 +
    1.20 +open DatatypeAux;
    1.21 +
    1.22 +structure SizeData = TheoryDataFun(
    1.23 +struct
    1.24 +  type T = thm list Symtab.table;
    1.25 +  val empty = Symtab.empty;
    1.26 +  val copy = I
    1.27 +  val extend = I
    1.28 +  fun merge _ = Symtab.merge (K true);
    1.29 +end);
    1.30 +
    1.31 +fun specify_consts args thy =
    1.32 +  let
    1.33 +    val specs = map (fn (c, T, mx) =>
    1.34 +      Const (Sign.full_name thy (Syntax.const_name c mx), T)) args;
    1.35 +  in
    1.36 +    thy
    1.37 +    |> Sign.add_consts_authentic args
    1.38 +    |> Theory.add_finals_i false specs
    1.39 +  end;
    1.40 +
    1.41 +fun add_axioms label ts atts thy =
    1.42 +  thy
    1.43 +  |> PureThy.add_axiomss_i [((label, ts), atts)];
    1.44 +
    1.45 +val Const (size_name, _) = HOLogic.size_const dummyT;
    1.46 +val size_name_base = NameSpace.base size_name;
    1.47 +val size_suffix = "_" ^ size_name_base;
    1.48 +
    1.49 +fun instance_size_class tyco thy =
    1.50 +  let
    1.51 +    val n = Sign.arity_number thy tyco;
    1.52 +  in
    1.53 +    thy
    1.54 +    |> Class.prove_instance (Class.intro_classes_tac [])
    1.55 +        [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
    1.56 +    |> snd
    1.57 +  end
    1.58 +
    1.59 +fun plus (t1, t2) = Const ("HOL.plus_class.plus",
    1.60 +  HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
    1.61 +
    1.62 +fun indexify_names names =
    1.63 +  let
    1.64 +    fun index (x :: xs) tab =
    1.65 +      (case AList.lookup (op =) tab x of
    1.66 +        NONE => if member (op =) xs x then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab
    1.67 +      | SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab))
    1.68 +    | index [] _ = [];
    1.69 +  in index names [] end;
    1.70 +
    1.71 +fun make_size head_len descr' sorts recTs thy =
    1.72 +  let
    1.73 +    val size_names = replicate head_len size_name @
    1.74 +      map (Sign.intern_const thy) (indexify_names
    1.75 +        (map (fn T => name_of_typ T ^ size_suffix) (Library.drop (head_len, recTs))));
    1.76 +    val size_consts = map2 (fn s => fn T => Const (s, T --> HOLogic.natT))
    1.77 +      size_names recTs;
    1.78 +
    1.79 +    fun make_tnames Ts =
    1.80 +      let
    1.81 +        fun type_name (TFree (name, _)) = implode (tl (explode name))
    1.82 +          | type_name (Type (name, _)) = 
    1.83 +              let val name' = Sign.base_name name
    1.84 +              in if Syntax.is_identifier name' then name' else "x" end;
    1.85 +      in indexify_names (map type_name Ts) end;
    1.86 +
    1.87 +    fun make_size_eqn size_const T (cname, cargs) =
    1.88 +      let
    1.89 +        val recs = filter is_rec_type cargs;
    1.90 +        val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.91 +        val recTs = map (typ_of_dtyp descr' sorts) recs;
    1.92 +        val tnames = make_tnames Ts;
    1.93 +        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
    1.94 +        val ts = map2 (fn (r, s) => fn T => nth size_consts (dest_DtRec r) $
    1.95 +          Free (s, T)) (recs ~~ rec_tnames) recTs;
    1.96 +        val t = if null ts then HOLogic.zero else
    1.97 +          Library.foldl plus (hd ts, tl ts @ [HOLogic.Suc_zero]);
    1.98 +      in
    1.99 +        HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
   1.100 +          list_comb (Const (cname, Ts ---> T), map2 (curry Free) tnames Ts), t))
   1.101 +      end
   1.102 +
   1.103 +  in
   1.104 +    maps (fn (((_, (_, _, constrs)), size_const), T) =>
   1.105 +      map (make_size_eqn size_const T) constrs) (descr' ~~ size_consts ~~ recTs)
   1.106 +  end;
   1.107 +
   1.108 +fun prove_size_thms (info : datatype_info) head_len thy =
   1.109 +  let
   1.110 +    val descr' = #descr info;
   1.111 +    val sorts = #sorts info;
   1.112 +    val reccomb_names = #rec_names info;
   1.113 +    val primrec_thms = #rec_rewrites info;
   1.114 +    val recTs = get_rec_types descr' sorts;
   1.115 +
   1.116 +    val size_names = replicate head_len size_name @
   1.117 +      map (Sign.full_name thy) (DatatypeProp.indexify_names
   1.118 +        (map (fn T => name_of_typ T ^ size_suffix) (Library.drop (head_len, recTs))));
   1.119 +    val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
   1.120 +      (map (fn T => name_of_typ T ^ size_suffix) recTs));
   1.121 +
   1.122 +    fun make_sizefun (_, cargs) =
   1.123 +      let
   1.124 +        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   1.125 +        val k = length (filter is_rec_type cargs);
   1.126 +        val ts = map Bound (k - 1 downto 0);
   1.127 +        val t = if null ts then HOLogic.zero else
   1.128 +          Library.foldl plus (hd ts, tl ts @ [HOLogic.Suc_zero]);
   1.129 +
   1.130 +      in
   1.131 +        foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
   1.132 +      end;
   1.133 +
   1.134 +    val fs = maps (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr';
   1.135 +    val fTs = map fastype_of fs;
   1.136 +
   1.137 +    val (size_def_thms, thy') =
   1.138 +      thy
   1.139 +      |> Theory.add_consts_i (map (fn (s, T) =>
   1.140 +           (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   1.141 +           (Library.drop (head_len, size_names ~~ recTs)))
   1.142 +      |> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
   1.143 +      |> PureThy.add_defs_i true (map (Thm.no_attributes o (fn (((s, T), def_name), rec_name) =>
   1.144 +           (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
   1.145 +            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs)))))
   1.146 +            (size_names ~~ recTs ~~ def_names ~~ reccomb_names));
   1.147 +
   1.148 +    val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
   1.149 +
   1.150 +    val size_thms = map (fn t => Goal.prove_global thy' [] [] t
   1.151 +      (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))
   1.152 +        (make_size head_len descr' sorts recTs thy')
   1.153 +
   1.154 +  in
   1.155 +    thy'
   1.156 +    |> PureThy.add_thmss [((size_name_base, size_thms), [])]
   1.157 +    |>> flat
   1.158 +  end;
   1.159 +
   1.160 +fun axiomatize_size_thms (info : datatype_info) head_len thy =
   1.161 +  let
   1.162 +    val descr' = #descr info;
   1.163 +    val sorts = #sorts info;
   1.164 +    val recTs = get_rec_types descr' sorts;
   1.165 +
   1.166 +    val used = map fst (fold Term.add_tfreesT recTs []);
   1.167 +
   1.168 +    val size_names = DatatypeProp.indexify_names
   1.169 +      (map (fn T => name_of_typ T ^ size_suffix) (Library.drop (head_len, recTs)));
   1.170 +
   1.171 +    val thy' = thy
   1.172 +      |> specify_consts (map (fn (s, T) =>
   1.173 +        (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   1.174 +          (size_names ~~ Library.drop (head_len, recTs)))
   1.175 +    val size_axs = make_size head_len descr' sorts recTs thy';
   1.176 +  in
   1.177 +    thy'
   1.178 +    |> add_axioms size_name_base size_axs []
   1.179 +    ||> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
   1.180 +    |>> flat
   1.181 +  end;
   1.182 +
   1.183 +fun add_size_thms (name :: _) thy =
   1.184 +  let
   1.185 +    val info = DatatypePackage.the_datatype thy name;
   1.186 +    val descr' = #descr info;
   1.187 +    val head_len = #head_len info;
   1.188 +    val typnames = map (#1 o snd) (curry Library.take head_len descr');
   1.189 +    val prefix = space_implode "_" (map NameSpace.base typnames);
   1.190 +    val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
   1.191 +      is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs)
   1.192 +        (#descr info)
   1.193 +  in if no_size then thy
   1.194 +    else
   1.195 +      thy
   1.196 +      |> Theory.add_path prefix
   1.197 +      |> (if ! quick_and_dirty
   1.198 +        then axiomatize_size_thms info head_len
   1.199 +        else prove_size_thms info head_len)
   1.200 +      ||> Theory.parent_path
   1.201 +      |-> (fn thms => PureThy.add_thmss [(("", thms),
   1.202 +            [Simplifier.simp_add, Thm.declaration_attribute
   1.203 +              (fn thm => Context.mapping (Code.add_default_func thm) I)])])
   1.204 +      |-> (fn thms => SizeData.map (fold (fn typname => Symtab.update_new
   1.205 +            (typname, flat thms)) typnames))
   1.206 +  end;
   1.207 +
   1.208 +fun size_thms thy = the o Symtab.lookup (SizeData.get thy);
   1.209 +
   1.210 +val setup = DatatypePackage.add_interpretator add_size_thms;
   1.211 +
   1.212 +end;
   1.213 \ No newline at end of file