# HG changeset patch
# User paulson
# Date 1121259964 -7200
# Node ID b400b53d8f7dd06910879bfc1de61ce4e947e555
# Parent  12d00dab530172fc0a8476f13ee275d41bdcdae9
relevance filtering is now optional

diff -r 12d00dab5301 -r b400b53d8f7d src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Jul 13 15:05:48 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Jul 13 15:06:04 2005 +0200
@@ -1,6 +1,4 @@
-
-(*  ID:         $Id$
-
+(*  ID:      $Id$
     Author:     Claire Quigley
     Copyright   2004  University of Cambridge
 *)
@@ -14,7 +12,8 @@
 
 fun add_term_consts_rm ncs (Const(c, _)) cs = 
     if (c mem ncs) then cs else (c ins_string cs)
-  | add_term_consts_rm ncs (t $ u) cs = add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
+  | add_term_consts_rm ncs (t $ u) cs =
+      add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
   | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
   | add_term_consts_rm ncs _ cs = cs;
 
@@ -27,9 +26,6 @@
 
 fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm;
 
-
-
-
 fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
 
 fun make_pairs [] _ = []
@@ -77,25 +73,16 @@
 	    let val thms1 = axioms_having_consts cs thmTab
 		val cs1 = ResLib.flat_noDup (map consts_of_thm thms1)
 	    in
-		if ((cs1 subset cs) orelse (n <= k)) then (k,thms1) 
+		if ((cs1 subset cs) orelse n <= k) then (k,thms1) 
 		else (relevant_axioms_aux1 (cs1 union cs) (k+1))
 	    end
 
-	fun relevant_axioms_aux2 cs k =
-	    let val thms1 = axioms_having_consts cs thmTab
-		val cs1 = ResLib.flat_noDup (map consts_of_thm thms1)
-	    in
-		if (cs1 subset cs)  then (k,thms1) 
-		else (relevant_axioms_aux2 (cs1 union cs) (k+1))
-	    end
-
-    in
-	if n <= 0 then (relevant_axioms_aux2 consts 1) else (relevant_axioms_aux1 consts 1)
-    end;
+    in  relevant_axioms_aux1 consts 1  end;
 
 
-
-fun relevant_filter n goal thms = #2 (relevant_axioms goal (make_thm_table thms) n);
+fun relevant_filter n goal thms = 
+    if n<=0 then thms 
+    else #2 (relevant_axioms goal (make_thm_table thms) n);
 
 
 (* find the thms from thy that contain relevant constants, n is the iteration number *)
@@ -113,7 +100,6 @@
 	val table = make_thm_table current_thms
     in
 	relevant_axioms goal table n
-
     end;
 
 end;
@@ -121,14 +107,19 @@
 
 signature RES_CLASIMP = 
   sig
-     val write_out_clasimp : string -> theory -> term -> 
+  val relevant : int ref
+  val write_out_clasimp : string -> theory -> term -> 
                              (ResClause.clause * thm) Array.array * int
-val write_out_clasimp_small :string -> theory -> (ResClause.clause * thm) Array.array * int
+  val write_out_clasimp_small :
+     string -> theory -> (ResClause.clause * thm) Array.array * int
   end;
 
 structure ResClasimp : RES_CLASIMP =
 struct
 
+(*Relevance filtering is off by default*)
+val relevant = ref 0;  
+
 fun has_name th = ((Thm.name_of_thm th)  <>  "")
 
 fun has_name_pair (a,b) = (a <> "");
@@ -190,14 +181,16 @@
 (*Write out the claset and simpset rules of the supplied theory.
   FIXME: argument "goal" is a hack to allow relevance filtering.*)
 fun write_out_clasimp filename thy goal = 
-    let val claset_rules = ReduceAxiomsN.relevant_filter 1 goal 
-                              (ResAxioms.claset_rules_of_thy thy);
+    let val claset_rules = 
+              ReduceAxiomsN.relevant_filter (!relevant) goal 
+                (ResAxioms.claset_rules_of_thy thy);
 	val named_claset = List.filter has_name_pair claset_rules;
 	val claset_names = map remove_spaces_pair (named_claset)
 	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
 
-	val simpset_rules = ReduceAxiomsN.relevant_filter 1 goal 
-	                       (ResAxioms.simpset_rules_of_thy thy);
+	val simpset_rules =
+	      ReduceAxiomsN.relevant_filter (!relevant) goal 
+                (ResAxioms.simpset_rules_of_thy thy);
 	val named_simpset = 
 	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
 	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);