mk_elims, add_cases_induct: name rule cases;
authorwenzelm
Wed Mar 08 18:06:12 2000 +0100 (2000-03-08)
changeset 83750544749a5e8f
parent 8374 ffb2eb084078
child 8376 f5628700ab9a
mk_elims, add_cases_induct: name rule cases;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Mar 08 18:02:36 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Mar 08 18:06:12 2000 +0100
     1.3 @@ -276,7 +276,13 @@
     1.4  
     1.5  (** elimination rules **)
     1.6  
     1.7 -fun mk_elims cs cTs params intr_ts =
     1.8 +fun tune_names raw_names =
     1.9 +  let
    1.10 +    fun tune ("", i) = Library.string_of_int i
    1.11 +      | tune (s, _) = s;
    1.12 +  in map2 tune (raw_names, 0 upto (length raw_names - 1)) end;
    1.13 +
    1.14 +fun mk_elims cs cTs params intr_ts intr_names =
    1.15    let
    1.16      val used = foldr add_term_names (intr_ts, []);
    1.17      val [aname, pname] = variantlist (["a", "P"], used);
    1.18 @@ -287,7 +293,7 @@
    1.19          HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
    1.20        in (u, t, Logic.strip_imp_prems r) end;
    1.21  
    1.22 -    val intrs = map dest_intr intr_ts;
    1.23 +    val intrs = map dest_intr intr_ts ~~ tune_names intr_names;
    1.24  
    1.25      fun mk_elim (c, T) =
    1.26        let
    1.27 @@ -296,9 +302,10 @@
    1.28          fun mk_elim_prem (_, t, ts) =
    1.29            list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
    1.30              Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
    1.31 +        val c_intrs = (filter (equal c o #1 o #1) intrs);
    1.32        in
    1.33 -        Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
    1.34 -          map mk_elim_prem (filter (equal c o #1) intrs), P)
    1.35 +        (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
    1.36 +          map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
    1.37        end
    1.38    in
    1.39      map mk_elim (cs ~~ cTs)
    1.40 @@ -394,17 +401,17 @@
    1.41              RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
    1.42        in names ~~ map proj (1 upto n) end;
    1.43  
    1.44 -fun add_cases_induct no_elim no_ind names elims induct =
    1.45 +fun add_cases_induct no_elim no_ind names elims induct induct_cases =
    1.46    let
    1.47 -    val cases_specs =
    1.48 -      if no_elim then []
    1.49 -      else map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name]))
    1.50 -        (names, elims);
    1.51 +    fun cases_spec (name, elim) = (("", elim), [InductMethod.cases_set_global name]);
    1.52 +    val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
    1.53  
    1.54 +    fun induct_spec (name, th) =
    1.55 +      (("", th), [RuleCases.case_names (tune_names induct_cases),
    1.56 +        InductMethod.induct_set_global name]);
    1.57      val induct_specs =
    1.58        if no_ind then []
    1.59 -      else map (fn (name, th) => (("", th), [InductMethod.induct_set_global name]))
    1.60 -        (project_rules names induct);
    1.61 +      else map induct_spec (project_rules names induct);
    1.62    in PureThy.add_thms (cases_specs @ induct_specs) end;
    1.63  
    1.64  
    1.65 @@ -459,25 +466,25 @@
    1.66  
    1.67  (** prove elimination rules **)
    1.68  
    1.69 -fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
    1.70 +fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
    1.71    let
    1.72      val _ = message "  Proving the elimination rules ...";
    1.73  
    1.74      val rules1 = [CollectE, disjE, make_elim vimageD, exE];
    1.75      val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
    1.76        map make_elim [Inl_inject, Inr_inject];
    1.77 -
    1.78 -    val elims = map (fn t => prove_goalw_cterm rec_sets_defs
    1.79 +  in
    1.80 +    map (fn (t, cases) => prove_goalw_cterm rec_sets_defs
    1.81        (cterm_of (Theory.sign_of thy) t) (fn prems =>
    1.82          [cut_facts_tac [hd prems] 1,
    1.83           dtac (unfold RS subst) 1,
    1.84           REPEAT (FIRSTGOAL (eresolve_tac rules1)),
    1.85           REPEAT (FIRSTGOAL (eresolve_tac rules2)),
    1.86           EVERY (map (fn prem =>
    1.87 -           DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]))
    1.88 -      (mk_elims cs cTs params intr_ts)
    1.89 -
    1.90 -  in elims end;
    1.91 +           DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
    1.92 +      |> RuleCases.name cases)
    1.93 +      (mk_elims cs cTs params intr_ts intr_names)
    1.94 +  end;
    1.95  
    1.96  
    1.97  (** derivation of simplified elimination rules **)
    1.98 @@ -680,7 +687,7 @@
    1.99      val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
   1.100        rec_sets_defs thy';
   1.101      val elims = if no_elim then [] else
   1.102 -      prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
   1.103 +      prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy';
   1.104      val raw_induct = if no_ind then Drule.asm_rl else
   1.105        if coind then standard (rule_by_tactic
   1.106          (rewrite_tac [mk_meta_eq vimage_Un] THEN
   1.107 @@ -722,7 +729,7 @@
   1.108      val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   1.109  
   1.110      val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   1.111 -    val elim_ts = mk_elims cs cTs params intr_ts;
   1.112 +    val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names);
   1.113  
   1.114      val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   1.115      val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
   1.116 @@ -733,18 +740,20 @@
   1.117                (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   1.118           else I)
   1.119        |> Theory.add_path rec_name
   1.120 -      |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])]
   1.121 +      |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("raw_elims", elim_ts), [])]
   1.122        |> (if coind then I else
   1.123              PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
   1.124  
   1.125      val intrs = PureThy.get_thms thy' "intrs";
   1.126 -    val elims = PureThy.get_thms thy' "elims";
   1.127 +    val elims = map2 (fn (th, cases) => RuleCases.name cases th)
   1.128 +      (PureThy.get_thms thy' "raw_elims", elim_cases);
   1.129      val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy' "raw_induct";
   1.130      val induct = if coind orelse length cs > 1 then raw_induct
   1.131        else standard (raw_induct RSN (2, rev_mp));
   1.132  
   1.133      val thy'' =
   1.134        thy'
   1.135 +      |> PureThy.add_thmss [(("elims", elims), [])]
   1.136        |> (if coind then I else PureThy.add_thms [(("induct", induct), [])])
   1.137        |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
   1.138        |> Theory.parent_path;
   1.139 @@ -790,7 +799,8 @@
   1.140          con_defs thy params paramTs cTs cnames;
   1.141      val thy2 = thy1
   1.142        |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   1.143 -      |> add_cases_induct no_elim no_ind full_cnames (#elims result) (#induct result);
   1.144 +      |> add_cases_induct no_elim no_ind full_cnames
   1.145 +        (#elims result) (#induct result) (map (#1 o #1) intros);
   1.146    in (thy2, result) end;
   1.147  
   1.148