src/HOL/Tools/inductive_package.ML
changeset 8401 50d5f4402305
parent 8380 c96953faf0a4
child 8410 5902c02fa122
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Mar 09 22:56:40 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Mar 09 22:57:13 2000 +0100
     1.3 @@ -402,9 +402,7 @@
     1.4  
     1.5      fun induct_spec (name, th) =
     1.6        (("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name]);
     1.7 -    val induct_specs =
     1.8 -      if no_ind then []
     1.9 -      else map induct_spec (project_rules names induct);
    1.10 +    val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct);
    1.11    in PureThy.add_thms (cases_specs @ induct_specs) end;
    1.12  
    1.13  
    1.14 @@ -605,7 +603,7 @@
    1.15  (** definitional introduction of (co)inductive sets **)
    1.16  
    1.17  fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
    1.18 -    atts intros monos con_defs thy params paramTs cTs cnames =
    1.19 +    atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
    1.20    let
    1.21      val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
    1.22        commas_quote cnames) else ();
    1.23 @@ -696,7 +694,7 @@
    1.24        |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
    1.25        |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])])
    1.26        |> (if no_ind then I else PureThy.add_thms
    1.27 -        [((coind_prefix coind ^ "induct", induct), [])])
    1.28 +        [((coind_prefix coind ^ "induct", induct), [RuleCases.case_names induct_cases])])
    1.29        |> Theory.parent_path;
    1.30      val intrs' = PureThy.get_thms thy'' "intrs";
    1.31      val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims";  (* FIXME improve *)
    1.32 @@ -717,7 +715,7 @@
    1.33  (** axiomatic introduction of (co)inductive sets **)
    1.34  
    1.35  fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
    1.36 -    atts intros monos con_defs thy params paramTs cTs cnames =
    1.37 +    atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
    1.38    let
    1.39      val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
    1.40  
    1.41 @@ -747,7 +745,8 @@
    1.42      val thy'' =
    1.43        thy'
    1.44        |> PureThy.add_thmss [(("elims", elims), [])]
    1.45 -      |> (if coind then I else PureThy.add_thms [(("induct", induct), [])])
    1.46 +      |> (if coind then I else PureThy.add_thms [(("induct", induct),
    1.47 +          [RuleCases.case_names induct_cases])])
    1.48        |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
    1.49        |> Theory.parent_path;
    1.50      val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct";
    1.51 @@ -785,15 +784,16 @@
    1.52      val cnames = map Sign.base_name full_cnames;
    1.53  
    1.54      val _ = seq (check_rule sign cs o snd o fst) intros;
    1.55 +    val induct_cases = map (#1 o #1) intros;
    1.56  
    1.57      val (thy1, result) =
    1.58        (if ! quick_and_dirty then add_ind_axm else add_ind_def)
    1.59          verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
    1.60 -        con_defs thy params paramTs cTs cnames;
    1.61 +        con_defs thy params paramTs cTs cnames induct_cases;
    1.62      val thy2 = thy1
    1.63        |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
    1.64 -      |> add_cases_induct no_elim no_ind full_cnames
    1.65 -        (#elims result) (#induct result) (map (#1 o #1) intros);
    1.66 +      |> add_cases_induct no_elim (no_ind orelse coind) full_cnames
    1.67 +          (#elims result) (#induct result) induct_cases;
    1.68    in (thy2, result) end;
    1.69  
    1.70