proper context for SAT tactics;
authorwenzelm
Mon Jul 27 23:17:40 2009 +0200 (2009-07-27)
changeset 322326c394343360f
parent 32231 95b8afcbb0ed
child 32233 2b175fc6668a
child 32241 a60f183eb63e
proper context for SAT tactics;
eliminated METAHYPS;
tuned signatures;
src/HOL/SAT.thy
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/ex/SAT_Examples.thy
     1.1 --- a/src/HOL/SAT.thy	Mon Jul 27 20:45:40 2009 +0200
     1.2 +++ b/src/HOL/SAT.thy	Mon Jul 27 23:17:40 2009 +0200
     1.3 @@ -25,12 +25,12 @@
     1.4    maxtime=60,
     1.5    satsolver="auto"]
     1.6  
     1.7 -ML {* structure sat = SATFunc(structure cnf = cnf); *}
     1.8 +ML {* structure sat = SATFunc(cnf) *}
     1.9  
    1.10 -method_setup sat = {* Scan.succeed (K (SIMPLE_METHOD' sat.sat_tac)) *}
    1.11 +method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}
    1.12    "SAT solver"
    1.13  
    1.14 -method_setup satx = {* Scan.succeed (K (SIMPLE_METHOD' sat.satx_tac)) *}
    1.15 +method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *}
    1.16    "SAT solver (with definitional CNF)"
    1.17  
    1.18  end
     2.1 --- a/src/HOL/Tools/cnf_funcs.ML	Mon Jul 27 20:45:40 2009 +0200
     2.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Mon Jul 27 23:17:40 2009 +0200
     2.3 @@ -33,19 +33,20 @@
     2.4  
     2.5  signature CNF =
     2.6  sig
     2.7 -	val is_atom           : Term.term -> bool
     2.8 -	val is_literal        : Term.term -> bool
     2.9 -	val is_clause         : Term.term -> bool
    2.10 -	val clause_is_trivial : Term.term -> bool
    2.11 +	val is_atom: term -> bool
    2.12 +	val is_literal: term -> bool
    2.13 +	val is_clause: term -> bool
    2.14 +	val clause_is_trivial: term -> bool
    2.15  
    2.16 -	val clause2raw_thm : Thm.thm -> Thm.thm
    2.17 +	val clause2raw_thm: thm -> thm
    2.18  
    2.19 -	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
    2.20 +	val weakening_tac: int -> tactic  (* removes the first hypothesis of a subgoal *)
    2.21  
    2.22 -	val make_cnf_thm  : theory -> Term.term -> Thm.thm
    2.23 -	val make_cnfx_thm : theory -> Term.term ->  Thm.thm
    2.24 -	val cnf_rewrite_tac  : int -> Tactical.tactic  (* converts all prems of a subgoal to CNF *)
    2.25 -	val cnfx_rewrite_tac : int -> Tactical.tactic  (* converts all prems of a subgoal to (almost) definitional CNF *)
    2.26 +	val make_cnf_thm: theory -> term -> thm
    2.27 +	val make_cnfx_thm: theory -> term -> thm
    2.28 +	val cnf_rewrite_tac: Proof.context -> int -> tactic  (* converts all prems of a subgoal to CNF *)
    2.29 +	val cnfx_rewrite_tac: Proof.context -> int -> tactic
    2.30 +	  (* converts all prems of a subgoal to (almost) definitional CNF *)
    2.31  end;
    2.32  
    2.33  structure cnf : CNF =
    2.34 @@ -505,8 +506,6 @@
    2.35  (* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
    2.36  (* ------------------------------------------------------------------------- *)
    2.37  
    2.38 -(* int -> Tactical.tactic *)
    2.39 -
    2.40  fun weakening_tac i =
    2.41  	dtac weakening_thm i THEN atac (i+1);
    2.42  
    2.43 @@ -516,17 +515,16 @@
    2.44  (*      premise)                                                             *)
    2.45  (* ------------------------------------------------------------------------- *)
    2.46  
    2.47 -(* int -> Tactical.tactic *)
    2.48 -
    2.49 -fun cnf_rewrite_tac i =
    2.50 +fun cnf_rewrite_tac ctxt i =
    2.51  	(* cut the CNF formulas as new premises *)
    2.52 -	OldGoals.METAHYPS (fn prems =>
    2.53 +	FOCUS (fn {prems, ...} =>
    2.54  		let
    2.55 -			val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
    2.56 +		  val thy = ProofContext.theory_of ctxt
    2.57 +			val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
    2.58  			val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
    2.59  		in
    2.60  			cut_facts_tac cut_thms 1
    2.61 -		end) i
    2.62 +		end) ctxt i
    2.63  	(* remove the original premises *)
    2.64  	THEN SELECT_GOAL (fn thm =>
    2.65  		let
    2.66 @@ -540,17 +538,16 @@
    2.67  (*      (possibly introducing new literals)                                  *)
    2.68  (* ------------------------------------------------------------------------- *)
    2.69  
    2.70 -(* int -> Tactical.tactic *)
    2.71 -
    2.72 -fun cnfx_rewrite_tac i =
    2.73 +fun cnfx_rewrite_tac ctxt i =
    2.74  	(* cut the CNF formulas as new premises *)
    2.75 -	OldGoals.METAHYPS (fn prems =>
    2.76 +	FOCUS (fn {prems, ...} =>
    2.77  		let
    2.78 -			val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
    2.79 +		  val thy = ProofContext.theory_of ctxt;
    2.80 +			val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems
    2.81  			val cut_thms  = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
    2.82  		in
    2.83  			cut_facts_tac cut_thms 1
    2.84 -		end) i
    2.85 +		end) ctxt i
    2.86  	(* remove the original premises *)
    2.87  	THEN SELECT_GOAL (fn thm =>
    2.88  		let
     3.1 --- a/src/HOL/Tools/sat_funcs.ML	Mon Jul 27 20:45:40 2009 +0200
     3.2 +++ b/src/HOL/Tools/sat_funcs.ML	Mon Jul 27 23:17:40 2009 +0200
     3.3 @@ -48,16 +48,16 @@
     3.4  
     3.5  signature SAT =
     3.6  sig
     3.7 -	val trace_sat  : bool ref    (* input: print trace messages *)
     3.8 -	val solver     : string ref  (* input: name of SAT solver to be used *)
     3.9 -	val counter    : int ref     (* output: number of resolution steps during last proof replay *)
    3.10 -	val rawsat_thm : cterm list -> thm
    3.11 -	val rawsat_tac : int -> Tactical.tactic
    3.12 -	val sat_tac    : int -> Tactical.tactic
    3.13 -	val satx_tac   : int -> Tactical.tactic
    3.14 +	val trace_sat: bool ref    (* input: print trace messages *)
    3.15 +	val solver: string ref  (* input: name of SAT solver to be used *)
    3.16 +	val counter: int ref     (* output: number of resolution steps during last proof replay *)
    3.17 +	val rawsat_thm: cterm list -> thm
    3.18 +	val rawsat_tac: Proof.context -> int -> tactic
    3.19 +	val sat_tac: Proof.context -> int -> tactic
    3.20 +	val satx_tac: Proof.context -> int -> tactic
    3.21  end
    3.22  
    3.23 -functor SATFunc (structure cnf : CNF) : SAT =
    3.24 +functor SATFunc(cnf : CNF) : SAT =
    3.25  struct
    3.26  
    3.27  val trace_sat = ref false;
    3.28 @@ -410,7 +410,8 @@
    3.29  (*      or "True"                                                            *)
    3.30  (* ------------------------------------------------------------------------- *)
    3.31  
    3.32 -fun rawsat_tac i = OldGoals.METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
    3.33 +fun rawsat_tac ctxt i =
    3.34 +  FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
    3.35  
    3.36  (* ------------------------------------------------------------------------- *)
    3.37  (* pre_cnf_tac: converts the i-th subgoal                                    *)
    3.38 @@ -436,8 +437,8 @@
    3.39  (*      subgoal                                                              *)
    3.40  (* ------------------------------------------------------------------------- *)
    3.41  
    3.42 -fun cnfsat_tac i =
    3.43 -	(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i);
    3.44 +fun cnfsat_tac ctxt i =
    3.45 +	(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
    3.46  
    3.47  (* ------------------------------------------------------------------------- *)
    3.48  (* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
    3.49 @@ -446,9 +447,9 @@
    3.50  (*      then applies 'rawsat_tac' to solve the subgoal                       *)
    3.51  (* ------------------------------------------------------------------------- *)
    3.52  
    3.53 -fun cnfxsat_tac i =
    3.54 +fun cnfxsat_tac ctxt i =
    3.55  	(etac FalseE i) ORELSE
    3.56 -		(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i);
    3.57 +		(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
    3.58  
    3.59  (* ------------------------------------------------------------------------- *)
    3.60  (* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
    3.61 @@ -456,8 +457,8 @@
    3.62  (*      an exponential blowup.                                               *)
    3.63  (* ------------------------------------------------------------------------- *)
    3.64  
    3.65 -fun sat_tac i =
    3.66 -	pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i;
    3.67 +fun sat_tac ctxt i =
    3.68 +	pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
    3.69  
    3.70  (* ------------------------------------------------------------------------- *)
    3.71  (* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
    3.72 @@ -465,7 +466,7 @@
    3.73  (*      introducing new literals.                                            *)
    3.74  (* ------------------------------------------------------------------------- *)
    3.75  
    3.76 -fun satx_tac i =
    3.77 -	pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i;
    3.78 +fun satx_tac ctxt i =
    3.79 +	pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
    3.80  
    3.81  end;
     4.1 --- a/src/HOL/ex/SAT_Examples.thy	Mon Jul 27 20:45:40 2009 +0200
     4.2 +++ b/src/HOL/ex/SAT_Examples.thy	Mon Jul 27 23:17:40 2009 +0200
     4.3 @@ -83,7 +83,7 @@
     4.4  ML {* reset quick_and_dirty; *}
     4.5  
     4.6  method_setup rawsat =
     4.7 -  {* Scan.succeed (K (SIMPLE_METHOD' sat.rawsat_tac)) *}
     4.8 +  {* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *}
     4.9    "SAT solver (no preprocessing)"
    4.10  
    4.11  (* ML {* Toplevel.profiling := 1; *} *)