src/HOL/Tools/datatype_prop.ML
changeset 22994 02440636214f
parent 22578 b0eb5652f210
child 24098 f1eb34ae33af
equal deleted inserted replaced
22993:838c66e760b5 22994:02440636214f
   351 
   351 
   352 (******************************* size functions *******************************)
   352 (******************************* size functions *******************************)
   353 
   353 
   354 fun make_size descr sorts thy =
   354 fun make_size descr sorts thy =
   355   let
   355   let
   356     val descr' = List.concat descr;
   356     val descr' = flat descr;
   357     val recTs = get_rec_types descr' sorts;
   357     val recTs = get_rec_types descr' sorts;
   358 
   358 
   359     val size_name = "Nat.size";
   359     val Const (size_name, _) = HOLogic.size_const dummyT;
   360     val size_names = replicate (length (hd descr)) size_name @
   360     val size_names = replicate (length (hd descr)) size_name @
   361       map (Sign.intern_const thy) (indexify_names
   361       map (Sign.intern_const thy) (indexify_names
   362         (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
   362         (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
   363     val size_consts = map (fn (s, T) =>
   363     val size_consts = map (fn (s, T) =>
   364       Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
   364       Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
   365 
   365 
   366     fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
   366     fun plus (t1, t2) = Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
   367 
   367 
   368     fun make_size_eqn size_const T (cname, cargs) =
   368     fun make_size_eqn size_const T (cname, cargs) =
   369       let
   369       let
   370         val recs = List.filter is_rec_type cargs;
   370         val recs = filter is_rec_type cargs;
   371         val Ts = map (typ_of_dtyp descr' sorts) cargs;
   371         val Ts = map (typ_of_dtyp descr' sorts) cargs;
   372         val recTs = map (typ_of_dtyp descr' sorts) recs;
   372         val recTs = map (typ_of_dtyp descr' sorts) recs;
   373         val tnames = make_tnames Ts;
   373         val tnames = make_tnames Ts;
   374         val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
   374         val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
   375         val ts = map (fn ((r, s), T) => List.nth (size_consts, dest_DtRec r) $
   375         val ts = map (fn ((r, s), T) => nth size_consts (dest_DtRec r) $
   376           Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
   376           Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
   377         val t = if ts = [] then HOLogic.zero else
   377         val t = if ts = [] then HOLogic.zero else
   378           foldl1 plus (ts @ [HOLogic.Suc_zero])
   378           foldl1 plus (ts @ [HOLogic.Suc_zero])
   379       in
   379       in
   380         HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
   380         HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $