# HG changeset patch # User wenzelm # Date 1243455629 -7200 # Node ID 40c00d6848002d3bd122232cb51a79ed894a9f7d # Parent dcbe1f9fe2cd460de463cb27ee684e57eec11fea# Parent 18085db7b1476aceff33583b92ac0b313d949c03 merged diff -r dcbe1f9fe2cd -r 40c00d684800 src/HOL/Decision_Procs/cooper_tac.ML --- 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 diff -r dcbe1f9fe2cd -r 40c00d684800 src/HOL/Decision_Procs/mir_tac.ML --- 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 diff -r dcbe1f9fe2cd -r 40c00d684800 src/HOL/Import/import_package.ML --- 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 diff -r dcbe1f9fe2cd -r 40c00d684800 src/HOL/Import/shuffler.ML --- 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 #> diff -r dcbe1f9fe2cd -r 40c00d684800 src/HOL/Library/comm_ring.ML --- 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; diff -r dcbe1f9fe2cd -r 40c00d684800 src/HOL/Tools/function_package/scnp_reconstruct.ML --- 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 diff -r dcbe1f9fe2cd -r 40c00d684800 src/HOL/Tools/recdef_package.ML --- 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; diff -r dcbe1f9fe2cd -r 40c00d684800 src/Pure/ML/ml_test.ML --- 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)); diff -r dcbe1f9fe2cd -r 40c00d684800 src/Tools/coherent.ML --- 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;