src/HOL/Tools/datatype_prop.ML
changeset 22578 b0eb5652f210
parent 21621 f9fd69d96c4e
child 22994 02440636214f
equal deleted inserted replaced
22577:1a08fce38565 22578:b0eb5652f210
   175 
   175 
   176   in (rec_result_Ts, reccomb_fn_Ts) end;
   176   in (rec_result_Ts, reccomb_fn_Ts) end;
   177 
   177 
   178 fun make_primrecs new_type_names descr sorts thy =
   178 fun make_primrecs new_type_names descr sorts thy =
   179   let
   179   let
   180     val sign = Theory.sign_of thy;
       
   181 
       
   182     val descr' = List.concat descr;
   180     val descr' = List.concat descr;
   183     val recTs = get_rec_types descr' sorts;
   181     val recTs = get_rec_types descr' sorts;
   184     val used = foldr add_typ_tfree_names [] recTs;
   182     val used = foldr add_typ_tfree_names [] recTs;
   185 
   183 
   186     val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
   184     val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
   187 
   185 
   188     val rec_fns = map (uncurry (mk_Free "f"))
   186     val rec_fns = map (uncurry (mk_Free "f"))
   189       (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
   187       (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
   190 
   188 
   191     val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
   189     val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
   192     val reccomb_names = map (Sign.intern_const sign)
   190     val reccomb_names = map (Sign.intern_const thy)
   193       (if length descr' = 1 then [big_reccomb_name] else
   191       (if length descr' = 1 then [big_reccomb_name] else
   194         (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
   192         (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
   195           (1 upto (length descr'))));
   193           (1 upto (length descr'))));
   196     val reccombs = map (fn ((name, T), T') => list_comb
   194     val reccombs = map (fn ((name, T), T') => list_comb
   197       (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
   195       (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
   239       map (fn (_, cargs) =>
   237       map (fn (_, cargs) =>
   240         let val Ts = map (typ_of_dtyp descr' sorts) cargs
   238         let val Ts = map (typ_of_dtyp descr' sorts) cargs
   241         in Ts ---> T' end) constrs) (hd descr);
   239         in Ts ---> T' end) constrs) (hd descr);
   242 
   240 
   243     val case_names = map (fn s =>
   241     val case_names = map (fn s =>
   244       Sign.intern_const (Theory.sign_of thy) (s ^ "_case")) new_type_names
   242       Sign.intern_const thy (s ^ "_case")) new_type_names
   245   in
   243   in
   246     map (fn ((name, Ts), T) => list_comb
   244     map (fn ((name, Ts), T) => list_comb
   247       (Const (name, Ts @ [T] ---> T'),
   245       (Const (name, Ts @ [T] ---> T'),
   248         map (uncurry (mk_Free fname)) (Ts ~~ (1 upto length Ts))))
   246         map (uncurry (mk_Free fname)) (Ts ~~ (1 upto length Ts))))
   249           (case_names ~~ case_fn_Ts ~~ newTs)
   247           (case_names ~~ case_fn_Ts ~~ newTs)
   358     val descr' = List.concat descr;
   356     val descr' = List.concat descr;
   359     val recTs = get_rec_types descr' sorts;
   357     val recTs = get_rec_types descr' sorts;
   360 
   358 
   361     val size_name = "Nat.size";
   359     val size_name = "Nat.size";
   362     val size_names = replicate (length (hd descr)) size_name @
   360     val size_names = replicate (length (hd descr)) size_name @
   363       map (Sign.intern_const (Theory.sign_of thy)) (indexify_names
   361       map (Sign.intern_const thy) (indexify_names
   364         (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))));
   365     val size_consts = map (fn (s, T) =>
   363     val size_consts = map (fn (s, T) =>
   366       Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
   364       Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
   367 
   365 
   368     fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
   366     fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;