add_cases_induct: accomodate no_elim and no_ind flags;
authorwenzelm
Mon Feb 28 13:39:45 2000 +0100 (2000-02-28)
changeset 8312b470bc28b59d
parent 8311 6218522253e7
child 8313 c7a87e79e9b1
add_cases_induct: accomodate no_elim and no_ind flags;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Feb 28 10:49:42 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Feb 28 13:39:45 2000 +0100
     1.3 @@ -661,7 +661,7 @@
     1.4        rec_sets_defs thy';
     1.5      val elims = if no_elim then [] else
     1.6        prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
     1.7 -    val raw_induct = if no_ind then TrueI else
     1.8 +    val raw_induct = if no_ind then Drule.asm_rl else
     1.9        if coind then standard (rule_by_tactic
    1.10          (rewrite_tac [mk_meta_eq vimage_Un] THEN
    1.11            fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
    1.12 @@ -679,8 +679,8 @@
    1.13          [((coind_prefix coind ^ "induct", induct), [])])
    1.14        |> Theory.parent_path;
    1.15      val intrs' = PureThy.get_thms thy'' "intrs";
    1.16 -    val elims' = PureThy.get_thms thy'' "elims";
    1.17 -    val induct' = PureThy.get_thm thy'' (coind_prefix coind ^ "induct");
    1.18 +    val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims";  (* FIXME improve *)
    1.19 +    val induct' = if no_ind then induct else PureThy.get_thm thy'' (coind_prefix coind ^ "induct");  (* FIXME improve *)
    1.20    in (thy'',
    1.21      {defs = fp_def::rec_sets_defs,
    1.22       mono = mono,
    1.23 @@ -719,7 +719,7 @@
    1.24  
    1.25      val intrs = PureThy.get_thms thy' "intrs";
    1.26      val elims = PureThy.get_thms thy' "elims";
    1.27 -    val raw_induct = if coind then TrueI else PureThy.get_thm thy' "raw_induct";
    1.28 +    val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy' "raw_induct";
    1.29      val induct = if coind orelse length cs > 1 then raw_induct
    1.30        else standard (raw_induct RSN (2, rev_mp));
    1.31  
    1.32 @@ -731,8 +731,8 @@
    1.33      val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct";
    1.34    in (thy'',
    1.35      {defs = [],
    1.36 -     mono = TrueI,
    1.37 -     unfold = TrueI,
    1.38 +     mono = Drule.asm_rl,
    1.39 +     unfold = Drule.asm_rl,
    1.40       intrs = intrs,
    1.41       elims = elims,
    1.42       mk_cases = mk_cases elims,
    1.43 @@ -744,10 +744,16 @@
    1.44  
    1.45  (** introduction of (co)inductive sets **)
    1.46  
    1.47 -fun add_cases_induct names elims induct =
    1.48 -  PureThy.add_thms
    1.49 -    (map (fn name => (("", induct), [InductMethod.induct_set_global name])) names @
    1.50 -     map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name])) (names, elims));
    1.51 +fun add_cases_induct no_elim no_ind names elims induct =
    1.52 +  let
    1.53 +    val cases_specs =
    1.54 +      if no_elim then []
    1.55 +      else map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name]))
    1.56 +        (names, elims);
    1.57 +    val induct_specs =
    1.58 +      if no_ind then []
    1.59 +      else map (fn name => (("", induct), [InductMethod.induct_set_global name])) names;
    1.60 +  in PureThy.add_thms (cases_specs @ induct_specs) end;
    1.61  
    1.62  
    1.63  fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
    1.64 @@ -776,7 +782,7 @@
    1.65          con_defs thy params paramTs cTs cnames;
    1.66      val thy2 = thy1
    1.67        |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
    1.68 -      |> add_cases_induct full_cnames (#elims result) (#induct result);
    1.69 +      |> add_cases_induct no_elim no_ind full_cnames (#elims result) (#induct result);
    1.70    in (thy2, result) end;
    1.71  
    1.72