src/HOL/Tools/datatype_package.ML
changeset 10121 fb9be005cc44
parent 9747 043098ba5098
child 10212 33fe2d701ddd
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Oct 02 14:21:12 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Oct 02 14:22:39 2000 +0200
     1.3 @@ -63,6 +63,7 @@
     1.4         size : thm list,
     1.5         simps : thm list}
     1.6    val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
     1.7 +  val get_datatypes_sg : Sign.sg -> DatatypeAux.datatype_info Symtab.table
     1.8    val print_datatypes : theory -> unit
     1.9    val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info option
    1.10    val datatype_info : theory -> string -> DatatypeAux.datatype_info option
    1.11 @@ -71,6 +72,8 @@
    1.12    val constrs_of : theory -> string -> term list option
    1.13    val constrs_of_sg : Sign.sg -> string -> term list option
    1.14    val case_const_of : theory -> string -> term option
    1.15 +  val weak_case_congs_of : theory -> thm list
    1.16 +  val weak_case_congs_of_sg : Sign.sg -> thm list
    1.17    val setup: (theory -> theory) list
    1.18  end;
    1.19  
    1.20 @@ -134,6 +137,9 @@
    1.21       (Theory.sign_of thy) case_name)))
    1.22   | _ => None);
    1.23  
    1.24 +val weak_case_congs_of_sg = map (#weak_case_cong o #2) o Symtab.dest o get_datatypes_sg;
    1.25 +val weak_case_congs_of = weak_case_congs_of_sg o Theory.sign_of;
    1.26 +
    1.27  fun find_tname var Bi =
    1.28    let val frees = map dest_Free (term_frees Bi)
    1.29        val params = Logic.strip_params Bi;
    1.30 @@ -379,20 +385,22 @@
    1.31  (**** make datatype info ****)
    1.32  
    1.33  fun make_dt_info descr induct reccomb_names rec_thms
    1.34 -  ((((((((i, (_, (tname, _, _))), case_name), case_thms),
    1.35 -    exhaustion_thm), distinct_thm), inject), nchotomy), case_cong) = (tname,
    1.36 -      {index = i,
    1.37 -       descr = descr,
    1.38 -       rec_names = reccomb_names,
    1.39 -       rec_rewrites = rec_thms,
    1.40 -       case_name = case_name,
    1.41 -       case_rewrites = case_thms,
    1.42 -       induction = induct,
    1.43 -       exhaustion = exhaustion_thm,
    1.44 -       distinct = distinct_thm,
    1.45 -       inject = inject,
    1.46 -       nchotomy = nchotomy,
    1.47 -       case_cong = case_cong});
    1.48 +    (((((((((i, (_, (tname, _, _))), case_name), case_thms),
    1.49 +      exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) =
    1.50 +  (tname,
    1.51 +   {index = i,
    1.52 +    descr = descr,
    1.53 +    rec_names = reccomb_names,
    1.54 +    rec_rewrites = rec_thms,
    1.55 +    case_name = case_name,
    1.56 +    case_rewrites = case_thms,
    1.57 +    induction = induct,
    1.58 +    exhaustion = exhaustion_thm,
    1.59 +    distinct = distinct_thm,
    1.60 +    inject = inject,
    1.61 +    nchotomy = nchotomy,
    1.62 +    case_cong = case_cong,
    1.63 +    weak_case_cong = weak_case_cong});
    1.64  
    1.65  
    1.66  (********************* axiomatic introduction of datatypes ********************)
    1.67 @@ -554,7 +562,7 @@
    1.68      val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
    1.69        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
    1.70          exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
    1.71 -          nchotomys ~~ case_congs);
    1.72 +          nchotomys ~~ case_congs ~~ weak_case_congs);
    1.73  
    1.74      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
    1.75      val split_thms = split ~~ split_asm;
    1.76 @@ -613,7 +621,7 @@
    1.77  
    1.78      val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
    1.79        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
    1.80 -        casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs);
    1.81 +        casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.82  
    1.83      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
    1.84  
    1.85 @@ -719,8 +727,8 @@
    1.86        PureThy.add_thms [(("induct", induction), [case_names_induct])];
    1.87  
    1.88      val dt_infos = map (make_dt_info descr induction' reccomb_names rec_thms)
    1.89 -      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~
    1.90 -        casedist_thms ~~ map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs);
    1.91 +      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
    1.92 +        map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.93  
    1.94      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
    1.95