src/HOL/Tools/ATP/res_clasimpset.ML
changeset 15907 f377ba412dba
parent 15872 8336ff711d80
child 15919 b30a35432f5a
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Mon May 02 13:30:36 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Mon May 02 13:30:48 2005 +0200
     1.3 @@ -5,22 +5,8 @@
     1.4  
     1.5  (* Get claset rules *)
     1.6  
     1.7 -
     1.8 -
     1.9 -fun remove_all [] rules = rules
    1.10 -|   remove_all (x::xs) rules = let val rules' = List.filter (not_equal x) rules
    1.11 -                              in
    1.12 -                                  remove_all xs rules'
    1.13 -                              end; 
    1.14 -
    1.15  fun has_name th = not((Thm.name_of_thm th)= "")
    1.16  
    1.17 -fun rule_is_fol th = let val tm = prop_of th
    1.18 -                     in 
    1.19 -                        Term.is_first_order tm
    1.20 -                     end
    1.21 -
    1.22 -
    1.23  fun has_name_pair (a,b) = not_equal a "";
    1.24  fun good_pair c (a,b) = not_equal b c;
    1.25  
    1.26 @@ -30,11 +16,9 @@
    1.27  val clause_arr = Array.array(3500, ("empty", 0));
    1.28  
    1.29  
    1.30 +(*
    1.31  val foo_arr = Array.array(20, ("a",0));
    1.32  
    1.33 -
    1.34 -(*
    1.35 -
    1.36  fill_cls_array foo_arr 0 [("b",1), ("c",2), ("d", 3), ("e", 4), ("f",5)];
    1.37  
    1.38  
    1.39 @@ -155,19 +139,6 @@
    1.40  fun memo_find_clause name = case Symtab.lookup (!nc,name) of
    1.41        	        NONE =>  []
    1.42                  |SOME cls  => cls ;
    1.43 -      	        	
    1.44 -
    1.45 -
    1.46 -
    1.47 -fun not_second c (a,b)  = not_equal b c;
    1.48 -
    1.49 -fun remove_all_simps [] name_rule_list:(string*thm) list = name_rule_list
    1.50 -|   remove_all_simps ((x:thm)::xs) (name_rule_list:(string*thm) list) = 
    1.51 -                              let val name_rules' = List.filter (not_second  x) name_rule_list
    1.52 -                              in
    1.53 -                                  remove_all_simps xs name_rules'
    1.54 -                              end; 
    1.55 -
    1.56  
    1.57  
    1.58  fun get_simp_metas [] = [[]]
    1.59 @@ -184,18 +155,12 @@
    1.60                                 
    1.61  
    1.62  fun write_out_clasimp filename (clause_arr:(string * int) Array.array)  = let 
    1.63 -                                  val  outfile = TextIO.openOut("wibble");                                  val _ = TextIO.output (outfile, ("in write_out_clasimpset"))
    1.64 -                                  val _ =  TextIO.closeOut outfile
    1.65 -                                   val _= (warning ("in writeoutclasimp"))
    1.66 +                                   val _= warning "in writeoutclasimp"
    1.67                                     (****************************************)
    1.68                                     (* add claset rules to array and write out as strings *)
    1.69                                     (****************************************)
    1.70 -                                   val claset_rules = ResAxioms.claset_rules_of_thy (the_context())
    1.71 -                                   val claset = ResAxioms.clausify_classical_rules_thy (the_context())
    1.72 -                                   val (claset_clauses,badthms) =  claset;
    1.73 -                                   val clausifiable_rules = remove_all badthms claset_rules;
    1.74 -                                   val named_claset = List.filter has_name clausifiable_rules;
    1.75 -                                   val name_fol_cs = List.filter rule_is_fol  named_claset;
    1.76 +                                   val clausifiable_rules = ResAxioms.claset_rules_of_thy (the_context())
    1.77 +                                   val name_fol_cs = List.filter has_name clausifiable_rules;
    1.78                                     (* length name_fol_cs is 93 *)
    1.79                                     val good_names = map Thm.name_of_thm name_fol_cs;
    1.80   
    1.81 @@ -248,14 +213,8 @@
    1.82                                    val simp_names = map #1 named_simps;
    1.83                                    val simp_rules = map #2 named_simps;
    1.84                                
    1.85 -                                  val (simpset_cls,badthms) = ResAxioms.clausify_rules  simp_rules [];
    1.86                                   (* 1137 clausif simps *)
    1.87 -                                  val name_fol_simps = remove_all_simps badthms named_simps;
    1.88                                     
    1.89 -                                    val simp_names = map #1 name_fol_simps;
    1.90 -                                    val simp_rules = map #2 name_fol_simps;
    1.91 -                                    
    1.92 -                                     (* 995 of these *)
    1.93                                      (* need to get names of claset_cluases so we can make sure we've*)
    1.94                                      (* got the same ones (ie. the named ones ) as the claset rules *)
    1.95                                      (* length 1374*)