wneuper/isa: src/HOL/Tools/Datatype/datatype

     1 (*  Title:      HOL/Tools/Datatype/datatype_prop.ML

     2     Author:     Stefan Berghofer, TU Muenchen

     4 Datatype package: characteristic properties of datatypes.

     5 *)

     7 signature DATATYPE_PROP =

     8 sig

     9   include DATATYPE_COMMON

    10   val indexify_names: string list -> string list

    11   val make_tnames: typ list -> string list

    12   val make_injs : descr list -> (string * sort) list -> term list list

    13   val make_distincts : descr list ->

    14     (string * sort) list -> (int * term list) list (*no symmetric inequalities*)

    15   val make_ind : descr list -> (string * sort) list -> term

    16   val make_casedists : descr list -> (string * sort) list -> term list

    17   val make_primrec_Ts : descr list -> (string * sort) list ->

    18     string list -> typ list * typ list

    19   val make_primrecs : string list -> descr list ->

    20     (string * sort) list -> theory -> term list

    21   val make_cases : string list -> descr list ->

    22     (string * sort) list -> theory -> term list list

    23   val make_splits : string list -> descr list ->

    24     (string * sort) list -> theory -> (term * term) list

    25   val make_case_combs : string list -> descr list ->

    26     (string * sort) list -> theory -> string -> term list

    27   val make_weak_case_congs : string list -> descr list ->

    28     (string * sort) list -> theory -> term list

    29   val make_case_congs : string list -> descr list ->

    30     (string * sort) list -> theory -> term list

    31   val make_nchotomys : descr list ->

    32     (string * sort) list -> term list

    33 end;

    35 structure Datatype_Prop : DATATYPE_PROP =

    36 struct

    38 fun indexify_names names =

    39   let

    40     fun index (x :: xs) tab =

    41       (case AList.lookup (op =) tab x of

    42         NONE => if member (op =) xs x then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab

    43       | SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab))

    44     | index [] _ = [];

    45   in index names [] end;

    47 fun make_tnames Ts =

    48   let

    49     fun type_name (TFree (name, _)) = unprefix "'" name

    50       | type_name (Type (name, _)) =

    51           let val name' = Long_Name.base_name name

    52           in if Lexicon.is_identifier name' then name' else "x" end;

    53   in indexify_names (map type_name Ts) end;

    56 (************************* injectivity of constructors ************************)

    58 fun make_injs descr sorts =

    59   let

    60     val descr' = flat descr;

    61     fun make_inj T (cname, cargs) =

    62       if null cargs then I else

    63         let

    64           val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;

    65           val constr_t = Const (cname, Ts ---> T);

    66           val tnames = make_tnames Ts;

    67           val frees = map Free (tnames ~~ Ts);

    68           val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);

    69         in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq

    70           (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),

    71            foldr1 (HOLogic.mk_binop @{const_name HOL.conj})

    72              (map HOLogic.mk_eq (frees ~~ frees')))))

    73         end;

    74   in

    75     map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])

    76       (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))

    77   end;

    80 (************************* distinctness of constructors ***********************)

    82 fun make_distincts descr sorts =

    83   let

    84     val descr' = flat descr;

    85     val recTs = Datatype_Aux.get_rec_types descr' sorts;

    86     val newTs = take (length (hd descr)) recTs;

    88     fun prep_constr (cname, cargs) = (cname, map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs);

    90     fun make_distincts' _ [] = []

    91       | make_distincts' T ((cname, cargs)::constrs) =

    92           let

    93             val frees = map Free ((make_tnames cargs) ~~ cargs);

    94             val t = list_comb (Const (cname, cargs ---> T), frees);

    96             fun make_distincts'' (cname', cargs') =

    97               let

    98                 val frees' = map Free ((map ((op ^) o (rpair "'"))

    99                   (make_tnames cargs')) ~~ cargs');

   100                 val t' = list_comb (Const (cname', cargs' ---> T), frees')

   101               in

   102                 HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t'))

   103               end

   105           in map make_distincts'' constrs @ make_distincts' T constrs end;

   107   in

   108     map2 (fn ((_, (_, _, constrs))) => fn T =>

   109       (length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs

   110   end;

   113 (********************************* induction **********************************)

   115 fun make_ind descr sorts =

   116   let

   117     val descr' = flat descr;

   118     val recTs = Datatype_Aux.get_rec_types descr' sorts;

   119     val pnames =

   120       if length descr' = 1 then ["P"]

   121       else map (fn i => "P" ^ string_of_int i) (1 upto length descr');

   123     fun make_pred i T =

   124       let val T' = T --> HOLogic.boolT

   125       in Free (nth pnames i, T') end;

   127     fun make_ind_prem k T (cname, cargs) =

   128       let

   129         fun mk_prem ((dt, s), T) =

   130           let val (Us, U) = strip_type T

   131           in

   132             list_all (map (pair "x") Us,

   133               HOLogic.mk_Trueprop

   134                 (make_pred (Datatype_Aux.body_index dt) U $

   135                   Datatype_Aux.app_bnds (Free (s, T)) (length Us)))

   136           end;

   138         val recs = filter Datatype_Aux.is_rec_type cargs;

   139         val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;

   140         val recTs' = map (Datatype_Aux.typ_of_dtyp descr' sorts) recs;

   141         val tnames = Name.variant_list pnames (make_tnames Ts);

   142         val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));

   143         val frees = tnames ~~ Ts;

   144         val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');

   146       in list_all_free (frees, Logic.list_implies (prems,

   147         HOLogic.mk_Trueprop (make_pred k T $

   148           list_comb (Const (cname, Ts ---> T), map Free frees))))

   149       end;

   151     val prems = maps (fn ((i, (_, _, constrs)), T) =>

   152       map (make_ind_prem i T) constrs) (descr' ~~ recTs);

   153     val tnames = make_tnames recTs;

   154     val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})

   155       (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))

   156         (descr' ~~ recTs ~~ tnames)))

   158   in Logic.list_implies (prems, concl) end;

   160 (******************************* case distinction *****************************)

   162 fun make_casedists descr sorts =

   163   let

   164     val descr' = flat descr;

   166     fun make_casedist_prem T (cname, cargs) =

   167       let

   168         val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;

   169         val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;

   170         val free_ts = map Free frees

   171       in list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop

   172         (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),

   173           HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))

   174       end;

   176     fun make_casedist ((_, (_, _, constrs))) T =

   177       let val prems = map (make_casedist_prem T) constrs

   178       in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)))

   179       end

   181   in

   182     map2 make_casedist (hd descr)

   183       (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))

   184   end;

   186 (*************** characteristic equations for primrec combinator **************)

   188 fun make_primrec_Ts descr sorts used =

   189   let

   190     val descr' = flat descr;

   192     val rec_result_Ts = map TFree (Name.variant_list used (replicate (length descr') "'t") ~~

   193       replicate (length descr') HOLogic.typeS);

   195     val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>

   196       map (fn (_, cargs) =>

   197         let

   198           val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;

   199           val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts);

   201           fun mk_argT (dt, T) =

   202             binder_types T ---> nth rec_result_Ts (Datatype_Aux.body_index dt);

   204           val argTs = Ts @ map mk_argT recs

   205         in argTs ---> nth rec_result_Ts i end) constrs) descr';

   207   in (rec_result_Ts, reccomb_fn_Ts) end;

   209 fun make_primrecs new_type_names descr sorts thy =

   210   let

   211     val descr' = flat descr;

   212     val recTs = Datatype_Aux.get_rec_types descr' sorts;

   213     val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;

   215     val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;

   217     val rec_fns = map (uncurry (Datatype_Aux.mk_Free "f"))

   218       (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));

   220     val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";

   221     val reccomb_names = map (Sign.intern_const thy)

   222       (if length descr' = 1 then [big_reccomb_name] else

   223         (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)

   224           (1 upto (length descr'))));

   225     val reccombs = map (fn ((name, T), T') => list_comb

   226       (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))

   227         (reccomb_names ~~ recTs ~~ rec_result_Ts);

   229     fun make_primrec T comb_t (cname, cargs) (ts, f::fs) =

   230       let

   231         val recs = filter Datatype_Aux.is_rec_type cargs;

   232         val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;

   233         val recTs' = map (Datatype_Aux.typ_of_dtyp descr' sorts) recs;

   234         val tnames = make_tnames Ts;

   235         val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));

   236         val frees = map Free (tnames ~~ Ts);

   237         val frees' = map Free (rec_tnames ~~ recTs');

   239         fun mk_reccomb ((dt, T), t) =

   240           let val (Us, U) = strip_type T in

   241             list_abs (map (pair "x") Us,

   242               nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))

   243           end;

   245         val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees')

   247       in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq

   248         (comb_t $ list_comb (Const (cname, Ts ---> T), frees),

   249          list_comb (f, frees @ reccombs')))], fs)

   250       end;

   252   in

   253     fold (fn ((dt, T), comb_t) => fold (make_primrec T comb_t) (#3 (snd dt)))

   254       (descr' ~~ recTs ~~ reccombs) ([], rec_fns)

   255     |> fst

   256   end;

   258 (****************** make terms of form  t_case f1 ... fn  *********************)

   260 fun make_case_combs new_type_names descr sorts thy fname =

   261   let

   262     val descr' = flat descr;

   263     val recTs = Datatype_Aux.get_rec_types descr' sorts;

   264     val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;

   265     val newTs = take (length (hd descr)) recTs;

   266     val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);

   268     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>

   269       map (fn (_, cargs) =>

   270         let val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs

   271         in Ts ---> T' end) constrs) (hd descr);

   273     val case_names = map (fn s =>

   274       Sign.intern_const thy (s ^ "_case")) new_type_names

   275   in

   276     map (fn ((name, Ts), T) => list_comb

   277       (Const (name, Ts @ [T] ---> T'),

   278         map (uncurry (Datatype_Aux.mk_Free fname)) (Ts ~~ (1 upto length Ts))))

   279           (case_names ~~ case_fn_Ts ~~ newTs)

   280   end;

   282 (**************** characteristic equations for case combinator ****************)

   284 fun make_cases new_type_names descr sorts thy =

   285   let

   286     val descr' = flat descr;

   287     val recTs = Datatype_Aux.get_rec_types descr' sorts;

   288     val newTs = take (length (hd descr)) recTs;

   290     fun make_case T comb_t ((cname, cargs), f) =

   291       let

   292         val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;

   293         val frees = map Free ((make_tnames Ts) ~~ Ts)

   294       in HOLogic.mk_Trueprop (HOLogic.mk_eq

   295         (comb_t $ list_comb (Const (cname, Ts ---> T), frees),

   296          list_comb (f, frees)))

   297       end

   299   in map (fn (((_, (_, _, constrs)), T), comb_t) =>

   300     map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t))))

   301       ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))

   302   end;

   305 (*************************** the "split" - equations **************************)

   307 fun make_splits new_type_names descr sorts thy =

   308   let

   309     val descr' = flat descr;

   310     val recTs = Datatype_Aux.get_rec_types descr' sorts;

   311     val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;

   312     val newTs = take (length (hd descr)) recTs;

   313     val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);

   314     val P = Free ("P", T' --> HOLogic.boolT);

   316     fun make_split (((_, (_, _, constrs)), T), comb_t) =

   317       let

   318         val (_, fs) = strip_comb comb_t;

   319         val used = ["P", "x"] @ (map (fst o dest_Free) fs);

   321         fun process_constr ((cname, cargs), f) (t1s, t2s) =

   322           let

   323             val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;

   324             val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);

   325             val eqn = HOLogic.mk_eq (Free ("x", T),

   326               list_comb (Const (cname, Ts ---> T), frees));

   327             val P' = P $ list_comb (f, frees)

   328           in (fold_rev (fn Free (s, T) => fn t => HOLogic.mk_all (s, T, t)) frees

   329                 (HOLogic.imp $ eqn $ P') :: t1s,

   330               fold_rev (fn Free (s, T) => fn t => HOLogic.mk_exists (s, T, t)) frees

   331                 (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) :: t2s)

   332           end;

   334         val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);

   335         val lhs = P $ (comb_t $ Free ("x", T))

   336       in

   337         (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, Datatype_Aux.mk_conj t1s)),

   338          HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ Datatype_Aux.mk_disj t2s)))

   339       end

   341   in map make_split ((hd descr) ~~ newTs ~~

   342     (make_case_combs new_type_names descr sorts thy "f"))

   343   end;

   345 (************************* additional rules for TFL ***************************)

   347 fun make_weak_case_congs new_type_names descr sorts thy =

   348   let

   349     val case_combs = make_case_combs new_type_names descr sorts thy "f";

   351     fun mk_case_cong comb =

   352       let

   353         val Type ("fun", [T, _]) = fastype_of comb;

   354         val M = Free ("M", T);

   355         val M' = Free ("M'", T);

   356       in

   357         Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')),

   358           HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb $ M')))

   359       end

   360   in

   361     map mk_case_cong case_combs

   362   end;

   365 (*---------------------------------------------------------------------------

   366  * Structure of case congruence theorem looks like this:

   367  *

   368  *    (M = M')

   369  *    ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = g1 x1..xk))

   370  *    ==> ...

   371  *    ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = gn x1..xj))

   372  *    ==>

   373  *      (ty_case f1..fn M = ty_case g1..gn M')

   374  *---------------------------------------------------------------------------*)

   376 fun make_case_congs new_type_names descr sorts thy =

   377   let

   378     val case_combs = make_case_combs new_type_names descr sorts thy "f";

   379     val case_combs' = make_case_combs new_type_names descr sorts thy "g";

   381     fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) =

   382       let

   383         val Type ("fun", [T, _]) = fastype_of comb;

   384         val (_, fs) = strip_comb comb;

   385         val (_, gs) = strip_comb comb';

   386         val used = ["M", "M'"] @ map (fst o dest_Free) (fs @ gs);

   387         val M = Free ("M", T);

   388         val M' = Free ("M'", T);

   390         fun mk_clause ((f, g), (cname, _)) =

   391           let

   392             val Ts = binder_types (fastype_of f);

   393             val tnames = Name.variant_list used (make_tnames Ts);

   394             val frees = map Free (tnames ~~ Ts)

   395           in

   396             list_all_free (tnames ~~ Ts, Logic.mk_implies

   397               (HOLogic.mk_Trueprop

   398                 (HOLogic.mk_eq (M', list_comb (Const (cname, Ts ---> T), frees))),

   399                HOLogic.mk_Trueprop

   400                 (HOLogic.mk_eq (list_comb (f, frees), list_comb (g, frees)))))

   401           end

   403       in

   404         Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')) ::

   405           map mk_clause (fs ~~ gs ~~ constrs),

   406             HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb' $ M')))

   407       end

   409   in

   410     map mk_case_cong (case_combs ~~ case_combs' ~~ hd descr)

   411   end;

   413 (*---------------------------------------------------------------------------

   414  * Structure of exhaustion theorem looks like this:

   415  *

   416  *    !v. (? y1..yi. v = C1 y1..yi) | ... | (? y1..yj. v = Cn y1..yj)

   417  *---------------------------------------------------------------------------*)

   419 fun make_nchotomys descr sorts =

   420   let

   421     val descr' = flat descr;

   422     val recTs = Datatype_Aux.get_rec_types descr' sorts;

   423     val newTs = take (length (hd descr)) recTs;

   425     fun mk_eqn T (cname, cargs) =

   426       let

   427         val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;

   428         val tnames = Name.variant_list ["v"] (make_tnames Ts);

   429         val frees = tnames ~~ Ts

   430       in

   431         fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees

   432           (HOLogic.mk_eq (Free ("v", T),

   433             list_comb (Const (cname, Ts ---> T), map Free frees)))

   434       end

   436   in map (fn ((_, (_, _, constrs)), T) =>

   437     HOLogic.mk_Trueprop (HOLogic.mk_all ("v", T, Datatype_Aux.mk_disj (map (mk_eqn T) constrs))))

   438       (hd descr ~~ newTs)

   439   end;

   442 open Datatype_Aux;

   444 end;

author	wenzelm
	Thu, 09 Jun 2011 16:34:49 +0200
changeset 44206	2b47822868e4
parent 43235	8c674b3b8e44
child 45004	44adaa6db327
permissions	-rw-r--r--