# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1249228699 -7200
# Node ID ba59e95a5d2be081d7bd5e8092d2cf491f34f9b9
# Parent  aa48c2b8f8e023b5334758bbe885b3ed5dc8f66d
the derived induction principles can be given an explicit name

diff -r aa48c2b8f8e0 -r ba59e95a5d2b src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Aug 01 20:34:34 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Aug 02 17:58:19 2009 +0200
@@ -8,7 +8,7 @@
 
 signature NOMINAL_INDUCTIVE2 =
 sig
-  val prove_strong_ind: string -> (string * string list) list -> local_theory -> Proof.state
+  val prove_strong_ind: string -> string option -> (string * string list) list -> local_theory -> Proof.state
 end
 
 structure NominalInductive2 : NOMINAL_INDUCTIVE2 =
@@ -150,7 +150,7 @@
     map (Envir.subst_term env #> cterm_of thy) vs ~~ cts) th
   end;
 
-fun prove_strong_ind s avoids ctxt =
+fun prove_strong_ind s rule_name avoids ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val ({names, ...}, {raw_induct, intrs, elims, ...}) =
@@ -461,8 +461,14 @@
             (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
           else (strong_raw_induct RSN (2, rev_mp),
             [ind_case_names, RuleCases.consumes 1]);
+        val (thm_name1, thm_name2) = 
+         (case rule_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') = LocalTheory.note Thm.generatedK
-          ((rec_qualified (Binding.name "strong_induct"),
+          ((thm_name1,
             map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
           ctxt;
         val strong_inducts =
@@ -470,7 +476,7 @@
       in
         ctxt' |>
         LocalTheory.note Thm.generatedK
-          ((rec_qualified (Binding.name "strong_inducts"),
+          ((thm_name2,
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (RuleCases.consumes 1))]),
            strong_inducts) |> snd
@@ -486,9 +492,11 @@
 val _ =
   OuterSyntax.local_theory_to_proof "nominal_inductive2"
     "prove strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
-    (P.xname -- Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
-      (P.$$$ ":" |-- P.and_list1 P.term))) [] >> (fn (name, avoids) =>
-        prove_strong_ind name avoids));
+    (P.xname -- 
+     Scan.option (P.$$$ "[" |-- P.name --| P.$$$ "]") --
+     (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
+      (P.$$$ ":" |-- P.and_list1 P.term))) []) >> (fn ((name, rule_name), avoids) =>
+        prove_strong_ind name rule_name avoids));
 
 end;