invents theorem names; also patches write_out_clasimp
authorpaulson
Thu Jul 28 17:56:27 2005 +0200 (2005-07-28)
changeset 169565b413c866593
parent 16955 93270c5f56f6
child 16957 8dcd14e8db7a
invents theorem names; also patches write_out_clasimp
src/HOL/Tools/ATP/res_clasimpset.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Jul 28 17:55:39 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Jul 28 17:56:27 2005 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4    val relevant : int ref
     1.5    val use_simpset: bool ref
     1.6    val write_out_clasimp : string -> theory -> term -> 
     1.7 -                             (ResClause.clause * thm) Array.array * int * ResClause.clause list
     1.8 +                             (ResClause.clause * thm) Array.array * int (* * ResClause.clause list *)
     1.9  
    1.10    end;
    1.11  
    1.12 @@ -121,10 +121,14 @@
    1.13  (*Relevance filtering is off by default*)
    1.14  val relevant = ref 0;  
    1.15  
    1.16 -fun has_name th = ((Thm.name_of_thm th)  <>  "")
    1.17 +(*The "name" of a theorem is its statement, if nothing else is available.*)
    1.18 +val plain_string_of_thm =
    1.19 +    setmp show_question_marks false 
    1.20 +      (setmp print_mode [] 
    1.21 +	(Pretty.setmp_margin 999 string_of_thm));
    1.22  
    1.23 -fun has_name_pair (a,b) = (a <> "");
    1.24 -
    1.25 +fun put_name_pair ("",th) = (ResLib.trim_ends (plain_string_of_thm th), th)
    1.26 +  | put_name_pair (a,th)  = (a,th);
    1.27  
    1.28  (* changed, now it also finds out the name of the theorem. *)
    1.29  (* convert a theorem into CNF and then into Clause.clause format. *)
    1.30 @@ -142,6 +146,8 @@
    1.31      then  ((String.substring(str,0,5)) ^ (String.extract (str, 10, NONE)))
    1.32      else str;
    1.33  
    1.34 +(*FIXME: this logic (especially concat_with_stop) needs to be replaced by code
    1.35 +to invert the function ascii_of.*)
    1.36  fun remove_spaces str = 
    1.37      let val strlist = String.tokens Char.isSpace str
    1.38  	val spaceless = concat strlist
    1.39 @@ -190,17 +196,16 @@
    1.40    To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
    1.41  fun write_out_clasimp filename thy goal = 
    1.42      let val claset_rules = 
    1.43 -              ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.44 -                (ResAxioms.claset_rules_of_thy thy);
    1.45 -	val named_claset = List.filter has_name_pair claset_rules;
    1.46 -
    1.47 -	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
    1.48 +              map put_name_pair
    1.49 +	        (ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.50 +		  (ResAxioms.claset_rules_of_thy thy));
    1.51 +	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs claset_rules []);
    1.52  
    1.53  	val simpset_rules =
    1.54  	      ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.55                  (ResAxioms.simpset_rules_of_thy thy);
    1.56  	val named_simpset = 
    1.57 -	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
    1.58 +	      map remove_spaces_pair (map put_name_pair simpset_rules)
    1.59          val justnames = map #1 named_simpset
    1.60          val namestring = concat_with "\n" justnames
    1.61          val _ = File.append (File.tmp_path (Path.basic "clasimp_names"))
    1.62 @@ -233,7 +238,7 @@
    1.63  	val _= TextIO.flushOut out;
    1.64  	val _= TextIO.closeOut out
    1.65    in
    1.66 -	(clause_arr, num_of_clauses, clauses)
    1.67 +	(clause_arr, num_of_clauses)
    1.68    end;
    1.69  
    1.70