--- a/src/HOL/Decision_Procs/cooper_tac.ML Wed May 27 22:11:06 2009 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed May 27 22:20:29 2009 +0200
@@ -2,7 +2,14 @@
Author: Amine Chaieb, TU Muenchen
*)
-structure Cooper_Tac =
+signature COOPER_TAC =
+sig
+ val trace: bool ref
+ val linz_tac: Proof.context -> bool -> int -> tactic
+ val setup: theory -> theory
+end
+
+structure Cooper_Tac: COOPER_TAC =
struct
val trace = ref false;
@@ -33,7 +40,7 @@
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
-fun prepare_for_linz q fm =
+fun prepare_for_linz q fm =
let
val ps = Logic.strip_params fm
val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
@@ -66,8 +73,8 @@
(* Transform the term*)
val (t,np,nh) = prepare_for_linz q g
(* Some simpsets for dealing with mod div abs and nat*)
- val mod_div_simpset = HOL_basic_ss
- addsimps [refl,mod_add_eq, mod_add_left_eq,
+ val mod_div_simpset = HOL_basic_ss
+ addsimps [refl,mod_add_eq, mod_add_left_eq,
mod_add_right_eq,
nat_div_add_eq, int_div_add_eq,
@{thm mod_self}, @{thm "zmod_self"},
@@ -105,30 +112,24 @@
val (th, tac) = case (prop_of pre_thm) of
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
- in
+ in
((pth RS iffD2) RS pre_thm,
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
end
| _ => (pre_thm, assm_tac i)
- in (rtac (((mp_step nh) o (spec_step np)) th) i
+ in (rtac (((mp_step nh) o (spec_step np)) th) i
THEN tac) st
end handle Subscript => no_tac st);
-fun linz_args meth =
- let val parse_flag =
- Args.$$$ "no_quantify" >> (K (K false));
- in
- Method.simple_args
- (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
- curry (Library.foldl op |>) true)
- (fn q => fn ctxt => meth ctxt q)
- end;
-
-fun linz_method ctxt q = SIMPLE_METHOD' (linz_tac ctxt q);
-
val setup =
- Method.add_method ("cooper",
- linz_args linz_method,
- "decision procedure for linear integer arithmetic");
+ 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
--- a/src/HOL/Decision_Procs/mir_tac.ML Wed May 27 22:11:06 2009 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed May 27 22:20:29 2009 +0200
@@ -2,6 +2,13 @@
Author: Amine Chaieb, TU Muenchen
*)
+signature MIR_TAC =
+sig
+ val trace: bool ref
+ val mir_tac: Proof.context -> bool -> int -> tactic
+ val setup: theory -> theory
+end
+
structure Mir_Tac =
struct
@@ -82,9 +89,9 @@
fun mir_tac ctxt q i =
- (ObjectLogic.atomize_prems_tac i)
- THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
- THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
+ ObjectLogic.atomize_prems_tac i
+ THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i
+ THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)
THEN (fn st =>
let
val g = List.nth (prems_of st, i - 1)
@@ -143,22 +150,15 @@
THEN tac) st
end handle Subscript => no_tac st);
-fun mir_args meth =
- let val parse_flag =
- Args.$$$ "no_quantify" >> (K (K false));
- in
- Method.simple_args
- (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
- curry (Library.foldl op |>) true)
- (fn q => fn ctxt => meth ctxt q)
- end;
-
-fun mir_method ctxt q = SIMPLE_METHOD' (mir_tac ctxt q);
-
val setup =
- Method.add_method ("mir",
- mir_args mir_method,
- "decision procedure for MIR arithmetic");
-
+ 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
--- a/src/HOL/Import/import_package.ML Wed May 27 22:11:06 2009 +0200
+++ b/src/HOL/Import/import_package.ML Wed May 27 22:20:29 2009 +0200
@@ -1,13 +1,12 @@
(* Title: HOL/Import/import_package.ML
- ID: $Id$
Author: Sebastian Skalberg (TU Muenchen)
*)
signature IMPORT_PACKAGE =
sig
- val import_meth: Method.src -> Proof.context -> Proof.method
+ val debug : bool ref
+ val import_tac : Proof.context -> string * string -> tactic
val setup : theory -> theory
- val debug : bool ref
end
structure ImportData = TheoryDataFun
@@ -25,20 +24,16 @@
val debug = ref false
fun message s = if !debug then writeln s else ()
-val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
-val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
-
-fun import_tac (thyname,thmname) =
+fun import_tac ctxt (thyname, thmname) =
if ! quick_and_dirty
- then SkipProof.cheat_tac
+ then SkipProof.cheat_tac (ProofContext.theory_of ctxt)
else
- fn thy =>
fn th =>
let
- val sg = Thm.theory_of_thm th
+ val thy = ProofContext.theory_of ctxt
val prem = hd (prems_of th)
- val _ = message ("Import_tac: thyname="^thyname^", thmname="^thmname)
- val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem)))
+ val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname)
+ val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem)
val int_thms = case ImportData.get thy of
NONE => fst (Replay.setup_int_thms thyname thy)
| SOME a => a
@@ -49,9 +44,9 @@
val thm = equal_elim rew thm
val prew = ProofKernel.rewrite_hol4_term prem thy
val prem' = #2 (Logic.dest_equals (prop_of prew))
- val _ = message ("Import proved " ^ (string_of_thm thm))
+ val _ = message ("Import proved " ^ Display.string_of_thm thm)
val thm = ProofKernel.disambiguate_frees thm
- val _ = message ("Disambiguate: " ^ (string_of_thm thm))
+ val _ = message ("Disambiguate: " ^ Display.string_of_thm thm)
in
case Shuffler.set_prop thy prem' [("",thm)] of
SOME (_,thm) =>
@@ -67,15 +62,10 @@
| NONE => (message "import: set_prop didn't succeed"; no_tac th)
end
-val import_meth = Method.simple_args (Args.name -- Args.name)
- (fn arg =>
- fn ctxt =>
- let
- val thy = ProofContext.theory_of ctxt
- in
- SIMPLE_METHOD (import_tac arg thy)
- end)
+val setup = Method.setup @{binding import}
+ (Scan.lift (Args.name -- Args.name) >>
+ (fn arg => fn ctxt => SIMPLE_METHOD (import_tac ctxt arg)))
+ "import HOL4 theorem"
-val setup = Method.add_method("import",import_meth,"Import HOL4 theorem")
end
--- a/src/HOL/Import/shuffler.ML Wed May 27 22:11:06 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Wed May 27 22:20:29 2009 +0200
@@ -15,10 +15,9 @@
val find_potential: theory -> term -> (string * thm) list
- val gen_shuffle_tac: theory -> bool -> (string * thm) list -> int -> tactic
-
- val shuffle_tac: (string * thm) list -> int -> tactic
- val search_tac : (string * thm) list -> int -> tactic
+ val gen_shuffle_tac: Proof.context -> bool -> (string * thm) list -> int -> tactic
+ val shuffle_tac: Proof.context -> thm list -> int -> tactic
+ val search_tac : Proof.context -> int -> tactic
val print_shuffles: theory -> unit
@@ -631,8 +630,9 @@
List.filter (match_consts ignored t) all_thms
end
-fun gen_shuffle_tac thy search thms i st =
+fun gen_shuffle_tac ctxt search thms i st =
let
+ val thy = ProofContext.theory_of ctxt
val _ = message ("Shuffling " ^ (string_of_thm st))
val t = List.nth(prems_of st,i-1)
val set = set_prop thy t
@@ -646,26 +646,11 @@
else no_tac)) st
end
-fun shuffle_tac thms i st =
- gen_shuffle_tac (the_context()) false thms i st
-
-fun search_tac thms i st =
- gen_shuffle_tac (the_context()) true thms i st
+fun shuffle_tac ctxt thms =
+ gen_shuffle_tac ctxt false (map (pair "") thms);
-fun shuffle_meth (thms:thm list) ctxt =
- let
- val thy = ProofContext.theory_of ctxt
- in
- SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms))
- end
-
-fun search_meth ctxt =
- let
- val thy = ProofContext.theory_of ctxt
- val prems = Assumption.all_prems_of ctxt
- in
- SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
- end
+fun search_tac ctxt =
+ gen_shuffle_tac ctxt true (map (pair "premise") (Assumption.all_prems_of ctxt));
fun add_shuffle_rule thm thy =
let
@@ -680,10 +665,11 @@
val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
val setup =
- Method.add_method ("shuffle_tac",
- Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
- Method.add_method ("search_tac",
- Method.ctxt_args search_meth,"search for suitable theorems") #>
+ Method.setup @{binding shuffle_tac}
+ (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (shuffle_tac ctxt ths)))
+ "solve goal by shuffling terms around" #>
+ Method.setup @{binding search_tac}
+ (Scan.succeed (SIMPLE_METHOD' o search_tac)) "search for suitable theorems" #>
add_shuffle_rule weaken #>
add_shuffle_rule equiv_comm #>
add_shuffle_rule imp_comm #>
--- a/src/HOL/Library/comm_ring.ML Wed May 27 22:11:06 2009 +0200
+++ b/src/HOL/Library/comm_ring.ML Wed May 27 22:20:29 2009 +0200
@@ -100,13 +100,10 @@
THEN (simp_tac cring_ss i)
end);
-val comm_ring_meth =
- Method.ctxt_args (SIMPLE_METHOD' o comm_ring_tac);
-
val setup =
- Method.add_method ("comm_ring", comm_ring_meth,
- "reflective decision procedure for equalities over commutative rings") #>
- Method.add_method ("algebra", comm_ring_meth,
- "method for proving algebraic properties (same as comm_ring)");
+ Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
+ "reflective decision procedure for equalities over commutative rings" #>
+ Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
+ "method for proving algebraic properties (same as comm_ring)";
end;
--- a/src/HOL/Tools/function_package/scnp_reconstruct.ML Wed May 27 22:11:06 2009 +0200
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML Wed May 27 22:20:29 2009 +0200
@@ -416,14 +416,14 @@
(* Method setup *)
val orders =
- (Scan.repeat1
+ Scan.repeat1
((Args.$$$ "max" >> K MAX) ||
(Args.$$$ "min" >> K MIN) ||
(Args.$$$ "ms" >> K MS))
- || Scan.succeed [MAX, MS, MIN])
+ || Scan.succeed [MAX, MS, MIN]
-val setup = Method.add_method
- ("sizechange", Method.sectioned_args (Scan.lift orders) clasimp_modifiers decomp_scnp,
- "termination prover with graph decomposition and the NP subset of size change termination")
+val setup = Method.setup @{binding sizechange}
+ (Scan.lift orders --| Method.sections clasimp_modifiers >> decomp_scnp)
+ "termination prover with graph decomposition and the NP subset of size change termination"
end
--- a/src/HOL/Tools/recdef_package.ML Wed May 27 22:11:06 2009 +0200
+++ b/src/HOL/Tools/recdef_package.ML Wed May 27 22:20:29 2009 +0200
@@ -170,7 +170,7 @@
val ctxt =
(case opt_src of
NONE => ctxt0
- | SOME src => Method.only_sectioned_args recdef_modifiers I src ctxt0);
+ | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
val {simps, congs, wfs} = get_hints ctxt;
val cs = local_claset_of ctxt;
val ss = local_simpset_of ctxt addsimps simps;
--- a/src/Pure/ML/ml_test.ML Wed May 27 22:11:06 2009 +0200
+++ b/src/Pure/ML/ml_test.ML Wed May 27 22:20:29 2009 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/ML/ml_test.ML
Author: Makarius
-Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 719).
+Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 744).
*)
signature ML_TEST =
@@ -44,11 +44,11 @@
(* parse trees *)
-fun report_parse_tree context depth =
+fun report_parse_tree context depth space =
let
val pos_of = position_of (Context.proof_of context);
fun report loc (PTtype types) =
- PolyML.NameSpace.displayTypeExpression (types, depth)
+ PolyML.NameSpace.displayTypeExpression (types, depth, space)
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of
|> Position.report_text Markup.ML_typing (pos_of loc)
| report loc (PTdeclaredAt decl) =
@@ -132,7 +132,7 @@
fun result_fun (phase1, phase2) () =
(case phase1 of NONE => ()
- | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) depth parse_tree;
+ | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) depth space parse_tree;
case phase2 of NONE => error "Static Errors"
| SOME code => apply_result (Toplevel.program code));
--- a/src/Tools/coherent.ML Wed May 27 22:11:06 2009 +0200
+++ b/src/Tools/coherent.ML Wed May 27 22:20:29 2009 +0200
@@ -1,6 +1,6 @@
(* Title: Tools/coherent.ML
Author: Stefan Berghofer, TU Muenchen
- Author: Marc Bezem, Institutt for Informatikk, Universitetet i Bergen
+ Author: Marc Bezem, Institutt for Informatikk, Universitetet i Bergen
Prover for coherent logic, see e.g.
@@ -22,14 +22,15 @@
sig
val verbose: bool ref
val show_facts: bool ref
- val coherent_tac: thm list -> Proof.context -> int -> tactic
- val coherent_meth: thm list -> Proof.context -> Proof.method
+ val coherent_tac: Proof.context -> thm list -> int -> tactic
val setup: theory -> theory
end;
functor CoherentFun(Data: COHERENT_DATA) : COHERENT =
struct
+(** misc tools **)
+
val verbose = ref false;
fun message f = if !verbose then tracing (f ()) else ();
@@ -170,6 +171,7 @@
| SOME prfs => SOME ((params, prf) :: prfs))
end;
+
(** proof replaying **)
fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
@@ -210,7 +212,7 @@
(** external interface **)
-fun coherent_tac rules ctxt = SUBPROOF (fn {prems, concl, params, context, ...} =>
+fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
SUBPROOF (fn {prems = prems', concl, context, ...} =>
let val xs = map term_of params @
@@ -224,10 +226,9 @@
rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1
end) context 1) ctxt;
-fun coherent_meth rules ctxt =
- METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
-
-val setup = Method.add_method
- ("coherent", Method.thms_ctxt_args coherent_meth, "prove coherent formula");
+val setup = Method.setup @{binding coherent}
+ (Attrib.thms >> (fn rules => fn ctxt =>
+ METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
+ "prove coherent formula";
end;