# HG changeset patch
# User berghofe
# Date 1264866988 -3600
# Node ID 7f7939c9370f98f62d88ec2e8940e3f39c835ed4
# Parent  cc1d4c3ca9db4df7a38e390bfc4af4e4e9cec612
Added "constraints" tag / attribute for specifying the number of equality
constraints in cases rules.

diff -r cc1d4c3ca9db -r 7f7939c9370f src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOL/Tools/inductive.ML	Sat Jan 30 16:56:28 2010 +0100
@@ -72,7 +72,7 @@
     term list -> (binding * mixfix) list ->
     local_theory -> inductive_result * local_theory
   val declare_rules: binding -> bool -> bool -> string list ->
-    thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
+    thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
     thm -> local_theory -> thm list * thm list * thm * local_theory
   val add_ind_def: add_ind_def
   val gen_add_inductive_i: add_ind_def -> inductive_flags ->
@@ -411,7 +411,7 @@
                DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
           |> rulify
           |> singleton (ProofContext.export ctxt'' ctxt),
-         map #2 c_intrs)
+         map #2 c_intrs, length Ts)
       end
 
    in map prove_elim cs end;
@@ -724,11 +724,12 @@
     val (((_, elims'), (_, [induct'])), lthy2) =
       lthy1 |>
       Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
-      fold_map (fn (name, (elim, cases)) =>
+      fold_map (fn (name, (elim, cases, k)) =>
         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.constraints k)),
              Attrib.internal (K (Induct.cases_pred name)),
              Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
         apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
diff -r cc1d4c3ca9db -r 7f7939c9370f src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Sat Jan 30 16:56:28 2010 +0100
@@ -522,7 +522,8 @@
       Inductive.declare_rules rec_name coind no_ind cnames
         (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
         (map (fn th => (to_set [] (Context.Proof lthy3) th,
-           map fst (fst (Rule_Cases.get th)))) elims)
+           map fst (fst (Rule_Cases.get th)),
+           Rule_Cases.get_constraints th)) elims)
         raw_induct' lthy3;
   in
     ({intrs = intrs', elims = elims', induct = induct,
diff -r cc1d4c3ca9db -r 7f7939c9370f src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Jan 30 16:56:28 2010 +0100
@@ -288,6 +288,8 @@
   setup (Binding.name "folded") folded "folded definitions" #>
   setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
     "number of consumed facts" #>
+  setup (Binding.name "constraints") (Scan.lift P.nat >> Rule_Cases.constraints)
+    "number of equality constraints" #>
   setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
     "named rule cases" #>
   setup (Binding.name "case_conclusion")
diff -r cc1d4c3ca9db -r 7f7939c9370f src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sat Jan 30 16:56:28 2010 +0100
@@ -34,6 +34,8 @@
   val get_consumes: thm -> int
   val consumes: int -> attribute
   val consumes_default: int -> attribute
+  val get_constraints: thm -> int
+  val constraints: int -> attribute
   val name: string list -> thm -> thm
   val case_names: string list -> attribute
   val case_conclusion: string * string list -> attribute
@@ -236,6 +238,30 @@
 
 
 
+(** equality constraints **)
+
+val constraints_tagN = "constraints";
+
+fun lookup_constraints th =
+  (case AList.lookup (op =) (Thm.get_tags th) constraints_tagN of
+    NONE => NONE
+  | SOME s =>
+      (case Lexicon.read_nat s of SOME n => SOME n
+      | _ => raise THM ("Malformed 'constraints' tag of theorem", 0, [th])));
+
+fun get_constraints th = the_default 0 (lookup_constraints th);
+
+fun put_constraints NONE th = th
+  | put_constraints (SOME n) th = th
+      |> Thm.untag_rule constraints_tagN
+      |> Thm.tag_rule (constraints_tagN, string_of_int (if n < 0 then 0 else n));
+
+val save_constraints = put_constraints o lookup_constraints;
+
+fun constraints n = Thm.rule_attribute (K (put_constraints (SOME n)));
+
+
+
 (** case names **)
 
 val implode_args = space_implode ";";
@@ -308,6 +334,7 @@
 
 fun save th =
   save_consumes th #>
+  save_constraints th #>
   save_case_names th #>
   save_case_concls th #>
   save_inner_rule th;