Added inducts field to inductive_result.
authorberghofe
Mon Mar 08 15:00:34 2010 +0100 (2010-03-08)
changeset 35646b32d6c1bdb4d
parent 35645 74e4542d0a4a
child 35649 7418ea4b999b
child 35650 64fff18d7f08
Added inducts field to inductive_result.
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Mon Mar 08 09:38:59 2010 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Mon Mar 08 15:00:34 2010 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4  sig
     1.5    type inductive_result =
     1.6      {preds: term list, elims: thm list, raw_induct: thm,
     1.7 -     induct: thm, intrs: thm list}
     1.8 +     induct: thm, inducts: thm list, intrs: thm list}
     1.9    val morph_result: morphism -> inductive_result -> inductive_result
    1.10    type inductive_info = {names: string list, coind: bool} * inductive_result
    1.11    val the_inductive: Proof.context -> string -> inductive_info
    1.12 @@ -73,7 +73,7 @@
    1.13      local_theory -> inductive_result * local_theory
    1.14    val declare_rules: binding -> bool -> bool -> string list ->
    1.15      thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
    1.16 -    thm -> local_theory -> thm list * thm list * thm * local_theory
    1.17 +    thm -> local_theory -> thm list * thm list * thm * thm list * local_theory
    1.18    val add_ind_def: add_ind_def
    1.19    val gen_add_inductive_i: add_ind_def -> inductive_flags ->
    1.20      ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
    1.21 @@ -121,16 +121,16 @@
    1.22  
    1.23  type inductive_result =
    1.24    {preds: term list, elims: thm list, raw_induct: thm,
    1.25 -   induct: thm, intrs: thm list};
    1.26 +   induct: thm, inducts: thm list, intrs: thm list};
    1.27  
    1.28 -fun morph_result phi {preds, elims, raw_induct: thm, induct, intrs} =
    1.29 +fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs} =
    1.30    let
    1.31      val term = Morphism.term phi;
    1.32      val thm = Morphism.thm phi;
    1.33      val fact = Morphism.fact phi;
    1.34    in
    1.35     {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
    1.36 -    induct = thm induct, intrs = fact intrs}
    1.37 +    induct = thm induct, inducts = fact inducts, intrs = fact intrs}
    1.38    end;
    1.39  
    1.40  type inductive_info =
    1.41 @@ -737,8 +737,8 @@
    1.42          ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
    1.43            map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
    1.44  
    1.45 -    val lthy3 =
    1.46 -      if no_ind orelse coind then lthy2
    1.47 +    val (inducts, lthy3) =
    1.48 +      if no_ind orelse coind then ([], lthy2)
    1.49        else
    1.50          let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in
    1.51            lthy2 |>
    1.52 @@ -746,9 +746,9 @@
    1.53              inducts |> map (fn (name, th) => ([th],
    1.54                [Attrib.internal (K ind_case_names),
    1.55                 Attrib.internal (K (Rule_Cases.consumes 1)),
    1.56 -               Attrib.internal (K (Induct.induct_pred name))])))] |> snd
    1.57 +               Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd
    1.58          end;
    1.59 -  in (intrs', elims', induct', lthy3) end;
    1.60 +  in (intrs', elims', induct', inducts, lthy3) end;
    1.61  
    1.62  type inductive_flags =
    1.63    {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
    1.64 @@ -796,7 +796,7 @@
    1.65           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
    1.66             rec_preds_defs lthy1);
    1.67  
    1.68 -    val (intrs', elims', induct, lthy2) = declare_rules rec_name coind no_ind
    1.69 +    val (intrs', elims', induct, inducts, lthy2) = declare_rules rec_name coind no_ind
    1.70        cnames intrs intr_names intr_atts elims raw_induct lthy1;
    1.71  
    1.72      val result =
    1.73 @@ -804,7 +804,8 @@
    1.74         intrs = intrs',
    1.75         elims = elims',
    1.76         raw_induct = rulify raw_induct,
    1.77 -       induct = induct};
    1.78 +       induct = induct,
    1.79 +       inducts = inducts};
    1.80  
    1.81      val lthy3 = lthy2
    1.82        |> Local_Theory.declaration false (fn phi =>
     2.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Mar 08 09:38:59 2010 +0100
     2.2 +++ b/src/HOL/Tools/inductive_set.ML	Mon Mar 08 15:00:34 2010 +0100
     2.3 @@ -520,7 +520,7 @@
     2.4      val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
     2.5      val (intr_names, intr_atts) = split_list (map fst intros);
     2.6      val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
     2.7 -    val (intrs', elims', induct, lthy4) =
     2.8 +    val (intrs', elims', induct, inducts, lthy4) =
     2.9        Inductive.declare_rules rec_name coind no_ind cnames
    2.10          (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
    2.11          (map (fn th => (to_set [] (Context.Proof lthy3) th,
    2.12 @@ -528,7 +528,7 @@
    2.13             Rule_Cases.get_constraints th)) elims)
    2.14          raw_induct' lthy3;
    2.15    in
    2.16 -    ({intrs = intrs', elims = elims', induct = induct,
    2.17 +    ({intrs = intrs', elims = elims', induct = induct, inducts = inducts,
    2.18        raw_induct = raw_induct', preds = map fst defs},
    2.19       lthy4)
    2.20    end;