separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
--- a/src/HOL/Tools/Datatype/datatype.ML Thu Oct 29 12:59:25 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Thu Oct 29 13:21:38 2009 +0100
@@ -63,9 +63,11 @@
val get_all = #types o DatatypesData.get;
val get_info = Symtab.lookup o get_all;
-fun the_info thy name = (case get_info thy name of
- SOME info => info
- | NONE => error ("Unknown datatype " ^ quote name));
+
+fun the_info thy name =
+ (case get_info thy name of
+ SOME info => info
+ | NONE => error ("Unknown datatype " ^ quote name));
fun info_of_constr thy (c, T) =
let
@@ -319,7 +321,7 @@
[((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
val unnamed_rules = map (fn induct =>
- ((Binding.empty, [induct]), [Thm.kind_internal, Induct.induct_type ""]))
+ ((Binding.empty, [induct]), [RuleCases.inner_rule, Induct.induct_type ""]))
(Library.drop (length dt_names, inducts));
in
thy9
--- a/src/Pure/Isar/rule_cases.ML Thu Oct 29 12:59:25 2009 +0100
+++ b/src/Pure/Isar/rule_cases.ML Thu Oct 29 13:21:38 2009 +0100
@@ -37,6 +37,8 @@
val name: string list -> thm -> thm
val case_names: string list -> attribute
val case_conclusion: string * string list -> attribute
+ val is_inner_rule: thm -> bool
+ val inner_rule: attribute
val save: thm -> thm -> thm
val get: thm -> (string * string list) list * int
val rename_params: string list list -> thm -> thm
@@ -90,7 +92,7 @@
fun extract_case is_open thy (case_outline, raw_prop) name concls =
let
- val rename = if is_open then I else (apfst (Name.internal o Name.clean));
+ val rename = if is_open then I else apfst (Name.internal o Name.clean);
val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
val len = length props;
@@ -212,7 +214,7 @@
val consumes_tagN = "consumes";
fun lookup_consumes th =
- (case AList.lookup (op =) (Thm.get_tags th) (consumes_tagN) of
+ (case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of
NONE => NONE
| SOME s =>
(case Lexicon.read_nat s of SOME n => SOME n
@@ -223,14 +225,13 @@
fun put_consumes NONE th = th
| put_consumes (SOME n) th = th
|> Thm.untag_rule consumes_tagN
- |> Thm.tag_rule
- (consumes_tagN, Library.string_of_int (if n < 0 then Thm.nprems_of th + n else n));
+ |> Thm.tag_rule (consumes_tagN, string_of_int (if n < 0 then Thm.nprems_of th + n else n));
fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
val save_consumes = put_consumes o lookup_consumes;
-fun consumes n x = Thm.rule_attribute (K (put_consumes (SOME n))) x;
+fun consumes n = Thm.rule_attribute (K (put_consumes (SOME n)));
fun consumes_default n x =
if is_some (lookup_consumes (#2 x)) then x else consumes n x;
@@ -282,7 +283,24 @@
else NONE)
in fold add_case_concl concls end;
-fun case_conclusion concl = Thm.rule_attribute (fn _ => add_case_concl concl);
+fun case_conclusion concl = Thm.rule_attribute (K (add_case_concl concl));
+
+
+
+(** inner rule **)
+
+val inner_rule_tagN = "inner_rule";
+
+fun is_inner_rule th =
+ AList.defined (op =) (Thm.get_tags th) inner_rule_tagN;
+
+fun put_inner_rule inner =
+ Thm.untag_rule inner_rule_tagN
+ #> inner ? Thm.tag_rule (inner_rule_tagN, "");
+
+val save_inner_rule = put_inner_rule o is_inner_rule;
+
+val inner_rule = Thm.rule_attribute (K (put_inner_rule true));
@@ -290,7 +308,11 @@
(* access hints *)
-fun save th = save_consumes th #> save_case_names th #> save_case_concls th;
+fun save th =
+ save_consumes th #>
+ save_case_names th #>
+ save_case_concls th #>
+ save_inner_rule th;
fun get th =
let
@@ -357,5 +379,5 @@
end;
-structure BasicRuleCases: BASIC_RULE_CASES = RuleCases;
-open BasicRuleCases;
+structure Basic_Rule_Cases: BASIC_RULE_CASES = RuleCases;
+open Basic_Rule_Cases;
--- a/src/Tools/induct.ML Thu Oct 29 12:59:25 2009 +0100
+++ b/src/Tools/induct.ML Thu Oct 29 13:21:38 2009 +0100
@@ -570,7 +570,7 @@
((fn [] => NONE | ts => List.last ts) #>
(fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
find_inductT ctxt)) [[]]
- |> filter_out (forall Thm.is_internal);
+ |> filter_out (forall RuleCases.is_inner_rule);
fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
| get_inductP _ _ = [];