src/HOL/Tools/inductive_package.ML
changeset 11005 86f662ba3c3f
parent 10988 e0016a009c17
child 11036 3c30f7b97a50
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Jan 30 23:53:46 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Jan 31 01:13:01 2001 +0100
     1.3 @@ -452,7 +452,7 @@
     1.4              RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
     1.5        in names ~~ map proj (1 upto n) end;
     1.6  
     1.7 -fun add_cases_induct no_elim no_ind names elims induct induct_cases =
     1.8 +fun add_cases_induct no_elim no_ind names elims induct =
     1.9    let
    1.10      fun cases_spec (name, elim) thy =
    1.11        thy
    1.12 @@ -461,8 +461,8 @@
    1.13        |> Theory.parent_path;
    1.14      val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
    1.15  
    1.16 -    fun induct_spec (name, th) = (#1 o PureThy.add_thms
    1.17 -      [(("", th), [RuleCases.case_names induct_cases, InductAttrib.induct_set_global name])]);
    1.18 +    fun induct_spec (name, th) = #1 o PureThy.add_thms
    1.19 +      [(("", RuleCases.save induct th), [InductAttrib.induct_set_global name])];
    1.20      val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct);
    1.21    in Library.apply (cases_specs @ induct_specs) end;
    1.22  
    1.23 @@ -521,16 +521,16 @@
    1.24      val rules1 = [CollectE, disjE, make_elim vimageD, exE];
    1.25      val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
    1.26    in
    1.27 -    map (fn (t, cases) => SkipProof.prove_goalw_cterm thy rec_sets_defs
    1.28 -      (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
    1.29 -        [cut_facts_tac [hd prems] 1,
    1.30 -         dtac (unfold RS subst) 1,
    1.31 -         REPEAT (FIRSTGOAL (eresolve_tac rules1)),
    1.32 -         REPEAT (FIRSTGOAL (eresolve_tac rules2)),
    1.33 -         EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
    1.34 -      |> rulify
    1.35 -      |> RuleCases.name cases)
    1.36 -      (mk_elims cs cTs params intr_ts intr_names)
    1.37 +    mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
    1.38 +      SkipProof.prove_goalw_cterm thy rec_sets_defs
    1.39 +        (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
    1.40 +          [cut_facts_tac [hd prems] 1,
    1.41 +           dtac (unfold RS subst) 1,
    1.42 +           REPEAT (FIRSTGOAL (eresolve_tac rules1)),
    1.43 +           REPEAT (FIRSTGOAL (eresolve_tac rules2)),
    1.44 +           EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
    1.45 +        |> rulify
    1.46 +        |> RuleCases.name cases)
    1.47    end;
    1.48  
    1.49  
    1.50 @@ -768,9 +768,13 @@
    1.51        thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
    1.52      val (thy3, ([intrs'', elims'], [induct'])) =
    1.53        thy2
    1.54 -      |> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])]
    1.55 +      |> PureThy.add_thmss
    1.56 +        [(("intros", intrs'), atts),
    1.57 +          (("elims", elims), [RuleCases.consumes 1])]
    1.58        |>>> PureThy.add_thms
    1.59 -        [((coind_prefix coind ^ "induct", rulify induct), [RuleCases.case_names induct_cases])]
    1.60 +        [((coind_prefix coind ^ "induct", rulify induct),
    1.61 +         [RuleCases.case_names induct_cases,
    1.62 +          RuleCases.consumes 1])]
    1.63        |>> Theory.parent_path;
    1.64    in (thy3,
    1.65      {defs = fp_def :: rec_sets_defs,
    1.66 @@ -819,7 +823,7 @@
    1.67          con_defs thy params paramTs cTs cnames induct_cases;
    1.68      val thy2 = thy1
    1.69        |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
    1.70 -      |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases;
    1.71 +      |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct;
    1.72    in (thy2, result) end;
    1.73  
    1.74  fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =