simplifying the treatment of nameless theorems
authorpaulson
Tue Oct 11 15:03:36 2005 +0200 (2005-10-11)
changeset 17828c82fb51ee18d
parent 17827 b32fad049413
child 17829 35123f89801e
simplifying the treatment of nameless theorems
src/HOL/Tools/ATP/res_clasimpset.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Oct 11 14:02:33 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Oct 11 15:03:36 2005 +0200
     1.3 @@ -103,7 +103,6 @@
     1.4    sig
     1.5    val relevant : int ref
     1.6    val use_simpset: bool ref
     1.7 -  val use_nameless: bool ref
     1.8    val get_clasimp_lemmas : 
     1.9           Proof.context -> term -> 
    1.10           (ResClause.clause * thm) Array.array * ResClause.clause list 
    1.11 @@ -112,7 +111,6 @@
    1.12  structure ResClasimp : RES_CLASIMP =
    1.13  struct
    1.14  val use_simpset = ref false;   (*Performance is much better without simprules*)
    1.15 -val use_nameless = ref true;
    1.16  
    1.17  val relevant = ref 0;  (*Relevance filtering is off by default*)
    1.18  
    1.19 @@ -122,11 +120,14 @@
    1.20        (setmp print_mode [] 
    1.21  	(Pretty.setmp_margin 999 string_of_thm));
    1.22  	
    1.23 +(*Returns the first substring enclosed in quotation marks, typically omitting 
    1.24 +  the [.] of meta-level assumptions.*)
    1.25 +val firstquoted = hd o (String.tokens (fn c => c = #"\""))
    1.26 +	
    1.27  fun fake_thm_name th = 
    1.28 -    Context.theory_name (theory_of_thm th) ^ "." ^ unenclose (plain_string_of_thm th);
    1.29 +    Context.theory_name (theory_of_thm th) ^ "." ^ firstquoted (plain_string_of_thm th);
    1.30  
    1.31 -fun put_name_pair ("",th) = if !use_nameless then (fake_thm_name th, th)
    1.32 -                            else ("HOL.TrueI",TrueI)
    1.33 +fun put_name_pair ("",th) = (fake_thm_name th, th)
    1.34    | put_name_pair (a,th)  = (a,th);
    1.35  
    1.36  (* outputs a list of (thm,clause) pairs *)
    1.37 @@ -145,35 +146,27 @@
    1.38    FIXME: argument "goal" is a hack to allow relevance filtering.
    1.39    To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
    1.40  fun get_clasimp_lemmas ctxt goal = 
    1.41 -    let val claset_rules = 
    1.42 -              map put_name_pair
    1.43 -	        (ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.44 -		  (ResAxioms.claset_rules_of_ctxt ctxt));
    1.45 -	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs claset_rules []);
    1.46 -
    1.47 -	val simpset_rules =
    1.48 -	      ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.49 -                (ResAxioms.simpset_rules_of_ctxt ctxt);
    1.50 -	val named_simpset = map put_name_pair simpset_rules
    1.51 -	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
    1.52 -
    1.53 -	val cls_thms = if !use_simpset then (claset_cls_thms@simpset_cls_thms) 
    1.54 -	               else claset_cls_thms;
    1.55 -	val cls_thms_list = List.concat cls_thms;
    1.56 -	(*************************************************)
    1.57 +    let val claset_cls_thms =
    1.58 +              ResAxioms.clausify_rules_pairs
    1.59 +		(map put_name_pair
    1.60 +		  (ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.61 +		    (ResAxioms.claset_rules_of_ctxt ctxt)))
    1.62 +	val simpset_cls_thms = 
    1.63 +	      if !use_simpset then  
    1.64 +		  ResAxioms.clausify_rules_pairs 
    1.65 +		    (map put_name_pair 
    1.66 +		      (ReduceAxiomsN.relevant_filter (!relevant) goal
    1.67 +		        (ResAxioms.simpset_rules_of_ctxt ctxt))) 
    1.68 +	      else []
    1.69 +	val cls_thms_list = List.concat (claset_cls_thms@simpset_cls_thms)
    1.70  	(* Identify the set of clauses to be written out *)
    1.71 -	(*************************************************)
    1.72  	val clauses = map #1(cls_thms_list);
    1.73  	val cls_nums = map ResClause.num_of_clauses clauses;
    1.74          val whole_list = List.concat 
    1.75                (map clause_numbering (ListPair.zip (cls_thms_list, cls_nums)));
    1.76 - 
    1.77 -        (*********************************************************)
    1.78 -	(* create array and put clausename, number pairs into it *)
    1.79 -	(*********************************************************)
    1.80 -	val clause_arr = Array.fromList whole_list;
    1.81 -  in
    1.82 -	(clause_arr, clauses)
    1.83 + 	
    1.84 +  in  (* create array of put clausename, number pairs into it *)
    1.85 +      (Array.fromList whole_list, clauses)
    1.86    end;
    1.87  
    1.88