local setup of induction tools, with restricted access to auxiliary consts;
proper antiquotations for formerly inaccessible consts;

--- a/src/FOL/FOL.thy	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/FOL/FOL.thy	Mon Apr 06 23:14:05 2015 +0200
@@ -384,10 +384,13 @@
 
 text {* Proper handling of non-atomic rule statements. *}
 
-definition "induct_forall(P) == \<forall>x. P(x)"
-definition "induct_implies(A, B) == A \<longrightarrow> B"
-definition "induct_equal(x, y) == x = y"
-definition "induct_conj(A, B) == A \<and> B"
+context
+begin
+
+restricted definition "induct_forall(P) == \<forall>x. P(x)"
+restricted definition "induct_implies(A, B) == A \<longrightarrow> B"
+restricted definition "induct_equal(x, y) == x = y"
+restricted definition "induct_conj(A, B) == A \<and> B"
 
 lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
   unfolding atomize_all induct_forall_def .
@@ -406,9 +409,6 @@
 lemmas induct_rulify_fallback =
   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
 
-hide_const induct_forall induct_implies induct_equal induct_conj
-
-
 text {* Method setup. *}
 
 ML_file "~~/src/Tools/induct.ML"
@@ -427,6 +427,8 @@
 
 declare case_split [cases type: o]
 
+end
+
 ML_file "~~/src/Tools/case_product.ML"
 
 

--- a/src/HOL/Extraction.thy	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/HOL/Extraction.thy	Mon Apr 06 23:14:05 2015 +0200
@@ -34,8 +34,8 @@
   True_implies_equals TrueE
 
 lemmas [extraction_expand_def] =
-  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
-  induct_true_def induct_false_def
+  HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
+  HOL.induct_true_def HOL.induct_false_def
 
 datatype (plugins only: code extraction) sumbool = Left | Right
 

--- a/src/HOL/HOL.thy	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/HOL/HOL.thy	Mon Apr 06 23:14:05 2015 +0200
@@ -1374,12 +1374,15 @@
 );
 *}
 
-definition "induct_forall P \<equiv> \<forall>x. P x"
-definition "induct_implies A B \<equiv> A \<longrightarrow> B"
-definition "induct_equal x y \<equiv> x = y"
-definition "induct_conj A B \<equiv> A \<and> B"
-definition "induct_true \<equiv> True"
-definition "induct_false \<equiv> False"
+context
+begin
+
+restricted definition "induct_forall P \<equiv> \<forall>x. P x"
+restricted definition "induct_implies A B \<equiv> A \<longrightarrow> B"
+restricted definition "induct_equal x y \<equiv> x = y"
+restricted definition "induct_conj A B \<equiv> A \<and> B"
+restricted definition "induct_true \<equiv> True"
+restricted definition "induct_false \<equiv> False"
 
 lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
   by (unfold atomize_all induct_forall_def)
@@ -1444,8 +1447,8 @@
 
 ML_file "~~/src/Tools/induction.ML"
 
-setup {*
-  Context.theory_map (Induct.map_simpset (fn ss => ss
+declaration {*
+  fn _ => Induct.map_simpset (fn ss => ss
     addsimprocs
       [Simplifier.simproc_global @{theory} "swap_induct_false"
          ["induct_false ==> PROP P ==> PROP Q"]
@@ -1468,7 +1471,7 @@
               | _ => NONE))]
     |> Simplifier.set_mksimps (fn ctxt =>
         Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
-        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
+        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
 *}
 
 text {* Pre-simplification of induction and cases rules *}
@@ -1523,7 +1526,7 @@
 lemma [induct_simp]: "x = x \<longleftrightarrow> True"
   by (rule simp_thms)
 
-hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
+end
 
 ML_file "~~/src/Tools/induct_tacs.ML"
 

--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Apr 06 23:14:05 2015 +0200
@@ -247,10 +247,10 @@
   end
 
 val forbidden_mutant_constnames =
- ["HOL.induct_equal",
-  "HOL.induct_implies",
-  "HOL.induct_conj",
-  "HOL.induct_forall",
+[@{const_name HOL.induct_equal},
+ @{const_name HOL.induct_implies},
+ @{const_name HOL.induct_conj},
+ @{const_name HOL.induct_forall},
  @{const_name undefined},
  @{const_name default},
  @{const_name Pure.dummy_pattern},

--- a/src/HOL/Nominal/Nominal.thy	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Apr 06 23:14:05 2015 +0200
@@ -3563,7 +3563,7 @@
   (* connectives *)
   if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt 
   true_eqvt false_eqvt
-  imp_eqvt [folded induct_implies_def]
+  imp_eqvt [folded HOL.induct_implies_def]
   
   (* datatypes *)
   perm_unit.simps

--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 06 23:14:05 2015 +0200
@@ -28,7 +28,7 @@
 val finite_emptyI = @{thm "finite.emptyI"};
 val Collect_const = @{thm "Collect_const"};
 
-val inductive_forall_def = @{thm "induct_forall_def"};
+val inductive_forall_def = @{thm HOL.induct_forall_def};
 
 
 (* theory data *)

--- a/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 23:14:05 2015 +0200
@@ -14,7 +14,7 @@
 structure NominalInductive : NOMINAL_INDUCTIVE =
 struct
 
-val inductive_forall_def = @{thm induct_forall_def};
+val inductive_forall_def = @{thm HOL.induct_forall_def};
 val inductive_atomize = @{thms induct_atomize};
 val inductive_rulify = @{thms induct_rulify};
 

--- a/src/HOL/Nominal/nominal_inductive2.ML	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Apr 06 23:14:05 2015 +0200
@@ -15,7 +15,7 @@
 structure NominalInductive2 : NOMINAL_INDUCTIVE2 =
 struct
 
-val inductive_forall_def = @{thm induct_forall_def};
+val inductive_forall_def = @{thm HOL.induct_forall_def};
 val inductive_atomize = @{thms induct_atomize};
 val inductive_rulify = @{thms induct_rulify};
 

--- a/src/HOL/Tools/inductive.ML	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon Apr 06 23:14:05 2015 +0200
@@ -97,9 +97,8 @@
 
 (** theory context references **)
 
-val inductive_forall_def = @{thm induct_forall_def};
-val inductive_conj_name = "HOL.induct_conj";
-val inductive_conj_def = @{thm induct_conj_def};
+val inductive_forall_def = @{thm HOL.induct_forall_def};
+val inductive_conj_def = @{thm HOL.induct_conj_def};
 val inductive_conj = @{thms induct_conj};
 val inductive_atomize = @{thms induct_atomize};
 val inductive_rulify = @{thms induct_rulify};
@@ -689,7 +688,7 @@
                 val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
                 val Q =
                   fold_rev Term.abs (mk_names "x" k ~~ Ts)
-                    (HOLogic.mk_binop inductive_conj_name
+                    (HOLogic.mk_binop @{const_name HOL.induct_conj}
                       (list_comb (incr_boundvars k s, bs), P));
               in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
           | NONE =>

--- a/src/Tools/induct.ML	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/Tools/induct.ML	Mon Apr 06 23:14:05 2015 +0200
@@ -88,7 +88,7 @@
    (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> cases_tactic) ->
-   theory -> theory
+   local_theory -> local_theory
 end;
 
 functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
@@ -363,14 +363,14 @@
 in
 
 val _ =
-  Theory.setup
-   (Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
+  Theory.local_setup
+   (Attrib.local_setup @{binding cases} (attrib cases_type cases_pred cases_del)
       "declaration of cases rule" #>
-    Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
+    Attrib.local_setup @{binding induct} (attrib induct_type induct_pred induct_del)
       "declaration of induction rule" #>
-    Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
+    Attrib.local_setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
       "declaration of coinduction rule" #>
-    Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
+    Attrib.local_setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
       "declaration of rules for simplifying induction or cases rules");
 
 end;
@@ -737,10 +737,10 @@
   SUBGOAL_CASES (fn (_, i, st) =>
     let
       val thy = Proof_Context.theory_of ctxt;
-  
+
       val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
       val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
-  
+
       fun inst_rule (concls, r) =
         (if null insts then `Rule_Cases.get r
          else (align_left "Rule has fewer conclusions than arguments given"
@@ -749,7 +749,7 @@
           |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
         |> mod_cases thy
         |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
-  
+
       val ruleq =
         (case opt_rule of
           SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
@@ -759,7 +759,7 @@
             |> map_filter (Rule_Cases.mutual_rule ctxt)
             |> tap (trace_rules ctxt inductN o map #2)
             |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
-  
+
       fun rule_cases ctxt rule cases =
         let
           val rule' = Rule_Cases.internalize_params rule;
@@ -910,18 +910,8 @@
 
 in
 
-val _ =
-  Theory.setup
-    (Method.setup @{binding cases}
-      (Scan.lift (Args.mode no_simpN) --
-        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
-        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
-          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
-            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
-      "case analysis on types or predicates/sets");
-
 fun gen_induct_setup binding tac =
-  Method.setup binding
+  Method.local_setup binding
     (Scan.lift (Args.mode no_simpN) --
       (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
         (arbitrary -- taking -- Scan.option induct_rule)) >>
@@ -929,11 +919,17 @@
         Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
     "induction on types or predicates/sets";
 
-val _ = Theory.setup (gen_induct_setup @{binding induct} induct_tac);
-
 val _ =
-  Theory.setup
-    (Method.setup @{binding coinduct}
+  Theory.local_setup
+    (Method.local_setup @{binding cases}
+      (Scan.lift (Args.mode no_simpN) --
+        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
+        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
+          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
+            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
+      "case analysis on types or predicates/sets" #>
+    gen_induct_setup @{binding induct} induct_tac #>
+     Method.local_setup @{binding coinduct}
       (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
         (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
           Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))

--- a/src/Tools/induction.ML	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/Tools/induction.ML	Mon Apr 06 23:14:05 2015 +0200
@@ -45,6 +45,6 @@
 
 val induction_tac = Induct.gen_induct_tac (K name_hyps);
 
-val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac);
+val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);
 
 end