src/HOL/Tools/Datatype/datatype_prop.ML
author wenzelm
Sat Mar 22 18:19:57 2014 +0100 (2014-03-22)
changeset 56254 a2dd9200854d
parent 54398 100c0eaf63d5
child 57983 6edc3529bb4e
permissions -rw-r--r--
more antiquotations;
haftmann@33968
     1
(*  Title:      HOL/Tools/Datatype/datatype_prop.ML
wenzelm@11539
     2
    Author:     Stefan Berghofer, TU Muenchen
berghofe@5177
     3
haftmann@33968
     4
Datatype package: characteristic properties of datatypes.
berghofe@5177
     5
*)
berghofe@5177
     6
berghofe@5177
     7
signature DATATYPE_PROP =
berghofe@5177
     8
sig
wenzelm@45896
     9
  type descr = Datatype_Aux.descr
wenzelm@8434
    10
  val indexify_names: string list -> string list
berghofe@13465
    11
  val make_tnames: typ list -> string list
wenzelm@45822
    12
  val make_injs : descr list -> term list list
wenzelm@45889
    13
  val make_distincts : descr list -> term list list (*no symmetric inequalities*)
wenzelm@45822
    14
  val make_ind : descr list -> term
wenzelm@45822
    15
  val make_casedists : descr list -> term list
wenzelm@45822
    16
  val make_primrec_Ts : descr list -> string list -> typ list * typ list
wenzelm@45822
    17
  val make_primrecs : string list -> descr list -> theory -> term list
wenzelm@45822
    18
  val make_cases : string list -> descr list -> theory -> term list list
wenzelm@45822
    19
  val make_splits : string list -> descr list -> theory -> (term * term) list
wenzelm@45822
    20
  val make_case_combs : string list -> descr list -> theory -> string -> term list
wenzelm@45822
    21
  val make_weak_case_congs : string list -> descr list -> theory -> term list
wenzelm@45822
    22
  val make_case_congs : string list -> descr list -> theory -> term list
wenzelm@45822
    23
  val make_nchotomys : descr list -> term list
berghofe@5177
    24
end;
berghofe@5177
    25
haftmann@33968
    26
structure Datatype_Prop : DATATYPE_PROP =
berghofe@5177
    27
struct
berghofe@5177
    28
wenzelm@45896
    29
type descr = Datatype_Aux.descr;
wenzelm@45896
    30
wenzelm@45896
    31
blanchet@54398
    32
val indexify_names = Case_Translation.indexify_names;
blanchet@54398
    33
val make_tnames = Case_Translation.make_tnames;
wenzelm@8434
    34
berghofe@5177
    35
fun make_tnames Ts =
berghofe@5177
    36
  let
wenzelm@40720
    37
    fun type_name (TFree (name, _)) = unprefix "'" name
wenzelm@40720
    38
      | type_name (Type (name, _)) =
wenzelm@30364
    39
          let val name' = Long_Name.base_name name
wenzelm@50239
    40
          in if Symbol_Pos.is_identifier name' then name' else "x" end;
wenzelm@8434
    41
  in indexify_names (map type_name Ts) end;
berghofe@5177
    42
berghofe@5177
    43
berghofe@5177
    44
(************************* injectivity of constructors ************************)
berghofe@5177
    45
wenzelm@45822
    46
fun make_injs descr =
berghofe@5177
    47
  let
haftmann@21078
    48
    val descr' = flat descr;
haftmann@21078
    49
    fun make_inj T (cname, cargs) =
wenzelm@45700
    50
      if null cargs then I
wenzelm@45700
    51
      else
berghofe@5177
    52
        let
wenzelm@45822
    53
          val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
berghofe@5177
    54
          val constr_t = Const (cname, Ts ---> T);
berghofe@5177
    55
          val tnames = make_tnames Ts;
berghofe@5177
    56
          val frees = map Free (tnames ~~ Ts);
wenzelm@45743
    57
          val frees' = map Free (map (suffix "'") tnames ~~ Ts);
wenzelm@45743
    58
        in
wenzelm@45743
    59
          cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
wenzelm@45743
    60
            (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
wenzelm@45743
    61
             foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
wenzelm@45743
    62
               (map HOLogic.mk_eq (frees ~~ frees')))))
berghofe@5177
    63
        end;
haftmann@21078
    64
  in
haftmann@21078
    65
    map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
wenzelm@45822
    66
      (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr'))
berghofe@5177
    67
  end;
berghofe@5177
    68
haftmann@27300
    69
haftmann@27300
    70
(************************* distinctness of constructors ***********************)
haftmann@27300
    71
wenzelm@45822
    72
fun make_distincts descr =
haftmann@27300
    73
  let
haftmann@27300
    74
    val descr' = flat descr;
wenzelm@45822
    75
    val recTs = Datatype_Aux.get_rec_types descr';
haftmann@33957
    76
    val newTs = take (length (hd descr)) recTs;
haftmann@27300
    77
wenzelm@45822
    78
    fun prep_constr (cname, cargs) = (cname, map (Datatype_Aux.typ_of_dtyp descr') cargs);
haftmann@27300
    79
haftmann@27300
    80
    fun make_distincts' _ [] = []
wenzelm@45700
    81
      | make_distincts' T ((cname, cargs) :: constrs) =
haftmann@27300
    82
          let
wenzelm@45743
    83
            val frees = map Free (make_tnames cargs ~~ cargs);
haftmann@27300
    84
            val t = list_comb (Const (cname, cargs ---> T), frees);
haftmann@27300
    85
haftmann@27300
    86
            fun make_distincts'' (cname', cargs') =
haftmann@27300
    87
              let
wenzelm@45700
    88
                val frees' = map Free (map (suffix "'") (make_tnames cargs') ~~ cargs');
wenzelm@45700
    89
                val t' = list_comb (Const (cname', cargs' ---> T), frees');
haftmann@27300
    90
              in
haftmann@27300
    91
                HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t'))
wenzelm@45700
    92
              end;
haftmann@27300
    93
          in map make_distincts'' constrs @ make_distincts' T constrs end;
haftmann@27300
    94
  in
haftmann@27300
    95
    map2 (fn ((_, (_, _, constrs))) => fn T =>
wenzelm@45889
    96
      make_distincts' T (map prep_constr constrs)) (hd descr) newTs
haftmann@27300
    97
  end;
haftmann@27300
    98
haftmann@27300
    99
berghofe@5177
   100
(********************************* induction **********************************)
berghofe@5177
   101
wenzelm@45822
   102
fun make_ind descr =
berghofe@5177
   103
  let
wenzelm@32952
   104
    val descr' = flat descr;
wenzelm@45822
   105
    val recTs = Datatype_Aux.get_rec_types descr';
wenzelm@41423
   106
    val pnames =
wenzelm@41423
   107
      if length descr' = 1 then ["P"]
berghofe@5177
   108
      else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
berghofe@5177
   109
berghofe@5177
   110
    fun make_pred i T =
berghofe@5177
   111
      let val T' = T --> HOLogic.boolT
wenzelm@42364
   112
      in Free (nth pnames i, T') end;
berghofe@5177
   113
berghofe@5177
   114
    fun make_ind_prem k T (cname, cargs) =
berghofe@5177
   115
      let
berghofe@13641
   116
        fun mk_prem ((dt, s), T) =
berghofe@13641
   117
          let val (Us, U) = strip_type T
wenzelm@41423
   118
          in
wenzelm@46218
   119
            Logic.list_all (map (pair "x") Us,
wenzelm@41423
   120
              HOLogic.mk_Trueprop
wenzelm@41423
   121
                (make_pred (Datatype_Aux.body_index dt) U $
wenzelm@41423
   122
                  Datatype_Aux.app_bnds (Free (s, T)) (length Us)))
berghofe@13641
   123
          end;
berghofe@7015
   124
wenzelm@41423
   125
        val recs = filter Datatype_Aux.is_rec_type cargs;
wenzelm@45822
   126
        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
wenzelm@45822
   127
        val recTs' = map (Datatype_Aux.typ_of_dtyp descr') recs;
wenzelm@20071
   128
        val tnames = Name.variant_list pnames (make_tnames Ts);
wenzelm@41423
   129
        val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
berghofe@5177
   130
        val frees = tnames ~~ Ts;
berghofe@7015
   131
        val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
wenzelm@45700
   132
      in
wenzelm@46215
   133
        fold_rev (Logic.all o Free) frees
wenzelm@46215
   134
          (Logic.list_implies (prems,
wenzelm@45700
   135
            HOLogic.mk_Trueprop (make_pred k T $
wenzelm@45700
   136
              list_comb (Const (cname, Ts ---> T), map Free frees))))
berghofe@5177
   137
      end;
berghofe@5177
   138
wenzelm@45700
   139
    val prems =
wenzelm@45700
   140
      maps (fn ((i, (_, _, constrs)), T) => map (make_ind_prem i T) constrs) (descr' ~~ recTs);
berghofe@5177
   141
    val tnames = make_tnames recTs;
wenzelm@45700
   142
    val concl =
wenzelm@45700
   143
      HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
wenzelm@45700
   144
        (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
wenzelm@45700
   145
          (descr' ~~ recTs ~~ tnames)));
berghofe@5177
   146
berghofe@5177
   147
  in Logic.list_implies (prems, concl) end;
berghofe@5177
   148
berghofe@5177
   149
(******************************* case distinction *****************************)
berghofe@5177
   150
wenzelm@45822
   151
fun make_casedists descr =
berghofe@5177
   152
  let
wenzelm@32952
   153
    val descr' = flat descr;
berghofe@5177
   154
berghofe@5177
   155
    fun make_casedist_prem T (cname, cargs) =
berghofe@5177
   156
      let
wenzelm@45822
   157
        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
wenzelm@20071
   158
        val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
wenzelm@45700
   159
        val free_ts = map Free frees;
wenzelm@45700
   160
      in
wenzelm@46215
   161
        fold_rev (Logic.all o Free) frees
wenzelm@46215
   162
          (Logic.mk_implies (HOLogic.mk_Trueprop
wenzelm@45700
   163
            (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
wenzelm@45700
   164
              HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))
berghofe@5177
   165
      end;
berghofe@5177
   166
haftmann@33957
   167
    fun make_casedist ((_, (_, _, constrs))) T =
berghofe@5177
   168
      let val prems = map (make_casedist_prem T) constrs
wenzelm@45700
   169
      in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))) end;
berghofe@5177
   170
wenzelm@41423
   171
  in
wenzelm@41423
   172
    map2 make_casedist (hd descr)
wenzelm@45822
   173
      (take (length (hd descr)) (Datatype_Aux.get_rec_types descr'))
wenzelm@41423
   174
  end;
berghofe@5177
   175
berghofe@5177
   176
(*************** characteristic equations for primrec combinator **************)
berghofe@5177
   177
wenzelm@45822
   178
fun make_primrec_Ts descr used =
berghofe@5177
   179
  let
wenzelm@32952
   180
    val descr' = flat descr;
berghofe@5177
   181
wenzelm@45700
   182
    val rec_result_Ts =
wenzelm@45700
   183
      map TFree
wenzelm@45700
   184
        (Name.variant_list used (replicate (length descr') "'t") ~~
wenzelm@56254
   185
          replicate (length descr') @{sort type});
berghofe@5177
   186
wenzelm@32952
   187
    val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
berghofe@5177
   188
      map (fn (_, cargs) =>
berghofe@5177
   189
        let
wenzelm@45822
   190
          val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
wenzelm@41423
   191
          val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts);
berghofe@7015
   192
berghofe@13641
   193
          fun mk_argT (dt, T) =
wenzelm@42364
   194
            binder_types T ---> nth rec_result_Ts (Datatype_Aux.body_index dt);
berghofe@7015
   195
berghofe@7015
   196
          val argTs = Ts @ map mk_argT recs
wenzelm@42364
   197
        in argTs ---> nth rec_result_Ts i end) constrs) descr';
berghofe@5177
   198
berghofe@15459
   199
  in (rec_result_Ts, reccomb_fn_Ts) end;
berghofe@15459
   200
wenzelm@45879
   201
fun make_primrecs reccomb_names descr thy =
berghofe@15459
   202
  let
wenzelm@32952
   203
    val descr' = flat descr;
wenzelm@45822
   204
    val recTs = Datatype_Aux.get_rec_types descr';
wenzelm@45738
   205
    val used = fold Term.add_tfree_namesT recTs [];
berghofe@15459
   206
wenzelm@45822
   207
    val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr used;
berghofe@15459
   208
wenzelm@45700
   209
    val rec_fns =
wenzelm@45700
   210
      map (uncurry (Datatype_Aux.mk_Free "f"))
wenzelm@45700
   211
        (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
berghofe@5177
   212
wenzelm@45700
   213
    val reccombs =
wenzelm@45700
   214
      map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
berghofe@5177
   215
        (reccomb_names ~~ recTs ~~ rec_result_Ts);
berghofe@5177
   216
wenzelm@45700
   217
    fun make_primrec T comb_t (cname, cargs) (ts, f :: fs) =
berghofe@5177
   218
      let
wenzelm@41423
   219
        val recs = filter Datatype_Aux.is_rec_type cargs;
wenzelm@45822
   220
        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
wenzelm@45822
   221
        val recTs' = map (Datatype_Aux.typ_of_dtyp descr') recs;
berghofe@5177
   222
        val tnames = make_tnames Ts;
wenzelm@41423
   223
        val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
berghofe@5177
   224
        val frees = map Free (tnames ~~ Ts);
berghofe@5177
   225
        val frees' = map Free (rec_tnames ~~ recTs');
berghofe@7015
   226
berghofe@13641
   227
        fun mk_reccomb ((dt, T), t) =
wenzelm@42364
   228
          let val (Us, U) = strip_type T in
wenzelm@46219
   229
            fold_rev (Term.abs o pair "x") Us
wenzelm@46219
   230
              (nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
berghofe@13641
   231
          end;
berghofe@7015
   232
wenzelm@45700
   233
        val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees');
berghofe@5177
   234
wenzelm@45700
   235
      in
wenzelm@45700
   236
        (ts @ [HOLogic.mk_Trueprop
wenzelm@45700
   237
          (HOLogic.mk_eq (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
wenzelm@45700
   238
            list_comb (f, frees @ reccombs')))], fs)
wenzelm@33244
   239
      end;
wenzelm@33244
   240
  in
wenzelm@33244
   241
    fold (fn ((dt, T), comb_t) => fold (make_primrec T comb_t) (#3 (snd dt)))
wenzelm@33244
   242
      (descr' ~~ recTs ~~ reccombs) ([], rec_fns)
wenzelm@33244
   243
    |> fst
berghofe@5177
   244
  end;
berghofe@5177
   245
berghofe@5177
   246
(****************** make terms of form  t_case f1 ... fn  *********************)
berghofe@5177
   247
wenzelm@45879
   248
fun make_case_combs case_names descr thy fname =
berghofe@5177
   249
  let
wenzelm@32952
   250
    val descr' = flat descr;
wenzelm@45822
   251
    val recTs = Datatype_Aux.get_rec_types descr';
wenzelm@45738
   252
    val used = fold Term.add_tfree_namesT recTs [];
haftmann@33957
   253
    val newTs = take (length (hd descr)) recTs;
wenzelm@56254
   254
    val T' = TFree (singleton (Name.variant_list used) "'t", @{sort type});
berghofe@5177
   255
berghofe@5177
   256
    val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
berghofe@5177
   257
      map (fn (_, cargs) =>
wenzelm@45822
   258
        let val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs
berghofe@5177
   259
        in Ts ---> T' end) constrs) (hd descr);
berghofe@5177
   260
  in
berghofe@5177
   261
    map (fn ((name, Ts), T) => list_comb
berghofe@5177
   262
      (Const (name, Ts @ [T] ---> T'),
wenzelm@41423
   263
        map (uncurry (Datatype_Aux.mk_Free fname)) (Ts ~~ (1 upto length Ts))))
berghofe@5177
   264
          (case_names ~~ case_fn_Ts ~~ newTs)
berghofe@5177
   265
  end;
berghofe@5177
   266
berghofe@5177
   267
(**************** characteristic equations for case combinator ****************)
berghofe@5177
   268
wenzelm@45879
   269
fun make_cases case_names descr thy =
berghofe@5177
   270
  let
wenzelm@32952
   271
    val descr' = flat descr;
wenzelm@45822
   272
    val recTs = Datatype_Aux.get_rec_types descr';
haftmann@33957
   273
    val newTs = take (length (hd descr)) recTs;
berghofe@5177
   274
berghofe@5177
   275
    fun make_case T comb_t ((cname, cargs), f) =
berghofe@5177
   276
      let
wenzelm@45822
   277
        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
wenzelm@45700
   278
        val frees = map Free ((make_tnames Ts) ~~ Ts);
wenzelm@45700
   279
      in
wenzelm@45700
   280
        HOLogic.mk_Trueprop
wenzelm@45700
   281
          (HOLogic.mk_eq (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
wenzelm@45700
   282
            list_comb (f, frees)))
wenzelm@45700
   283
      end;
wenzelm@45700
   284
  in
wenzelm@45700
   285
    map (fn (((_, (_, _, constrs)), T), comb_t) =>
wenzelm@45879
   286
      map (make_case T comb_t) (constrs ~~ snd (strip_comb comb_t)))
wenzelm@45879
   287
        (hd descr ~~ newTs ~~ make_case_combs case_names descr thy "f")
berghofe@5177
   288
  end;
berghofe@5177
   289
berghofe@7015
   290
berghofe@5177
   291
(*************************** the "split" - equations **************************)
berghofe@5177
   292
wenzelm@45879
   293
fun make_splits case_names descr thy =
berghofe@5177
   294
  let
wenzelm@32952
   295
    val descr' = flat descr;
wenzelm@45822
   296
    val recTs = Datatype_Aux.get_rec_types descr';
wenzelm@45738
   297
    val used' = fold Term.add_tfree_namesT recTs [];
haftmann@33957
   298
    val newTs = take (length (hd descr)) recTs;
wenzelm@56254
   299
    val T' = TFree (singleton (Name.variant_list used') "'t", @{sort type});
berghofe@5177
   300
    val P = Free ("P", T' --> HOLogic.boolT);
berghofe@5177
   301
berghofe@5177
   302
    fun make_split (((_, (_, _, constrs)), T), comb_t) =
berghofe@5177
   303
      let
berghofe@5177
   304
        val (_, fs) = strip_comb comb_t;
wenzelm@45700
   305
        val used = ["P", "x"] @ map (fst o dest_Free) fs;
berghofe@5177
   306
wenzelm@33338
   307
        fun process_constr ((cname, cargs), f) (t1s, t2s) =
berghofe@5177
   308
          let
wenzelm@45822
   309
            val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
wenzelm@20071
   310
            val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
wenzelm@45700
   311
            val eqn = HOLogic.mk_eq (Free ("x", T), list_comb (Const (cname, Ts ---> T), frees));
wenzelm@45700
   312
            val P' = P $ list_comb (f, frees);
wenzelm@45700
   313
          in
wenzelm@45700
   314
           (fold_rev (fn Free (s, T) => fn t => HOLogic.mk_all (s, T, t)) frees
wenzelm@45700
   315
             (HOLogic.imp $ eqn $ P') :: t1s,
wenzelm@45700
   316
            fold_rev (fn Free (s, T) => fn t => HOLogic.mk_exists (s, T, t)) frees
wenzelm@45700
   317
             (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) :: t2s)
berghofe@5177
   318
          end;
berghofe@5177
   319
wenzelm@33338
   320
        val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);
wenzelm@45700
   321
        val lhs = P $ (comb_t $ Free ("x", T));
berghofe@5177
   322
      in
wenzelm@41423
   323
        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, Datatype_Aux.mk_conj t1s)),
wenzelm@41423
   324
         HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ Datatype_Aux.mk_disj t2s)))
berghofe@5177
   325
      end
berghofe@5177
   326
wenzelm@45700
   327
  in
wenzelm@45879
   328
    map make_split (hd descr ~~ newTs ~~ make_case_combs case_names descr thy "f")
berghofe@5177
   329
  end;
berghofe@5177
   330
berghofe@5177
   331
(************************* additional rules for TFL ***************************)
berghofe@5177
   332
wenzelm@45879
   333
fun make_weak_case_congs case_names descr thy =
nipkow@8601
   334
  let
wenzelm@45879
   335
    val case_combs = make_case_combs case_names descr thy "f";
nipkow@8601
   336
nipkow@8601
   337
    fun mk_case_cong comb =
wenzelm@45700
   338
      let
nipkow@8601
   339
        val Type ("fun", [T, _]) = fastype_of comb;
nipkow@8601
   340
        val M = Free ("M", T);
nipkow@8601
   341
        val M' = Free ("M'", T);
nipkow@8601
   342
      in
nipkow@8601
   343
        Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')),
nipkow@8601
   344
          HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb $ M')))
wenzelm@45700
   345
      end;
nipkow@8601
   346
  in
nipkow@8601
   347
    map mk_case_cong case_combs
nipkow@8601
   348
  end;
wenzelm@45700
   349
nipkow@8601
   350
berghofe@5177
   351
(*---------------------------------------------------------------------------
berghofe@5177
   352
 * Structure of case congruence theorem looks like this:
berghofe@5177
   353
 *
wenzelm@45700
   354
 *    (M = M')
wenzelm@45700
   355
 *    ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = g1 x1..xk))
wenzelm@45700
   356
 *    ==> ...
wenzelm@45700
   357
 *    ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = gn x1..xj))
berghofe@5177
   358
 *    ==>
berghofe@5177
   359
 *      (ty_case f1..fn M = ty_case g1..gn M')
berghofe@5177
   360
 *---------------------------------------------------------------------------*)
berghofe@5177
   361
wenzelm@45879
   362
fun make_case_congs case_names descr thy =
berghofe@5177
   363
  let
wenzelm@45879
   364
    val case_combs = make_case_combs case_names descr thy "f";
wenzelm@45879
   365
    val case_combs' = make_case_combs case_names descr thy "g";
berghofe@5177
   366
berghofe@5177
   367
    fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) =
berghofe@5177
   368
      let
berghofe@5177
   369
        val Type ("fun", [T, _]) = fastype_of comb;
berghofe@5177
   370
        val (_, fs) = strip_comb comb;
berghofe@5177
   371
        val (_, gs) = strip_comb comb';
berghofe@5177
   372
        val used = ["M", "M'"] @ map (fst o dest_Free) (fs @ gs);
berghofe@5177
   373
        val M = Free ("M", T);
berghofe@5177
   374
        val M' = Free ("M'", T);
berghofe@5177
   375
berghofe@5177
   376
        fun mk_clause ((f, g), (cname, _)) =
berghofe@5177
   377
          let
wenzelm@40844
   378
            val Ts = binder_types (fastype_of f);
wenzelm@20071
   379
            val tnames = Name.variant_list used (make_tnames Ts);
wenzelm@45743
   380
            val frees = map Free (tnames ~~ Ts);
berghofe@5177
   381
          in
wenzelm@46215
   382
            fold_rev Logic.all frees
wenzelm@46215
   383
              (Logic.mk_implies
wenzelm@46215
   384
                (HOLogic.mk_Trueprop
wenzelm@46215
   385
                  (HOLogic.mk_eq (M', list_comb (Const (cname, Ts ---> T), frees))),
wenzelm@46215
   386
                 HOLogic.mk_Trueprop
wenzelm@46215
   387
                  (HOLogic.mk_eq (list_comb (f, frees), list_comb (g, frees)))))
wenzelm@45700
   388
          end;
berghofe@5177
   389
      in
berghofe@5177
   390
        Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')) ::
berghofe@5177
   391
          map mk_clause (fs ~~ gs ~~ constrs),
berghofe@5177
   392
            HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb' $ M')))
wenzelm@45700
   393
      end;
berghofe@5177
   394
  in
berghofe@5177
   395
    map mk_case_cong (case_combs ~~ case_combs' ~~ hd descr)
berghofe@5177
   396
  end;
berghofe@5177
   397
berghofe@5177
   398
(*---------------------------------------------------------------------------
berghofe@5177
   399
 * Structure of exhaustion theorem looks like this:
berghofe@5177
   400
 *
berghofe@5177
   401
 *    !v. (? y1..yi. v = C1 y1..yi) | ... | (? y1..yj. v = Cn y1..yj)
berghofe@5177
   402
 *---------------------------------------------------------------------------*)
berghofe@5177
   403
wenzelm@45822
   404
fun make_nchotomys descr =
berghofe@5177
   405
  let
wenzelm@32952
   406
    val descr' = flat descr;
wenzelm@45822
   407
    val recTs = Datatype_Aux.get_rec_types descr';
haftmann@33957
   408
    val newTs = take (length (hd descr)) recTs;
berghofe@5177
   409
berghofe@5177
   410
    fun mk_eqn T (cname, cargs) =
berghofe@5177
   411
      let
wenzelm@45822
   412
        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
wenzelm@20071
   413
        val tnames = Name.variant_list ["v"] (make_tnames Ts);
wenzelm@45743
   414
        val frees = tnames ~~ Ts;
berghofe@5177
   415
      in
wenzelm@33338
   416
        fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees
skalberg@15574
   417
          (HOLogic.mk_eq (Free ("v", T),
wenzelm@33338
   418
            list_comb (Const (cname, Ts ---> T), map Free frees)))
wenzelm@45700
   419
      end;
wenzelm@45700
   420
  in
wenzelm@45700
   421
    map (fn ((_, (_, _, constrs)), T) =>
wenzelm@45700
   422
        HOLogic.mk_Trueprop
wenzelm@45700
   423
          (HOLogic.mk_all ("v", T, Datatype_Aux.mk_disj (map (mk_eqn T) constrs))))
berghofe@5177
   424
      (hd descr ~~ newTs)
berghofe@5177
   425
  end;
berghofe@5177
   426
berghofe@5177
   427
end;