src/HOL/Tools/ATP/res_clasimpset.ML
changeset 19356 794802e95d35
parent 19320 d3688974a063
child 19480 868cf5051ff5
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Apr 07 05:14:06 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Apr 07 05:14:54 2006 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4        Proof.context ->
     1.5        Term.term list ->
     1.6        (string * Thm.thm) list ->
     1.7 -      (bool * bool * bool) -> bool -> string Array.array * (Term.term * (string * int)) list
     1.8 +      (bool * bool * bool) -> bool -> string Array.array * (thm * (string * int)) list
     1.9    end;
    1.10    
    1.11  structure ResClasimp : RES_CLASIMP =
    1.12 @@ -249,23 +249,25 @@
    1.13  
    1.14  fun hash_term term = Word.toIntX (xor_words (map hash_literal (get_literals term [])));
    1.15  
    1.16 +fun hash_thm  thm = hash_term (prop_of thm);
    1.17  
    1.18 +fun eq_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
    1.19  (*Create a hash table for clauses, of the given size*)
    1.20  fun mk_clause_table n =
    1.21 -      Polyhash.mkTable (hash_term, Term.aconv)
    1.22 +      Polyhash.mkTable (hash_thm, eq_thm)
    1.23                         (n, HASH_CLAUSE);
    1.24  
    1.25  (*Use a hash table to eliminate duplicates from xs*)
    1.26  fun make_unique ht xs = 
    1.27        (app (ignore o Polyhash.peekInsert ht) xs;  Polyhash.listItems ht);
    1.28  
    1.29 -fun mem_tm tm [] = false
    1.30 -  | mem_tm tm ((tm',name)::tms_names) = Term.aconv (tm,tm') orelse mem_tm tm tms_names;
    1.31 +fun mem_thm thm [] = false
    1.32 +  | mem_thm thm ((thm',name)::thms_names) = eq_thm (thm,thm') orelse mem_thm thm thms_names;
    1.33  
    1.34 -fun insert_tms [] tms_names = tms_names
    1.35 -  | insert_tms ((tm,name)::tms_names) tms_names' =
    1.36 -      if mem_tm tm tms_names' then insert_tms tms_names tms_names' 
    1.37 -      else insert_tms tms_names ((tm,name)::tms_names');
    1.38 +fun insert_thms [] thms_names = thms_names
    1.39 +  | insert_thms ((thm,name)::thms_names) thms_names' =
    1.40 +      if mem_thm thm thms_names' then insert_thms thms_names thms_names' 
    1.41 +      else insert_thms thms_names ((thm,name)::thms_names');
    1.42  
    1.43  fun display_thms [] = ()
    1.44    | display_thms ((name,thm)::nthms) = 
    1.45 @@ -294,25 +296,25 @@
    1.46  	     | _  => map put_name_pair user_thms
    1.47        val banned = make_banned_test (map #1 (user_rules@atpset_thms@claset_thms@simpset_thms))
    1.48        fun ok (a,_) = not (banned a) 	   
    1.49 -      val claset_cls_tms = 
    1.50 -            if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok claset_thms)
    1.51 -            else ResAxioms.clausify_rules_pairs_abs claset_thms
    1.52 -      val simpset_cls_tms = 
    1.53 -      	    if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok simpset_thms)
    1.54 -	    else ResAxioms.clausify_rules_pairs_abs simpset_thms
    1.55 -      val atpset_cls_tms = 
    1.56 -      	    if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok atpset_thms)
    1.57 -	    else ResAxioms.clausify_rules_pairs_abs atpset_thms
    1.58 -      val user_cls_tms = ResAxioms.clausify_rules_pairs_abs user_rules (* no filter here, because user supplied rules *)
    1.59 -      val cls_tms_list = make_unique (mk_clause_table 2200) 
    1.60 -                           (List.concat (user_cls_tms@atpset_cls_tms@simpset_cls_tms@claset_cls_tms))
    1.61 -      val relevant_cls_tms_list =
    1.62 +      val claset_cls_thms = 
    1.63 +            if run_filter then ResAxioms.cnf_rules_pairs (filter ok claset_thms)
    1.64 +            else ResAxioms.cnf_rules_pairs claset_thms
    1.65 +      val simpset_cls_thms = 
    1.66 +      	    if run_filter then ResAxioms.cnf_rules_pairs (filter ok simpset_thms)
    1.67 +	    else ResAxioms.cnf_rules_pairs simpset_thms
    1.68 +      val atpset_cls_thms = 
    1.69 +      	    if run_filter then ResAxioms.cnf_rules_pairs (filter ok atpset_thms)
    1.70 +	    else ResAxioms.cnf_rules_pairs atpset_thms
    1.71 +      val user_cls_thms = ResAxioms.cnf_rules_pairs user_rules (* no filter here, because user supplied rules *)
    1.72 +      val cls_thms_list = make_unique (mk_clause_table 2200) 
    1.73 +                           (List.concat (user_cls_thms@atpset_cls_thms@simpset_cls_thms@claset_cls_thms))
    1.74 +      val relevant_cls_thms_list =
    1.75  	  if run_filter 
    1.76 -	  then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_tms_list goals
    1.77 -	  else cls_tms_list
    1.78 -      val all_relevant_cls_tms_list = insert_tms (List.concat user_cls_tms) relevant_cls_tms_list (*ensure all user supplied rules are output*)	  
    1.79 +	  then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals
    1.80 +	  else cls_thms_list
    1.81 +      val all_relevant_cls_thms_list = insert_thms (List.concat user_cls_thms) relevant_cls_thms_list (*ensure all user supplied rules are output*)	  
    1.82      in
    1.83 -	(Array.fromList (map fst (map snd all_relevant_cls_tms_list)), all_relevant_cls_tms_list)
    1.84 +	(Array.fromList (map fst (map snd all_relevant_cls_thms_list)), all_relevant_cls_thms_list)
    1.85  end;
    1.86  
    1.87