src/HOL/Tools/datatype_package.ML
changeset 8437 258281c43dea
parent 8405 0255394a05da
child 8442 96023903c2df
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Mar 13 13:24:12 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Mar 13 13:27:44 2000 +0100
     1.3 @@ -9,8 +9,8 @@
     1.4  signature BASIC_DATATYPE_PACKAGE =
     1.5  sig
     1.6    val induct_tac : string -> int -> tactic
     1.7 -  val exhaust_tac : string -> int -> tactic
     1.8 -  val cases_tac : string -> int -> tactic
     1.9 +  val exhaust_tac : string -> int -> tactic		(* FIXME remove !? *)
    1.10 +  val case_tac : string -> int -> tactic
    1.11    val distinct_simproc : simproc
    1.12  end;
    1.13  
    1.14 @@ -71,7 +71,6 @@
    1.15    val constrs_of : theory -> string -> term list option
    1.16    val constrs_of_sg : Sign.sg -> string -> term list option
    1.17    val case_const_of : theory -> string -> term option
    1.18 -  val cases_of: Sign.sg -> string -> thm
    1.19    val setup: (theory -> theory) list
    1.20  end;
    1.21  
    1.22 @@ -130,9 +129,6 @@
    1.23  
    1.24  val constrs_of = constrs_of_sg o Theory.sign_of;
    1.25  
    1.26 -val exhaustion_of = #exhaustion oo datatype_info_sg_err
    1.27 -fun cases_of sg name = if name = HOLogic.boolN then case_split_thm else exhaustion_of sg name;
    1.28 -
    1.29  fun case_const_of thy tname = (case datatype_info thy tname of
    1.30     Some {case_name, ...} => Some (Const (case_name, the (Sign.const_type
    1.31       (Theory.sign_of thy) case_name)))
    1.32 @@ -191,21 +187,58 @@
    1.33    end;
    1.34  
    1.35  
    1.36 -(* generic exhaustion tactic for datatypes *)
    1.37 +(* generic case tactic for datatypes *)
    1.38  
    1.39 -fun gen_exhaust_tac get_rule aterm i state =
    1.40 -  let
    1.41 -    val rule = get_rule (Thm.sign_of_thm state) (infer_tname state i aterm);
    1.42 -    val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
    1.43 -      (hd (Logic.strip_assums_hyp (hd (Thm.prems_of rule))));
    1.44 -    val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
    1.45 -  in res_inst_tac [(exh_vname, aterm)] rule i state end;
    1.46 +fun case_tac aterm i state =
    1.47 +  let val name = infer_tname state i aterm in
    1.48 +    if name = HOLogic.boolN then res_inst_tac [("P", aterm)] case_split_thm i state
    1.49 +    else
    1.50 +      let
    1.51 +        val {exhaustion, ...} = datatype_info_sg_err (Thm.sign_of_thm state) name;
    1.52 +        val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
    1.53 +          (hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))));
    1.54 +        val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
    1.55 +      in res_inst_tac [(exh_vname, aterm)] exhaustion i state end
    1.56 +  end;
    1.57  
    1.58 -val exhaust_tac = gen_exhaust_tac exhaustion_of;
    1.59 -val cases_tac = gen_exhaust_tac cases_of;
    1.60 +val exhaust_tac = case_tac;
    1.61 +
    1.62  
    1.63  
    1.64 -(* add_cases_induct -- interface to induct method *)
    1.65 +(** induct method setup **)
    1.66 +
    1.67 +(* case names *)
    1.68 +
    1.69 +local
    1.70 +
    1.71 +fun dt_recs (DtTFree _) = []
    1.72 +  | dt_recs (DtType (_, dts)) = flat (map dt_recs dts)
    1.73 +  | dt_recs (DtRec i) = [i];
    1.74 +
    1.75 +fun dt_cases (descr: descr) (_, args, constrs) =
    1.76 +  let
    1.77 +    fun the_bname i = Sign.base_name (#1 (the (assoc (descr, i))));
    1.78 +    val bnames = map the_bname (distinct (flat (map dt_recs args)));
    1.79 +  in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
    1.80 +
    1.81 +
    1.82 +fun induct_cases descr =
    1.83 +  DatatypeProp.indexify_names (flat (map (dt_cases descr) (map #2 descr)));
    1.84 +
    1.85 +fun exhaust_cases descr i = dt_cases descr (the (assoc (descr, i)));
    1.86 +
    1.87 +in
    1.88 +
    1.89 +fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
    1.90 +
    1.91 +fun mk_case_names_exhausts descr new =
    1.92 +  map (RuleCases.case_names o exhaust_cases descr o #1)
    1.93 +    (filter (fn ((_, (name, _, _))) => name mem_string new) descr);
    1.94 +
    1.95 +end;
    1.96 +
    1.97 +
    1.98 +(* add_cases_induct *)
    1.99  
   1.100  fun add_cases_induct infos =
   1.101    let
   1.102 @@ -215,27 +248,10 @@
   1.103              (Library.funpow i (fn th => th RS conjunct2) thm)
   1.104            |> Drule.standard;
   1.105  
   1.106 -    fun dt_recs (DtTFree _) = []
   1.107 -      | dt_recs (DtType (_, dts)) = flat (map dt_recs dts)
   1.108 -      | dt_recs (DtRec i) = [i];
   1.109 -
   1.110 -    fun dt_cases (descr: descr) (_, args, constrs) =
   1.111 -      let
   1.112 -        fun the_bname i = Sign.base_name (#1 (the (assoc (descr, i))));
   1.113 -        val bnames = map the_bname (distinct (flat (map dt_recs args)));
   1.114 -      in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
   1.115 -
   1.116 -    fun induct_cases descr =
   1.117 -      Term.variantlist (flat (map (dt_cases descr) (map #2 descr)), []);
   1.118 -
   1.119 -    fun exhaust_cases descr i = dt_cases descr (the (assoc (descr, i)));
   1.120 -
   1.121      fun add (ths, (name, {index, descr, induction, exhaustion, ...}: datatype_info)) =
   1.122 -      (("", proj index (length descr) induction),
   1.123 -        [RuleCases.case_names (induct_cases descr), InductMethod.induct_type_global name]) ::
   1.124 -      (("", exhaustion), [RuleCases.case_names (exhaust_cases descr index),
   1.125 -        InductMethod.cases_type_global name]) :: ths;
   1.126 -  in PureThy.add_thms (foldl add ([], infos)) end;
   1.127 +      (("", proj index (length descr) induction), [InductMethod.induct_type_global name]) ::
   1.128 +      (("", exhaustion), [InductMethod.cases_type_global name]) :: ths;
   1.129 +  in #1 o PureThy.add_thms (foldl add ([], infos)) end;
   1.130  
   1.131  
   1.132  
   1.133 @@ -341,27 +357,29 @@
   1.134  
   1.135  (********************* axiomatic introduction of datatypes ********************)
   1.136  
   1.137 -fun add_and_get_axioms label tnames ts thy =
   1.138 -  foldr (fn ((tname, t), (thy', axs)) =>
   1.139 +fun add_and_get_axioms_atts label tnames attss ts thy =
   1.140 +  foldr (fn (((tname, atts), t), (thy', axs)) =>
   1.141      let
   1.142 -      val thy'' = thy' |>
   1.143 +      val (thy'', [ax]) = thy' |>
   1.144          Theory.add_path tname |>
   1.145 -        PureThy.add_axioms_i [((label, t), [])];
   1.146 -      val ax = PureThy.get_thm thy'' label
   1.147 +        PureThy.add_axioms_i [((label, t), atts)];
   1.148      in (Theory.parent_path thy'', ax::axs)
   1.149 -    end) (tnames ~~ ts, (thy, []));
   1.150 +    end) (tnames ~~ attss ~~ ts, (thy, []));
   1.151 +
   1.152 +fun add_and_get_axioms label tnames =
   1.153 +  add_and_get_axioms_atts label tnames (replicate (length tnames) []);
   1.154  
   1.155  fun add_and_get_axiomss label tnames tss thy =
   1.156    foldr (fn ((tname, ts), (thy', axss)) =>
   1.157      let
   1.158 -      val thy'' = thy' |>
   1.159 +      val (thy'', [axs]) = thy' |>
   1.160          Theory.add_path tname |>
   1.161          PureThy.add_axiomss_i [((label, ts), [])];
   1.162 -      val axs = PureThy.get_thms thy'' label
   1.163      in (Theory.parent_path thy'', axs::axss)
   1.164      end) (tnames ~~ tss, (thy, []));
   1.165  
   1.166 -fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
   1.167 +fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
   1.168 +    case_names_induct case_names_exhausts thy =
   1.169    let
   1.170      val descr' = flat descr;
   1.171      val recTs = get_rec_types descr' sorts;
   1.172 @@ -465,21 +483,22 @@
   1.173      val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
   1.174      val size_axs = if no_size then [] else DatatypeProp.make_size new_type_names descr sorts thy2;
   1.175  
   1.176 -    val (thy3, inject) = thy2 |>
   1.177 +    val (thy3, (([induct], [rec_thms]), inject)) =
   1.178 +      thy2 |>
   1.179        Theory.add_path (space_implode "_" new_type_names) |>
   1.180 -      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
   1.181 -      PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>
   1.182 -      (if no_size then I else PureThy.add_axiomss_i [(("size", size_axs), [])]) |>
   1.183 -      Theory.parent_path |>
   1.184 +      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [case_names_induct])] |>>>
   1.185 +      PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>>
   1.186 +      (if no_size then I else #1 o PureThy.add_axiomss_i [(("size", size_axs), [])]) |>>
   1.187 +      Theory.parent_path |>>>
   1.188        add_and_get_axiomss "inject" new_type_names
   1.189          (DatatypeProp.make_injs descr sorts);
   1.190 -    val induct = get_thm thy3 "induct";
   1.191 -    val rec_thms = get_thms thy3 "recs";
   1.192      val size_thms = if no_size then [] else get_thms thy3 "size";
   1.193      val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
   1.194        (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
   1.195 -    val (thy5, exhaustion) = add_and_get_axioms "exhaust" new_type_names
   1.196 -      (DatatypeProp.make_casedists descr sorts) thy4;
   1.197 +
   1.198 +    val exhaust_ts = DatatypeProp.make_casedists descr sorts;
   1.199 +    val (thy5, exhaustion) = add_and_get_axioms_atts "exhaust" new_type_names
   1.200 +      (map Library.single case_names_exhausts) exhaust_ts thy4;
   1.201      val (thy6, case_thms) = add_and_get_axiomss "cases" new_type_names
   1.202        (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
   1.203      val (split_ts, split_asm_ts) = ListPair.unzip
   1.204 @@ -501,7 +520,7 @@
   1.205  
   1.206      val thy11 = thy10 |>
   1.207        Theory.add_path (space_implode "_" new_type_names) |>
   1.208 -      PureThy.add_thmss [(("simps", simps), [])] |>
   1.209 +      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>
   1.210        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   1.211        add_cases_induct dt_infos |>
   1.212        Theory.parent_path;
   1.213 @@ -526,19 +545,20 @@
   1.214  
   1.215  (******************* definitional introduction of datatypes *******************)
   1.216  
   1.217 -fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
   1.218 +fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
   1.219 +    case_names_induct case_names_exhausts thy =
   1.220    let
   1.221      val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   1.222  
   1.223      val (thy2, inject, distinct, dist_rewrites, simproc_dists, induct) = thy |>
   1.224        DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
   1.225 -        types_syntax constr_syntax;
   1.226 +        types_syntax constr_syntax case_names_induct;
   1.227  
   1.228 -    val (thy3, casedist_thms) =
   1.229 -      DatatypeAbsProofs.prove_casedist_thms new_type_names descr sorts induct thy2;
   1.230 +    val (thy3, casedist_thms) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
   1.231 +      sorts induct case_names_exhausts thy2;
   1.232      val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   1.233        flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3;
   1.234 -    val (thy6, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
   1.235 +    val (thy6, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms
   1.236        flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
   1.237      val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
   1.238        descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   1.239 @@ -557,7 +577,7 @@
   1.240  
   1.241      val thy11 = thy10 |>
   1.242        Theory.add_path (space_implode "_" new_type_names) |>
   1.243 -      PureThy.add_thmss [(("simps", simps), [])] |>
   1.244 +      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>
   1.245        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   1.246        add_cases_induct dt_infos |>
   1.247        Theory.parent_path;
   1.248 @@ -602,7 +622,7 @@
   1.249            ((tname, map dest_TFree Ts) handle TERM _ => err t)
   1.250        | get_typ t = err t;
   1.251  
   1.252 -    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induction')));
   1.253 +    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induction')));
   1.254      val new_type_names = if_none alt_names (map fst dtnames);
   1.255  
   1.256      fun get_constr t = (case Logic.strip_assums_concl t of
   1.257 @@ -624,13 +644,18 @@
   1.258      val sorts = add_term_tfrees (concl_of induction', []);
   1.259      val dt_info = get_datatypes thy1;
   1.260  
   1.261 +    val case_names_induct = mk_case_names_induct descr;
   1.262 +    val case_names_exhausts = mk_case_names_exhausts descr (map #1 dtnames);
   1.263 +    
   1.264 +
   1.265      val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   1.266  
   1.267      val (thy2, casedist_thms) = thy1 |>
   1.268 -      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
   1.269 +      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction
   1.270 +        case_names_exhausts;
   1.271      val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   1.272        false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2;
   1.273 -    val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms false
   1.274 +    val (thy4, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms false
   1.275        new_type_names [descr] sorts reccomb_names rec_thms thy3;
   1.276      val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
   1.277        new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
   1.278 @@ -650,20 +675,20 @@
   1.279  
   1.280      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.281  
   1.282 -    val thy9 = thy8 |>
   1.283 -      store_thmss "inject" new_type_names inject |>
   1.284 -      store_thmss "distinct" new_type_names distinct |>
   1.285 +    val (thy9, [induction']) = thy8 |>
   1.286 +      (#1 o store_thmss "inject" new_type_names inject) |>
   1.287 +      (#1 o store_thmss "distinct" new_type_names distinct) |>
   1.288        Theory.add_path (space_implode "_" new_type_names) |>
   1.289 -      PureThy.add_thms [(("induct", induction), [])] |>
   1.290 -      PureThy.add_thmss [(("simps", simps), [])] |>
   1.291 -      put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   1.292 -      add_cases_induct dt_infos |>
   1.293 +      PureThy.add_thms [(("induct", induction), [case_names_induct])] |>>
   1.294 +      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>>
   1.295 +      put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>>
   1.296 +      add_cases_induct dt_infos |>>
   1.297        Theory.parent_path;
   1.298  
   1.299 +    (* FIXME use attributes *)
   1.300      val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)
   1.301        addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   1.302        addIffs flat (inject @ distinct));
   1.303 -
   1.304    in
   1.305      (thy9,
   1.306       {distinct = distinct,
   1.307 @@ -672,7 +697,7 @@
   1.308        rec_thms = rec_thms,
   1.309        case_thms = case_thms,
   1.310        split_thms = split_thms,
   1.311 -      induction = induction,
   1.312 +      induction = induction',
   1.313        size = size_thms,
   1.314        simps = simps})
   1.315    end;
   1.316 @@ -744,9 +769,13 @@
   1.317      val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
   1.318      val _ = check_nonempty descr;
   1.319  
   1.320 +    val descr' = flat descr;
   1.321 +    val case_names_induct = mk_case_names_induct descr';
   1.322 +    val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   1.323    in
   1.324      (if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
   1.325 -      flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy
   1.326 +      flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
   1.327 +      case_names_induct case_names_exhausts thy
   1.328    end;
   1.329  
   1.330  val add_datatype_i = gen_add_datatype cert_typ;