--- a/src/HOL/Algebra/Ring.thy Mon Apr 23 18:42:05 2012 +0200
+++ b/src/HOL/Algebra/Ring.thy Mon Apr 23 21:44:36 2012 +0200
@@ -391,7 +391,11 @@
use "ringsimp.ML"
-setup Algebra.setup
+setup Algebra.attrib_setup
+
+method_setup algebra = {*
+ Scan.succeed (SIMPLE_METHOD' o Algebra.algebra_tac)
+*} "normalisation of algebraic structure"
lemmas (in ring) ring_simprules
[algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
--- a/src/HOL/Algebra/ringsimp.ML Mon Apr 23 18:42:05 2012 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Mon Apr 23 21:44:36 2012 +0200
@@ -6,7 +6,8 @@
signature ALGEBRA =
sig
val print_structures: Proof.context -> unit
- val setup: theory -> theory
+ val attrib_setup: theory -> theory
+ val algebra_tac: Proof.context -> int -> tactic
end;
structure Algebra: ALGEBRA =
@@ -58,6 +59,7 @@
fun add_struct_thm s =
Thm.declaration_attribute
(fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
+
fun del_struct s =
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
@@ -69,13 +71,4 @@
>> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)))
"theorems controlling algebra method";
-
-
-(** Setup **)
-
-val setup =
- Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
- "normalisation of algebraic structure" #>
- attrib_setup;
-
end;
--- a/src/HOL/FunDef.thy Mon Apr 23 18:42:05 2012 +0200
+++ b/src/HOL/FunDef.thy Mon Apr 23 21:44:36 2012 +0200
@@ -108,6 +108,11 @@
use "Tools/Function/mutual.ML"
use "Tools/Function/pattern_split.ML"
use "Tools/Function/relation.ML"
+
+method_setup relation = {*
+ Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
+*} "prove termination using a user-specified wellfounded relation"
+
use "Tools/Function/function.ML"
use "Tools/Function/pat_completeness.ML"
@@ -122,7 +127,7 @@
Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
*} "prove an induction principle"
-setup {*
+setup {*
Function.setup
#> Function_Fun.setup
*}
@@ -150,7 +155,7 @@
(K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
*} "termination prover for lexicographic orderings"
-setup Lexicographic_Order.setup
+setup Lexicographic_Order.setup
subsection {* Congruence Rules *}
@@ -175,7 +180,7 @@
subsection {* Simp rules for termination proofs *}
lemma termination_basic_simps[termination_simp]:
- "x < (y::nat) \<Longrightarrow> x < y + z"
+ "x < (y::nat) \<Longrightarrow> x < y + z"
"x < z \<Longrightarrow> x < y + z"
"x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
"x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
@@ -190,13 +195,13 @@
subsection {* Decomposition *}
-lemma less_by_empty:
+lemma less_by_empty:
"A = {} \<Longrightarrow> A \<subseteq> B"
and union_comp_emptyL:
"\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
and union_comp_emptyR:
"\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
-and wf_no_loop:
+and wf_no_loop:
"R O R = {} \<Longrightarrow> wf R"
by (auto simp add: wf_comp_self[of R])
@@ -218,10 +223,10 @@
proof -
from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
unfolding reduction_pair_def by auto
- with `wf S` have "wf (fst P \<union> S)"
+ with `wf S` have "wf (fst P \<union> S)"
by (auto intro: wf_union_compatible)
moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
- ultimately show ?thesis by (rule wf_subset)
+ ultimately show ?thesis by (rule wf_subset)
qed
definition
@@ -253,33 +258,33 @@
unfolding pair_leq_def pair_less_def by auto
text {* Introduction rules for max *}
-lemma smax_emptyI:
- "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
- and smax_insertI:
+lemma smax_emptyI:
+ "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
+ and smax_insertI:
"\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
- and wmax_emptyI:
- "finite X \<Longrightarrow> ({}, X) \<in> max_weak"
+ and wmax_emptyI:
+ "finite X \<Longrightarrow> ({}, X) \<in> max_weak"
and wmax_insertI:
- "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
+ "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
text {* Introduction rules for min *}
-lemma smin_emptyI:
- "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
- and smin_insertI:
+lemma smin_emptyI:
+ "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
+ and smin_insertI:
"\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
- and wmin_emptyI:
- "(X, {}) \<in> min_weak"
- and wmin_insertI:
- "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
+ and wmin_emptyI:
+ "(X, {}) \<in> min_weak"
+ and wmin_insertI:
+ "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
by (auto simp: min_strict_def min_weak_def min_ext_def)
text {* Reduction Pairs *}
-lemma max_ext_compat:
+lemma max_ext_compat:
assumes "R O S \<subseteq> R"
shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
-using assms
+using assms
apply auto
apply (elim max_ext.cases)
apply rule
@@ -291,16 +296,16 @@
by auto
lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
- unfolding max_strict_def max_weak_def
+ unfolding max_strict_def max_weak_def
apply (intro reduction_pairI max_ext_wf)
apply simp
apply (rule max_ext_compat)
by (auto simp: pair_less_def pair_leq_def)
-lemma min_ext_compat:
+lemma min_ext_compat:
assumes "R O S \<subseteq> R"
shows "min_ext R O (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
-using assms
+using assms
apply (auto simp: min_ext_def)
apply (drule_tac x=ya in bspec, assumption)
apply (erule bexE)
@@ -309,7 +314,7 @@
by auto
lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
- unfolding min_strict_def min_weak_def
+ unfolding min_strict_def min_weak_def
apply (intro reduction_pairI min_ext_wf)
apply simp
apply (rule min_ext_compat)
--- a/src/HOL/SMT.thy Mon Apr 23 18:42:05 2012 +0200
+++ b/src/HOL/SMT.thy Mon Apr 23 21:44:36 2012 +0200
@@ -153,13 +153,17 @@
setup {*
SMT_Config.setup #>
SMT_Normalize.setup #>
- SMT_Solver.setup #>
SMTLIB_Interface.setup #>
Z3_Interface.setup #>
Z3_Proof_Reconstruction.setup #>
SMT_Setup_Solvers.setup
*}
+method_setup smt = {*
+ Scan.optional Attrib.thms [] >>
+ (fn thms => fn ctxt =>
+ METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
+*} "apply an SMT solver to the current goal"
subsection {* Configuration *}
--- a/src/HOL/Tools/Function/function.ML Mon Apr 23 18:42:05 2012 +0200
+++ b/src/HOL/Tools/Function/function.ML Mon Apr 23 21:44:36 2012 +0200
@@ -265,7 +265,6 @@
(Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
"declaration of congruence rule for function definitions"
#> setup_case_cong
- #> Function_Relation.setup
#> Function_Common.Termination_Simps.setup
val get_congs = Function_Ctx_Tree.get_function_congs
--- a/src/HOL/Tools/Function/relation.ML Mon Apr 23 18:42:05 2012 +0200
+++ b/src/HOL/Tools/Function/relation.ML Mon Apr 23 21:44:36 2012 +0200
@@ -1,13 +1,13 @@
(* Title: HOL/Tools/Function/relation.ML
Author: Alexander Krauss, TU Muenchen
-Method "relation" to start a termination proof using a user-specified relation.
+Tactics to start a termination proof using a user-specified relation.
*)
signature FUNCTION_RELATION =
sig
val relation_tac: Proof.context -> (typ -> term) -> int -> tactic
- val setup: theory -> theory
+ val relation_infer_tac: Proof.context -> term -> int -> tactic
end
structure Function_Relation : FUNCTION_RELATION =
@@ -27,7 +27,7 @@
THEN inst_state_tac rel;
-(* method version (with type inference) *)
+(* version with type inference *)
fun inst_state_infer_tac ctxt rel st =
case Term.add_vars (prop_of st) [] of
@@ -44,12 +44,8 @@
end
| _ => Seq.empty;
-fun relation_meth rel ctxt = SIMPLE_METHOD' (fn i =>
+fun relation_infer_tac ctxt rel i =
TRY (Function_Common.apply_termination_rule ctxt i)
- THEN inst_state_infer_tac ctxt rel);
-
-val setup =
- Method.setup @{binding relation} (Args.term >> relation_meth)
- "proves termination using a user-specified wellfounded relation";
+ THEN inst_state_infer_tac ctxt rel;
end
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon Apr 23 18:42:05 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Apr 23 21:44:36 2012 +0200
@@ -41,9 +41,6 @@
(*tactic*)
val smt_tac: Proof.context -> thm list -> int -> tactic
val smt_tac': Proof.context -> thm list -> int -> tactic
-
- (*setup*)
- val setup: theory -> theory
end
structure SMT_Solver: SMT_SOLVER =
@@ -373,17 +370,4 @@
end
-
-val smt_method =
- Scan.optional Attrib.thms [] >>
- (fn thms => fn ctxt => METHOD (fn facts =>
- HEADGOAL (smt_tac ctxt (thms @ facts))))
-
-
-(* setup *)
-
-val setup =
- Method.setup @{binding smt} smt_method
- "Applies an SMT solver to the current goal."
-
end