# HG changeset patch
# User paulson
# Date 1143104703 -3600
# Node ID 30b5bb35dd33e735254d0b857ba9f7a8f03ef6c3
# Parent  d3688974a063cbec43a08c374ab4a0df7c359cb8
detection of definitions of relevant constants

diff -r d3688974a063 -r 30b5bb35dd33 src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Thu Mar 23 06:18:38 2006 +0100
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Thu Mar 23 10:05:03 2006 +0100
@@ -89,6 +89,7 @@
 
 (**** Constant / Type Frequencies ****)
 
+
 local
 
 fun cons_nr CTVar = 0
@@ -187,30 +188,49 @@
 fun showax ((_,cname), (_,w)) = 
     Output.debug ("Axiom " ^ show_cname cname ^ " has weight " ^ Real.toString w)
 	      
+exception ConstFree;
+fun dest_ConstFree (Const aT) = aT
+  | dest_ConstFree (Free aT) = aT
+  | dest_ConstFree _ = raise ConstFree;
+
+(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
+fun defines thy (tm,(name,n)) gctypes =
+  let fun defs hs =
+        let val (rator,args) = strip_comb hs
+            val ct = const_with_typ thy (dest_ConstFree rator)
+        in  forall is_Var args andalso uni_mem ct gctypes  end
+        handle ConstFree => false
+  in    
+    case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ _) => 
+          defs lhs andalso
+          (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
+      | _ => false
+  end
+
 fun relevance_filter_aux thy axioms goals = 
   let val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
       val goals_consts_typs = get_goal_consts_typs thy goals
-      fun relevant [] (ax,r) = (ax,r)
-	| relevant ((clstm,consts_typs)::y) (ax,r) =
+      fun relevant [] (rels,nonrels) = (rels,nonrels)
+	| relevant ((clstm,consts_typs)::axs) (rels,nonrels) =
 	    let val weight = clause_weight const_tab goals_consts_typs consts_typs
 		val ccc = (clstm, (consts_typs,weight))
 	    in
-	      if !pass_mark <= weight 
-	      then relevant y (ccc::ax, r)
-	      else relevant y (ax, ccc::r)
+	      if !pass_mark <= weight orelse defines thy clstm goals_consts_typs
+	      then relevant axs (ccc::rels, nonrels)
+	      else relevant axs (rels, ccc::nonrels)
 	    end
       val (rel_clauses,nrel_clauses) =
 	  relevant (map (pair_consts_typs_axiom thy) axioms) ([],[]) 
-      val (ax,r) = relevant_clauses const_tab rel_clauses nrel_clauses ([],[]) []
-      val max_filtered = floor (!reduction_factor * real (length ax))
-      val ax' = Library.take(max_filtered, Library.sort axiom_ord ax)
+      val (rels,nonrels) = relevant_clauses const_tab rel_clauses nrel_clauses ([],[]) []
+      val max_filtered = floor (!reduction_factor * real (length rels))
+      val rels' = Library.take(max_filtered, Library.sort axiom_ord rels)
   in
       if !Output.show_debug_msgs then
 	   (List.app showconst (Symtab.dest const_tab);
-	    List.app showax ax)
+	    List.app showax rels)
       else ();
-      if !add_unit then (filter good_unit_clause r) @ ax'
-      else ax'
+      if !add_unit then (filter good_unit_clause nonrels) @ rels'
+      else rels'
   end;
 
 fun relevance_filter thy axioms goals =