adapted to new PureThy.add_thms etc.;
authorwenzelm
Mon Mar 13 13:20:51 2000 +0100 (2000-03-13)
changeset 84338ae16c770fc8
parent 8432 daf6b3961ed4
child 8434 5e4bba59bfaa
adapted to new PureThy.add_thms etc.;
tuned case names;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Mar 13 13:20:13 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Mar 13 13:20:51 2000 +0100
     1.3 @@ -403,7 +403,7 @@
     1.4      fun induct_spec (name, th) =
     1.5        (("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name]);
     1.6      val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct);
     1.7 -  in PureThy.add_thms (cases_specs @ induct_specs) end;
     1.8 +  in #1 o PureThy.add_thms (cases_specs @ induct_specs) end;
     1.9  
    1.10  
    1.11  
    1.12 @@ -658,19 +658,17 @@
    1.13      val def_terms = fp_def_term :: (if length cs < 2 then [] else
    1.14        map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
    1.15  
    1.16 -    val thy' = thy |>
    1.17 -      (if declare_consts then
    1.18 -        Theory.add_consts_i (map (fn (c, n) =>
    1.19 -          (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
    1.20 -       else I) |>
    1.21 -      (if length cs < 2 then I else
    1.22 -       Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |>
    1.23 -      Theory.add_path rec_name |>
    1.24 -      PureThy.add_defss_i [(("defs", def_terms), [])];
    1.25 +    val (thy', [fp_def :: rec_sets_defs]) =
    1.26 +      thy
    1.27 +      |> (if declare_consts then
    1.28 +          Theory.add_consts_i (map (fn (c, n) =>
    1.29 +            (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
    1.30 +          else I)
    1.31 +      |> (if length cs < 2 then I
    1.32 +          else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
    1.33 +      |> Theory.add_path rec_name
    1.34 +      |> PureThy.add_defss_i [(("defs", def_terms), [])];
    1.35  
    1.36 -    (* get definitions from theory *)
    1.37 -
    1.38 -    val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs";
    1.39  
    1.40      (* prove and store theorems *)
    1.41  
    1.42 @@ -689,14 +687,14 @@
    1.43      val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
    1.44        else standard (raw_induct RSN (2, rev_mp));
    1.45  
    1.46 -    val thy'' = thy'
    1.47 +    val (thy'', [intrs']) =
    1.48 +      thy'
    1.49        |> PureThy.add_thmss [(("intrs", intrs), atts)]
    1.50 -      |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
    1.51 -      |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])])
    1.52 -      |> (if no_ind then I else PureThy.add_thms
    1.53 +      |>> (#1 o PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts))
    1.54 +      |>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])])
    1.55 +      |>> (if no_ind then I else #1 o PureThy.add_thms
    1.56          [((coind_prefix coind ^ "induct", induct), [RuleCases.case_names induct_cases])])
    1.57 -      |> Theory.parent_path;
    1.58 -    val intrs' = PureThy.get_thms thy'' "intrs";
    1.59 +      |>> Theory.parent_path;
    1.60      val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims";  (* FIXME improve *)
    1.61      val induct' = if no_ind then induct else PureThy.get_thm thy'' (coind_prefix coind ^ "induct");  (* FIXME improve *)
    1.62    in (thy'',
    1.63 @@ -725,15 +723,16 @@
    1.64      val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
    1.65      val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
    1.66      
    1.67 -    val thy' = thy
    1.68 +    val thy' =
    1.69 +      thy
    1.70        |> (if declare_consts then
    1.71              Theory.add_consts_i
    1.72                (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
    1.73           else I)
    1.74        |> Theory.add_path rec_name
    1.75 -      |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("raw_elims", elim_ts), [])]
    1.76 +      |> (#1 o PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("raw_elims", elim_ts), [])])
    1.77        |> (if coind then I else
    1.78 -            PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
    1.79 +            #1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
    1.80  
    1.81      val intrs = PureThy.get_thms thy' "intrs";
    1.82      val elims = map2 (fn (th, cases) => RuleCases.name cases th)
    1.83 @@ -742,21 +741,21 @@
    1.84      val induct = if coind orelse length cs > 1 then raw_induct
    1.85        else standard (raw_induct RSN (2, rev_mp));
    1.86  
    1.87 -    val thy'' =
    1.88 +    val (thy'', ([elims'], intrs')) =
    1.89        thy'
    1.90        |> PureThy.add_thmss [(("elims", elims), [])]
    1.91 -      |> (if coind then I else PureThy.add_thms [(("induct", induct),
    1.92 -          [RuleCases.case_names induct_cases])])
    1.93 -      |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
    1.94 -      |> Theory.parent_path;
    1.95 +      |>> (if coind then I
    1.96 +          else #1 o PureThy.add_thms [(("induct", induct), [RuleCases.case_names induct_cases])])
    1.97 +      |>>> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
    1.98 +      |>> Theory.parent_path;
    1.99      val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct";
   1.100    in (thy'',
   1.101      {defs = [],
   1.102       mono = Drule.asm_rl,
   1.103       unfold = Drule.asm_rl,
   1.104 -     intrs = intrs,
   1.105 -     elims = elims,
   1.106 -     mk_cases = mk_cases elims,
   1.107 +     intrs = intrs',
   1.108 +     elims = elims',
   1.109 +     mk_cases = mk_cases elims',
   1.110       raw_induct = raw_induct,
   1.111       induct = induct'})
   1.112    end;