Added "constraints" tag / attribute for specifying the number of equality
authorberghofe
Sat Jan 30 16:56:28 2010 +0100 (2010-01-30)
changeset 349867f7939c9370f
parent 34972 cc1d4c3ca9db
child 34987 c1e8af37ee75
Added "constraints" tag / attribute for specifying the number of equality
constraints in cases rules.
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/rule_cases.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Wed Jan 27 14:03:08 2010 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Jan 30 16:56:28 2010 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4      term list -> (binding * mixfix) list ->
     1.5      local_theory -> inductive_result * local_theory
     1.6    val declare_rules: binding -> bool -> bool -> string list ->
     1.7 -    thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
     1.8 +    thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
     1.9      thm -> local_theory -> thm list * thm list * thm * local_theory
    1.10    val add_ind_def: add_ind_def
    1.11    val gen_add_inductive_i: add_ind_def -> inductive_flags ->
    1.12 @@ -411,7 +411,7 @@
    1.13                 DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
    1.14            |> rulify
    1.15            |> singleton (ProofContext.export ctxt'' ctxt),
    1.16 -         map #2 c_intrs)
    1.17 +         map #2 c_intrs, length Ts)
    1.18        end
    1.19  
    1.20     in map prove_elim cs end;
    1.21 @@ -724,11 +724,12 @@
    1.22      val (((_, elims'), (_, [induct'])), lthy2) =
    1.23        lthy1 |>
    1.24        Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
    1.25 -      fold_map (fn (name, (elim, cases)) =>
    1.26 +      fold_map (fn (name, (elim, cases, k)) =>
    1.27          Local_Theory.note
    1.28            ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
    1.29              [Attrib.internal (K (Rule_Cases.case_names cases)),
    1.30               Attrib.internal (K (Rule_Cases.consumes 1)),
    1.31 +             Attrib.internal (K (Rule_Cases.constraints k)),
    1.32               Attrib.internal (K (Induct.cases_pred name)),
    1.33               Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
    1.34          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
     2.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Jan 27 14:03:08 2010 +0100
     2.2 +++ b/src/HOL/Tools/inductive_set.ML	Sat Jan 30 16:56:28 2010 +0100
     2.3 @@ -522,7 +522,8 @@
     2.4        Inductive.declare_rules rec_name coind no_ind cnames
     2.5          (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
     2.6          (map (fn th => (to_set [] (Context.Proof lthy3) th,
     2.7 -           map fst (fst (Rule_Cases.get th)))) elims)
     2.8 +           map fst (fst (Rule_Cases.get th)),
     2.9 +           Rule_Cases.get_constraints th)) elims)
    2.10          raw_induct' lthy3;
    2.11    in
    2.12      ({intrs = intrs', elims = elims', induct = induct,
     3.1 --- a/src/Pure/Isar/attrib.ML	Wed Jan 27 14:03:08 2010 +0100
     3.2 +++ b/src/Pure/Isar/attrib.ML	Sat Jan 30 16:56:28 2010 +0100
     3.3 @@ -288,6 +288,8 @@
     3.4    setup (Binding.name "folded") folded "folded definitions" #>
     3.5    setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
     3.6      "number of consumed facts" #>
     3.7 +  setup (Binding.name "constraints") (Scan.lift P.nat >> Rule_Cases.constraints)
     3.8 +    "number of equality constraints" #>
     3.9    setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
    3.10      "named rule cases" #>
    3.11    setup (Binding.name "case_conclusion")
     4.1 --- a/src/Pure/Isar/rule_cases.ML	Wed Jan 27 14:03:08 2010 +0100
     4.2 +++ b/src/Pure/Isar/rule_cases.ML	Sat Jan 30 16:56:28 2010 +0100
     4.3 @@ -34,6 +34,8 @@
     4.4    val get_consumes: thm -> int
     4.5    val consumes: int -> attribute
     4.6    val consumes_default: int -> attribute
     4.7 +  val get_constraints: thm -> int
     4.8 +  val constraints: int -> attribute
     4.9    val name: string list -> thm -> thm
    4.10    val case_names: string list -> attribute
    4.11    val case_conclusion: string * string list -> attribute
    4.12 @@ -236,6 +238,30 @@
    4.13  
    4.14  
    4.15  
    4.16 +(** equality constraints **)
    4.17 +
    4.18 +val constraints_tagN = "constraints";
    4.19 +
    4.20 +fun lookup_constraints th =
    4.21 +  (case AList.lookup (op =) (Thm.get_tags th) constraints_tagN of
    4.22 +    NONE => NONE
    4.23 +  | SOME s =>
    4.24 +      (case Lexicon.read_nat s of SOME n => SOME n
    4.25 +      | _ => raise THM ("Malformed 'constraints' tag of theorem", 0, [th])));
    4.26 +
    4.27 +fun get_constraints th = the_default 0 (lookup_constraints th);
    4.28 +
    4.29 +fun put_constraints NONE th = th
    4.30 +  | put_constraints (SOME n) th = th
    4.31 +      |> Thm.untag_rule constraints_tagN
    4.32 +      |> Thm.tag_rule (constraints_tagN, string_of_int (if n < 0 then 0 else n));
    4.33 +
    4.34 +val save_constraints = put_constraints o lookup_constraints;
    4.35 +
    4.36 +fun constraints n = Thm.rule_attribute (K (put_constraints (SOME n)));
    4.37 +
    4.38 +
    4.39 +
    4.40  (** case names **)
    4.41  
    4.42  val implode_args = space_implode ";";
    4.43 @@ -308,6 +334,7 @@
    4.44  
    4.45  fun save th =
    4.46    save_consumes th #>
    4.47 +  save_constraints th #>
    4.48    save_case_names th #>
    4.49    save_case_concls th #>
    4.50    save_inner_rule th;