# HG changeset patch # User wenzelm # Date 952535172 -3600 # Node ID 0544749a5e8f34d6e16978dd694f77e9628f6432 # Parent ffb2eb084078d4ade693a4139f8bcf42d70e7981 mk_elims, add_cases_induct: name rule cases; diff -r ffb2eb084078 -r 0544749a5e8f src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Wed Mar 08 18:02:36 2000 +0100 +++ b/src/HOL/Tools/inductive_package.ML Wed Mar 08 18:06:12 2000 +0100 @@ -276,7 +276,13 @@ (** elimination rules **) -fun mk_elims cs cTs params intr_ts = +fun tune_names raw_names = + let + fun tune ("", i) = Library.string_of_int i + | tune (s, _) = s; + in map2 tune (raw_names, 0 upto (length raw_names - 1)) end; + +fun mk_elims cs cTs params intr_ts intr_names = let val used = foldr add_term_names (intr_ts, []); val [aname, pname] = variantlist (["a", "P"], used); @@ -287,7 +293,7 @@ HOLogic.dest_Trueprop (Logic.strip_imp_concl r) in (u, t, Logic.strip_imp_prems r) end; - val intrs = map dest_intr intr_ts; + val intrs = map dest_intr intr_ts ~~ tune_names intr_names; fun mk_elim (c, T) = let @@ -296,9 +302,10 @@ fun mk_elim_prem (_, t, ts) = list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params), Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P)); + val c_intrs = (filter (equal c o #1 o #1) intrs); in - Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: - map mk_elim_prem (filter (equal c o #1) intrs), P) + (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: + map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs) end in map mk_elim (cs ~~ cTs) @@ -394,17 +401,17 @@ RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard; in names ~~ map proj (1 upto n) end; -fun add_cases_induct no_elim no_ind names elims induct = +fun add_cases_induct no_elim no_ind names elims induct induct_cases = let - val cases_specs = - if no_elim then [] - else map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name])) - (names, elims); + fun cases_spec (name, elim) = (("", elim), [InductMethod.cases_set_global name]); + val cases_specs = if no_elim then [] else map2 cases_spec (names, elims); + fun induct_spec (name, th) = + (("", th), [RuleCases.case_names (tune_names induct_cases), + InductMethod.induct_set_global name]); val induct_specs = if no_ind then [] - else map (fn (name, th) => (("", th), [InductMethod.induct_set_global name])) - (project_rules names induct); + else map induct_spec (project_rules names induct); in PureThy.add_thms (cases_specs @ induct_specs) end; @@ -459,25 +466,25 @@ (** prove elimination rules **) -fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy = +fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy = let val _ = message " Proving the elimination rules ..."; val rules1 = [CollectE, disjE, make_elim vimageD, exE]; val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject]; - - val elims = map (fn t => prove_goalw_cterm rec_sets_defs + in + map (fn (t, cases) => prove_goalw_cterm rec_sets_defs (cterm_of (Theory.sign_of thy) t) (fn prems => [cut_facts_tac [hd prems] 1, dtac (unfold RS subst) 1, REPEAT (FIRSTGOAL (eresolve_tac rules1)), REPEAT (FIRSTGOAL (eresolve_tac rules2)), EVERY (map (fn prem => - DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])) - (mk_elims cs cTs params intr_ts) - - in elims end; + DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]) + |> RuleCases.name cases) + (mk_elims cs cTs params intr_ts intr_names) + end; (** derivation of simplified elimination rules **) @@ -680,7 +687,7 @@ val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy'; val elims = if no_elim then [] else - prove_elims cs cTs params intr_ts unfold rec_sets_defs thy'; + prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy'; val raw_induct = if no_ind then Drule.asm_rl else if coind then standard (rule_by_tactic (rewrite_tac [mk_meta_eq vimage_Un] THEN @@ -722,7 +729,7 @@ val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); - val elim_ts = mk_elims cs cTs params intr_ts; + val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names); val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl); @@ -733,18 +740,20 @@ (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames)) else I) |> Theory.add_path rec_name - |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])] + |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("raw_elims", elim_ts), [])] |> (if coind then I else PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]); val intrs = PureThy.get_thms thy' "intrs"; - val elims = PureThy.get_thms thy' "elims"; + val elims = map2 (fn (th, cases) => RuleCases.name cases th) + (PureThy.get_thms thy' "raw_elims", elim_cases); val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy' "raw_induct"; val induct = if coind orelse length cs > 1 then raw_induct else standard (raw_induct RSN (2, rev_mp)); val thy'' = thy' + |> PureThy.add_thmss [(("elims", elims), [])] |> (if coind then I else PureThy.add_thms [(("induct", induct), [])]) |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) |> Theory.parent_path; @@ -790,7 +799,8 @@ con_defs thy params paramTs cTs cnames; val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result) - |> add_cases_induct no_elim no_ind full_cnames (#elims result) (#induct result); + |> add_cases_induct no_elim no_ind full_cnames + (#elims result) (#induct result) (map (#1 o #1) intros); in (thy2, result) end;