# HG changeset patch # User wenzelm # Date 1357657267 -3600 # Node ID 2852f997bfb58f36e239cf9ae468a81b0e901b21 # Parent 82d48783fd7ad6856e492ced5c2fafa83a9148cf 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'); diff -r 82d48783fd7a -r 2852f997bfb5 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Tue Jan 08 13:24:12 2013 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Tue Jan 08 16:01:07 2013 +0100 @@ -540,7 +540,7 @@ in ctxt'' |> - Proof.theorem NONE (fn thss => fn ctxt => + Proof.theorem NONE (fn thss => fn ctxt => (* FIXME ctxt/ctxt' should be called lthy/lthy' *) let val rec_name = space_implode "_" (map Long_Name.base_name names); val rec_qualified = Binding.qualify false rec_name; @@ -553,27 +553,27 @@ mk_ind_proof ctxt thss' |> Inductive.rulify; val strong_cases = map (mk_cases_proof ##> Inductive.rulify) (thsss ~~ elims ~~ cases_prems ~~ cases_prems'); + val strong_induct_atts = + map (Attrib.internal o K) + [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))]; val strong_induct = - if length names > 1 then - (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0]) - else (strong_raw_induct RSN (2, rev_mp), - [ind_case_names, Rule_Cases.consumes 1]); + if length names > 1 then strong_raw_induct + else strong_raw_induct RSN (2, rev_mp); val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note - ((rec_qualified (Binding.name "strong_induct"), - map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]); + ((rec_qualified (Binding.name "strong_induct"), strong_induct_atts), [strong_induct]); val strong_inducts = Project_Rule.projects ctxt (1 upto length names) strong_induct'; in ctxt' |> - Local_Theory.note - ((rec_qualified (Binding.name "strong_inducts"), - [Attrib.internal (K ind_case_names), - Attrib.internal (K (Rule_Cases.consumes 1))]), - strong_inducts) |> snd |> + Local_Theory.notes + [((rec_qualified (Binding.name "strong_inducts"), []), + strong_inducts |> map (fn th => ([th], + [Attrib.internal (K ind_case_names), + Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd |> Local_Theory.notes (map (fn ((name, elim), (_, cases)) => ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"), [Attrib.internal (K (Rule_Cases.case_names (map snd cases))), - Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])])) + Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim)))]), [([elim], [])])) (strong_cases ~~ induct_cases')) |> snd end) (map (map (rulify_term thy #> rpair [])) vc_compat) diff -r 82d48783fd7a -r 2852f997bfb5 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Tue Jan 08 13:24:12 2013 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Tue Jan 08 16:01:07 2013 +0100 @@ -443,7 +443,7 @@ in ctxt'' |> - Proof.theorem NONE (fn thss => fn ctxt => + Proof.theorem NONE (fn thss => fn ctxt => (* FIXME ctxt/ctxt' should be called lthy/lthy' *) let val rec_name = space_implode "_" (map Long_Name.base_name names); val rec_qualified = Binding.qualify false rec_name; @@ -454,28 +454,27 @@ val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss'); val strong_raw_induct = mk_ind_proof ctxt thss' |> Inductive.rulify; + val strong_induct_atts = + map (Attrib.internal o K) + [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))]; val strong_induct = - if length names > 1 then - (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0]) - else (strong_raw_induct RSN (2, rev_mp), - [ind_case_names, Rule_Cases.consumes 1]); + if length names > 1 then strong_raw_induct + else strong_raw_induct RSN (2, rev_mp); val (induct_name, inducts_name) = case alt_name of NONE => (rec_qualified (Binding.name "strong_induct"), rec_qualified (Binding.name "strong_inducts")) | SOME s => (Binding.name s, Binding.name (s ^ "s")); val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note - ((induct_name, - map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]); + ((induct_name, strong_induct_atts), [strong_induct]); val strong_inducts = Project_Rule.projects ctxt' (1 upto length names) strong_induct' in ctxt' |> - Local_Theory.note - ((inducts_name, + Local_Theory.notes [((inducts_name, []), + strong_inducts |> map (fn th => ([th], [Attrib.internal (K ind_case_names), - Attrib.internal (K (Rule_Cases.consumes 1))]), - strong_inducts) |> snd + Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd end) (map (map (rulify_term thy #> rpair [])) vc_compat) end; diff -r 82d48783fd7a -r 2852f997bfb5 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Tue Jan 08 13:24:12 2013 +0100 +++ b/src/HOL/Tools/Function/function.ML Tue Jan 08 16:01:07 2013 +0100 @@ -105,14 +105,15 @@ val addsmps = add_simps fnames post sort_cont - val (((psimps', pinducts'), (_, [termination'])), lthy) = + val (((psimps', [pinducts']), (_, [termination'])), lthy) = lthy |> addsmps (conceal_partial o Binding.qualify false "partial") "psimps" conceal_partial psimp_attribs psimps - ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), + ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []), + simple_pinducts |> map (fn th => ([th], [Attrib.internal (K (Rule_Cases.case_names cnames)), - Attrib.internal (K (Rule_Cases.consumes 1)), - Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) + Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))), + Attrib.internal (K (Induct.induct_pred ""))])))] ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]) ||> (snd o Local_Theory.note ((qualify "cases", [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) diff -r 82d48783fd7a -r 2852f997bfb5 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Tue Jan 08 13:24:12 2013 +0100 +++ b/src/HOL/Tools/inductive.ML Tue Jan 08 16:01:07 2013 +0100 @@ -860,12 +860,17 @@ val ind_case_names = Rule_Cases.case_names intr_names; val induct = if coind then - (raw_induct, [Rule_Cases.case_names [rec_name], + (raw_induct, + [Rule_Cases.case_names [rec_name], Rule_Cases.case_conclusion (rec_name, intr_names), - Rule_Cases.consumes 1, Induct.coinduct_pred (hd cnames)]) + Rule_Cases.consumes (1 - Thm.nprems_of raw_induct), + Induct.coinduct_pred (hd cnames)]) else if no_ind orelse length cnames > 1 then - (raw_induct, [ind_case_names, Rule_Cases.consumes 0]) - else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]); + (raw_induct, + [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))]) + else + (raw_induct RSN (2, rev_mp), + [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))]); val (intrs', lthy1) = lthy |> @@ -883,7 +888,7 @@ Local_Theory.note ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"), [Attrib.internal (K (Rule_Cases.case_names cases)), - Attrib.internal (K (Rule_Cases.consumes 1)), + Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim))), Attrib.internal (K (Rule_Cases.constraints k)), Attrib.internal (K (Induct.cases_pred name)), Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #> @@ -906,7 +911,7 @@ Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []), inducts |> map (fn (name, th) => ([th], [Attrib.internal (K ind_case_names), - Attrib.internal (K (Rule_Cases.consumes 1)), + Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))), Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd end; in (intrs', elims', eqs', induct', inducts, lthy4) end;