src/HOL/Tools/datatype_prop.ML
changeset 24699 c6674504103f
parent 24112 6c4e7d17f9b0
child 25154 6155f2faf23e
equal deleted inserted replaced
24698:9800a7602629 24699:c6674504103f
    22     (string * sort) list -> theory -> term list list
    22     (string * sort) list -> theory -> term list list
    23   val make_distincts : string list -> DatatypeAux.descr list ->
    23   val make_distincts : string list -> DatatypeAux.descr list ->
    24     (string * sort) list -> theory -> term list list
    24     (string * sort) list -> theory -> term list list
    25   val make_splits : string list -> DatatypeAux.descr list ->
    25   val make_splits : string list -> DatatypeAux.descr list ->
    26     (string * sort) list -> theory -> (term * term) list
    26     (string * sort) list -> theory -> (term * term) list
    27   val make_size : DatatypeAux.descr list -> (string * sort) list ->
       
    28     theory -> term list
       
    29   val make_weak_case_congs : string list -> DatatypeAux.descr list ->
    27   val make_weak_case_congs : string list -> DatatypeAux.descr list ->
    30     (string * sort) list -> theory -> term list
    28     (string * sort) list -> theory -> term list
    31   val make_case_congs : string list -> DatatypeAux.descr list ->
    29   val make_case_congs : string list -> DatatypeAux.descr list ->
    32     (string * sort) list -> theory -> term list
    30     (string * sort) list -> theory -> term list
    33   val make_nchotomys : DatatypeAux.descr list ->
    31   val make_nchotomys : DatatypeAux.descr list ->
    57     fun type_name (TFree (name, _)) = implode (tl (explode name))
    55     fun type_name (TFree (name, _)) = implode (tl (explode name))
    58       | type_name (Type (name, _)) = 
    56       | type_name (Type (name, _)) = 
    59           let val name' = Sign.base_name name
    57           let val name' = Sign.base_name name
    60           in if Syntax.is_identifier name' then name' else "x" end;
    58           in if Syntax.is_identifier name' then name' else "x" end;
    61   in indexify_names (map type_name Ts) end;
    59   in indexify_names (map type_name Ts) end;
    62 
       
    63 
    60 
    64 
    61 
    65 (************************* injectivity of constructors ************************)
    62 (************************* injectivity of constructors ************************)
    66 
    63 
    67 fun make_injs descr sorts =
    64 fun make_injs descr sorts =
   349 
   346 
   350   in map make_split ((hd descr) ~~ newTs ~~
   347   in map make_split ((hd descr) ~~ newTs ~~
   351     (make_case_combs new_type_names descr sorts thy "f"))
   348     (make_case_combs new_type_names descr sorts thy "f"))
   352   end;
   349   end;
   353 
   350 
   354 
       
   355 (******************************* size functions *******************************)
       
   356 
       
   357 fun make_size descr sorts thy =
       
   358   let
       
   359     val descr' = flat descr;
       
   360     val recTs = get_rec_types descr' sorts;
       
   361 
       
   362     val Const (size_name, _) = HOLogic.size_const dummyT;
       
   363     val size_names = replicate (length (hd descr)) size_name @
       
   364       map (Sign.intern_const thy) (indexify_names
       
   365         (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
       
   366     val size_consts = map (fn (s, T) =>
       
   367       Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
       
   368 
       
   369     fun plus (t1, t2) = Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
       
   370 
       
   371     fun make_size_eqn size_const T (cname, cargs) =
       
   372       let
       
   373         val recs = filter is_rec_type cargs;
       
   374         val Ts = map (typ_of_dtyp descr' sorts) cargs;
       
   375         val recTs = map (typ_of_dtyp descr' sorts) recs;
       
   376         val tnames = make_tnames Ts;
       
   377         val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
       
   378         val ts = map (fn ((r, s), T) => nth size_consts (dest_DtRec r) $
       
   379           Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
       
   380         val t = if ts = [] then HOLogic.zero else
       
   381           foldl1 plus (ts @ [HOLogic.Suc_zero])
       
   382       in
       
   383         HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
       
   384           list_comb (Const (cname, Ts ---> T), map Free (tnames ~~ Ts)), t))
       
   385       end
       
   386 
       
   387   in
       
   388     List.concat (map (fn (((_, (_, _, constrs)), size_const), T) =>
       
   389       map (make_size_eqn size_const T) constrs) (descr' ~~ size_consts ~~ recTs))
       
   390   end;
       
   391 
       
   392 (************************* additional rules for TFL ***************************)
   351 (************************* additional rules for TFL ***************************)
   393 
   352 
   394 fun make_weak_case_congs new_type_names descr sorts thy =
   353 fun make_weak_case_congs new_type_names descr sorts thy =
   395   let
   354   let
   396     val case_combs = make_case_combs new_type_names descr sorts thy "f";
   355     val case_combs = make_case_combs new_type_names descr sorts thy "f";