src/HOL/Tools/ATP/res_clasimpset.ML
author paulson
Fri Dec 16 12:15:54 2005 +0100 (2005-12-16)
changeset 18420 9470061ab283
parent 18144 4edcb5fdc3b0
child 18449 e314fb38307d
permissions -rw-r--r--
hashing to eliminate the output of duplicate clauses
     1 (*  ID:      $Id$
     2     Author:     Claire Quigley
     3     Copyright   2004  University of Cambridge
     4 *)
     5 
     6 
     7 structure ReduceAxiomsN =
     8 (* Author: Jia Meng, Cambridge University Computer Laboratory
     9    Remove irrelevant axioms used for a proof of a goal, with with iteration control
    10    
    11    Initial version. Needs elaboration. *)
    12 
    13 struct
    14 
    15 fun add_term_consts_rm ncs (Const(c, _)) cs = 
    16     if (c mem ncs) then cs else (c ins_string cs)
    17   | add_term_consts_rm ncs (t $ u) cs =
    18       add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
    19   | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
    20   | add_term_consts_rm ncs _ cs = cs;
    21 
    22 
    23 fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
    24 
    25 fun thm_consts_rm ncs thm = term_consts_rm ncs (prop_of thm);
    26 
    27 fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm;
    28 
    29 fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
    30 
    31 fun make_pairs [] _ = []
    32   | make_pairs (x::xs) y = (x,y)::(make_pairs xs y);
    33 
    34 fun const_thm_list_aux [] cthms = cthms
    35   | const_thm_list_aux (thm::thms) cthms =
    36     let val consts = consts_of_thm thm
    37 	val cthms' = make_pairs consts thm 
    38     in
    39 	const_thm_list_aux thms (cthms' @ cthms)
    40     end;
    41 
    42 
    43 fun const_thm_list thms = const_thm_list_aux thms [];
    44 
    45 fun make_thm_table thms  = 
    46     let val consts_thms = const_thm_list thms
    47     in
    48 	Symtab.make_multi consts_thms
    49     end;
    50 
    51 
    52 fun consts_in_goal goal = consts_of_term goal;
    53 
    54 fun axioms_having_consts_aux [] tab thms = thms
    55   | axioms_having_consts_aux (c::cs) tab thms =
    56     let val thms1 = Symtab.lookup tab c
    57       val thms2 = 
    58           case thms1 of (SOME x) => x
    59                       | NONE => []
    60     in
    61       axioms_having_consts_aux cs tab (thms2 union thms)
    62     end;
    63 
    64 fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab [];
    65 
    66 
    67 fun relevant_axioms goal thmTab n =  
    68     let val consts = consts_in_goal goal
    69 	fun relevant_axioms_aux1 cs k =
    70 	    let val thms1 = axioms_having_consts cs thmTab
    71 		val cs1 = foldl (op union_string) [] (map consts_of_thm thms1)
    72 	    in
    73 		if ((cs1 subset cs) orelse n <= k) then (k,thms1) 
    74 		else (relevant_axioms_aux1 (cs1 union cs) (k+1))
    75 	    end
    76 
    77     in  relevant_axioms_aux1 consts 1  end;
    78 
    79 fun relevant_filter n goal thms = 
    80     if n<=0 then thms 
    81     else #2 (relevant_axioms goal (make_thm_table thms) n);
    82 
    83 (* find the thms from thy that contain relevant constants, n is the iteration number *)
    84 fun find_axioms_n thy goal n =
    85     let val clasetR = ResAxioms.claset_rules_of_thy thy
    86 	val simpsetR = ResAxioms.simpset_rules_of_thy thy	  
    87 	val table = make_thm_table (clasetR @ simpsetR)	
    88     in
    89 	relevant_axioms goal table n
    90     end;
    91 
    92 fun find_axioms_n_c thy goal n =
    93     let val current_thms = PureThy.thms_of thy
    94 	val table = make_thm_table current_thms
    95     in
    96 	relevant_axioms goal table n
    97     end;
    98 
    99 end;
   100 
   101 
   102 signature RES_CLASIMP = 
   103   sig
   104   val relevant : int ref
   105   val use_simpset: bool ref
   106   val get_clasimp_lemmas : 
   107          Proof.context -> term -> 
   108          (ResClause.clause * thm) Array.array * ResClause.clause list 
   109   end;
   110 
   111 structure ResClasimp : RES_CLASIMP =
   112 struct
   113 val use_simpset = ref false;   (*Performance is much better without simprules*)
   114 
   115 val relevant = ref 0;  (*Relevance filtering is off by default*)
   116 
   117 (*The "name" of a theorem is its statement, if nothing else is available.*)
   118 val plain_string_of_thm =
   119     setmp show_question_marks false 
   120       (setmp print_mode [] 
   121 	(Pretty.setmp_margin 999 string_of_thm));
   122 	
   123 (*Returns the first substring enclosed in quotation marks, typically omitting 
   124   the [.] of meta-level assumptions.*)
   125 val firstquoted = hd o (String.tokens (fn c => c = #"\""))
   126 	
   127 fun fake_thm_name th = 
   128     Context.theory_name (theory_of_thm th) ^ "." ^ firstquoted (plain_string_of_thm th);
   129 
   130 fun put_name_pair ("",th) = (fake_thm_name th, th)
   131   | put_name_pair (a,th)  = (a,th);
   132 
   133 (* outputs a list of (thm,clause) pairs *)
   134 
   135 fun multi x 0 xlist = xlist
   136    |multi x n xlist = multi x (n-1) (x::xlist);
   137 
   138 fun clause_numbering ((clause, theorem), num_of_cls) = 
   139     let val numbers = 0 upto (num_of_cls - 1)
   140     in 
   141 	multi (clause, theorem) num_of_cls []
   142     end;
   143     
   144 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute
   145 Some primes from http://primes.utm.edu/:
   146    1823   1831   1847   1861   1867   1871   1873   1877   1879   1889 
   147    1901   1907   1913   1931   1933   1949   1951   1973   1979   1987 
   148    1993   1997   1999   2003   2011   2017   2027   2029   2039   2053 
   149    2063   2069   2081   2083   2087   2089   2099   2111   2113   2129 
   150 *)
   151 
   152 exception HASH_CLAUSE;
   153 
   154 (*Create a hash table for clauses, of the given size*)
   155 fun mk_clause_table size =
   156       Hashtable.create{hash = ResClause.hash1_clause, 
   157 		       exn = HASH_CLAUSE,
   158 		       == = ResClause.clause_eq, 
   159 		       size = size};
   160 
   161 (*Insert x only if fresh*)
   162 fun insert_new ht (x,y) = ignore (Hashtable.lookup ht x)
   163             handle HASH_CLAUSE => Hashtable.insert ht (x,y); 
   164 
   165 (*Use a hash table to eliminate duplicates from xs*)
   166 fun make_unique ht xs = (app (insert_new ht) xs;  Hashtable.map Library.I ht);
   167 
   168 (*Write out the claset and simpset rules of the supplied theory.
   169   FIXME: argument "goal" is a hack to allow relevance filtering.
   170   To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
   171 fun get_clasimp_lemmas ctxt goal = 
   172   let val claset_thms =
   173 	    map put_name_pair
   174 	      (ReduceAxiomsN.relevant_filter (!relevant) goal 
   175 		(ResAxioms.claset_rules_of_ctxt ctxt))
   176       val claset_cls_thms = ResAxioms.clausify_rules_pairs claset_thms
   177       val simpset_cls_thms = 
   178 	    if !use_simpset then 
   179 	       ResAxioms.clausify_rules_pairs 
   180 		  (map put_name_pair 
   181 		    (ReduceAxiomsN.relevant_filter (!relevant) goal
   182 		      (ResAxioms.simpset_rules_of_ctxt ctxt)))
   183 	    else []
   184       val cls_thms_list = make_unique (mk_clause_table 2129) 
   185                                       (List.concat (simpset_cls_thms@claset_cls_thms))
   186       (* Identify the set of clauses to be written out *)
   187       val clauses = map #1(cls_thms_list);
   188       val cls_nums = map ResClause.num_of_clauses clauses;
   189       (*Note: in every case, cls_num = 1.  I think that only conjecture clauses
   190 	can have any other value.*)
   191       val whole_list = List.concat 
   192 	    (map clause_numbering (ListPair.zip (cls_thms_list, cls_nums)));
   193       
   194   in  (* create array of put clausename, number pairs into it *)
   195       (Array.fromList whole_list, clauses)
   196   end;
   197 
   198 
   199 end;
   200 
   201 
   202