local setup of induction tools, with restricted access to auxiliary consts;
authorwenzelm
Mon Apr 06 23:14:05 2015 +0200 (2015-04-06)
changeset 59940087d81f5213e
parent 59939 7d46aa03696e
child 59941 bafba7916d5e
local setup of induction tools, with restricted access to auxiliary consts;
proper antiquotations for formerly inaccessible consts;
src/FOL/FOL.thy
src/HOL/Extraction.thy
src/HOL/HOL.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Tools/inductive.ML
src/Tools/induct.ML
src/Tools/induction.ML
     1.1 --- a/src/FOL/FOL.thy	Mon Apr 06 22:11:01 2015 +0200
     1.2 +++ b/src/FOL/FOL.thy	Mon Apr 06 23:14:05 2015 +0200
     1.3 @@ -384,10 +384,13 @@
     1.4  
     1.5  text {* Proper handling of non-atomic rule statements. *}
     1.6  
     1.7 -definition "induct_forall(P) == \<forall>x. P(x)"
     1.8 -definition "induct_implies(A, B) == A \<longrightarrow> B"
     1.9 -definition "induct_equal(x, y) == x = y"
    1.10 -definition "induct_conj(A, B) == A \<and> B"
    1.11 +context
    1.12 +begin
    1.13 +
    1.14 +restricted definition "induct_forall(P) == \<forall>x. P(x)"
    1.15 +restricted definition "induct_implies(A, B) == A \<longrightarrow> B"
    1.16 +restricted definition "induct_equal(x, y) == x = y"
    1.17 +restricted definition "induct_conj(A, B) == A \<and> B"
    1.18  
    1.19  lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
    1.20    unfolding atomize_all induct_forall_def .
    1.21 @@ -406,9 +409,6 @@
    1.22  lemmas induct_rulify_fallback =
    1.23    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.24  
    1.25 -hide_const induct_forall induct_implies induct_equal induct_conj
    1.26 -
    1.27 -
    1.28  text {* Method setup. *}
    1.29  
    1.30  ML_file "~~/src/Tools/induct.ML"
    1.31 @@ -427,6 +427,8 @@
    1.32  
    1.33  declare case_split [cases type: o]
    1.34  
    1.35 +end
    1.36 +
    1.37  ML_file "~~/src/Tools/case_product.ML"
    1.38  
    1.39  
     2.1 --- a/src/HOL/Extraction.thy	Mon Apr 06 22:11:01 2015 +0200
     2.2 +++ b/src/HOL/Extraction.thy	Mon Apr 06 23:14:05 2015 +0200
     2.3 @@ -34,8 +34,8 @@
     2.4    True_implies_equals TrueE
     2.5  
     2.6  lemmas [extraction_expand_def] =
     2.7 -  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
     2.8 -  induct_true_def induct_false_def
     2.9 +  HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
    2.10 +  HOL.induct_true_def HOL.induct_false_def
    2.11  
    2.12  datatype (plugins only: code extraction) sumbool = Left | Right
    2.13  
     3.1 --- a/src/HOL/HOL.thy	Mon Apr 06 22:11:01 2015 +0200
     3.2 +++ b/src/HOL/HOL.thy	Mon Apr 06 23:14:05 2015 +0200
     3.3 @@ -1374,12 +1374,15 @@
     3.4  );
     3.5  *}
     3.6  
     3.7 -definition "induct_forall P \<equiv> \<forall>x. P x"
     3.8 -definition "induct_implies A B \<equiv> A \<longrightarrow> B"
     3.9 -definition "induct_equal x y \<equiv> x = y"
    3.10 -definition "induct_conj A B \<equiv> A \<and> B"
    3.11 -definition "induct_true \<equiv> True"
    3.12 -definition "induct_false \<equiv> False"
    3.13 +context
    3.14 +begin
    3.15 +
    3.16 +restricted definition "induct_forall P \<equiv> \<forall>x. P x"
    3.17 +restricted definition "induct_implies A B \<equiv> A \<longrightarrow> B"
    3.18 +restricted definition "induct_equal x y \<equiv> x = y"
    3.19 +restricted definition "induct_conj A B \<equiv> A \<and> B"
    3.20 +restricted definition "induct_true \<equiv> True"
    3.21 +restricted definition "induct_false \<equiv> False"
    3.22  
    3.23  lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
    3.24    by (unfold atomize_all induct_forall_def)
    3.25 @@ -1444,8 +1447,8 @@
    3.26  
    3.27  ML_file "~~/src/Tools/induction.ML"
    3.28  
    3.29 -setup {*
    3.30 -  Context.theory_map (Induct.map_simpset (fn ss => ss
    3.31 +declaration {*
    3.32 +  fn _ => Induct.map_simpset (fn ss => ss
    3.33      addsimprocs
    3.34        [Simplifier.simproc_global @{theory} "swap_induct_false"
    3.35           ["induct_false ==> PROP P ==> PROP Q"]
    3.36 @@ -1468,7 +1471,7 @@
    3.37                | _ => NONE))]
    3.38      |> Simplifier.set_mksimps (fn ctxt =>
    3.39          Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
    3.40 -        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
    3.41 +        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
    3.42  *}
    3.43  
    3.44  text {* Pre-simplification of induction and cases rules *}
    3.45 @@ -1523,7 +1526,7 @@
    3.46  lemma [induct_simp]: "x = x \<longleftrightarrow> True"
    3.47    by (rule simp_thms)
    3.48  
    3.49 -hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
    3.50 +end
    3.51  
    3.52  ML_file "~~/src/Tools/induct_tacs.ML"
    3.53  
     4.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Apr 06 22:11:01 2015 +0200
     4.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Apr 06 23:14:05 2015 +0200
     4.3 @@ -247,10 +247,10 @@
     4.4    end
     4.5  
     4.6  val forbidden_mutant_constnames =
     4.7 - ["HOL.induct_equal",
     4.8 -  "HOL.induct_implies",
     4.9 -  "HOL.induct_conj",
    4.10 -  "HOL.induct_forall",
    4.11 +[@{const_name HOL.induct_equal},
    4.12 + @{const_name HOL.induct_implies},
    4.13 + @{const_name HOL.induct_conj},
    4.14 + @{const_name HOL.induct_forall},
    4.15   @{const_name undefined},
    4.16   @{const_name default},
    4.17   @{const_name Pure.dummy_pattern},
     5.1 --- a/src/HOL/Nominal/Nominal.thy	Mon Apr 06 22:11:01 2015 +0200
     5.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon Apr 06 23:14:05 2015 +0200
     5.3 @@ -3563,7 +3563,7 @@
     5.4    (* connectives *)
     5.5    if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt 
     5.6    true_eqvt false_eqvt
     5.7 -  imp_eqvt [folded induct_implies_def]
     5.8 +  imp_eqvt [folded HOL.induct_implies_def]
     5.9    
    5.10    (* datatypes *)
    5.11    perm_unit.simps
     6.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 06 22:11:01 2015 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 06 23:14:05 2015 +0200
     6.3 @@ -28,7 +28,7 @@
     6.4  val finite_emptyI = @{thm "finite.emptyI"};
     6.5  val Collect_const = @{thm "Collect_const"};
     6.6  
     6.7 -val inductive_forall_def = @{thm "induct_forall_def"};
     6.8 +val inductive_forall_def = @{thm HOL.induct_forall_def};
     6.9  
    6.10  
    6.11  (* theory data *)
     7.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 22:11:01 2015 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 23:14:05 2015 +0200
     7.3 @@ -14,7 +14,7 @@
     7.4  structure NominalInductive : NOMINAL_INDUCTIVE =
     7.5  struct
     7.6  
     7.7 -val inductive_forall_def = @{thm induct_forall_def};
     7.8 +val inductive_forall_def = @{thm HOL.induct_forall_def};
     7.9  val inductive_atomize = @{thms induct_atomize};
    7.10  val inductive_rulify = @{thms induct_rulify};
    7.11  
     8.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Mon Apr 06 22:11:01 2015 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Apr 06 23:14:05 2015 +0200
     8.3 @@ -15,7 +15,7 @@
     8.4  structure NominalInductive2 : NOMINAL_INDUCTIVE2 =
     8.5  struct
     8.6  
     8.7 -val inductive_forall_def = @{thm induct_forall_def};
     8.8 +val inductive_forall_def = @{thm HOL.induct_forall_def};
     8.9  val inductive_atomize = @{thms induct_atomize};
    8.10  val inductive_rulify = @{thms induct_rulify};
    8.11  
     9.1 --- a/src/HOL/Tools/inductive.ML	Mon Apr 06 22:11:01 2015 +0200
     9.2 +++ b/src/HOL/Tools/inductive.ML	Mon Apr 06 23:14:05 2015 +0200
     9.3 @@ -97,9 +97,8 @@
     9.4  
     9.5  (** theory context references **)
     9.6  
     9.7 -val inductive_forall_def = @{thm induct_forall_def};
     9.8 -val inductive_conj_name = "HOL.induct_conj";
     9.9 -val inductive_conj_def = @{thm induct_conj_def};
    9.10 +val inductive_forall_def = @{thm HOL.induct_forall_def};
    9.11 +val inductive_conj_def = @{thm HOL.induct_conj_def};
    9.12  val inductive_conj = @{thms induct_conj};
    9.13  val inductive_atomize = @{thms induct_atomize};
    9.14  val inductive_rulify = @{thms induct_rulify};
    9.15 @@ -689,7 +688,7 @@
    9.16                  val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
    9.17                  val Q =
    9.18                    fold_rev Term.abs (mk_names "x" k ~~ Ts)
    9.19 -                    (HOLogic.mk_binop inductive_conj_name
    9.20 +                    (HOLogic.mk_binop @{const_name HOL.induct_conj}
    9.21                        (list_comb (incr_boundvars k s, bs), P));
    9.22                in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
    9.23            | NONE =>
    10.1 --- a/src/Tools/induct.ML	Mon Apr 06 22:11:01 2015 +0200
    10.2 +++ b/src/Tools/induct.ML	Mon Apr 06 23:14:05 2015 +0200
    10.3 @@ -88,7 +88,7 @@
    10.4     (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    10.5      (string * typ) list list -> term option list -> thm list option ->
    10.6      thm list -> int -> cases_tactic) ->
    10.7 -   theory -> theory
    10.8 +   local_theory -> local_theory
    10.9  end;
   10.10  
   10.11  functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
   10.12 @@ -363,14 +363,14 @@
   10.13  in
   10.14  
   10.15  val _ =
   10.16 -  Theory.setup
   10.17 -   (Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
   10.18 +  Theory.local_setup
   10.19 +   (Attrib.local_setup @{binding cases} (attrib cases_type cases_pred cases_del)
   10.20        "declaration of cases rule" #>
   10.21 -    Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
   10.22 +    Attrib.local_setup @{binding induct} (attrib induct_type induct_pred induct_del)
   10.23        "declaration of induction rule" #>
   10.24 -    Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
   10.25 +    Attrib.local_setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
   10.26        "declaration of coinduction rule" #>
   10.27 -    Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
   10.28 +    Attrib.local_setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
   10.29        "declaration of rules for simplifying induction or cases rules");
   10.30  
   10.31  end;
   10.32 @@ -737,10 +737,10 @@
   10.33    SUBGOAL_CASES (fn (_, i, st) =>
   10.34      let
   10.35        val thy = Proof_Context.theory_of ctxt;
   10.36 -  
   10.37 +
   10.38        val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
   10.39        val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
   10.40 -  
   10.41 +
   10.42        fun inst_rule (concls, r) =
   10.43          (if null insts then `Rule_Cases.get r
   10.44           else (align_left "Rule has fewer conclusions than arguments given"
   10.45 @@ -749,7 +749,7 @@
   10.46            |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
   10.47          |> mod_cases thy
   10.48          |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
   10.49 -  
   10.50 +
   10.51        val ruleq =
   10.52          (case opt_rule of
   10.53            SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
   10.54 @@ -759,7 +759,7 @@
   10.55              |> map_filter (Rule_Cases.mutual_rule ctxt)
   10.56              |> tap (trace_rules ctxt inductN o map #2)
   10.57              |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   10.58 -  
   10.59 +
   10.60        fun rule_cases ctxt rule cases =
   10.61          let
   10.62            val rule' = Rule_Cases.internalize_params rule;
   10.63 @@ -910,18 +910,8 @@
   10.64  
   10.65  in
   10.66  
   10.67 -val _ =
   10.68 -  Theory.setup
   10.69 -    (Method.setup @{binding cases}
   10.70 -      (Scan.lift (Args.mode no_simpN) --
   10.71 -        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
   10.72 -        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
   10.73 -          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
   10.74 -            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
   10.75 -      "case analysis on types or predicates/sets");
   10.76 -
   10.77  fun gen_induct_setup binding tac =
   10.78 -  Method.setup binding
   10.79 +  Method.local_setup binding
   10.80      (Scan.lift (Args.mode no_simpN) --
   10.81        (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
   10.82          (arbitrary -- taking -- Scan.option induct_rule)) >>
   10.83 @@ -929,11 +919,17 @@
   10.84          Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
   10.85      "induction on types or predicates/sets";
   10.86  
   10.87 -val _ = Theory.setup (gen_induct_setup @{binding induct} induct_tac);
   10.88 -
   10.89  val _ =
   10.90 -  Theory.setup
   10.91 -    (Method.setup @{binding coinduct}
   10.92 +  Theory.local_setup
   10.93 +    (Method.local_setup @{binding cases}
   10.94 +      (Scan.lift (Args.mode no_simpN) --
   10.95 +        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
   10.96 +        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
   10.97 +          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
   10.98 +            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
   10.99 +      "case analysis on types or predicates/sets" #>
  10.100 +    gen_induct_setup @{binding induct} induct_tac #>
  10.101 +     Method.local_setup @{binding coinduct}
  10.102        (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
  10.103          (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
  10.104            Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
    11.1 --- a/src/Tools/induction.ML	Mon Apr 06 22:11:01 2015 +0200
    11.2 +++ b/src/Tools/induction.ML	Mon Apr 06 23:14:05 2015 +0200
    11.3 @@ -45,6 +45,6 @@
    11.4  
    11.5  val induction_tac = Induct.gen_induct_tac (K name_hyps);
    11.6  
    11.7 -val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac);
    11.8 +val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);
    11.9  
   11.10  end