--- 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
--- 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 #>
--- 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;