more standard method setup;
authorwenzelm
Mon Apr 23 21:44:36 2012 +0200 (2012-04-23)
changeset 47701157e6108a342
parent 47700 27a04da9c6e6
child 47702 5f9ce06f281e
more standard method setup;
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/ringsimp.ML
src/HOL/FunDef.thy
src/HOL/SMT.thy
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/relation.ML
src/HOL/Tools/SMT/smt_solver.ML
     1.1 --- a/src/HOL/Algebra/Ring.thy	Mon Apr 23 18:42:05 2012 +0200
     1.2 +++ b/src/HOL/Algebra/Ring.thy	Mon Apr 23 21:44:36 2012 +0200
     1.3 @@ -391,7 +391,11 @@
     1.4  
     1.5  use "ringsimp.ML"
     1.6  
     1.7 -setup Algebra.setup
     1.8 +setup Algebra.attrib_setup
     1.9 +
    1.10 +method_setup algebra = {*
    1.11 +  Scan.succeed (SIMPLE_METHOD' o Algebra.algebra_tac)
    1.12 +*} "normalisation of algebraic structure"
    1.13  
    1.14  lemmas (in ring) ring_simprules
    1.15    [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
     2.1 --- a/src/HOL/Algebra/ringsimp.ML	Mon Apr 23 18:42:05 2012 +0200
     2.2 +++ b/src/HOL/Algebra/ringsimp.ML	Mon Apr 23 21:44:36 2012 +0200
     2.3 @@ -6,7 +6,8 @@
     2.4  signature ALGEBRA =
     2.5  sig
     2.6    val print_structures: Proof.context -> unit
     2.7 -  val setup: theory -> theory
     2.8 +  val attrib_setup: theory -> theory
     2.9 +  val algebra_tac: Proof.context -> int -> tactic
    2.10  end;
    2.11  
    2.12  structure Algebra: ALGEBRA =
    2.13 @@ -58,6 +59,7 @@
    2.14  fun add_struct_thm s =
    2.15    Thm.declaration_attribute
    2.16      (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
    2.17 +
    2.18  fun del_struct s =
    2.19    Thm.declaration_attribute
    2.20      (fn _ => Data.map (AList.delete struct_eq s));
    2.21 @@ -69,13 +71,4 @@
    2.22        >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)))
    2.23      "theorems controlling algebra method";
    2.24  
    2.25 -
    2.26 -
    2.27 -(** Setup **)
    2.28 -
    2.29 -val setup =
    2.30 -  Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
    2.31 -    "normalisation of algebraic structure" #>
    2.32 -  attrib_setup;
    2.33 -
    2.34  end;
     3.1 --- a/src/HOL/FunDef.thy	Mon Apr 23 18:42:05 2012 +0200
     3.2 +++ b/src/HOL/FunDef.thy	Mon Apr 23 21:44:36 2012 +0200
     3.3 @@ -108,6 +108,11 @@
     3.4  use "Tools/Function/mutual.ML"
     3.5  use "Tools/Function/pattern_split.ML"
     3.6  use "Tools/Function/relation.ML"
     3.7 +
     3.8 +method_setup relation = {*
     3.9 +  Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
    3.10 +*} "prove termination using a user-specified wellfounded relation"
    3.11 +
    3.12  use "Tools/Function/function.ML"
    3.13  use "Tools/Function/pat_completeness.ML"
    3.14  
    3.15 @@ -122,7 +127,7 @@
    3.16    Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
    3.17  *} "prove an induction principle"
    3.18  
    3.19 -setup {* 
    3.20 +setup {*
    3.21    Function.setup
    3.22    #> Function_Fun.setup
    3.23  *}
    3.24 @@ -150,7 +155,7 @@
    3.25    (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
    3.26  *} "termination prover for lexicographic orderings"
    3.27  
    3.28 -setup Lexicographic_Order.setup 
    3.29 +setup Lexicographic_Order.setup
    3.30  
    3.31  
    3.32  subsection {* Congruence Rules *}
    3.33 @@ -175,7 +180,7 @@
    3.34  subsection {* Simp rules for termination proofs *}
    3.35  
    3.36  lemma termination_basic_simps[termination_simp]:
    3.37 -  "x < (y::nat) \<Longrightarrow> x < y + z" 
    3.38 +  "x < (y::nat) \<Longrightarrow> x < y + z"
    3.39    "x < z \<Longrightarrow> x < y + z"
    3.40    "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
    3.41    "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
    3.42 @@ -190,13 +195,13 @@
    3.43  
    3.44  subsection {* Decomposition *}
    3.45  
    3.46 -lemma less_by_empty: 
    3.47 +lemma less_by_empty:
    3.48    "A = {} \<Longrightarrow> A \<subseteq> B"
    3.49  and  union_comp_emptyL:
    3.50    "\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
    3.51  and union_comp_emptyR:
    3.52    "\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
    3.53 -and wf_no_loop: 
    3.54 +and wf_no_loop:
    3.55    "R O R = {} \<Longrightarrow> wf R"
    3.56  by (auto simp add: wf_comp_self[of R])
    3.57  
    3.58 @@ -218,10 +223,10 @@
    3.59  proof -
    3.60    from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
    3.61      unfolding reduction_pair_def by auto
    3.62 -  with `wf S` have "wf (fst P \<union> S)" 
    3.63 +  with `wf S` have "wf (fst P \<union> S)"
    3.64      by (auto intro: wf_union_compatible)
    3.65    moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
    3.66 -  ultimately show ?thesis by (rule wf_subset) 
    3.67 +  ultimately show ?thesis by (rule wf_subset)
    3.68  qed
    3.69  
    3.70  definition
    3.71 @@ -253,33 +258,33 @@
    3.72    unfolding pair_leq_def pair_less_def by auto
    3.73  
    3.74  text {* Introduction rules for max *}
    3.75 -lemma smax_emptyI: 
    3.76 -  "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict" 
    3.77 -  and smax_insertI: 
    3.78 +lemma smax_emptyI:
    3.79 +  "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
    3.80 +  and smax_insertI:
    3.81    "\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
    3.82 -  and wmax_emptyI: 
    3.83 -  "finite X \<Longrightarrow> ({}, X) \<in> max_weak" 
    3.84 +  and wmax_emptyI:
    3.85 +  "finite X \<Longrightarrow> ({}, X) \<in> max_weak"
    3.86    and wmax_insertI:
    3.87 -  "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak" 
    3.88 +  "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
    3.89  unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
    3.90  
    3.91  text {* Introduction rules for min *}
    3.92 -lemma smin_emptyI: 
    3.93 -  "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict" 
    3.94 -  and smin_insertI: 
    3.95 +lemma smin_emptyI:
    3.96 +  "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
    3.97 +  and smin_insertI:
    3.98    "\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
    3.99 -  and wmin_emptyI: 
   3.100 -  "(X, {}) \<in> min_weak" 
   3.101 -  and wmin_insertI: 
   3.102 -  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak" 
   3.103 +  and wmin_emptyI:
   3.104 +  "(X, {}) \<in> min_weak"
   3.105 +  and wmin_insertI:
   3.106 +  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
   3.107  by (auto simp: min_strict_def min_weak_def min_ext_def)
   3.108  
   3.109  text {* Reduction Pairs *}
   3.110  
   3.111 -lemma max_ext_compat: 
   3.112 +lemma max_ext_compat:
   3.113    assumes "R O S \<subseteq> R"
   3.114    shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
   3.115 -using assms 
   3.116 +using assms
   3.117  apply auto
   3.118  apply (elim max_ext.cases)
   3.119  apply rule
   3.120 @@ -291,16 +296,16 @@
   3.121  by auto
   3.122  
   3.123  lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
   3.124 -  unfolding max_strict_def max_weak_def 
   3.125 +  unfolding max_strict_def max_weak_def
   3.126  apply (intro reduction_pairI max_ext_wf)
   3.127  apply simp
   3.128  apply (rule max_ext_compat)
   3.129  by (auto simp: pair_less_def pair_leq_def)
   3.130  
   3.131 -lemma min_ext_compat: 
   3.132 +lemma min_ext_compat:
   3.133    assumes "R O S \<subseteq> R"
   3.134    shows "min_ext R O  (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
   3.135 -using assms 
   3.136 +using assms
   3.137  apply (auto simp: min_ext_def)
   3.138  apply (drule_tac x=ya in bspec, assumption)
   3.139  apply (erule bexE)
   3.140 @@ -309,7 +314,7 @@
   3.141  by auto
   3.142  
   3.143  lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
   3.144 -  unfolding min_strict_def min_weak_def 
   3.145 +  unfolding min_strict_def min_weak_def
   3.146  apply (intro reduction_pairI min_ext_wf)
   3.147  apply simp
   3.148  apply (rule min_ext_compat)
     4.1 --- a/src/HOL/SMT.thy	Mon Apr 23 18:42:05 2012 +0200
     4.2 +++ b/src/HOL/SMT.thy	Mon Apr 23 21:44:36 2012 +0200
     4.3 @@ -153,13 +153,17 @@
     4.4  setup {*
     4.5    SMT_Config.setup #>
     4.6    SMT_Normalize.setup #>
     4.7 -  SMT_Solver.setup #>
     4.8    SMTLIB_Interface.setup #>
     4.9    Z3_Interface.setup #>
    4.10    Z3_Proof_Reconstruction.setup #>
    4.11    SMT_Setup_Solvers.setup
    4.12  *}
    4.13  
    4.14 +method_setup smt = {*
    4.15 +  Scan.optional Attrib.thms [] >>
    4.16 +    (fn thms => fn ctxt =>
    4.17 +      METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
    4.18 +*} "apply an SMT solver to the current goal"
    4.19  
    4.20  
    4.21  subsection {* Configuration *}
     5.1 --- a/src/HOL/Tools/Function/function.ML	Mon Apr 23 18:42:05 2012 +0200
     5.2 +++ b/src/HOL/Tools/Function/function.ML	Mon Apr 23 21:44:36 2012 +0200
     5.3 @@ -265,7 +265,6 @@
     5.4      (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
     5.5      "declaration of congruence rule for function definitions"
     5.6    #> setup_case_cong
     5.7 -  #> Function_Relation.setup
     5.8    #> Function_Common.Termination_Simps.setup
     5.9  
    5.10  val get_congs = Function_Ctx_Tree.get_function_congs
     6.1 --- a/src/HOL/Tools/Function/relation.ML	Mon Apr 23 18:42:05 2012 +0200
     6.2 +++ b/src/HOL/Tools/Function/relation.ML	Mon Apr 23 21:44:36 2012 +0200
     6.3 @@ -1,13 +1,13 @@
     6.4  (*  Title:      HOL/Tools/Function/relation.ML
     6.5      Author:     Alexander Krauss, TU Muenchen
     6.6  
     6.7 -Method "relation" to start a termination proof using a user-specified relation.
     6.8 +Tactics to start a termination proof using a user-specified relation.
     6.9  *)
    6.10  
    6.11  signature FUNCTION_RELATION =
    6.12  sig
    6.13    val relation_tac: Proof.context -> (typ -> term) -> int -> tactic
    6.14 -  val setup: theory -> theory
    6.15 +  val relation_infer_tac: Proof.context -> term -> int -> tactic
    6.16  end
    6.17  
    6.18  structure Function_Relation : FUNCTION_RELATION =
    6.19 @@ -27,7 +27,7 @@
    6.20    THEN inst_state_tac rel;
    6.21  
    6.22  
    6.23 -(* method version (with type inference) *)
    6.24 +(* version with type inference *)
    6.25  
    6.26  fun inst_state_infer_tac ctxt rel st =
    6.27    case Term.add_vars (prop_of st) [] of
    6.28 @@ -44,12 +44,8 @@
    6.29        end
    6.30    | _ => Seq.empty;
    6.31  
    6.32 -fun relation_meth rel ctxt = SIMPLE_METHOD' (fn i =>
    6.33 +fun relation_infer_tac ctxt rel i =
    6.34    TRY (Function_Common.apply_termination_rule ctxt i)
    6.35 -  THEN inst_state_infer_tac ctxt rel);
    6.36 -
    6.37 -val setup =
    6.38 -  Method.setup @{binding relation} (Args.term >> relation_meth)
    6.39 -    "proves termination using a user-specified wellfounded relation";
    6.40 +  THEN inst_state_infer_tac ctxt rel;
    6.41  
    6.42  end
     7.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Apr 23 18:42:05 2012 +0200
     7.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Apr 23 21:44:36 2012 +0200
     7.3 @@ -41,9 +41,6 @@
     7.4    (*tactic*)
     7.5    val smt_tac: Proof.context -> thm list -> int -> tactic
     7.6    val smt_tac': Proof.context -> thm list -> int -> tactic
     7.7 -
     7.8 -  (*setup*)
     7.9 -  val setup: theory -> theory
    7.10  end
    7.11  
    7.12  structure SMT_Solver: SMT_SOLVER =
    7.13 @@ -373,17 +370,4 @@
    7.14  
    7.15  end
    7.16  
    7.17 -
    7.18 -val smt_method =
    7.19 -  Scan.optional Attrib.thms [] >>
    7.20 -  (fn thms => fn ctxt => METHOD (fn facts =>
    7.21 -    HEADGOAL (smt_tac ctxt (thms @ facts))))
    7.22 -
    7.23 -
    7.24 -(* setup *)
    7.25 -
    7.26 -val setup =
    7.27 -  Method.setup @{binding smt} smt_method
    7.28 -    "Applies an SMT solver to the current goal."
    7.29 -
    7.30  end