add_cases_induct: induct_method setup;
authorwenzelm
Sun Feb 27 15:32:10 2000 +0100 (2000-02-27)
changeset 83076600c6e53111
parent 8306 9855f1801d2b
child 8308 45e11d3ccbe4
add_cases_induct: induct_method setup;
removed cases_of, all_cases, all_inducts;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sun Feb 27 15:31:40 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Feb 27 15:32:10 2000 +0100
     1.3 @@ -36,9 +36,6 @@
     1.4      {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
     1.5        induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
     1.6    val print_inductives: theory -> unit
     1.7 -  val cases_of: Sign.sg -> string -> thm
     1.8 -  val all_cases: Sign.sg -> thm list
     1.9 -  val all_inducts: Sign.sg -> thm list
    1.10    val mono_add_global: theory attribute
    1.11    val mono_del_global: theory attribute
    1.12    val get_monos: theory -> thm list
    1.13 @@ -106,24 +103,6 @@
    1.14    in InductiveData.put tab_monos thy end;
    1.15  
    1.16  
    1.17 -(* cases and induct rules *)
    1.18 -
    1.19 -fun cases_of sg name =
    1.20 -  let
    1.21 -    fun find (None, (_, ({names, ...}, {elims, ...}): inductive_info)) =
    1.22 -          assoc (names ~~ elims, name)
    1.23 -      | find (some, _) = some;
    1.24 -    val (tab, _) = InductiveData.get_sg sg;
    1.25 -  in
    1.26 -    (case Symtab.foldl find (None, tab) of
    1.27 -      None => error ("Unknown (co)inductive set " ^ quote name)
    1.28 -    | Some thm => thm)
    1.29 -  end;
    1.30 -
    1.31 -fun all_cases sg = flat (map (#elims o #2 o #2) (Symtab.dest (#1 (InductiveData.get_sg sg))));
    1.32 -fun all_inducts sg = map (#induct o #2 o #2) (Symtab.dest (#1 (InductiveData.get_sg sg)));
    1.33 -      
    1.34 -
    1.35  
    1.36  (** monotonicity rules **)
    1.37  
    1.38 @@ -765,6 +744,12 @@
    1.39  
    1.40  (** introduction of (co)inductive sets **)
    1.41  
    1.42 +fun add_cases_induct names elims induct =
    1.43 +  PureThy.add_thms
    1.44 +    (map (fn name => (("", induct), [InductMethod.induct_set_global name])) names @
    1.45 +     map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name])) (names, elims));
    1.46 +
    1.47 +
    1.48  fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
    1.49      atts intros monos con_defs thy =
    1.50    let
    1.51 @@ -789,7 +774,9 @@
    1.52        (if ! quick_and_dirty then add_ind_axm else add_ind_def)
    1.53          verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
    1.54          con_defs thy params paramTs cTs cnames;
    1.55 -    val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result);
    1.56 +    val thy2 = thy1
    1.57 +      |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
    1.58 +      |> add_cases_induct full_cnames (#elims result) (#induct result);
    1.59    in (thy2, result) end;
    1.60  
    1.61