--- a/src/FOL/FOL.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/FOL/FOL.thy Wed Oct 29 19:01:49 2014 +0100
@@ -12,8 +12,6 @@
ML_file "~~/src/Provers/classical.ML"
ML_file "~~/src/Provers/blast.ML"
ML_file "~~/src/Provers/clasimp.ML"
-ML_file "~~/src/Tools/induct.ML"
-ML_file "~~/src/Tools/case_product.ML"
subsection {* The classical axiom *}
@@ -181,8 +179,6 @@
open Basic_Classical;
*}
-setup Cla.setup
-
(*Propositional rules*)
lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
and [elim!] = conjE disjE impCE FalseE iffCE
@@ -209,8 +205,6 @@
val blast_tac = Blast.blast_tac;
*}
-setup Blast.setup
-
lemma ex1_functional: "[| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c"
by blast
@@ -344,14 +338,12 @@
|> simpset_of;
*}
-setup {* map_theory_simpset (put_simpset FOL_ss) *}
-
-setup "Simplifier.method_setup Splitter.split_modifiers"
-setup Splitter.setup
-setup clasimp_setup
+setup {*
+ map_theory_simpset (put_simpset FOL_ss) #>
+ Simplifier.method_setup Splitter.split_modifiers
+*}
ML_file "~~/src/Tools/eqsubst.ML"
-setup EqSubst.setup
subsection {* Other simple lemmas *}
@@ -418,6 +410,7 @@
text {* Method setup. *}
+ML_file "~~/src/Tools/induct.ML"
ML {*
structure Induct = Induct
(
@@ -431,10 +424,9 @@
);
*}
-setup Induct.setup
declare case_split [cases type: o]
-setup Case_Product.setup
+ML_file "~~/src/Tools/case_product.ML"
hide_const (open) eq
--- a/src/FOL/IFOL.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/FOL/IFOL.thy Wed Oct 29 19:01:49 2014 +0100
@@ -591,7 +591,6 @@
open Hypsubst;
*}
-setup hypsubst_setup
ML_file "intprover.ML"
--- a/src/HOL/BNF_Greatest_Fixpoint.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy Wed Oct 29 19:01:49 2014 +0100
@@ -17,9 +17,7 @@
"primcorec" :: thy_decl
begin
-setup {*
-Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
-*}
+setup {* Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj} *}
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by simp
--- a/src/HOL/Fields.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Fields.thy Wed Oct 29 19:01:49 2014 +0100
@@ -23,8 +23,7 @@
fixes inverse :: "'a \<Rightarrow> 'a"
and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
-setup {* Sign.add_const_constraint
- (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
context semiring
@@ -47,8 +46,7 @@
end
-setup {* Sign.add_const_constraint
- (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
--- a/src/HOL/Fun_Def.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Fun_Def.thy Wed Oct 29 19:01:49 2014 +0100
@@ -106,11 +106,6 @@
Scan.succeed (NO_CASES oo Induction_Schema.induction_schema_tac)
*} "prove an induction principle"
-setup {*
- Function.setup
- #> Function_Fun.setup
-*}
-
subsection {* Measure functions *}
--- a/src/HOL/HOL.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/HOL.thy Wed Oct 29 19:01:49 2014 +0100
@@ -27,18 +27,12 @@
ML_file "~~/src/Tools/eqsubst.ML"
ML_file "~~/src/Provers/quantifier1.ML"
ML_file "~~/src/Tools/atomize_elim.ML"
-ML_file "~~/src/Tools/induct.ML"
ML_file "~~/src/Tools/cong_tac.ML"
-ML_file "~~/src/Tools/intuitionistic.ML"
+ML_file "~~/src/Tools/intuitionistic.ML" setup \<open>Intuitionistic.method_setup @{binding iprover}\<close>
ML_file "~~/src/Tools/project_rule.ML"
ML_file "~~/src/Tools/subtyping.ML"
ML_file "~~/src/Tools/case_product.ML"
-setup {*
- Intuitionistic.method_setup @{binding iprover}
- #> Subtyping.setup
- #> Case_Product.setup
-*}
ML \<open>Plugin_Name.declare_setup @{binding extraction}\<close>
@@ -231,7 +225,7 @@
lemma trans_sym [Pure.elim?]: "r = s ==> t = s ==> r = t"
by (rule trans [OF _ sym])
-lemma meta_eq_to_obj_eq:
+lemma meta_eq_to_obj_eq:
assumes meq: "A == B"
shows "A = B"
by (unfold meq) (rule refl)
@@ -847,26 +841,23 @@
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
);
-structure Basic_Classical: BASIC_CLASSICAL = Classical;
+structure Basic_Classical: BASIC_CLASSICAL = Classical;
open Basic_Classical;
*}
-setup Classical.setup
-
setup {*
-let
- fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
- | non_bool_eq _ = false;
- fun hyp_subst_tac' ctxt =
- SUBGOAL (fn (goal, i) =>
- if Term.exists_Const non_bool_eq goal
- then Hypsubst.hyp_subst_tac ctxt i
- else no_tac);
-in
- Hypsubst.hypsubst_setup
(*prevent substitution on bool*)
- #> Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
-end
+ let
+ fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
+ | non_bool_eq _ = false;
+ fun hyp_subst_tac' ctxt =
+ SUBGOAL (fn (goal, i) =>
+ if Term.exists_Const non_bool_eq goal
+ then Hypsubst.hyp_subst_tac ctxt i
+ else no_tac);
+ in
+ Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
+ end
*}
declare iffI [intro!]
@@ -932,8 +923,6 @@
val blast_tac = Blast.blast_tac;
*}
-setup Blast.setup
-
subsubsection {* Simplifier *}
@@ -1197,18 +1186,14 @@
ML_file "Tools/simpdata.ML"
ML {* open Simpdata *}
-setup {* map_theory_simpset (put_simpset HOL_basic_ss) *}
+setup {*
+ map_theory_simpset (put_simpset HOL_basic_ss) #>
+ Simplifier.method_setup Splitter.split_modifiers
+*}
simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
-setup {*
- Simplifier.method_setup Splitter.split_modifiers
- #> Splitter.setup
- #> clasimp_setup
- #> EqSubst.setup
-*}
-
text {* Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}: *}
simproc_setup neq ("x = y") = {* fn _ =>
@@ -1467,6 +1452,7 @@
text {* Method setup. *}
+ML_file "~~/src/Tools/induct.ML"
ML {*
structure Induct = Induct
(
@@ -1484,7 +1470,6 @@
ML_file "~~/src/Tools/induction.ML"
setup {*
- Induct.setup #> Induction.setup #>
Context.theory_map (Induct.map_simpset (fn ss => ss
addsimprocs
[Simplifier.simproc_global @{theory} "swap_induct_false"
@@ -1558,13 +1543,12 @@
lemma [induct_simp]: "induct_implies induct_true P == P"
by (simp add: induct_implies_def induct_true_def)
-lemma [induct_simp]: "(x = x) = True"
+lemma [induct_simp]: "(x = x) = True"
by (rule simp_thms)
hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
ML_file "~~/src/Tools/induct_tacs.ML"
-setup Induct_Tacs.setup
subsubsection {* Coherent logic *}
@@ -1640,8 +1624,8 @@
lemmas eq_sym_conv = eq_commute
lemma nnf_simps:
- "(\<not>(P \<and> Q)) = (\<not> P \<or> \<not> Q)" "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
- "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
+ "(\<not>(P \<and> Q)) = (\<not> P \<or> \<not> Q)" "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
+ "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
"(\<not> \<not>(P)) = P"
by blast+
@@ -1737,10 +1721,11 @@
by (fact arg_cong)
setup {*
- Code_Preproc.map_pre (put_simpset HOL_basic_ss)
- #> Code_Preproc.map_post (put_simpset HOL_basic_ss)
- #> Code_Simp.map_ss (put_simpset HOL_basic_ss
- #> Simplifier.add_cong @{thm conj_left_cong} #> Simplifier.add_cong @{thm disj_left_cong})
+ Code_Preproc.map_pre (put_simpset HOL_basic_ss) #>
+ Code_Preproc.map_post (put_simpset HOL_basic_ss) #>
+ Code_Simp.map_ss (put_simpset HOL_basic_ss #>
+ Simplifier.add_cong @{thm conj_left_cong} #>
+ Simplifier.add_cong @{thm disj_left_cong})
*}
@@ -1799,7 +1784,7 @@
text {* More about @{typ prop} *}
lemma [code nbe]:
- shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
+ shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
@@ -1828,9 +1813,7 @@
"equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
by (simp add: equal)
-setup {*
- Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
-*}
+setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"}) *}
lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
proof
@@ -1843,14 +1826,10 @@
show "PROP ?ofclass" proof
qed (simp add: `PROP ?equal`)
qed
-
-setup {*
- Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})
-*}
-setup {*
- Nbe.add_const_alias @{thm equal_alias_cert}
-*}
+setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"}) *}
+
+setup {* Nbe.add_const_alias @{thm equal_alias_cert} *}
text {* Cases *}
@@ -1860,8 +1839,8 @@
using assms by simp_all
setup {*
- Code.add_case @{thm Let_case_cert}
- #> Code.add_undefined @{const_name undefined}
+ Code.add_case @{thm Let_case_cert} #>
+ Code.add_undefined @{const_name undefined}
*}
declare [[code abort: undefined]]
@@ -1877,7 +1856,7 @@
| constant True \<rightharpoonup>
(SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true"
| constant False \<rightharpoonup>
- (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false"
+ (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false"
code_reserved SML
bool true false
@@ -1936,13 +1915,13 @@
subsubsection {* Evaluation and normalization by evaluation *}
method_setup eval = {*
-let
- fun eval_tac ctxt =
- let val conv = Code_Runtime.dynamic_holds_conv ctxt
- in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
-in
- Scan.succeed (SIMPLE_METHOD' o eval_tac)
-end
+ let
+ fun eval_tac ctxt =
+ let val conv = Code_Runtime.dynamic_holds_conv ctxt
+ in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
+ in
+ Scan.succeed (SIMPLE_METHOD' o eval_tac)
+ end
*} "solve goal by evaluation"
method_setup normalization = {*
@@ -1989,23 +1968,23 @@
subsection {* Legacy tactics and ML bindings *}
ML {*
-(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
-local
- fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
- | wrong_prem (Bound _) = true
- | wrong_prem _ = false;
- val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
-in
- fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
- fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
-end;
+ (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
+ local
+ fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
+ | wrong_prem (Bound _) = true
+ | wrong_prem _ = false;
+ val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
+ in
+ fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
+ fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
+ end;
-local
- val nnf_ss =
- simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
-in
- fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
-end
+ local
+ val nnf_ss =
+ simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
+ in
+ fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
+ end
*}
hide_const (open) eq equal
--- a/src/HOL/Orderings.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Orderings.thy Wed Oct 29 19:01:49 2014 +0100
@@ -400,6 +400,8 @@
sig
val print_structures: Proof.context -> unit
val order_tac: Proof.context -> thm list -> int -> tactic
+ val add_struct: string * term list -> string -> attribute
+ val del_struct: string * term list -> attribute
end;
structure Orders: ORDERS =
@@ -483,26 +485,24 @@
(* attributes *)
-fun add_struct_thm s tag =
+fun add_struct s tag =
Thm.declaration_attribute
(fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm)));
fun del_struct s =
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
-val _ =
- Theory.setup
- (Attrib.setup @{binding order}
- (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
- Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
- | ((NONE, n), ts) => del_struct (n, ts)))
- "theorems controlling transitivity reasoner");
-
end;
*}
+attribute_setup order = {*
+ Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
+ Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
+ Scan.repeat Args.term
+ >> (fn ((SOME tag, n), ts) => Orders.add_struct (n, ts) tag
+ | ((NONE, n), ts) => Orders.del_struct (n, ts))
+*} "theorems controlling transitivity reasoner"
+
method_setup order = {*
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
*} "transitivity reasoner"
--- a/src/HOL/Product_Type.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Product_Type.thy Wed Oct 29 19:01:49 2014 +0100
@@ -50,9 +50,7 @@
shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
using assms by simp_all
-setup {*
- Code.add_case @{thm If_case_cert}
-*}
+setup {* Code.add_case @{thm If_case_cert} *}
code_printing
constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
--- a/src/HOL/Quickcheck_Exhaustive.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Wed Oct 29 19:01:49 2014 +0100
@@ -618,8 +618,6 @@
ML_file "Tools/Quickcheck/exhaustive_generators.ML"
-setup Exhaustive_Generators.setup
-
declare [[quickcheck_batch_tester = exhaustive]]
subsection {* Defining generators for abstract types *}
--- a/src/HOL/Quickcheck_Narrowing.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Wed Oct 29 19:01:49 2014 +0100
@@ -197,8 +197,6 @@
ML_file "Tools/Quickcheck/narrowing_generators.ML"
-setup Narrowing_Generators.setup
-
definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
where
"narrowing_dummy_partial_term_of = partial_term_of"
--- a/src/HOL/Quickcheck_Random.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Quickcheck_Random.thy Wed Oct 29 19:01:49 2014 +0100
@@ -207,7 +207,6 @@
ML_file "Tools/Quickcheck/quickcheck_common.ML"
ML_file "Tools/Quickcheck/random_generators.ML"
-setup Random_Generators.setup
subsection {* Code setup *}
--- a/src/HOL/Semiring_Normalization.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Semiring_Normalization.thy Wed Oct 29 19:01:49 2014 +0100
@@ -8,8 +8,6 @@
imports Numeral_Simprocs Nat_Transfer
begin
-ML_file "Tools/semiring_normalizer.ML"
-
text {* Prelude *}
class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel +
@@ -69,7 +67,7 @@
text {* Semiring normalization proper *}
-setup Semiring_Normalizer.setup
+ML_file "Tools/semiring_normalizer.ML"
context comm_semiring_1
begin
--- a/src/HOL/Tools/Function/fun.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Function/fun.ML Wed Oct 29 19:01:49 2014 +0100
@@ -14,8 +14,6 @@
val add_fun_cmd : (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> Function_Common.function_config ->
bool -> local_theory -> Proof.context
-
- val setup : theory -> theory
end
structure Function_Fun : FUNCTION_FUN =
@@ -148,8 +146,8 @@
else
Function_Common.empty_preproc check_defs config ctxt fixes spec
-val setup =
- Context.theory_map (Function_Common.set_preproc sequential_preproc)
+val _ = Theory.setup (Context.theory_map (Function_Common.set_preproc sequential_preproc))
+
val fun_config = FunctionConfig { sequential=true, default=NONE,
--- a/src/HOL/Tools/Function/function.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML Wed Oct 29 19:01:49 2014 +0100
@@ -32,7 +32,6 @@
val termination : term option -> local_theory -> Proof.state
val termination_cmd : string option -> local_theory -> Proof.state
- val setup : theory -> theory
val get_congs : Proof.context -> thm list
val get_info : Proof.context -> term -> info
@@ -264,7 +263,6 @@
(* Datatype hook to declare datatype congs as "function_congs" *)
-
fun add_case_cong n thy =
let
val cong = #case_cong (Old_Datatype_Data.the_info thy n)
@@ -274,12 +272,10 @@
(Function_Context_Tree.map_function_congs (Thm.add_thm cong)) thy
end
-val setup_case_cong = Old_Datatype_Data.interpretation (K (fold add_case_cong))
+val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_case_cong)))
-(* setup *)
-
-val setup = setup_case_cong
+(* get info *)
val get_congs = Function_Context_Tree.get_function_congs
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Oct 29 19:01:49 2014 +0100
@@ -21,7 +21,6 @@
val quickcheck_pretty : bool Config.T
val setup_exhaustive_datatype_interpretation : theory -> theory
val setup_bounded_forall_datatype_interpretation : theory -> theory
- val setup: theory -> theory
val instantiate_full_exhaustive_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
(string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
@@ -547,11 +546,12 @@
val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
-val setup =
- Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive}
- (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
- #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
- #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
- #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));
+val _ =
+ Theory.setup
+ (Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive}
+ (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
+ #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
+ #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
+ #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)));
end;
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Oct 29 19:01:49 2014 +0100
@@ -16,7 +16,6 @@
| Empty_Assignment
val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context
val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context
- val setup: theory -> theory
end;
structure Narrowing_Generators : NARROWING_GENERATORS =
@@ -522,11 +521,12 @@
val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
-val setup =
- Code.datatype_interpretation ensure_partial_term_of
- #> Code.datatype_interpretation ensure_partial_term_of_code
- #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
- (@{sort narrowing}, instantiate_narrowing_datatype)
- #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
+val _ =
+ Theory.setup
+ (Code.datatype_interpretation ensure_partial_term_of
+ #> Code.datatype_interpretation ensure_partial_term_of_code
+ #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
+ (@{sort narrowing}, instantiate_narrowing_datatype)
+ #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals))));
end;
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Wed Oct 29 19:01:49 2014 +0100
@@ -18,7 +18,6 @@
-> Proof.context -> Proof.context
val instantiate_random_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
(string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
- val setup: theory -> theory
end;
structure Random_Generators : RANDOM_GENERATORS =
@@ -469,9 +468,10 @@
val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
-val setup =
- Quickcheck_Common.datatype_interpretation @{plugin quickcheck_random}
- (@{sort random}, instantiate_random_datatype)
- #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
+val _ =
+ Theory.setup
+ (Quickcheck_Common.datatype_interpretation @{plugin quickcheck_random}
+ (@{sort random}, instantiate_random_datatype) #>
+ Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals))));
end;
--- a/src/HOL/Tools/semiring_normalizer.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML Wed Oct 29 19:01:49 2014 +0100
@@ -41,8 +41,6 @@
main: Proof.context -> conv,
pow: Proof.context -> conv,
sub: Proof.context -> conv}
-
- val setup: theory -> theory
end
structure Semiring_Normalizer: SEMIRING_NORMALIZER =
@@ -912,20 +910,21 @@
in
-val setup =
- Attrib.setup @{binding normalizer}
- (Scan.lift (Args.$$$ delN >> K del) ||
- ((keyword2 semiringN opsN |-- terms) --
- (keyword2 semiringN rulesN |-- thms)) --
- (optional (keyword2 ringN opsN |-- terms) --
- optional (keyword2 ringN rulesN |-- thms)) --
- (optional (keyword2 fieldN opsN |-- terms) --
- optional (keyword2 fieldN rulesN |-- thms)) --
- optional (keyword2 idomN rulesN |-- thms) --
- optional (keyword2 idealN rulesN |-- thms)
- >> (fn ((((sr, r), f), id), idl) =>
- add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
- "semiring normalizer data";
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding normalizer}
+ (Scan.lift (Args.$$$ delN >> K del) ||
+ ((keyword2 semiringN opsN |-- terms) --
+ (keyword2 semiringN rulesN |-- thms)) --
+ (optional (keyword2 ringN opsN |-- terms) --
+ optional (keyword2 ringN rulesN |-- thms)) --
+ (optional (keyword2 fieldN opsN |-- terms) --
+ optional (keyword2 fieldN rulesN |-- thms)) --
+ optional (keyword2 idomN rulesN |-- thms) --
+ optional (keyword2 idealN rulesN |-- thms)
+ >> (fn ((((sr, r), f), id), idl) =>
+ add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
+ "semiring normalizer data");
end;
--- a/src/Provers/blast.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Provers/blast.ML Wed Oct 29 19:01:49 2014 +0100
@@ -62,7 +62,6 @@
val trace: bool Config.T
val stats: bool Config.T
val blast_tac: Proof.context -> int -> tactic
- val setup: theory -> theory
(*debugging tools*)
type branch
val tryIt: Proof.context -> int -> string ->
@@ -77,7 +76,7 @@
(* options *)
-val (depth_limit, setup_depth_limit) = Attrib.config_int @{binding blast_depth_limit} (K 20);
+val depth_limit = Attrib.setup_config_int @{binding blast_depth_limit} (K 20);
val (trace, _) = Attrib.config_bool @{binding blast_trace} (K false);
val (stats, _) = Attrib.config_bool @{binding blast_stats} (K false);
@@ -1294,14 +1293,15 @@
in {fullTrace = !fullTrace, result = res} end;
+
(** method setup **)
-val setup =
- setup_depth_limit #>
- Method.setup @{binding blast}
- (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
- (fn NONE => SIMPLE_METHOD' o blast_tac
- | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
- "classical tableau prover";
+val _ =
+ Theory.setup
+ (Method.setup @{binding blast}
+ (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
+ (fn NONE => SIMPLE_METHOD' o blast_tac
+ | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
+ "classical tableau prover");
end;
--- a/src/Provers/clasimp.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Provers/clasimp.ML Wed Oct 29 19:01:49 2014 +0100
@@ -31,7 +31,6 @@
val iff_del: attribute
val iff_modifiers: Method.modifier parser list
val clasimp_modifiers: Method.modifier parser list
- val clasimp_setup: theory -> theory
end;
functor Clasimp(Data: CLASIMP_DATA): CLASIMP =
@@ -180,10 +179,14 @@
(* attributes *)
-fun iff_att x = (Scan.lift
- (Args.del >> K iff_del ||
- Scan.option Args.add -- Args.query >> K iff_add' ||
- Scan.option Args.add >> K iff_add)) x;
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding iff}
+ (Scan.lift
+ (Args.del >> K iff_del ||
+ Scan.option Args.add -- Args.query >> K iff_add' ||
+ Scan.option Args.add >> K iff_add))
+ "declaration of Simplifier / Classical rules");
(* method modifiers *)
@@ -211,17 +214,14 @@
(fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
| SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
-
-(* theory setup *)
-
-val clasimp_setup =
- Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
- Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
- Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
- Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
- Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
- Method.setup @{binding auto} auto_method "auto" #>
- Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
- "clarify simplified goal";
+val _ =
+ Theory.setup
+ (Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
+ Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
+ Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
+ Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
+ Method.setup @{binding auto} auto_method "auto" #>
+ Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
+ "clarify simplified goal");
end;
--- a/src/Provers/classical.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Provers/classical.ML Wed Oct 29 19:01:49 2014 +0100
@@ -124,7 +124,6 @@
(Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser
val cla_method':
(Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
- val setup: theory -> theory
end;
@@ -882,17 +881,18 @@
val elimN = "elim";
val destN = "dest";
-val setup_attrs =
- Attrib.setup @{binding swapped} (Scan.succeed swapped)
- "classical swap of introduction rule" #>
- Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
- "declaration of Classical destruction rule" #>
- Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
- "declaration of Classical elimination rule" #>
- Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
- "declaration of Classical introduction rule" #>
- Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
- "remove declaration of intro/elim/dest rule";
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding swapped} (Scan.succeed swapped)
+ "classical swap of introduction rule" #>
+ Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
+ "declaration of Classical destruction rule" #>
+ Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
+ "declaration of Classical elimination rule" #>
+ Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
+ "declaration of Classical introduction rule" #>
+ Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
+ "remove declaration of intro/elim/dest rule");
@@ -941,46 +941,40 @@
-(** setup_methods **)
+(** method setup **)
-val setup_methods =
- Method.setup @{binding default}
- (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
- "apply some intro/elim rule (potentially classical)" #>
- Method.setup @{binding rule}
- (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
- "apply some intro/elim rule (potentially classical)" #>
- Method.setup @{binding contradiction}
- (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
- "proof by contradiction" #>
- Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
- "repeatedly apply safe steps" #>
- Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
- Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
- Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
- Method.setup @{binding deepen}
- (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
- >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
- "classical prover (iterative deepening)" #>
- Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
- "classical prover (apply safe rules)" #>
- Method.setup @{binding safe_step} (cla_method' safe_step_tac)
- "single classical step (safe rules)" #>
- Method.setup @{binding inst_step} (cla_method' inst_step_tac)
- "single classical step (safe rules, allow instantiations)" #>
- Method.setup @{binding step} (cla_method' step_tac)
- "single classical step (safe and unsafe rules)" #>
- Method.setup @{binding slow_step} (cla_method' slow_step_tac)
- "single classical step (safe and unsafe rules, allow backtracking)" #>
- Method.setup @{binding clarify_step} (cla_method' clarify_step_tac)
- "single classical step (safe rules, without splitting)";
-
-
-
-(** theory setup **)
-
-val setup = setup_attrs #> setup_methods;
-
+val _ =
+ Theory.setup
+ (Method.setup @{binding default}
+ (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
+ "apply some intro/elim rule (potentially classical)" #>
+ Method.setup @{binding rule}
+ (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
+ "apply some intro/elim rule (potentially classical)" #>
+ Method.setup @{binding contradiction}
+ (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
+ "proof by contradiction" #>
+ Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
+ "repeatedly apply safe steps" #>
+ Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
+ Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
+ Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
+ Method.setup @{binding deepen}
+ (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
+ >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
+ "classical prover (iterative deepening)" #>
+ Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
+ "classical prover (apply safe rules)" #>
+ Method.setup @{binding safe_step} (cla_method' safe_step_tac)
+ "single classical step (safe rules)" #>
+ Method.setup @{binding inst_step} (cla_method' inst_step_tac)
+ "single classical step (safe rules, allow instantiations)" #>
+ Method.setup @{binding step} (cla_method' step_tac)
+ "single classical step (safe and unsafe rules)" #>
+ Method.setup @{binding slow_step} (cla_method' slow_step_tac)
+ "single classical step (safe and unsafe rules, allow backtracking)" #>
+ Method.setup @{binding clarify_step} (cla_method' clarify_step_tac)
+ "single classical step (safe rules, without splitting)");
(** outer syntax **)
--- a/src/Provers/hypsubst.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Provers/hypsubst.ML Wed Oct 29 19:01:49 2014 +0100
@@ -52,7 +52,6 @@
val hyp_subst_tac : Proof.context -> int -> tactic
val blast_hyp_subst_tac : bool -> int -> tactic
val stac : thm -> int -> tactic
- val hypsubst_setup : theory -> theory
end;
functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
@@ -120,7 +119,7 @@
handle TERM _ => eq_var_aux (k+1) B (A :: hs)
| Match => eq_var_aux (k+1) B (A :: hs))
| eq_var_aux k _ _ = raise EQ_VAR
-
+
in eq_var_aux 0 t [] end;
val thin_free_eq_tac = SUBGOAL (fn (t, i) => let
@@ -228,11 +227,10 @@
gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
if thin then thin_free_eq_tac else K no_tac];
-val (hyp_subst_thin, hyp_subst_thin_setup) = Attrib.config_bool
- @{binding hypsubst_thin} (K false);
+val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false);
-fun hyp_subst_tac ctxt = hyp_subst_tac_thin
- (Config.get ctxt hyp_subst_thin) ctxt
+fun hyp_subst_tac ctxt =
+ hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt;
(*Substitutes for Bound variables only -- this is always safe*)
fun bound_hyp_subst_tac ctxt =
@@ -296,18 +294,18 @@
in CHANGED_GOAL (rtac (th' RS ssubst)) end;
-(* theory setup *)
+(* method setup *)
-val hypsubst_setup =
- Method.setup @{binding hypsubst}
- (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
- "substitution using an assumption (improper)" #>
- Method.setup @{binding hypsubst_thin}
- (Scan.succeed (fn ctxt => SIMPLE_METHOD'
- (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
- "substitution using an assumption, eliminating assumptions" #>
- hyp_subst_thin_setup #>
- Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
- "simple substitution";
+val _ =
+ Theory.setup
+ (Method.setup @{binding hypsubst}
+ (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
+ "substitution using an assumption (improper)" #>
+ Method.setup @{binding hypsubst_thin}
+ (Scan.succeed (fn ctxt => SIMPLE_METHOD'
+ (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
+ "substitution using an assumption, eliminating assumptions" #>
+ Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
+ "simple substitution");
end;
--- a/src/Provers/splitter.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Provers/splitter.ML Wed Oct 29 19:01:49 2014 +0100
@@ -37,7 +37,6 @@
val split_add: attribute
val split_del: attribute
val split_modifiers : Method.modifier parser list
- val setup: theory -> theory
end;
functor Splitter(Data: SPLITTER_DATA): SPLITTER =
@@ -453,6 +452,11 @@
val split_add = Simplifier.attrib add_split;
val split_del = Simplifier.attrib del_split;
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding split}
+ (Attrib.add_del split_add split_del) "declare case split rule");
+
(* methods *)
@@ -461,14 +465,10 @@
Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier split_add @{here}),
Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del @{here})];
-
-(* theory setup *)
-
-val setup =
- Attrib.setup @{binding split}
- (Attrib.add_del split_add split_del) "declare case split rule" #>
- Method.setup @{binding split}
- (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
- "apply case split rule";
+val _ =
+ Theory.setup
+ (Method.setup @{binding split}
+ (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
+ "apply case split rule");
end;
--- a/src/Tools/case_product.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/case_product.ML Wed Oct 29 19:01:49 2014 +0100
@@ -12,7 +12,7 @@
sig
val combine: Proof.context -> thm -> thm -> thm
val combine_annotated: Proof.context -> thm -> thm -> thm
- val setup: theory -> theory
+ val annotation: thm -> thm -> attribute
end
structure Case_Product: CASE_PRODUCT =
@@ -104,15 +104,15 @@
(* attribute setup *)
-val case_prod_attr =
- let
- fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
- in
- Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
- combine_list (Context.proof_of ctxt) thms thm))
- end
-
-val setup =
- Attrib.setup @{binding case_product} case_prod_attr "product with other case rules"
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding case_product}
+ let
+ fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
+ in
+ Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
+ combine_list (Context.proof_of ctxt) thms thm))
+ end
+ "product with other case rules")
end
--- a/src/Tools/eqsubst.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/eqsubst.ML Wed Oct 29 19:01:49 2014 +0100
@@ -45,8 +45,6 @@
val searchf_lr_unify_all: searchinfo -> term -> match Seq.seq Seq.seq
val searchf_lr_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
val searchf_bt_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
-
- val setup : theory -> theory
end;
structure EqSubst: EQSUBST =
@@ -418,12 +416,12 @@
(* combination method that takes a flag (true indicates that subst
should be done to an assumption, false = apply to the conclusion of
the goal) as well as the theorems to use *)
-val setup =
- Method.setup @{binding subst}
- (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
- Attrib.thms >>
- (fn ((asm, occs), inthms) => fn ctxt =>
- SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
- "single-step substitution";
+val _ =
+ Theory.setup
+ (Method.setup @{binding subst}
+ (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
+ Attrib.thms >> (fn ((asm, occs), inthms) => fn ctxt =>
+ SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
+ "single-step substitution");
end;
--- a/src/Tools/induct.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/induct.ML Wed Oct 29 19:01:49 2014 +0100
@@ -89,7 +89,6 @@
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic) ->
theory -> theory
- val setup: theory -> theory
end;
functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
@@ -368,15 +367,16 @@
in
-val attrib_setup =
- Attrib.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)
- "declaration of induction rule" #>
- Attrib.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)
- "declaration of rules for simplifying induction or cases rules";
+val _ =
+ Theory.setup
+ (Attrib.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)
+ "declaration of induction rule" #>
+ Attrib.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)
+ "declaration of rules for simplifying induction or cases rules");
end;
@@ -923,14 +923,15 @@
in
-val cases_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";
+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
@@ -941,21 +942,16 @@
Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
"induction on types or predicates/sets";
-val induct_setup = gen_induct_setup @{binding induct} induct_tac;
+val _ = Theory.setup (gen_induct_setup @{binding induct} induct_tac);
-val coinduct_setup =
- Method.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))))
- "coinduction on types or predicates/sets";
+val _ =
+ Theory.setup
+ (Method.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))))
+ "coinduction on types or predicates/sets");
end;
-
-
-(** theory setup **)
-
-val setup = attrib_setup #> cases_setup #> induct_setup #> coinduct_setup;
-
end;
--- a/src/Tools/induct_tacs.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/induct_tacs.ML Wed Oct 29 19:01:49 2014 +0100
@@ -10,7 +10,6 @@
val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
val induct_tac: Proof.context -> string option list list -> int -> tactic
val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
- val setup: theory -> theory
end
structure Induct_Tacs: INDUCT_TACS =
@@ -128,15 +127,16 @@
in
-val setup =
- Method.setup @{binding case_tac}
- (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
- (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
- "unstructured case analysis on types" #>
- Method.setup @{binding induct_tac}
- (Args.goal_spec -- varss -- opt_rules >>
- (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
- "unstructured induction on types";
+val _ =
+ Theory.setup
+ (Method.setup @{binding case_tac}
+ (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
+ (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
+ "unstructured case analysis on types" #>
+ Method.setup @{binding induct_tac}
+ (Args.goal_spec -- varss -- opt_rules >>
+ (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
+ "unstructured induction on types");
end;
--- a/src/Tools/induction.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/induction.ML Wed Oct 29 19:01:49 2014 +0100
@@ -3,7 +3,6 @@
val induction_tac: 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
- val setup: theory -> theory
end
structure Induction: INDUCTION =
@@ -37,7 +36,7 @@
val induction_tac = Induct.gen_induct_tac (K name_hyps)
-val setup = Induct.gen_induct_setup @{binding induction} induction_tac
+val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
end
--- a/src/Tools/subtyping.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/subtyping.ML Wed Oct 29 19:01:49 2014 +0100
@@ -10,7 +10,6 @@
val add_type_map: term -> Context.generic -> Context.generic
val add_coercion: term -> Context.generic -> Context.generic
val print_coercions: Proof.context -> unit
- val setup: theory -> theory
end;
structure Subtyping: SUBTYPING =
@@ -884,9 +883,11 @@
val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false);
-val add_term_check =
- Syntax_Phases.term_check ~100 "coercions"
- (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt);
+val _ =
+ Theory.setup
+ (Context.theory_map
+ (Syntax_Phases.term_check ~100 "coercions"
+ (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt)));
(* declarations *)
@@ -1088,26 +1089,26 @@
end |> Pretty.writeln_chunks;
-(* theory setup *)
+(* attribute setup *)
val parse_coerce_args =
Args.$$$ "+" >> K PERMIT || Args.$$$ "-" >> K FORBID || Args.$$$ "0" >> K LEAVE
-val setup =
- Context.theory_map add_term_check #>
- Attrib.setup @{binding coercion}
- (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))
- "declaration of new coercions" #>
- Attrib.setup @{binding coercion_delete}
- (Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t))))
- "deletion of coercions" #>
- Attrib.setup @{binding coercion_map}
- (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
- "declaration of new map functions" #>
- Attrib.setup @{binding coercion_args}
- (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
- (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
- "declaration of new constants with coercion-invariant arguments";
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding coercion}
+ (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))
+ "declaration of new coercions" #>
+ Attrib.setup @{binding coercion_delete}
+ (Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t))))
+ "deletion of coercions" #>
+ Attrib.setup @{binding coercion_map}
+ (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
+ "declaration of new map functions" #>
+ Attrib.setup @{binding coercion_args}
+ (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
+ (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
+ "declaration of new constants with coercion-invariant arguments");
(* outer syntax commands *)