src/HOL/Tools/datatype_prop.ML
changeset 21078 101aefd61aac
parent 20071 8f3e1ddb50e6
child 21621 f9fd69d96c4e
equal deleted inserted replaced
21077:d6c141871b29 21078:101aefd61aac
    62 
    62 
    63 (************************* injectivity of constructors ************************)
    63 (************************* injectivity of constructors ************************)
    64 
    64 
    65 fun make_injs descr sorts =
    65 fun make_injs descr sorts =
    66   let
    66   let
    67     val descr' = List.concat descr;
    67     val descr' = flat descr;
    68 
    68     fun make_inj T (cname, cargs) =
    69     fun make_inj T ((cname, cargs), injs) =
    69       if null cargs then I else
    70       if null cargs then injs else
       
    71         let
    70         let
    72           val Ts = map (typ_of_dtyp descr' sorts) cargs;
    71           val Ts = map (typ_of_dtyp descr' sorts) cargs;
    73           val constr_t = Const (cname, Ts ---> T);
    72           val constr_t = Const (cname, Ts ---> T);
    74           val tnames = make_tnames Ts;
    73           val tnames = make_tnames Ts;
    75           val frees = map Free (tnames ~~ Ts);
    74           val frees = map Free (tnames ~~ Ts);
    76           val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
    75           val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
    77         in (HOLogic.mk_Trueprop (HOLogic.mk_eq
    76         in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
    78           (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
    77           (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
    79            foldr1 (HOLogic.mk_binop "op &")
    78            foldr1 (HOLogic.mk_binop "op &")
    80              (map HOLogic.mk_eq (frees ~~ frees')))))::injs
    79              (map HOLogic.mk_eq (frees ~~ frees')))))
    81         end;
    80         end;
    82 
    81   in
    83   in map (fn (d, T) => foldr (make_inj T) [] (#3 (snd d)))
    82     map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
    84     ((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
    83       (hd descr) (Library.take (length (hd descr), get_rec_types descr' sorts))
    85   end;
    84   end;
    86 
    85 
    87 (********************************* induction **********************************)
    86 (********************************* induction **********************************)
    88 
    87 
    89 fun make_ind descr sorts =
    88 fun make_ind descr sorts =