# HG changeset patch # User krauss # Date 1334267496 -7200 # Node ID 22e64252eb3596c6b8afd2b3078b52b8bfbeda26 # Parent ed0795caec95367293a86095552d3b855d907595# Parent 3efc06fc8d619033e905d2f87f3cec140845690e merged diff -r ed0795caec95 -r 22e64252eb35 Admin/java/README --- a/Admin/java/README Thu Apr 12 23:15:34 2012 +0200 +++ b/Admin/java/README Thu Apr 12 23:51:36 2012 +0200 @@ -1,3 +1,3 @@ -This is JDK 1.7.0_03 for Linux and Linux x86 from +This is JDK 1.7.0_03 for Linux from http://www.oracle.com/technetwork/java/javase/downloads/index.html diff -r ed0795caec95 -r 22e64252eb35 Admin/java/etc/settings --- a/Admin/java/etc/settings Thu Apr 12 23:15:34 2012 +0200 +++ b/Admin/java/etc/settings Thu Apr 12 23:51:36 2012 +0200 @@ -1,4 +1,4 @@ # -*- shell-script -*- :mode=shellscript: -ISABELLE_JDK_HOME="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}/jdk1.7.0_03" +ISABELLE_JDK_HOME="$COMPONENT/jdk1.7.0_03" diff -r ed0795caec95 -r 22e64252eb35 lib/Tools/scala --- a/lib/Tools/scala Thu Apr 12 23:15:34 2012 +0200 +++ b/lib/Tools/scala Thu Apr 12 23:51:36 2012 +0200 @@ -6,6 +6,8 @@ [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } +export JAVA_HOME="$ISABELLE_JDK_HOME" + CLASSPATH="$(jvmpath "$CLASSPATH")" isabelle_scala scala -Dfile.encoding=UTF-8 \ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@" diff -r ed0795caec95 -r 22e64252eb35 lib/Tools/scalac --- a/lib/Tools/scalac Thu Apr 12 23:15:34 2012 +0200 +++ b/lib/Tools/scalac Thu Apr 12 23:51:36 2012 +0200 @@ -6,6 +6,8 @@ [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } +export JAVA_HOME="$ISABELLE_JDK_HOME" + CLASSPATH="$(jvmpath "$CLASSPATH")" isabelle_scala scalac -Dfile.encoding=UTF-8 \ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@" diff -r ed0795caec95 -r 22e64252eb35 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/CCL/Wfd.thy Thu Apr 12 23:51:36 2012 +0200 @@ -493,26 +493,19 @@ subsection {* Evaluation *} ML {* - -local - structure Data = Named_Thms(val name = @{binding eval} val description = "evaluation rules"); -in +structure Eval_Rules = + Named_Thms(val name = @{binding eval} val description = "evaluation rules"); fun eval_tac ths = Subgoal.FOCUS_PREMS (fn {context, prems, ...} => - DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1)); + DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Eval_Rules.get context) 1)); +*} +setup Eval_Rules.setup -val eval_setup = - Data.setup #> - Method.setup @{binding eval} - (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt))) - "evaluation"; - -end; - +method_setup eval = {* + Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt)) *} -setup eval_setup lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Auth/Smartcard/ShoupRubin.thy --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Apr 12 23:51:36 2012 +0200 @@ -762,7 +762,7 @@ method_setup prepare = {* Scan.succeed (K (SIMPLE_METHOD ShoupRubin.prepare_tac)) *} - "to launch a few simple facts that'll help the simplifier" + "to launch a few simple facts that will help the simplifier" method_setup parts_prepare = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *} diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Thu Apr 12 23:51:36 2012 +0200 @@ -771,7 +771,7 @@ method_setup prepare = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *} - "to launch a few simple facts that'll help the simplifier" + "to launch a few simple facts that will help the simplifier" method_setup parts_prepare = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *} diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Boogie/Tools/boogie_tactics.ML --- a/src/HOL/Boogie/Tools/boogie_tactics.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Thu Apr 12 23:51:36 2012 +0200 @@ -45,12 +45,12 @@ in tac ctxt (thms @ facts) end)) val setup_boogie = Method.setup @{binding boogie} (boogie_method false) - ("Applies an SMT solver to the current goal " ^ - "using the current set of Boogie background axioms") + "apply an SMT solver to the current goal \ + \using the current set of Boogie background axioms" val setup_boogie_all = Method.setup @{binding boogie_all} (boogie_method true) - ("Applies an SMT solver to all goals " ^ - "using the current set of Boogie background axioms") + "apply an SMT solver to all goals \ + \using the current set of Boogie background axioms" local @@ -96,7 +96,7 @@ in val setup_boogie_cases = Method.setup @{binding boogie_cases} (Scan.succeed boogie_cases) - "Prepares a set of Boogie assertions for case-based proofs" + "prepare a set of Boogie assertions for case-based proofs" end diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Decision_Procs/Commutative_Ring.thy --- a/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Apr 12 23:51:36 2012 +0200 @@ -314,6 +314,9 @@ use "commutative_ring_tac.ML" -setup Commutative_Ring_Tac.setup + +method_setup comm_ring = {* + Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac) +*} "reflective decision procedure for equalities over commutative rings" end diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Thu Apr 12 23:51:36 2012 +0200 @@ -2005,7 +2005,12 @@ *} use "cooper_tac.ML" -setup "Cooper_Tac.setup" + +method_setup cooper = {* + Args.mode "no_quantify" >> + (fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q))) +*} "decision procedure for linear integer arithmetic" + text {* Tests *} diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Apr 12 23:51:36 2012 +0200 @@ -2004,7 +2004,12 @@ *} use "ferrack_tac.ML" -setup Ferrack_Tac.setup + +method_setup rferrack = {* + Args.mode "no_quantify" >> + (fn q => fn ctxt => SIMPLE_METHOD' (Ferrack_Tac.linr_tac ctxt (not q))) +*} "decision procedure for linear real arithmetic" + lemma fixes x :: real diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Apr 12 23:51:36 2012 +0200 @@ -5635,7 +5635,12 @@ *} use "mir_tac.ML" -setup "Mir_Tac.setup" + +method_setup mir = {* + Args.mode "no_quantify" >> + (fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q))) +*} "decision procedure for MIR arithmetic" + lemma "ALL (x::real). (\x\ = \x\ = (x = real \x\))" by mir diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Decision_Procs/commutative_ring_tac.ML --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Thu Apr 12 23:51:36 2012 +0200 @@ -7,7 +7,6 @@ signature COMMUTATIVE_RING_TAC = sig val tac: Proof.context -> int -> tactic - val setup: theory -> theory end structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC = @@ -98,8 +97,4 @@ THEN (simp_tac cring_ss i) end); -val setup = - Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o tac)) - "reflective decision procedure for equalities over commutative rings"; - end; diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Thu Apr 12 23:51:36 2012 +0200 @@ -6,7 +6,6 @@ sig val trace: bool Unsynchronized.ref val linz_tac: Proof.context -> bool -> int -> tactic - val setup: theory -> theory end structure Cooper_Tac: COOPER_TAC = @@ -115,15 +114,4 @@ | _ => (pre_thm, assm_tac i) in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end); -val setup = - Method.setup @{binding cooper} - let - val parse_flag = Args.$$$ "no_quantify" >> K (K false) - in - Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >> - curry (Library.foldl op |>) true) >> - (fn q => fn ctxt => SIMPLE_METHOD' (linz_tac ctxt q)) - end - "decision procedure for linear integer arithmetic"; - end diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Thu Apr 12 23:51:36 2012 +0200 @@ -6,7 +6,6 @@ sig val trace: bool Unsynchronized.ref val linr_tac: Proof.context -> bool -> int -> tactic - val setup: theory -> theory end structure Ferrack_Tac = @@ -96,10 +95,4 @@ | _ => (pre_thm, assm_tac i) in rtac ((mp_step nh o spec_step np) th) i THEN tac end); -val setup = - Method.setup @{binding rferrack} - (Args.mode "no_quantify" >> (fn q => fn ctxt => - SIMPLE_METHOD' (linr_tac ctxt (not q)))) - "decision procedure for linear real arithmetic"; - end diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Thu Apr 12 23:51:36 2012 +0200 @@ -6,7 +6,6 @@ sig val trace: bool Unsynchronized.ref val mir_tac: Proof.context -> bool -> int -> tactic - val setup: theory -> theory end structure Mir_Tac = @@ -143,15 +142,4 @@ | _ => (pre_thm, assm_tac i) in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end); -val setup = - Method.setup @{binding mir} - let - val parse_flag = Args.$$$ "no_quantify" >> K (K false) - in - Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >> - curry (Library.foldl op |>) true) >> - (fn q => fn ctxt => SIMPLE_METHOD' (mir_tac ctxt q)) - end - "decision procedure for MIR arithmetic"; - end diff -r ed0795caec95 -r 22e64252eb35 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/FunDef.thy Thu Apr 12 23:51:36 2012 +0200 @@ -110,14 +110,21 @@ use "Tools/Function/relation.ML" use "Tools/Function/function.ML" use "Tools/Function/pat_completeness.ML" + +method_setup pat_completeness = {* + Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac) +*} "prove completeness of datatype patterns" + use "Tools/Function/fun.ML" use "Tools/Function/induction_schema.ML" +method_setup induction_schema = {* + Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac) +*} "prove an induction principle" + setup {* Function.setup - #> Pat_Completeness.setup #> Function_Fun.setup - #> Induction_Schema.setup *} subsection {* Measure Functions *} @@ -137,6 +144,12 @@ by (rule is_measure_trivial) use "Tools/Function/lexicographic_order.ML" + +method_setup lexicographic_order = {* + Method.sections clasimp_modifiers >> + (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false)) +*} "termination prover for lexicographic orderings" + setup Lexicographic_Order.setup diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Groebner_Basis.thy Thu Apr 12 23:51:36 2012 +0200 @@ -43,8 +43,20 @@ use "Tools/groebner.ML" -method_setup algebra = Groebner.algebra_method - "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" +method_setup algebra = {* + let + fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () + val addN = "add" + val delN = "del" + val any_keyword = keyword addN || keyword delN + val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; + in + Scan.optional (keyword addN |-- thms) [] -- + Scan.optional (keyword delN |-- thms) [] >> + (fn (add_ths, del_ths) => fn ctxt => + SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt)) + end +*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" declare dvd_def[algebra] declare dvd_eq_mod_eq_0[symmetric, algebra] diff -r ed0795caec95 -r 22e64252eb35 src/HOL/HOLCF/Fixrec.thy --- a/src/HOL/HOLCF/Fixrec.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/HOLCF/Fixrec.thy Thu Apr 12 23:51:36 2012 +0200 @@ -230,7 +230,9 @@ use "Tools/holcf_library.ML" use "Tools/fixrec.ML" -setup {* Fixrec.setup *} +method_setup fixrec_simp = {* + Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac) +*} "pattern prover for fixrec constants" setup {* Fixrec.add_matchers diff -r ed0795caec95 -r 22e64252eb35 src/HOL/HOLCF/Tools/fixrec.ML --- a/src/HOL/HOLCF/Tools/fixrec.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Thu Apr 12 23:51:36 2012 +0200 @@ -12,7 +12,6 @@ -> (bool * (Attrib.binding * string)) list -> local_theory -> local_theory val add_matchers: (string * string) list -> theory -> theory val fixrec_simp_tac: Proof.context -> int -> tactic - val setup: theory -> theory end structure Fixrec : FIXREC = @@ -406,9 +405,4 @@ (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs') >> (fn (fixes, specs) => add_fixrec_cmd fixes specs)) -val setup = - Method.setup @{binding fixrec_simp} - (Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac)) - "pattern prover for fixrec constants" - end diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Library/Countable.thy Thu Apr 12 23:51:36 2012 +0200 @@ -269,8 +269,7 @@ by - (rule exI) qed -method_setup countable_datatype = {* -let +ML {* fun countable_tac ctxt = SUBGOAL (fn (goal, i) => let @@ -297,9 +296,10 @@ etac induct_thm i, REPEAT (resolve_tac rules i ORELSE atac i)]) 1 end) -in +*} + +method_setup countable_datatype = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (countable_tac ctxt)) -end *} "prove countable class instances for datatypes" hide_const (open) finite_item nth_item diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Library/Eval_Witness.thy --- a/src/HOL/Library/Eval_Witness.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Library/Eval_Witness.thy Thu Apr 12 23:51:36 2012 +0200 @@ -77,8 +77,8 @@ method_setup eval_witness = {* Scan.lift (Scan.repeat Args.name) >> - (fn ws => K (SIMPLE_METHOD' - (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)))) + (fn ws => K (SIMPLE_METHOD' + (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)))) *} "evaluation with ML witnesses" diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Limits.thy Thu Apr 12 23:51:36 2012 +0200 @@ -112,7 +112,8 @@ qed ML {* - fun ev_elim_tac ctxt thms thm = let + fun eventually_elim_tac ctxt thms thm = + let val thy = Proof_Context.theory_of ctxt val mp_thms = thms RL [@{thm eventually_rev_mp}] val raw_elim_thm = @@ -124,13 +125,11 @@ in CASES cases (rtac raw_elim_thm 1) thm end - - fun eventually_elim_setup name = - Method.setup name (Scan.succeed (fn ctxt => METHOD_CASES (ev_elim_tac ctxt))) - "elimination of eventually quantifiers" *} -setup {* eventually_elim_setup @{binding "eventually_elim"} *} +method_setup eventually_elim = {* + Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt)) +*} "elimination of eventually quantifiers" subsection {* Finer-than relation *} diff -r ed0795caec95 -r 22e64252eb35 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/NSA/StarDef.thy Thu Apr 12 23:51:36 2012 +0200 @@ -91,6 +91,12 @@ use "transfer.ML" setup Transfer_Principle.setup +method_setup transfer = {* + Attrib.thms >> (fn ths => fn ctxt => + SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths)) +*} "transfer principle" + + text {* Transfer introduction rules. *} lemma transfer_ex [transfer_intro]: diff -r ed0795caec95 -r 22e64252eb35 src/HOL/NSA/transfer.ML --- a/src/HOL/NSA/transfer.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/NSA/transfer.ML Thu Apr 12 23:51:36 2012 +0200 @@ -112,8 +112,6 @@ Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del) "declaration of transfer unfolding rule" #> Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del) - "declaration of transfer refolding rule" #> - Method.setup @{binding transfer} (Attrib.thms >> (fn ths => fn ctxt => - SIMPLE_METHOD' (transfer_tac ctxt ths))) "transfer principle"; + "declaration of transfer refolding rule" end; diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Orderings.thy Thu Apr 12 23:51:36 2012 +0200 @@ -312,7 +312,7 @@ signature ORDERS = sig val print_structures: Proof.context -> unit - val setup: theory -> theory + val attrib_setup: theory -> theory val order_tac: Proof.context -> thm list -> int -> tactic end; @@ -414,19 +414,15 @@ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o Toplevel.keep (print_structures o Toplevel.context_of))); - -(** Setup **) - -val setup = - Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt []))) - "transitivity reasoner" #> - attrib_setup; - end; *} -setup Orders.setup +setup Orders.attrib_setup + +method_setup order = {* + Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt [])) +*} "transitivity reasoner" text {* Declarations to set up transitivity reasoner of partial and linear orders. *} diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Presburger.thy Thu Apr 12 23:51:36 2012 +0200 @@ -387,10 +387,25 @@ by (simp cong: conj_cong) use "Tools/Qelim/cooper.ML" - setup Cooper.setup -method_setup presburger = "Cooper.method" "Cooper's algorithm for Presburger arithmetic" +method_setup presburger = {* + let + fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () + fun simple_keyword k = Scan.lift (Args.$$$ k) >> K () + val addN = "add" + val delN = "del" + val elimN = "elim" + val any_keyword = keyword addN || keyword delN || simple_keyword elimN + val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; + in + Scan.optional (simple_keyword elimN >> K false) true -- + Scan.optional (keyword addN |-- thms) [] -- + Scan.optional (keyword delN |-- thms) [] >> + (fn ((elim, add_ths), del_ths) => fn ctxt => + SIMPLE_METHOD' (Cooper.tac elim add_ths del_ths ctxt)) + end +*} "Cooper's algorithm for Presburger arithmetic" declare dvd_eq_mod_eq_0[symmetric, presburger] declare mod_1[presburger] diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Tools/Function/induction_schema.ML Thu Apr 12 23:51:36 2012 +0200 @@ -9,7 +9,6 @@ val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic) -> Proof.context -> thm list -> tactic val induction_schema_tac : Proof.context -> thm list -> tactic - val setup : theory -> theory end @@ -395,8 +394,4 @@ fun induction_schema_tac ctxt = mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; -val setup = - Method.setup @{binding induction_schema} (Scan.succeed (RAW_METHOD o induction_schema_tac)) - "proves an induction principle" - end diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Apr 12 23:51:36 2012 +0200 @@ -9,8 +9,6 @@ sig val lex_order_tac : bool -> Proof.context -> tactic -> tactic val lexicographic_order_tac : bool -> Proof.context -> tactic - val lexicographic_order : Proof.context -> Proof.method - val setup: theory -> theory end @@ -218,12 +216,7 @@ lex_order_tac quiet ctxt (auto_tac (map_simpset (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt)) -val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false - val setup = - Method.setup @{binding lexicographic_order} - (Method.sections clasimp_modifiers >> (K lexicographic_order)) - "termination prover for lexicographic orderings" - #> Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false)) + Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false)) end; diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Tools/Function/pat_completeness.ML --- a/src/HOL/Tools/Function/pat_completeness.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Tools/Function/pat_completeness.ML Thu Apr 12 23:51:36 2012 +0200 @@ -7,11 +7,8 @@ signature PAT_COMPLETENESS = sig val pat_completeness_tac: Proof.context -> int -> tactic - val pat_completeness: Proof.context -> Proof.method val prove_completeness : theory -> term list -> term -> term list list -> term list list -> thm - - val setup : theory -> theory end structure Pat_Completeness : PAT_COMPLETENESS = @@ -153,11 +150,4 @@ end handle COMPLETENESS => no_tac) - -val pat_completeness = SIMPLE_METHOD' o pat_completeness_tac - -val setup = - Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness) - "Completeness prover for datatype patterns" - end diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Thu Apr 12 23:51:36 2012 +0200 @@ -13,7 +13,6 @@ exception COOPER of string val conv: Proof.context -> conv val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic - val method: (Proof.context -> Method.method) context_parser val setup: theory -> theory end; @@ -857,23 +856,6 @@ THEN_ALL_NEW finish_tac elim end; -val method = - let - fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () - fun simple_keyword k = Scan.lift (Args.$$$ k) >> K () - val addN = "add" - val delN = "del" - val elimN = "elim" - val any_keyword = keyword addN || keyword delN || simple_keyword elimN - val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; - in - Scan.optional (simple_keyword elimN >> K false) true -- - Scan.optional (keyword addN |-- thms) [] -- - Scan.optional (keyword delN |-- thms) [] >> - (fn ((elim, add_ths), del_ths) => fn ctxt => - SIMPLE_METHOD' (tac elim add_ths del_ths ctxt)) - end; - (* theory setup *) diff -r ed0795caec95 -r 22e64252eb35 src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/Tools/groebner.ML Thu Apr 12 23:51:36 2012 +0200 @@ -16,7 +16,6 @@ val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic - val algebra_method: (Proof.context -> Method.method) context_parser end structure Groebner : GROEBNER = @@ -1027,21 +1026,4 @@ fun algebra_tac add_ths del_ths ctxt i = ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i -local - -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () -val addN = "add" -val delN = "del" -val any_keyword = keyword addN || keyword delN -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; - -in - -val algebra_method = ((Scan.optional (keyword addN |-- thms) []) -- - (Scan.optional (keyword delN |-- thms) [])) >> - (fn (add_ths, del_ths) => fn ctxt => - SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt)) - end; - -end; diff -r ed0795caec95 -r 22e64252eb35 src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Thu Apr 12 23:15:34 2012 +0200 +++ b/src/HOL/ex/SAT_Examples.thy Thu Apr 12 23:51:36 2012 +0200 @@ -80,11 +80,9 @@ ML {* sat.trace_sat := false; *} ML {* quick_and_dirty := false; *} -method_setup rawsat = - {* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *} - "SAT solver (no preprocessing)" - -(* ML {* Toplevel.profiling := 1; *} *) +method_setup rawsat = {* + Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) +*} "SAT solver (no preprocessing)" (* Translated from TPTP problem library: PUZ015-2.006.dimacs *) @@ -512,8 +510,6 @@ (as of 2006-08-30, on a 2.5 GHz Pentium 4) *) -(* ML {* Toplevel.profiling := 0; *} *) - text {* Function {\tt benchmark} takes the name of an existing DIMACS CNF file, parses this file, passes the problem to a SAT solver, and checks diff -r ed0795caec95 -r 22e64252eb35 src/Pure/Concurrent/lazy.ML --- a/src/Pure/Concurrent/lazy.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/Pure/Concurrent/lazy.ML Thu Apr 12 23:51:36 2012 +0200 @@ -61,15 +61,15 @@ SOME e => let val res0 = Exn.capture (restore_attributes e) (); - val res1 = Exn.capture (fn () => Future.fulfill_result x res0) (); - val res2 = Future.join_result x; - in + val _ = Exn.capture (fn () => Future.fulfill_result x res0) (); + val res = Future.join_result x; (*semantic race: some other threads might see the same interrupt, until there is a fresh start*) - if Exn.is_interrupt_exn res1 orelse Exn.is_interrupt_exn res2 then - (Synchronized.change var (fn _ => Expr e); Exn.interrupt ()) - else res2 - end + val _ = + if Exn.is_interrupt_exn res then + Synchronized.change var (fn _ => Expr e) + else (); + in res end | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ()) end) ()); diff -r ed0795caec95 -r 22e64252eb35 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Apr 12 23:15:34 2012 +0200 +++ b/src/Pure/Isar/proof.ML Thu Apr 12 23:51:36 2012 +0200 @@ -198,6 +198,9 @@ val context_of = #context o current; val theory_of = Proof_Context.theory_of o context_of; +fun map_node_context f = + map_node (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); + fun map_context f = map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); @@ -292,24 +295,27 @@ (* nested goal *) -fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) = +fun map_goal f g h (State (Node {context, facts, mode, goal = SOME goal}, node :: nodes)) = let val Goal {statement, messages, using, goal, before_qed, after_qed} = goal; val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed)); - in State (make_node (f context, facts, mode, SOME goal'), nodes) end - | map_goal f g (State (nd, node :: nodes)) = - let val State (node', nodes') = map_goal f g (State (node, nodes)) - in map_context f (State (nd, node' :: nodes')) end - | map_goal _ _ state = state; + val node' = map_node_context h node; + in State (make_node (f context, facts, mode, SOME goal'), node' :: nodes) end + | map_goal f g h (State (nd, node :: nodes)) = + let + val nd' = map_node_context f nd; + val State (node', nodes') = map_goal f g h (State (node, nodes)); + in State (nd', node' :: nodes') end + | map_goal _ _ _ state = state; fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) => - (statement, [], using, goal, before_qed, after_qed)); + (statement, [], using, goal, before_qed, after_qed)) I; fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) => - (statement, msg :: messages, using, goal, before_qed, after_qed)); + (statement, msg :: messages, using, goal, before_qed, after_qed)) I; fun using_facts using = map_goal I (fn (statement, _, _, goal, before_qed, after_qed) => - (statement, [], using, goal, before_qed, after_qed)); + (statement, [], using, goal, before_qed, after_qed)) I; local fun find i state = @@ -407,7 +413,7 @@ |> map_goal (Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #> Proof_Context.add_cases true meth_cases) - (K (statement, [], using, goal', before_qed, after_qed))) + (K (statement, [], using, goal', before_qed, after_qed)) I) end; fun select_goals n meth state = @@ -717,7 +723,7 @@ let val ctxt = context_of state'; val ths = maps snd named_facts; - in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end)); + in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I); fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths); @@ -1074,7 +1080,9 @@ val _ = assert_backward state; val (goal_ctxt, (_, goal)) = find_goal state; val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal; - val goal_txt = prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt); + val goal_tfrees = + fold Term.add_tfrees + (prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) []; val _ = is_relevant state andalso error "Cannot fork relevant proof"; @@ -1090,8 +1098,8 @@ val result_ctxt = state - |> map_contexts (fold Variable.declare_term goal_txt) |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed')) + (fold (Variable.declare_typ o TFree) goal_tfrees) |> fork_proof; val future_thm = result_ctxt |> Future.map (fn (_, x) => @@ -1099,7 +1107,7 @@ val finished_goal = Goal.future_result goal_ctxt future_thm prop'; val state' = state - |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) + |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I |> done; in (Future.map #1 result_ctxt, state') end;