HOLogic.dest_conj;
authorwenzelm
Sun Feb 27 15:31:40 2000 +0100 (2000-02-27)
changeset 83069855f1801d2b
parent 8305 93aa21ec5494
child 8307 6600c6e53111
HOLogic.dest_conj;
add_cases_induct: induct_method setup;
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sun Feb 27 15:26:47 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun Feb 27 15:31:40 2000 +0100
     1.3 @@ -183,7 +183,7 @@
     1.4      val {induction, ...} = datatype_info_sg_err sign tn;
     1.5      val ind_vnames = map (fn (_ $ Var (ixn, _)) =>
     1.6        implode (tl (explode (Syntax.string_of_vname ixn))))
     1.7 -        (dest_conj (HOLogic.dest_Trueprop (concl_of induction)));
     1.8 +        (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induction)));
     1.9      val insts = (ind_vnames ~~ vars) handle LIST _ =>
    1.10        error ("Induction rule for type " ^ tn ^ " has different number of variables")
    1.11    in
    1.12 @@ -205,6 +205,15 @@
    1.13  val cases_tac = gen_exhaust_tac cases_of;
    1.14  
    1.15  
    1.16 +(* add_cases_induct *)
    1.17 +
    1.18 +fun add_cases_induct infos =
    1.19 +  let
    1.20 +    fun add (ths, (name, {induction, exhaustion, ...}: datatype_info)) =
    1.21 +      (("", induction), [InductMethod.induct_type_global name]) ::
    1.22 +       (("", exhaustion), [InductMethod.cases_type_global name]) :: ths;
    1.23 +  in PureThy.add_thms (foldl add ([], infos)) end;
    1.24 +
    1.25  
    1.26  (**** simplification procedure for showing distinctness of constructors ****)
    1.27  
    1.28 @@ -470,6 +479,7 @@
    1.29        Theory.add_path (space_implode "_" new_type_names) |>
    1.30        PureThy.add_thmss [(("simps", simps), [])] |>
    1.31        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.32 +      add_cases_induct dt_infos |>
    1.33        Theory.parent_path;
    1.34  
    1.35      val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
    1.36 @@ -525,6 +535,7 @@
    1.37        Theory.add_path (space_implode "_" new_type_names) |>
    1.38        PureThy.add_thmss [(("simps", simps), [])] |>
    1.39        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.40 +      add_cases_induct dt_infos |>
    1.41        Theory.parent_path;
    1.42  
    1.43      val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
    1.44 @@ -567,7 +578,7 @@
    1.45            ((tname, map dest_TFree Ts) handle TERM _ => err t)
    1.46        | get_typ t = err t;
    1.47  
    1.48 -    val dtnames = map get_typ (dest_conj (HOLogic.dest_Trueprop (concl_of induction')));
    1.49 +    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induction')));
    1.50      val new_type_names = if_none alt_names (map fst dtnames);
    1.51  
    1.52      fun get_constr t = (case Logic.strip_assums_concl t of
    1.53 @@ -622,6 +633,7 @@
    1.54        PureThy.add_thms [(("induct", induction), [])] |>
    1.55        PureThy.add_thmss [(("simps", simps), [])] |>
    1.56        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.57 +      add_cases_induct dt_infos |>
    1.58        Theory.parent_path;
    1.59  
    1.60      val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)