# HG changeset patch # User wenzelm # Date 1243248498 -7200 # Node ID b3c7044d47b6ffd13d7348ec8dd0b65402e3d838 # Parent 2c20bcd70fbe6a6ecb50c0e4824addf4f74dd303 modernized method setup; tuned signature; diff -r 2c20bcd70fbe -r b3c7044d47b6 src/HOL/Import/import_package.ML --- a/src/HOL/Import/import_package.ML Mon May 25 12:46:14 2009 +0200 +++ b/src/HOL/Import/import_package.ML Mon May 25 12:48:18 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 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 2c20bcd70fbe -r b3c7044d47b6 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Mon May 25 12:46:14 2009 +0200 +++ b/src/HOL/Import/shuffler.ML Mon May 25 12:48:18 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,8 @@ 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_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 shuffle_tac ctxt thms = gen_shuffle_tac ctxt false (map (pair "") thms); +fun search_tac ctxt = gen_shuffle_tac thy true (map (pair "premise") (Assumption.all_prems_of ctxt); fun add_shuffle_rule thm thy = let @@ -680,10 +662,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 thms))) + "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 2c20bcd70fbe -r b3c7044d47b6 src/Tools/coherent.ML --- a/src/Tools/coherent.ML Mon May 25 12:46:14 2009 +0200 +++ b/src/Tools/coherent.ML Mon May 25 12:48:18 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;