prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
authorwenzelm
Tue Jan 08 16:01:07 2013 +0100 (2013-01-08)
changeset 507712852f997bfb5
parent 50770 82d48783fd7a
child 50772 6973b3f41334
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Tue Jan 08 13:24:12 2013 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Jan 08 16:01:07 2013 +0100
     1.3 @@ -540,7 +540,7 @@
     1.4  
     1.5    in
     1.6      ctxt'' |>
     1.7 -    Proof.theorem NONE (fn thss => fn ctxt =>
     1.8 +    Proof.theorem NONE (fn thss => fn ctxt => (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
     1.9        let
    1.10          val rec_name = space_implode "_" (map Long_Name.base_name names);
    1.11          val rec_qualified = Binding.qualify false rec_name;
    1.12 @@ -553,27 +553,27 @@
    1.13            mk_ind_proof ctxt thss' |> Inductive.rulify;
    1.14          val strong_cases = map (mk_cases_proof ##> Inductive.rulify)
    1.15            (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
    1.16 +        val strong_induct_atts =
    1.17 +          map (Attrib.internal o K)
    1.18 +            [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
    1.19          val strong_induct =
    1.20 -          if length names > 1 then
    1.21 -            (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
    1.22 -          else (strong_raw_induct RSN (2, rev_mp),
    1.23 -            [ind_case_names, Rule_Cases.consumes 1]);
    1.24 +          if length names > 1 then strong_raw_induct
    1.25 +          else strong_raw_induct RSN (2, rev_mp);
    1.26          val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
    1.27 -          ((rec_qualified (Binding.name "strong_induct"),
    1.28 -            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
    1.29 +          ((rec_qualified (Binding.name "strong_induct"), strong_induct_atts), [strong_induct]);
    1.30          val strong_inducts =
    1.31            Project_Rule.projects ctxt (1 upto length names) strong_induct';
    1.32        in
    1.33          ctxt' |>
    1.34 -        Local_Theory.note
    1.35 -          ((rec_qualified (Binding.name "strong_inducts"),
    1.36 -            [Attrib.internal (K ind_case_names),
    1.37 -             Attrib.internal (K (Rule_Cases.consumes 1))]),
    1.38 -           strong_inducts) |> snd |>
    1.39 +        Local_Theory.notes
    1.40 +          [((rec_qualified (Binding.name "strong_inducts"), []),
    1.41 +            strong_inducts |> map (fn th => ([th],
    1.42 +              [Attrib.internal (K ind_case_names),
    1.43 +               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd |>
    1.44          Local_Theory.notes (map (fn ((name, elim), (_, cases)) =>
    1.45              ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
    1.46                [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
    1.47 -               Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
    1.48 +               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim)))]), [([elim], [])]))
    1.49            (strong_cases ~~ induct_cases')) |> snd
    1.50        end)
    1.51        (map (map (rulify_term thy #> rpair [])) vc_compat)
     2.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Jan 08 13:24:12 2013 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Jan 08 16:01:07 2013 +0100
     2.3 @@ -443,7 +443,7 @@
     2.4  
     2.5    in
     2.6      ctxt'' |>
     2.7 -    Proof.theorem NONE (fn thss => fn ctxt =>
     2.8 +    Proof.theorem NONE (fn thss => fn ctxt =>  (* FIXME ctxt/ctxt' should be called lthy/lthy' *)
     2.9        let
    2.10          val rec_name = space_implode "_" (map Long_Name.base_name names);
    2.11          val rec_qualified = Binding.qualify false rec_name;
    2.12 @@ -454,28 +454,27 @@
    2.13          val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
    2.14          val strong_raw_induct =
    2.15            mk_ind_proof ctxt thss' |> Inductive.rulify;
    2.16 +        val strong_induct_atts =
    2.17 +          map (Attrib.internal o K)
    2.18 +            [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
    2.19          val strong_induct =
    2.20 -          if length names > 1 then
    2.21 -            (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
    2.22 -          else (strong_raw_induct RSN (2, rev_mp),
    2.23 -            [ind_case_names, Rule_Cases.consumes 1]);
    2.24 +          if length names > 1 then strong_raw_induct
    2.25 +          else strong_raw_induct RSN (2, rev_mp);
    2.26          val (induct_name, inducts_name) =
    2.27            case alt_name of
    2.28              NONE => (rec_qualified (Binding.name "strong_induct"),
    2.29                       rec_qualified (Binding.name "strong_inducts"))
    2.30            | SOME s => (Binding.name s, Binding.name (s ^ "s"));
    2.31          val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
    2.32 -          ((induct_name,
    2.33 -            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
    2.34 +          ((induct_name, strong_induct_atts), [strong_induct]);
    2.35          val strong_inducts =
    2.36            Project_Rule.projects ctxt' (1 upto length names) strong_induct'
    2.37        in
    2.38          ctxt' |>
    2.39 -        Local_Theory.note
    2.40 -          ((inducts_name,
    2.41 +        Local_Theory.notes [((inducts_name, []),
    2.42 +          strong_inducts |> map (fn th => ([th],
    2.43              [Attrib.internal (K ind_case_names),
    2.44 -             Attrib.internal (K (Rule_Cases.consumes 1))]),
    2.45 -           strong_inducts) |> snd
    2.46 +             Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd
    2.47        end)
    2.48        (map (map (rulify_term thy #> rpair [])) vc_compat)
    2.49    end;
     3.1 --- a/src/HOL/Tools/Function/function.ML	Tue Jan 08 13:24:12 2013 +0100
     3.2 +++ b/src/HOL/Tools/Function/function.ML	Tue Jan 08 16:01:07 2013 +0100
     3.3 @@ -105,14 +105,15 @@
     3.4  
     3.5          val addsmps = add_simps fnames post sort_cont
     3.6  
     3.7 -        val (((psimps', pinducts'), (_, [termination'])), lthy) =
     3.8 +        val (((psimps', [pinducts']), (_, [termination'])), lthy) =
     3.9            lthy
    3.10            |> addsmps (conceal_partial o Binding.qualify false "partial")
    3.11                 "psimps" conceal_partial psimp_attribs psimps
    3.12 -          ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
    3.13 +          ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []),
    3.14 +                simple_pinducts |> map (fn th => ([th],
    3.15                   [Attrib.internal (K (Rule_Cases.case_names cnames)),
    3.16 -                  Attrib.internal (K (Rule_Cases.consumes 1)),
    3.17 -                  Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
    3.18 +                  Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
    3.19 +                  Attrib.internal (K (Induct.induct_pred ""))])))]
    3.20            ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
    3.21            ||> (snd o Local_Theory.note ((qualify "cases",
    3.22                   [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
     4.1 --- a/src/HOL/Tools/inductive.ML	Tue Jan 08 13:24:12 2013 +0100
     4.2 +++ b/src/HOL/Tools/inductive.ML	Tue Jan 08 16:01:07 2013 +0100
     4.3 @@ -860,12 +860,17 @@
     4.4      val ind_case_names = Rule_Cases.case_names intr_names;
     4.5      val induct =
     4.6        if coind then
     4.7 -        (raw_induct, [Rule_Cases.case_names [rec_name],
     4.8 +        (raw_induct,
     4.9 +         [Rule_Cases.case_names [rec_name],
    4.10            Rule_Cases.case_conclusion (rec_name, intr_names),
    4.11 -          Rule_Cases.consumes 1, Induct.coinduct_pred (hd cnames)])
    4.12 +          Rule_Cases.consumes (1 - Thm.nprems_of raw_induct),
    4.13 +          Induct.coinduct_pred (hd cnames)])
    4.14        else if no_ind orelse length cnames > 1 then
    4.15 -        (raw_induct, [ind_case_names, Rule_Cases.consumes 0])
    4.16 -      else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]);
    4.17 +        (raw_induct,
    4.18 +          [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))])
    4.19 +      else
    4.20 +        (raw_induct RSN (2, rev_mp),
    4.21 +          [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))]);
    4.22  
    4.23      val (intrs', lthy1) =
    4.24        lthy |>
    4.25 @@ -883,7 +888,7 @@
    4.26          Local_Theory.note
    4.27            ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
    4.28              [Attrib.internal (K (Rule_Cases.case_names cases)),
    4.29 -             Attrib.internal (K (Rule_Cases.consumes 1)),
    4.30 +             Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim))),
    4.31               Attrib.internal (K (Rule_Cases.constraints k)),
    4.32               Attrib.internal (K (Induct.cases_pred name)),
    4.33               Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
    4.34 @@ -906,7 +911,7 @@
    4.35            Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []),
    4.36              inducts |> map (fn (name, th) => ([th],
    4.37                [Attrib.internal (K ind_case_names),
    4.38 -               Attrib.internal (K (Rule_Cases.consumes 1)),
    4.39 +               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
    4.40                 Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd
    4.41          end;
    4.42    in (intrs', elims', eqs', induct', inducts, lthy4) end;