--- a/src/HOL/SAT.thy Mon Jul 27 20:45:40 2009 +0200
+++ b/src/HOL/SAT.thy Mon Jul 27 23:17:40 2009 +0200
@@ -25,12 +25,12 @@
maxtime=60,
satsolver="auto"]
-ML {* structure sat = SATFunc(structure cnf = cnf); *}
+ML {* structure sat = SATFunc(cnf) *}
-method_setup sat = {* Scan.succeed (K (SIMPLE_METHOD' sat.sat_tac)) *}
+method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}
"SAT solver"
-method_setup satx = {* Scan.succeed (K (SIMPLE_METHOD' sat.satx_tac)) *}
+method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *}
"SAT solver (with definitional CNF)"
end
--- a/src/HOL/Tools/cnf_funcs.ML Mon Jul 27 20:45:40 2009 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Mon Jul 27 23:17:40 2009 +0200
@@ -33,19 +33,20 @@
signature CNF =
sig
- val is_atom : Term.term -> bool
- val is_literal : Term.term -> bool
- val is_clause : Term.term -> bool
- val clause_is_trivial : Term.term -> bool
+ val is_atom: term -> bool
+ val is_literal: term -> bool
+ val is_clause: term -> bool
+ val clause_is_trivial: term -> bool
- val clause2raw_thm : Thm.thm -> Thm.thm
+ val clause2raw_thm: thm -> thm
- val weakening_tac : int -> Tactical.tactic (* removes the first hypothesis of a subgoal *)
+ val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *)
- val make_cnf_thm : theory -> Term.term -> Thm.thm
- val make_cnfx_thm : theory -> Term.term -> Thm.thm
- val cnf_rewrite_tac : int -> Tactical.tactic (* converts all prems of a subgoal to CNF *)
- val cnfx_rewrite_tac : int -> Tactical.tactic (* converts all prems of a subgoal to (almost) definitional CNF *)
+ val make_cnf_thm: theory -> term -> thm
+ val make_cnfx_thm: theory -> term -> thm
+ val cnf_rewrite_tac: Proof.context -> int -> tactic (* converts all prems of a subgoal to CNF *)
+ val cnfx_rewrite_tac: Proof.context -> int -> tactic
+ (* converts all prems of a subgoal to (almost) definitional CNF *)
end;
structure cnf : CNF =
@@ -505,8 +506,6 @@
(* weakening_tac: removes the first hypothesis of the 'i'-th subgoal *)
(* ------------------------------------------------------------------------- *)
-(* int -> Tactical.tactic *)
-
fun weakening_tac i =
dtac weakening_thm i THEN atac (i+1);
@@ -516,17 +515,16 @@
(* premise) *)
(* ------------------------------------------------------------------------- *)
-(* int -> Tactical.tactic *)
-
-fun cnf_rewrite_tac i =
+fun cnf_rewrite_tac ctxt i =
(* cut the CNF formulas as new premises *)
- OldGoals.METAHYPS (fn prems =>
+ FOCUS (fn {prems, ...} =>
let
- val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
+ val thy = ProofContext.theory_of ctxt
+ val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
in
cut_facts_tac cut_thms 1
- end) i
+ end) ctxt i
(* remove the original premises *)
THEN SELECT_GOAL (fn thm =>
let
@@ -540,17 +538,16 @@
(* (possibly introducing new literals) *)
(* ------------------------------------------------------------------------- *)
-(* int -> Tactical.tactic *)
-
-fun cnfx_rewrite_tac i =
+fun cnfx_rewrite_tac ctxt i =
(* cut the CNF formulas as new premises *)
- OldGoals.METAHYPS (fn prems =>
+ FOCUS (fn {prems, ...} =>
let
- val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
+ val thy = ProofContext.theory_of ctxt;
+ val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems
val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
in
cut_facts_tac cut_thms 1
- end) i
+ end) ctxt i
(* remove the original premises *)
THEN SELECT_GOAL (fn thm =>
let
--- a/src/HOL/Tools/sat_funcs.ML Mon Jul 27 20:45:40 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Mon Jul 27 23:17:40 2009 +0200
@@ -48,16 +48,16 @@
signature SAT =
sig
- val trace_sat : bool ref (* input: print trace messages *)
- val solver : string ref (* input: name of SAT solver to be used *)
- val counter : int ref (* output: number of resolution steps during last proof replay *)
- val rawsat_thm : cterm list -> thm
- val rawsat_tac : int -> Tactical.tactic
- val sat_tac : int -> Tactical.tactic
- val satx_tac : int -> Tactical.tactic
+ val trace_sat: bool ref (* input: print trace messages *)
+ val solver: string ref (* input: name of SAT solver to be used *)
+ val counter: int ref (* output: number of resolution steps during last proof replay *)
+ val rawsat_thm: cterm list -> thm
+ val rawsat_tac: Proof.context -> int -> tactic
+ val sat_tac: Proof.context -> int -> tactic
+ val satx_tac: Proof.context -> int -> tactic
end
-functor SATFunc (structure cnf : CNF) : SAT =
+functor SATFunc(cnf : CNF) : SAT =
struct
val trace_sat = ref false;
@@ -410,7 +410,8 @@
(* or "True" *)
(* ------------------------------------------------------------------------- *)
-fun rawsat_tac i = OldGoals.METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
+fun rawsat_tac ctxt i =
+ FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
(* ------------------------------------------------------------------------- *)
(* pre_cnf_tac: converts the i-th subgoal *)
@@ -436,8 +437,8 @@
(* subgoal *)
(* ------------------------------------------------------------------------- *)
-fun cnfsat_tac i =
- (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i);
+fun cnfsat_tac ctxt i =
+ (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
(* ------------------------------------------------------------------------- *)
(* cnfxsat_tac: checks if the empty clause "False" occurs among the *)
@@ -446,9 +447,9 @@
(* then applies 'rawsat_tac' to solve the subgoal *)
(* ------------------------------------------------------------------------- *)
-fun cnfxsat_tac i =
+fun cnfxsat_tac ctxt i =
(etac FalseE i) ORELSE
- (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i);
+ (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
(* ------------------------------------------------------------------------- *)
(* sat_tac: tactic for calling an external SAT solver, taking as input an *)
@@ -456,8 +457,8 @@
(* an exponential blowup. *)
(* ------------------------------------------------------------------------- *)
-fun sat_tac i =
- pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i;
+fun sat_tac ctxt i =
+ pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
(* ------------------------------------------------------------------------- *)
(* satx_tac: tactic for calling an external SAT solver, taking as input an *)
@@ -465,7 +466,7 @@
(* introducing new literals. *)
(* ------------------------------------------------------------------------- *)
-fun satx_tac i =
- pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i;
+fun satx_tac ctxt i =
+ pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
end;
--- a/src/HOL/ex/SAT_Examples.thy Mon Jul 27 20:45:40 2009 +0200
+++ b/src/HOL/ex/SAT_Examples.thy Mon Jul 27 23:17:40 2009 +0200
@@ -83,7 +83,7 @@
ML {* reset quick_and_dirty; *}
method_setup rawsat =
- {* Scan.succeed (K (SIMPLE_METHOD' sat.rawsat_tac)) *}
+ {* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *}
"SAT solver (no preprocessing)"
(* ML {* Toplevel.profiling := 1; *} *)