# HG changeset patch
# User wenzelm
# Date 1183475827 -7200
# Node ID b86b764d576437c94389f5886bccb914e7ce3cd1
# Parent  802bdbe0817739b51d0fdb93c0c63fd7cb3a6622
Conjunction.intr/elim_balanced;
CONVERSION tactical;
tuned;

diff -r 802bdbe08177 -r b86b764d5764 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Tue Jul 03 17:17:07 2007 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Tue Jul 03 17:17:07 2007 +0200
@@ -69,7 +69,6 @@
 
 val counter = ref 0;
 
-(* Thm.thm *)
 val resolution_thm =  (* "[| ?P ==> False; ~ ?P ==> False |] ==> False" *)
 	let
 		val cterm = cterm_of (the_context ())
@@ -79,7 +78,6 @@
 		Thm.instantiate ([], [(cterm Q, cterm False)]) case_split_thm
 	end;
 
-(* Thm.cterm *)
 val cP = cterm_of (theory_of_thm resolution_thm) (Var (("P", 0), HOLogic.boolT));
 
 (* ------------------------------------------------------------------------- *)
@@ -322,7 +320,7 @@
 	val nontrivial_clauses = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
 	(* sort clauses according to the term order -- an optimization,       *)
 	(* useful because forming the union of hypotheses, as done by         *)
-	(* Conjunction.intr_list and foldr Thm.weaken below, is quadratic for *)
+	(* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
 	(* terms sorted in descending order, while only linear for terms      *)
 	(* sorted in ascending order                                          *)
 	val sorted_clauses = sort (Term.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
@@ -346,7 +344,7 @@
 		(* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
 		(* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
 		(* clauses in ascending order (which is linear for                  *)
-		(* 'Conjunction.intr_list', used below)                             *)
+		(* 'Conjunction.intr_balanced', used below)                         *)
 		fold Thm.weaken (rev sorted_clauses) False_thm
 	end
 in
@@ -364,12 +362,12 @@
 				(* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
 				(*               this avoids accumulation of hypotheses during resolution    *)
 				(* [c_1, ..., c_n] |- c_1 && ... && c_n *)
-				val clauses_thm = Conjunction.intr_list (map Thm.assume sorted_clauses)
+				val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
 				(* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
 				val cnf_cterm = cprop_of clauses_thm
 				val cnf_thm   = Thm.assume cnf_cterm
 				(* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
-				val cnf_clauses = Conjunction.elim_list cnf_thm
+				val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
 				(* initialize the clause array with the given clauses *)
 				val max_idx    = valOf (Inttab.max_key clause_table)
 				val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
@@ -414,8 +412,6 @@
 (*      or "True"                                                            *)
 (* ------------------------------------------------------------------------- *)
 
-(* int -> Tactical.tactic *)
-
 fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
 
 (* ------------------------------------------------------------------------- *)
@@ -430,11 +426,10 @@
 (*      subgoal                                                              *)
 (* ------------------------------------------------------------------------- *)
 
-(* int -> Tactical.tactic *)
-
-fun pre_cnf_tac i =
-	rtac ccontr i THEN ObjectLogic.atomize_tac i THEN
-		PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (equal i) (Drule.beta_eta_conversion)));
+val pre_cnf_tac =
+        rtac ccontr THEN'
+        ObjectLogic.atomize_tac THEN'
+        CONVERSION Drule.beta_eta_conversion;
 
 (* ------------------------------------------------------------------------- *)
 (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
@@ -443,8 +438,6 @@
 (*      subgoal                                                              *)
 (* ------------------------------------------------------------------------- *)
 
-(* int -> Tactical.tactic *)
-
 fun cnfsat_tac i =
 	(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i);
 
@@ -455,8 +448,6 @@
 (*      then applies 'rawsat_tac' to solve the subgoal                       *)
 (* ------------------------------------------------------------------------- *)
 
-(* int -> Tactical.tactic *)
-
 fun cnfxsat_tac i =
 	(etac FalseE i) ORELSE
 		(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i);
@@ -467,8 +458,6 @@
 (*      an exponential blowup.                                               *)
 (* ------------------------------------------------------------------------- *)
 
-(* int -> Tactical.tactic *)
-
 fun sat_tac i =
 	pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i;
 
@@ -478,9 +467,7 @@
 (*      introducing new literals.                                            *)
 (* ------------------------------------------------------------------------- *)
 
-(* int -> Tactical.tactic *)
-
 fun satx_tac i =
 	pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i;
 
-end;  (* of structure SATFunc *)
+end;