1.1 --- a/src/Cube/Example.thy Mon Mar 16 17:51:24 2009 +0100
1.2 +++ b/src/Cube/Example.thy Mon Mar 16 18:24:30 2009 +0100
1.3 @@ -15,20 +15,19 @@
1.4 *}
1.5
1.6 method_setup depth_solve = {*
1.7 - Method.thms_args (fn thms => METHOD (fn facts =>
1.8 - (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
1.9 + Attrib.thms >> (fn thms => K (METHOD (fn facts =>
1.10 + (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))
1.11 *} ""
1.12
1.13 method_setup depth_solve1 = {*
1.14 - Method.thms_args (fn thms => METHOD (fn facts =>
1.15 - (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))
1.16 + Attrib.thms >> (fn thms => K (METHOD (fn facts =>
1.17 + (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))
1.18 *} ""
1.19
1.20 method_setup strip_asms = {*
1.21 - let val strip_b = thm "strip_b" and strip_s = thm "strip_s" in
1.22 - Method.thms_args (fn thms => METHOD (fn facts =>
1.23 - REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))
1.24 - end
1.25 + Attrib.thms >> (fn thms => K (METHOD (fn facts =>
1.26 + REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN
1.27 + DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))))
1.28 *} ""
1.29
1.30
2.1 --- a/src/FOL/FOL.thy Mon Mar 16 17:51:24 2009 +0100
2.2 +++ b/src/FOL/FOL.thy Mon Mar 16 18:24:30 2009 +0100
2.3 @@ -73,9 +73,10 @@
2.4 fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
2.5 *}
2.6
2.7 -method_setup case_tac =
2.8 - {* Method.goal_args_ctxt Args.name_source case_tac *}
2.9 - "case_tac emulation (dynamic instantiation!)"
2.10 +method_setup case_tac = {*
2.11 + Args.goal_spec -- Scan.lift Args.name_source >>
2.12 + (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
2.13 +*} "case_tac emulation (dynamic instantiation!)"
2.14
2.15
2.16 (*** Special elimination rules *)
3.1 --- a/src/FOL/ex/Iff_Oracle.thy Mon Mar 16 17:51:24 2009 +0100
3.2 +++ b/src/FOL/ex/Iff_Oracle.thy Mon Mar 16 18:24:30 2009 +0100
3.3 @@ -52,7 +52,7 @@
3.4 subsection {* Oracle as proof method *}
3.5
3.6 method_setup iff = {*
3.7 - Method.simple_args OuterParse.nat (fn n => fn ctxt =>
3.8 + Scan.lift OuterParse.nat >> (fn n => fn ctxt =>
3.9 SIMPLE_METHOD
3.10 (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
3.11 handle Fail _ => no_tac))
4.1 --- a/src/HOL/Algebra/abstract/Ring2.thy Mon Mar 16 17:51:24 2009 +0100
4.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy Mon Mar 16 18:24:30 2009 +0100
4.3 @@ -222,7 +222,7 @@
4.4 *} (* Note: r_one is not necessary in ring_ss *)
4.5
4.6 method_setup ring =
4.7 - {* Method.no_args (SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
4.8 + {* Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss))) *}
4.9 {* computes distributive normal form in rings *}
4.10
4.11
5.1 --- a/src/HOL/Auth/Event.thy Mon Mar 16 17:51:24 2009 +0100
5.2 +++ b/src/HOL/Auth/Event.thy Mon Mar 16 18:24:30 2009 +0100
5.3 @@ -289,7 +289,7 @@
5.4 *}
5.5
5.6 method_setup analz_mono_contra = {*
5.7 - Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
5.8 + Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
5.9 "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
5.10
5.11 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
5.12 @@ -310,7 +310,7 @@
5.13 *}
5.14
5.15 method_setup synth_analz_mono_contra = {*
5.16 - Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
5.17 + Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
5.18 "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
5.19
5.20 end
6.1 --- a/src/HOL/Auth/Message.thy Mon Mar 16 17:51:24 2009 +0100
6.2 +++ b/src/HOL/Auth/Message.thy Mon Mar 16 18:24:30 2009 +0100
6.3 @@ -941,15 +941,15 @@
6.4 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
6.5
6.6 method_setup spy_analz = {*
6.7 - Method.ctxt_args (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
6.8 + Scan.succeed (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
6.9 "for proving the Fake case when analz is involved"
6.10
6.11 method_setup atomic_spy_analz = {*
6.12 - Method.ctxt_args (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
6.13 + Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
6.14 "for debugging spy_analz"
6.15
6.16 method_setup Fake_insert_simp = {*
6.17 - Method.ctxt_args (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
6.18 + Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
6.19 "for debugging spy_analz"
6.20
6.21 end
7.1 --- a/src/HOL/Auth/OtwayReesBella.thy Mon Mar 16 17:51:24 2009 +0100
7.2 +++ b/src/HOL/Auth/OtwayReesBella.thy Mon Mar 16 18:24:30 2009 +0100
7.3 @@ -137,7 +137,7 @@
7.4 *}
7.5
7.6 method_setup parts_explicit = {*
7.7 - Method.no_args (SIMPLE_METHOD' parts_explicit_tac) *}
7.8 + Scan.succeed (K (SIMPLE_METHOD' parts_explicit_tac)) *}
7.9 "to explicitly state that some message components belong to parts knows Spy"
7.10
7.11
7.12 @@ -257,7 +257,7 @@
7.13 *}
7.14
7.15 method_setup analz_freshCryptK = {*
7.16 - Method.ctxt_args (fn ctxt =>
7.17 + Scan.succeed (fn ctxt =>
7.18 (SIMPLE_METHOD
7.19 (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
7.20 REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
7.21 @@ -267,10 +267,10 @@
7.22
7.23
7.24 method_setup disentangle = {*
7.25 - Method.no_args
7.26 - (SIMPLE_METHOD
7.27 + Scan.succeed
7.28 + (K (SIMPLE_METHOD
7.29 (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE]
7.30 - ORELSE' hyp_subst_tac))) *}
7.31 + ORELSE' hyp_subst_tac)))) *}
7.32 "for eliminating conjunctions, disjunctions and the like"
7.33
7.34
8.1 --- a/src/HOL/Auth/Public.thy Mon Mar 16 17:51:24 2009 +0100
8.2 +++ b/src/HOL/Auth/Public.thy Mon Mar 16 18:24:30 2009 +0100
8.3 @@ -424,7 +424,7 @@
8.4 *}
8.5
8.6 method_setup analz_freshK = {*
8.7 - Method.ctxt_args (fn ctxt =>
8.8 + Scan.succeed (fn ctxt =>
8.9 (SIMPLE_METHOD
8.10 (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
8.11 REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
8.12 @@ -435,11 +435,11 @@
8.13 subsection{*Specialized Methods for Possibility Theorems*}
8.14
8.15 method_setup possibility = {*
8.16 - Method.ctxt_args (SIMPLE_METHOD o Public.possibility_tac) *}
8.17 + Scan.succeed (SIMPLE_METHOD o Public.possibility_tac) *}
8.18 "for proving possibility theorems"
8.19
8.20 method_setup basic_possibility = {*
8.21 - Method.ctxt_args (SIMPLE_METHOD o Public.basic_possibility_tac) *}
8.22 + Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac) *}
8.23 "for proving possibility theorems"
8.24
8.25 end
9.1 --- a/src/HOL/Auth/Shared.thy Mon Mar 16 17:51:24 2009 +0100
9.2 +++ b/src/HOL/Auth/Shared.thy Mon Mar 16 18:24:30 2009 +0100
9.3 @@ -238,7 +238,7 @@
9.4 (*Specialized methods*)
9.5
9.6 method_setup analz_freshK = {*
9.7 - Method.ctxt_args (fn ctxt =>
9.8 + Scan.succeed (fn ctxt =>
9.9 (SIMPLE_METHOD
9.10 (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
9.11 REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
9.12 @@ -246,11 +246,11 @@
9.13 "for proving the Session Key Compromise theorem"
9.14
9.15 method_setup possibility = {*
9.16 - Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
9.17 + Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
9.18 "for proving possibility theorems"
9.19
9.20 method_setup basic_possibility = {*
9.21 - Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
9.22 + Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
9.23 "for proving possibility theorems"
9.24
9.25 lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
10.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Mon Mar 16 17:51:24 2009 +0100
10.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Mon Mar 16 18:24:30 2009 +0100
10.3 @@ -769,15 +769,15 @@
10.4 *}
10.5
10.6 method_setup prepare = {*
10.7 - Method.no_args (SIMPLE_METHOD ShoupRubin.prepare_tac) *}
10.8 + Scan.succeed (K (SIMPLE_METHOD ShoupRubin.prepare_tac)) *}
10.9 "to launch a few simple facts that'll help the simplifier"
10.10
10.11 method_setup parts_prepare = {*
10.12 - Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
10.13 + Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
10.14 "additional facts to reason about parts"
10.15
10.16 method_setup analz_prepare = {*
10.17 - Method.no_args (SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *}
10.18 + Scan.succeed (K (SIMPLE_METHOD ShoupRubin.analz_prepare_tac)) *}
10.19 "additional facts to reason about analz"
10.20
10.21
10.22 @@ -822,7 +822,7 @@
10.23 done
10.24
10.25 method_setup sc_analz_freshK = {*
10.26 - Method.ctxt_args (fn ctxt =>
10.27 + Scan.succeed (fn ctxt =>
10.28 (SIMPLE_METHOD
10.29 (EVERY [REPEAT_FIRST
10.30 (resolve_tac [allI, ballI, impI]),
11.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Mon Mar 16 17:51:24 2009 +0100
11.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Mon Mar 16 18:24:30 2009 +0100
11.3 @@ -777,15 +777,15 @@
11.4 *}
11.5
11.6 method_setup prepare = {*
11.7 - Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
11.8 + Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
11.9 "to launch a few simple facts that'll help the simplifier"
11.10
11.11 method_setup parts_prepare = {*
11.12 - Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
11.13 + Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
11.14 "additional facts to reason about parts"
11.15
11.16 method_setup analz_prepare = {*
11.17 - Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
11.18 + Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
11.19 "additional facts to reason about analz"
11.20
11.21
11.22 @@ -831,7 +831,7 @@
11.23 done
11.24
11.25 method_setup sc_analz_freshK = {*
11.26 - Method.ctxt_args (fn ctxt =>
11.27 + Scan.succeed (fn ctxt =>
11.28 (SIMPLE_METHOD
11.29 (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
11.30 REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
12.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy Mon Mar 16 17:51:24 2009 +0100
12.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy Mon Mar 16 18:24:30 2009 +0100
12.3 @@ -407,7 +407,7 @@
12.4 (*Specialized methods*)
12.5
12.6 method_setup analz_freshK = {*
12.7 - Method.ctxt_args (fn ctxt =>
12.8 + Scan.succeed (fn ctxt =>
12.9 (SIMPLE_METHOD
12.10 (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
12.11 REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
12.12 @@ -415,12 +415,12 @@
12.13 "for proving the Session Key Compromise theorem"
12.14
12.15 method_setup possibility = {*
12.16 - Method.ctxt_args (fn ctxt =>
12.17 + Scan.succeed (fn ctxt =>
12.18 SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
12.19 "for proving possibility theorems"
12.20
12.21 method_setup basic_possibility = {*
12.22 - Method.ctxt_args (fn ctxt =>
12.23 + Scan.succeed (fn ctxt =>
12.24 SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
12.25 "for proving possibility theorems"
12.26
13.1 --- a/src/HOL/Code_Setup.thy Mon Mar 16 17:51:24 2009 +0100
13.2 +++ b/src/HOL/Code_Setup.thy Mon Mar 16 18:24:30 2009 +0100
13.3 @@ -226,19 +226,19 @@
13.4 *}
13.5
13.6 ML {*
13.7 -fun gen_eval_method conv = Method.ctxt_args (fn ctxt => SIMPLE_METHOD'
13.8 +fun gen_eval_method conv ctxt = SIMPLE_METHOD'
13.9 (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
13.10 - THEN' rtac TrueI))
13.11 + THEN' rtac TrueI)
13.12 *}
13.13
13.14 -method_setup eval = {* gen_eval_method eval_oracle *}
13.15 +method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
13.16 "solve goal by evaluation"
13.17
13.18 -method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
13.19 +method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
13.20 "solve goal by evaluation"
13.21
13.22 -method_setup normalization = {* (Method.no_args o SIMPLE_METHOD')
13.23 - (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
13.24 +method_setup normalization = {*
13.25 + Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
13.26 *} "solve goal by normalization"
13.27
13.28
14.1 --- a/src/HOL/Decision_Procs/Approximation.thy Mon Mar 16 17:51:24 2009 +0100
14.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Mon Mar 16 18:24:30 2009 +0100
14.3 @@ -2496,16 +2496,15 @@
14.4
14.5 *}
14.6
14.7 -method_setup approximation = {* fn src =>
14.8 - Method.syntax Args.term src #>
14.9 - (fn (prec, ctxt) => let
14.10 - in SIMPLE_METHOD' (fn i =>
14.11 +method_setup approximation = {*
14.12 + Args.term >>
14.13 + (fn prec => fn ctxt =>
14.14 + SIMPLE_METHOD' (fn i =>
14.15 (DETERM (reify_uneq ctxt i)
14.16 THEN rule_uneq ctxt prec i
14.17 THEN Simplifier.asm_full_simp_tac bounded_by_simpset i
14.18 THEN (TRY (filter_prems_tac (fn t => false) i))
14.19 - THEN (gen_eval_tac eval_oracle ctxt) i))
14.20 - end)
14.21 + THEN (gen_eval_tac eval_oracle ctxt) i)))
14.22 *} "real number approximation"
14.23
14.24 end
15.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Mar 16 17:51:24 2009 +0100
15.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Mar 16 18:24:30 2009 +0100
15.3 @@ -295,7 +295,7 @@
15.4
15.5 use "~~/src/HOL/Tools/Qelim/langford.ML"
15.6 method_setup dlo = {*
15.7 - Method.ctxt_args (SIMPLE_METHOD' o LangfordQE.dlo_tac)
15.8 + Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac)
15.9 *} "Langford's algorithm for quantifier elimination in dense linear orders"
15.10
15.11
15.12 @@ -546,7 +546,7 @@
15.13 use "~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML"
15.14
15.15 method_setup ferrack = {*
15.16 - Method.ctxt_args (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
15.17 + Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
15.18 *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
15.19
15.20 subsection {* Ferrante and Rackoff algorithm over ordered fields *}
16.1 --- a/src/HOL/Groebner_Basis.thy Mon Mar 16 17:51:24 2009 +0100
16.2 +++ b/src/HOL/Groebner_Basis.thy Mon Mar 16 18:24:30 2009 +0100
16.3 @@ -253,7 +253,7 @@
16.4
16.5
16.6 method_setup sring_norm = {*
16.7 - Method.ctxt_args (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
16.8 + Scan.succeed (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
16.9 *} "semiring normalizer"
16.10
16.11
16.12 @@ -427,10 +427,9 @@
16.13 val any_keyword = keyword addN || keyword delN
16.14 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
16.15 in
16.16 -fn src => Method.syntax
16.17 - ((Scan.optional (keyword addN |-- thms) []) --
16.18 - (Scan.optional (keyword delN |-- thms) [])) src
16.19 - #> (fn ((add_ths, del_ths), ctxt) =>
16.20 + ((Scan.optional (keyword addN |-- thms) []) --
16.21 + (Scan.optional (keyword delN |-- thms) [])) >>
16.22 + (fn (add_ths, del_ths) => fn ctxt =>
16.23 SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
16.24 end
16.25 *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
17.1 --- a/src/HOL/Hoare/Hoare.thy Mon Mar 16 17:51:24 2009 +0100
17.2 +++ b/src/HOL/Hoare/Hoare.thy Mon Mar 16 18:24:30 2009 +0100
17.3 @@ -234,11 +234,11 @@
17.4 use "hoare_tac.ML"
17.5
17.6 method_setup vcg = {*
17.7 - Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
17.8 + Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
17.9 "verification condition generator"
17.10
17.11 method_setup vcg_simp = {*
17.12 - Method.ctxt_args (fn ctxt =>
17.13 + Scan.succeed (fn ctxt =>
17.14 SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
17.15 "verification condition generator plus simplification"
17.16
18.1 --- a/src/HOL/Hoare/HoareAbort.thy Mon Mar 16 17:51:24 2009 +0100
18.2 +++ b/src/HOL/Hoare/HoareAbort.thy Mon Mar 16 18:24:30 2009 +0100
18.3 @@ -246,11 +246,11 @@
18.4 use "hoare_tac.ML"
18.5
18.6 method_setup vcg = {*
18.7 - Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
18.8 + Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
18.9 "verification condition generator"
18.10
18.11 method_setup vcg_simp = {*
18.12 - Method.ctxt_args (fn ctxt =>
18.13 + Scan.succeed (fn ctxt =>
18.14 SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
18.15 "verification condition generator plus simplification"
18.16
19.1 --- a/src/HOL/HoareParallel/OG_Tactics.thy Mon Mar 16 17:51:24 2009 +0100
19.2 +++ b/src/HOL/HoareParallel/OG_Tactics.thy Mon Mar 16 18:24:30 2009 +0100
19.3 @@ -465,21 +465,21 @@
19.4 Isabelle proofs. *}
19.5
19.6 method_setup oghoare = {*
19.7 - Method.no_args (SIMPLE_METHOD' oghoare_tac) *}
19.8 + Scan.succeed (K (SIMPLE_METHOD' oghoare_tac)) *}
19.9 "verification condition generator for the oghoare logic"
19.10
19.11 method_setup annhoare = {*
19.12 - Method.no_args (SIMPLE_METHOD' annhoare_tac) *}
19.13 + Scan.succeed (K (SIMPLE_METHOD' annhoare_tac)) *}
19.14 "verification condition generator for the ann_hoare logic"
19.15
19.16 method_setup interfree_aux = {*
19.17 - Method.no_args (SIMPLE_METHOD' interfree_aux_tac) *}
19.18 + Scan.succeed (K (SIMPLE_METHOD' interfree_aux_tac)) *}
19.19 "verification condition generator for interference freedom tests"
19.20
19.21 text {* Tactics useful for dealing with the generated verification conditions: *}
19.22
19.23 method_setup conjI_tac = {*
19.24 - Method.no_args (SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
19.25 + Scan.succeed (K (SIMPLE_METHOD' (conjI_Tac (K all_tac)))) *}
19.26 "verification condition generator for interference freedom tests"
19.27
19.28 ML {*
19.29 @@ -490,7 +490,7 @@
19.30 *}
19.31
19.32 method_setup disjE_tac = {*
19.33 - Method.no_args (SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
19.34 + Scan.succeed (K (SIMPLE_METHOD' (disjE_Tac (K all_tac)))) *}
19.35 "verification condition generator for interference freedom tests"
19.36
19.37 end
20.1 --- a/src/HOL/Isar_examples/Hoare.thy Mon Mar 16 17:51:24 2009 +0100
20.2 +++ b/src/HOL/Isar_examples/Hoare.thy Mon Mar 16 18:24:30 2009 +0100
20.3 @@ -454,7 +454,7 @@
20.4 use "~~/src/HOL/Hoare/hoare_tac.ML"
20.5
20.6 method_setup hoare = {*
20.7 - Method.ctxt_args (fn ctxt =>
20.8 + Scan.succeed (fn ctxt =>
20.9 (SIMPLE_METHOD'
20.10 (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *}
20.11 "verification condition generator for Hoare logic"
21.1 --- a/src/HOL/Library/Euclidean_Space.thy Mon Mar 16 17:51:24 2009 +0100
21.2 +++ b/src/HOL/Library/Euclidean_Space.thy Mon Mar 16 18:24:30 2009 +0100
21.3 @@ -134,8 +134,8 @@
21.4 (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *)
21.5 THEN' asm_full_simp_tac (ss2 addsimps ths)
21.6 in
21.7 - Method.thms_args (SIMPLE_METHOD' o vector_arith_tac)
21.8 -end
21.9 + Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))
21.10 + end
21.11 *} "Lifts trivial vector statements to real arith statements"
21.12
21.13 lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)
21.14 @@ -948,7 +948,7 @@
21.15
21.16 use "normarith.ML"
21.17
21.18 -method_setup norm = {* Method.ctxt_args (SIMPLE_METHOD' o NormArith.norm_arith_tac)
21.19 +method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
21.20 *} "Proves simple linear statements about vector norms"
21.21
21.22
22.1 --- a/src/HOL/Library/Eval_Witness.thy Mon Mar 16 17:51:24 2009 +0100
22.2 +++ b/src/HOL/Library/Eval_Witness.thy Mon Mar 16 18:24:30 2009 +0100
22.3 @@ -1,7 +1,5 @@
22.4 (* Title: HOL/Library/Eval_Witness.thy
22.5 - ID: $Id$
22.6 Author: Alexander Krauss, TU Muenchen
22.7 -
22.8 *)
22.9
22.10 header {* Evaluation Oracle with ML witnesses *}
22.11 @@ -78,15 +76,10 @@
22.12
22.13
22.14 method_setup eval_witness = {*
22.15 -let
22.16 -
22.17 -fun eval_tac ws = CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)
22.18 -
22.19 -in
22.20 - Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
22.21 - SIMPLE_METHOD' (eval_tac ws))
22.22 -end
22.23 -*} "Evaluation with ML witnesses"
22.24 + Scan.lift (Scan.repeat Args.name) >>
22.25 + (fn ws => K (SIMPLE_METHOD'
22.26 + (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
22.27 +*} "evaluation with ML witnesses"
22.28
22.29
22.30 subsection {* Toy Examples *}
23.1 --- a/src/HOL/Library/Reflection.thy Mon Mar 16 17:51:24 2009 +0100
23.2 +++ b/src/HOL/Library/Reflection.thy Mon Mar 16 18:24:30 2009 +0100
23.3 @@ -16,10 +16,10 @@
23.4
23.5 use "reflection.ML"
23.6
23.7 -method_setup reify = {* fn src =>
23.8 - Method.syntax (Attrib.thms --
23.9 - Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
23.10 - (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
23.11 +method_setup reify = {*
23.12 + Attrib.thms --
23.13 + Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
23.14 + (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
23.15 *} "partial automatic reification"
23.16
23.17 method_setup reflection = {*
23.18 @@ -30,16 +30,17 @@
23.19 val any_keyword = keyword onlyN || keyword rulesN;
23.20 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
23.21 val terms = thms >> map (term_of o Drule.dest_term);
23.22 - fun optional scan = Scan.optional scan [];
23.23 -in fn src =>
23.24 - Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #>
23.25 - (fn (((eqs,ths),to), ctxt) =>
23.26 - let
23.27 - val (ceqs,cths) = Reify_Data.get ctxt
23.28 - val corr_thms = ths@cths
23.29 - val raw_eqs = eqs@ceqs
23.30 - in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to)
23.31 - end) end
23.32 -*} "reflection method"
23.33 +in
23.34 + thms --
23.35 + Scan.optional (keyword rulesN |-- thms) [] --
23.36 + Scan.option (keyword onlyN |-- Args.term) >>
23.37 + (fn ((eqs,ths),to) => fn ctxt =>
23.38 + let
23.39 + val (ceqs,cths) = Reify_Data.get ctxt
23.40 + val corr_thms = ths@cths
23.41 + val raw_eqs = eqs@ceqs
23.42 + in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
23.43 +end
23.44 +*} "reflection"
23.45
23.46 end
24.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy Mon Mar 16 17:51:24 2009 +0100
24.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Mar 16 18:24:30 2009 +0100
24.3 @@ -978,9 +978,8 @@
24.4 val ss1 = HOL_basic_ss addsimps [@{thm expand_fun_eq} RS sym]
24.5 val ss2 = HOL_basic_ss addsimps [@{thm mknet_inverse'}]
24.6 fun tac ths = ObjectLogic.full_atomize_tac THEN' Simplifier.simp_tac (ss1 addsimps ths) THEN' Simplifier.asm_full_simp_tac ss2
24.7 - in Method.thms_args (SIMPLE_METHOD' o tac) end
24.8 -
24.9 -*} "Reduces goals about net"
24.10 + in Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (tac ths))) end
24.11 +*} "reduces goals about net"
24.12
24.13 lemma at: "\<And>x y. netord (at a) x y \<longleftrightarrow> 0 < dist x a \<and> dist x a <= dist y a"
24.14 apply (net at_def)
25.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML Mon Mar 16 17:51:24 2009 +0100
25.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Mon Mar 16 18:24:30 2009 +0100
25.3 @@ -199,9 +199,10 @@
25.4 (Args.parens (Args.$$$ "no_asm") >> (K true)) ||
25.5 (Scan.succeed false);
25.6
25.7 -val setup_generate_fresh =
25.8 - Method.goal_args_ctxt' Args.tyname (fn ctxt => generate_fresh_tac)
25.9 +fun setup_generate_fresh x =
25.10 + (Args.goal_spec -- Args.tyname >>
25.11 + (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
25.12
25.13 -val setup_fresh_fun_simp =
25.14 - Method.simple_args options_syntax
25.15 - (fn b => fn _ => SIMPLE_METHOD (fresh_fun_tac b 1))
25.16 +fun setup_fresh_fun_simp x =
25.17 + (Scan.lift options_syntax >> (fn b => K (SIMPLE_METHOD' (fresh_fun_tac b)))) x;
25.18 +
26.1 --- a/src/HOL/Nominal/nominal_induct.ML Mon Mar 16 17:51:24 2009 +0100
26.2 +++ b/src/HOL/Nominal/nominal_induct.ML Mon Mar 16 18:24:30 2009 +0100
26.3 @@ -8,7 +8,7 @@
26.4 val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
26.5 (string * typ) list -> (string * typ) list list -> thm list ->
26.6 thm list -> int -> RuleCases.cases_tactic
26.7 - val nominal_induct_method: Method.src -> Proof.context -> Proof.method
26.8 + val nominal_induct_method: (Proof.context -> Proof.method) context_parser
26.9 end =
26.10 struct
26.11
26.12 @@ -152,11 +152,10 @@
26.13
26.14 in
26.15
26.16 -fun nominal_induct_method src =
26.17 - Method.syntax
26.18 - (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
26.19 - avoiding -- fixing -- rule_spec) src
26.20 - #> (fn ((((x, y), z), w), ctxt) =>
26.21 +val nominal_induct_method =
26.22 + P.and_list' (Scan.repeat (unless_more_args def_inst)) --
26.23 + avoiding -- fixing -- rule_spec >>
26.24 + (fn (((x, y), z), w) => fn ctxt =>
26.25 RAW_METHOD_CASES (fn facts =>
26.26 HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
26.27
27.1 --- a/src/HOL/Nominal/nominal_permeq.ML Mon Mar 16 17:51:24 2009 +0100
27.2 +++ b/src/HOL/Nominal/nominal_permeq.ML Mon Mar 16 18:24:30 2009 +0100
27.3 @@ -1,5 +1,4 @@
27.4 (* Title: HOL/Nominal/nominal_permeq.ML
27.5 - ID: $Id$
27.6 Authors: Christian Urban, Julien Narboux, TU Muenchen
27.7
27.8 Methods for simplifying permutations and
27.9 @@ -36,16 +35,16 @@
27.10 val finite_guess_tac : simpset -> int -> tactic
27.11 val fresh_guess_tac : simpset -> int -> tactic
27.12
27.13 - val perm_simp_meth : Method.src -> Proof.context -> Proof.method
27.14 - val perm_simp_meth_debug : Method.src -> Proof.context -> Proof.method
27.15 - val perm_extend_simp_meth : Method.src -> Proof.context -> Proof.method
27.16 - val perm_extend_simp_meth_debug : Method.src -> Proof.context -> Proof.method
27.17 - val supports_meth : Method.src -> Proof.context -> Proof.method
27.18 - val supports_meth_debug : Method.src -> Proof.context -> Proof.method
27.19 - val finite_guess_meth : Method.src -> Proof.context -> Proof.method
27.20 - val finite_guess_meth_debug : Method.src -> Proof.context -> Proof.method
27.21 - val fresh_guess_meth : Method.src -> Proof.context -> Proof.method
27.22 - val fresh_guess_meth_debug : Method.src -> Proof.context -> Proof.method
27.23 + val perm_simp_meth : (Proof.context -> Proof.method) context_parser
27.24 + val perm_simp_meth_debug : (Proof.context -> Proof.method) context_parser
27.25 + val perm_extend_simp_meth : (Proof.context -> Proof.method) context_parser
27.26 + val perm_extend_simp_meth_debug : (Proof.context -> Proof.method) context_parser
27.27 + val supports_meth : (Proof.context -> Proof.method) context_parser
27.28 + val supports_meth_debug : (Proof.context -> Proof.method) context_parser
27.29 + val finite_guess_meth : (Proof.context -> Proof.method) context_parser
27.30 + val finite_guess_meth_debug : (Proof.context -> Proof.method) context_parser
27.31 + val fresh_guess_meth : (Proof.context -> Proof.method) context_parser
27.32 + val fresh_guess_meth_debug : (Proof.context -> Proof.method) context_parser
27.33 end
27.34
27.35 structure NominalPermeq : NOMINAL_PERMEQ =
27.36 @@ -400,26 +399,24 @@
27.37 Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac) ||
27.38 Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
27.39
27.40 -fun perm_simp_method (prems, tac) ctxt = METHOD (fn facts =>
27.41 - HEADGOAL (Method.insert_tac (prems @ facts) THEN'
27.42 - ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
27.43 -
27.44 -val perm_simp_meth = Method.sectioned_args
27.45 - (Args.bang_facts -- Scan.lift perm_simp_options)
27.46 - (Simplifier.simp_modifiers') perm_simp_method
27.47 +val perm_simp_meth =
27.48 + Args.bang_facts -- Scan.lift perm_simp_options --|
27.49 + Method.sections (Simplifier.simp_modifiers') >>
27.50 + (fn (prems, tac) => fn ctxt => METHOD (fn facts =>
27.51 + HEADGOAL (Method.insert_tac (prems @ facts) THEN'
27.52 + (CHANGED_PROP oo tac) (local_simpset_of ctxt))));
27.53
27.54 (* setup so that the simpset is used which is active at the moment when the tactic is called *)
27.55 fun local_simp_meth_setup tac =
27.56 - Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
27.57 - (SIMPLE_METHOD' o tac o local_simpset_of) ;
27.58 + Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
27.59 + (K (SIMPLE_METHOD' o tac o local_simpset_of));
27.60
27.61 (* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
27.62
27.63 fun basic_simp_meth_setup debug tac =
27.64 - Method.sectioned_args
27.65 - (fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l)))
27.66 - (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
27.67 - (fn _ => SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
27.68 + Scan.depend (fn ctxt => Scan.succeed (Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt, ())) --
27.69 + Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
27.70 + (K (SIMPLE_METHOD' o (fn ss => if debug then tac ss else SOLVEI (tac ss)) o local_simpset_of));
27.71
27.72 val perm_simp_meth_debug = local_simp_meth_setup dperm_simp_tac;
27.73 val perm_extend_simp_meth = local_simp_meth_setup perm_extend_simp_tac;
28.1 --- a/src/HOL/Presburger.thy Mon Mar 16 17:51:24 2009 +0100
28.2 +++ b/src/HOL/Presburger.thy Mon Mar 16 18:24:30 2009 +0100
28.3 @@ -455,12 +455,11 @@
28.4 val any_keyword = keyword addN || keyword delN || simple_keyword elimN
28.5 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
28.6 in
28.7 - fn src => Method.syntax
28.8 - ((Scan.optional (simple_keyword elimN >> K false) true) --
28.9 - (Scan.optional (keyword addN |-- thms) []) --
28.10 - (Scan.optional (keyword delN |-- thms) [])) src
28.11 - #> (fn (((elim, add_ths), del_ths),ctxt) =>
28.12 - SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
28.13 + Scan.optional (simple_keyword elimN >> K false) true --
28.14 + Scan.optional (keyword addN |-- thms) [] --
28.15 + Scan.optional (keyword delN |-- thms) [] >>
28.16 + (fn ((elim, add_ths), del_ths) => fn ctxt =>
28.17 + SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
28.18 end
28.19 *} "Cooper's algorithm for Presburger arithmetic"
28.20
29.1 --- a/src/HOL/Prolog/HOHH.thy Mon Mar 16 17:51:24 2009 +0100
29.2 +++ b/src/HOL/Prolog/HOHH.thy Mon Mar 16 18:24:30 2009 +0100
29.3 @@ -11,11 +11,11 @@
29.4 begin
29.5
29.6 method_setup ptac =
29.7 - {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
29.8 + {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
29.9 "Basic Lambda Prolog interpreter"
29.10
29.11 method_setup prolog =
29.12 - {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
29.13 + {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
29.14 "Lambda Prolog interpreter"
29.15
29.16 consts
30.1 --- a/src/HOL/SAT.thy Mon Mar 16 17:51:24 2009 +0100
30.2 +++ b/src/HOL/SAT.thy Mon Mar 16 18:24:30 2009 +0100
30.3 @@ -1,5 +1,4 @@
30.4 (* Title: HOL/SAT.thy
30.5 - ID: $Id$
30.6 Author: Alwen Tiu, Tjark Weber
30.7 Copyright 2005
30.8
30.9 @@ -28,10 +27,10 @@
30.10
30.11 ML {* structure sat = SATFunc(structure cnf = cnf); *}
30.12
30.13 -method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *}
30.14 +method_setup sat = {* Scan.succeed (K (SIMPLE_METHOD' sat.sat_tac)) *}
30.15 "SAT solver"
30.16
30.17 -method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *}
30.18 +method_setup satx = {* Scan.succeed (K (SIMPLE_METHOD' sat.satx_tac)) *}
30.19 "SAT solver (with definitional CNF)"
30.20
30.21 end
31.1 --- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Mon Mar 16 17:51:24 2009 +0100
31.2 +++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Mon Mar 16 18:24:30 2009 +0100
31.3 @@ -541,10 +541,11 @@
31.4 by (blast intro: analz_mono [THEN [2] rev_subsetD])
31.5
31.6 method_setup valid_certificate_tac = {*
31.7 - Method.goal_args (Scan.succeed ()) (fn () => fn i =>
31.8 - EVERY [ftac @{thm Gets_certificate_valid} i,
31.9 - assume_tac i,
31.10 - etac conjE i, REPEAT (hyp_subst_tac i)])
31.11 + Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant
31.12 + (fn i =>
31.13 + EVERY [ftac @{thm Gets_certificate_valid} i,
31.14 + assume_tac i,
31.15 + etac conjE i, REPEAT (hyp_subst_tac i)])))
31.16 *} ""
31.17
31.18 text{*The @{text "(no_asm)"} attribute is essential, since it retains
32.1 --- a/src/HOL/SET-Protocol/EventSET.thy Mon Mar 16 17:51:24 2009 +0100
32.2 +++ b/src/HOL/SET-Protocol/EventSET.thy Mon Mar 16 18:24:30 2009 +0100
32.3 @@ -189,7 +189,7 @@
32.4 *}
32.5
32.6 method_setup analz_mono_contra = {*
32.7 - Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
32.8 + Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
32.9 "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
32.10
32.11 end
33.1 --- a/src/HOL/SET-Protocol/MessageSET.thy Mon Mar 16 17:51:24 2009 +0100
33.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy Mon Mar 16 18:24:30 2009 +0100
33.3 @@ -940,17 +940,17 @@
33.4 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
33.5
33.6 method_setup spy_analz = {*
33.7 - Method.ctxt_args (fn ctxt =>
33.8 + Scan.succeed (fn ctxt =>
33.9 SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
33.10 "for proving the Fake case when analz is involved"
33.11
33.12 method_setup atomic_spy_analz = {*
33.13 - Method.ctxt_args (fn ctxt =>
33.14 + Scan.succeed (fn ctxt =>
33.15 SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
33.16 "for debugging spy_analz"
33.17
33.18 method_setup Fake_insert_simp = {*
33.19 - Method.ctxt_args (fn ctxt =>
33.20 + Scan.succeed (fn ctxt =>
33.21 SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
33.22 "for debugging spy_analz"
33.23
34.1 --- a/src/HOL/SET-Protocol/PublicSET.thy Mon Mar 16 17:51:24 2009 +0100
34.2 +++ b/src/HOL/SET-Protocol/PublicSET.thy Mon Mar 16 18:24:30 2009 +0100
34.3 @@ -371,7 +371,7 @@
34.4 *}
34.5
34.6 method_setup possibility = {*
34.7 - Method.ctxt_args (fn ctxt =>
34.8 + Scan.succeed (fn ctxt =>
34.9 SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
34.10 "for proving possibility theorems"
34.11
35.1 --- a/src/HOL/SET-Protocol/Purchase.thy Mon Mar 16 17:51:24 2009 +0100
35.2 +++ b/src/HOL/SET-Protocol/Purchase.thy Mon Mar 16 18:24:30 2009 +0100
35.3 @@ -477,9 +477,10 @@
35.4 by (frule Gets_imp_Says, auto)
35.5
35.6 method_setup valid_certificate_tac = {*
35.7 - Method.goal_args (Scan.succeed ()) (fn () => fn i =>
35.8 - EVERY [ftac @{thm Gets_certificate_valid} i,
35.9 - assume_tac i, REPEAT (hyp_subst_tac i)])
35.10 + Args.goal_spec >> (fn quant =>
35.11 + K (SIMPLE_METHOD'' quant (fn i =>
35.12 + EVERY [ftac @{thm Gets_certificate_valid} i,
35.13 + assume_tac i, REPEAT (hyp_subst_tac i)])))
35.14 *} ""
35.15
35.16
36.1 --- a/src/HOL/Transitive_Closure.thy Mon Mar 16 17:51:24 2009 +0100
36.2 +++ b/src/HOL/Transitive_Closure.thy Mon Mar 16 18:24:30 2009 +0100
36.3 @@ -695,16 +695,16 @@
36.4 (* Optional methods *)
36.5
36.6 method_setup trancl =
36.7 - {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
36.8 + {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.trancl_tac)) *}
36.9 {* simple transitivity reasoner *}
36.10 method_setup rtrancl =
36.11 - {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
36.12 + {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac)) *}
36.13 {* simple transitivity reasoner *}
36.14 method_setup tranclp =
36.15 - {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
36.16 + {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.trancl_tac)) *}
36.17 {* simple transitivity reasoner (predicate version) *}
36.18 method_setup rtranclp =
36.19 - {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
36.20 + {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac)) *}
36.21 {* simple transitivity reasoner (predicate version) *}
36.22
36.23 end
37.1 --- a/src/HOL/UNITY/Comp/Alloc.thy Mon Mar 16 17:51:24 2009 +0100
37.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Mar 16 18:24:30 2009 +0100
37.3 @@ -321,7 +321,7 @@
37.4 *}
37.5
37.6 method_setup record_auto = {*
37.7 - Method.ctxt_args (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
37.8 + Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
37.9 *} ""
37.10
37.11 lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
37.12 @@ -713,7 +713,7 @@
37.13 *}
37.14
37.15 method_setup rename_client_map = {*
37.16 - Method.ctxt_args (fn ctxt =>
37.17 + Scan.succeed (fn ctxt =>
37.18 SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
37.19 *} ""
37.20
38.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Mon Mar 16 17:51:24 2009 +0100
38.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Mon Mar 16 18:24:30 2009 +0100
38.3 @@ -124,7 +124,7 @@
38.4 *}
38.5
38.6 method_setup ns_induct = {*
38.7 - Method.ctxt_args (fn ctxt =>
38.8 + Scan.succeed (fn ctxt =>
38.9 SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
38.10 "for inductive reasoning about the Needham-Schroeder protocol"
38.11
39.1 --- a/src/HOL/UNITY/UNITY_Main.thy Mon Mar 16 17:51:24 2009 +0100
39.2 +++ b/src/HOL/UNITY/UNITY_Main.thy Mon Mar 16 18:24:30 2009 +0100
39.3 @@ -10,15 +10,13 @@
39.4 uses "UNITY_tactics.ML" begin
39.5
39.6 method_setup safety = {*
39.7 - Method.ctxt_args (fn ctxt =>
39.8 + Scan.succeed (fn ctxt =>
39.9 SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
39.10 "for proving safety properties"
39.11
39.12 method_setup ensures_tac = {*
39.13 - fn args => fn ctxt =>
39.14 - Method.goal_args' (Scan.lift Args.name_source)
39.15 - (ensures_tac (local_clasimpset_of ctxt))
39.16 - args ctxt *}
39.17 - "for proving progress properties"
39.18 + Args.goal_spec -- Scan.lift Args.name_source >>
39.19 + (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (local_clasimpset_of ctxt) s))
39.20 +*} "for proving progress properties"
39.21
39.22 end
40.1 --- a/src/HOL/Word/WordArith.thy Mon Mar 16 17:51:24 2009 +0100
40.2 +++ b/src/HOL/Word/WordArith.thy Mon Mar 16 18:24:30 2009 +0100
40.3 @@ -530,7 +530,7 @@
40.4 *}
40.5
40.6 method_setup uint_arith =
40.7 - "Method.ctxt_args (SIMPLE_METHOD' o uint_arith_tac)"
40.8 + {* Scan.succeed (SIMPLE_METHOD' o uint_arith_tac) *}
40.9 "solving word arithmetic via integers and arith"
40.10
40.11
40.12 @@ -1086,7 +1086,7 @@
40.13 *}
40.14
40.15 method_setup unat_arith =
40.16 - "Method.ctxt_args (SIMPLE_METHOD' o unat_arith_tac)"
40.17 + {* Scan.succeed (SIMPLE_METHOD' o unat_arith_tac) *}
40.18 "solving word arithmetic via natural numbers and arith"
40.19
40.20 lemma no_plus_overflow_unat_size:
41.1 --- a/src/HOL/ex/Binary.thy Mon Mar 16 17:51:24 2009 +0100
41.2 +++ b/src/HOL/ex/Binary.thy Mon Mar 16 18:24:30 2009 +0100
41.3 @@ -174,7 +174,7 @@
41.4 simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}
41.5
41.6 method_setup binary_simp = {*
41.7 - Method.no_args (SIMPLE_METHOD'
41.8 + Scan.succeed (K (SIMPLE_METHOD'
41.9 (full_simp_tac
41.10 (HOL_basic_ss
41.11 addsimps @{thms binary_simps}
41.12 @@ -183,7 +183,7 @@
41.13 @{simproc binary_nat_less},
41.14 @{simproc binary_nat_diff},
41.15 @{simproc binary_nat_div},
41.16 - @{simproc binary_nat_mod}])))
41.17 + @{simproc binary_nat_mod}]))))
41.18 *} "binary simplification"
41.19
41.20
42.1 --- a/src/HOL/ex/SAT_Examples.thy Mon Mar 16 17:51:24 2009 +0100
42.2 +++ b/src/HOL/ex/SAT_Examples.thy Mon Mar 16 18:24:30 2009 +0100
42.3 @@ -83,7 +83,7 @@
42.4 ML {* reset quick_and_dirty; *}
42.5
42.6 method_setup rawsat =
42.7 - {* Method.no_args (SIMPLE_METHOD' sat.rawsat_tac) *}
42.8 + {* Scan.succeed (K (SIMPLE_METHOD' sat.rawsat_tac)) *}
42.9 "SAT solver (no preprocessing)"
42.10
42.11 (* ML {* Toplevel.profiling := 1; *} *)
43.1 --- a/src/Sequents/ILL.thy Mon Mar 16 17:51:24 2009 +0100
43.2 +++ b/src/Sequents/ILL.thy Mon Mar 16 18:24:30 2009 +0100
43.3 @@ -146,7 +146,7 @@
43.4 *}
43.5
43.6 method_setup best_lazy =
43.7 - {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *}
43.8 + {* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *}
43.9 "lazy classical reasoning"
43.10
43.11 lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
43.12 @@ -282,10 +282,10 @@
43.13
43.14
43.15 method_setup best_safe =
43.16 - {* Method.no_args (SIMPLE_METHOD' (best_tac safe_cs)) *} ""
43.17 + {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} ""
43.18
43.19 method_setup best_power =
43.20 - {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} ""
43.21 + {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} ""
43.22
43.23
43.24 (* Some examples from Troelstra and van Dalen *)
44.1 --- a/src/Sequents/LK0.thy Mon Mar 16 17:51:24 2009 +0100
44.2 +++ b/src/Sequents/LK0.thy Mon Mar 16 18:24:30 2009 +0100
44.3 @@ -240,23 +240,23 @@
44.4 *}
44.5
44.6 method_setup fast_prop =
44.7 - {* Method.no_args (SIMPLE_METHOD' (fast_tac prop_pack)) *}
44.8 + {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *}
44.9 "propositional reasoning"
44.10
44.11 method_setup fast =
44.12 - {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_pack)) *}
44.13 + {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *}
44.14 "classical reasoning"
44.15
44.16 method_setup fast_dup =
44.17 - {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
44.18 + {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *}
44.19 "classical reasoning"
44.20
44.21 method_setup best =
44.22 - {* Method.no_args (SIMPLE_METHOD' (best_tac LK_pack)) *}
44.23 + {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *}
44.24 "classical reasoning"
44.25
44.26 method_setup best_dup =
44.27 - {* Method.no_args (SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
44.28 + {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *}
44.29 "classical reasoning"
44.30
44.31
45.1 --- a/src/Sequents/S4.thy Mon Mar 16 17:51:24 2009 +0100
45.2 +++ b/src/Sequents/S4.thy Mon Mar 16 18:24:30 2009 +0100
45.3 @@ -45,7 +45,7 @@
45.4 *}
45.5
45.6 method_setup S4_solve =
45.7 - {* Method.no_args (SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
45.8 + {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *} "S4 solver"
45.9
45.10
45.11 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
46.1 --- a/src/Sequents/S43.thy Mon Mar 16 17:51:24 2009 +0100
46.2 +++ b/src/Sequents/S43.thy Mon Mar 16 18:24:30 2009 +0100
46.3 @@ -92,8 +92,8 @@
46.4
46.5
46.6 method_setup S43_solve = {*
46.7 - Method.no_args (SIMPLE_METHOD
46.8 - (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))
46.9 + Scan.succeed (K (SIMPLE_METHOD
46.10 + (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
46.11 *} "S4 solver"
46.12
46.13
47.1 --- a/src/Sequents/T.thy Mon Mar 16 17:51:24 2009 +0100
47.2 +++ b/src/Sequents/T.thy Mon Mar 16 18:24:30 2009 +0100
47.3 @@ -44,7 +44,7 @@
47.4 *}
47.5
47.6 method_setup T_solve =
47.7 - {* Method.no_args (SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
47.8 + {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *} "T solver"
47.9
47.10
47.11 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
48.1 --- a/src/ZF/UNITY/Constrains.thy Mon Mar 16 17:51:24 2009 +0100
48.2 +++ b/src/ZF/UNITY/Constrains.thy Mon Mar 16 18:24:30 2009 +0100
48.3 @@ -496,11 +496,11 @@
48.4 setup ProgramDefs.setup
48.5
48.6 method_setup safety = {*
48.7 - Method.ctxt_args (SIMPLE_METHOD' o constrains_tac) *}
48.8 + Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
48.9 "for proving safety properties"
48.10
48.11 method_setup always = {*
48.12 - Method.ctxt_args (SIMPLE_METHOD' o always_tac) *}
48.13 + Scan.succeed (SIMPLE_METHOD' o always_tac) *}
48.14 "for proving invariants"
48.15
48.16 end
49.1 --- a/src/ZF/UNITY/SubstAx.thy Mon Mar 16 17:51:24 2009 +0100
49.2 +++ b/src/ZF/UNITY/SubstAx.thy Mon Mar 16 18:24:30 2009 +0100
49.3 @@ -377,9 +377,8 @@
49.4 *}
49.5
49.6 method_setup ensures_tac = {*
49.7 - fn args => fn ctxt =>
49.8 - Method.goal_args' (Scan.lift Args.name_source) (ensures_tac ctxt)
49.9 - args ctxt *}
49.10 - "for proving progress properties"
49.11 + Args.goal_spec -- Scan.lift Args.name_source >>
49.12 + (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
49.13 +*} "for proving progress properties"
49.14
49.15 end