inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
authorpaulson
Thu Jul 07 18:25:02 2005 +0200 (2005-07-07)
changeset 167417a6c17b826c0
parent 16740 a5ae2757dd09
child 16742 d1641dba61e5
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Jul 07 18:24:20 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Jul 07 18:25:02 2005 +0200
     1.3 @@ -5,9 +5,124 @@
     1.4      Copyright   2004  University of Cambridge
     1.5  *)
     1.6  
     1.7 +
     1.8 +structure ReduceAxiomsN =
     1.9 +(* Author: Jia Meng, Cambridge University Computer Laboratory
    1.10 +   Remove irrelevant axioms used for a proof of a goal, with with iteration control*)
    1.11 +
    1.12 +struct
    1.13 +
    1.14 +fun add_term_consts_rm ncs (Const(c, _)) cs = 
    1.15 +    if (c mem ncs) then cs else (c ins_string cs)
    1.16 +  | add_term_consts_rm ncs (t $ u) cs = add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
    1.17 +  | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
    1.18 +  | add_term_consts_rm ncs _ cs = cs;
    1.19 +
    1.20 +
    1.21 +fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
    1.22 +
    1.23 +
    1.24 +fun thm_consts_rm ncs thm = term_consts_rm ncs (prop_of thm);
    1.25 +
    1.26 +
    1.27 +fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm;
    1.28 +
    1.29 +
    1.30 +
    1.31 +
    1.32 +fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
    1.33 +
    1.34 +fun make_pairs [] _ = []
    1.35 +  | make_pairs (x::xs) y = (x,y)::(make_pairs xs y);
    1.36 +
    1.37 +
    1.38 +
    1.39 +fun const_thm_list_aux [] cthms = cthms
    1.40 +  | const_thm_list_aux (thm::thms) cthms =
    1.41 +    let val consts = consts_of_thm thm
    1.42 +	val cthms' = make_pairs consts thm 
    1.43 +    in
    1.44 +	const_thm_list_aux thms (cthms' @ cthms)
    1.45 +    end;
    1.46 +
    1.47 +
    1.48 +fun const_thm_list thms = const_thm_list_aux thms [];
    1.49 +
    1.50 +fun make_thm_table thms  = 
    1.51 +    let val consts_thms = const_thm_list thms
    1.52 +    in
    1.53 +	Symtab.make_multi consts_thms
    1.54 +    end;
    1.55 +
    1.56 +
    1.57 +fun consts_in_goal goal = consts_of_term goal;
    1.58 +
    1.59 +fun axioms_having_consts_aux [] tab thms = thms
    1.60 +  | axioms_having_consts_aux (c::cs) tab thms =
    1.61 +    let val thms1 = Symtab.lookup(tab,c)
    1.62 +	val thms2 = 
    1.63 +	    case thms1 of (SOME x) => x
    1.64 +			| NONE => []
    1.65 +    in
    1.66 +	axioms_having_consts_aux cs tab (thms2 union thms)
    1.67 +    end;
    1.68 +
    1.69 +
    1.70 +fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab [];
    1.71 +
    1.72 +
    1.73 +fun relevant_axioms goal thmTab n =  
    1.74 +    let val consts = consts_in_goal goal
    1.75 +	fun relevant_axioms_aux1 cs k =
    1.76 +	    let val thms1 = axioms_having_consts cs thmTab
    1.77 +		val cs1 = ResLib.flat_noDup (map consts_of_thm thms1)
    1.78 +	    in
    1.79 +		if ((cs1 subset cs) orelse (n <= k)) then (k,thms1) 
    1.80 +		else (relevant_axioms_aux1 (cs1 union cs) (k+1))
    1.81 +	    end
    1.82 +
    1.83 +	fun relevant_axioms_aux2 cs k =
    1.84 +	    let val thms1 = axioms_having_consts cs thmTab
    1.85 +		val cs1 = ResLib.flat_noDup (map consts_of_thm thms1)
    1.86 +	    in
    1.87 +		if (cs1 subset cs)  then (k,thms1) 
    1.88 +		else (relevant_axioms_aux2 (cs1 union cs) (k+1))
    1.89 +	    end
    1.90 +
    1.91 +    in
    1.92 +	if n <= 0 then (relevant_axioms_aux2 consts 1) else (relevant_axioms_aux1 consts 1)
    1.93 +    end;
    1.94 +
    1.95 +
    1.96 +
    1.97 +fun relevant_filter n goal thms = #2 (relevant_axioms goal (make_thm_table thms) n);
    1.98 +
    1.99 +
   1.100 +(* find the thms from thy that contain relevant constants, n is the iteration number *)
   1.101 +fun find_axioms_n thy goal n =
   1.102 +    let val clasetR = ResAxioms.claset_rules_of_thy thy
   1.103 +	val simpsetR = ResAxioms.simpset_rules_of_thy thy	  
   1.104 +	val table = make_thm_table (clasetR @ simpsetR)	
   1.105 +    in
   1.106 +	relevant_axioms goal table n
   1.107 +    end;
   1.108 +
   1.109 +
   1.110 +fun find_axioms_n_c thy goal n =
   1.111 +    let val current_thms = PureThy.thms_of thy
   1.112 +	val table = make_thm_table current_thms
   1.113 +    in
   1.114 +	relevant_axioms goal table n
   1.115 +
   1.116 +    end;
   1.117 +
   1.118 +end;
   1.119 +
   1.120 +
   1.121  signature RES_CLASIMP = 
   1.122    sig
   1.123 -     val write_out_clasimp :string -> theory -> (ResClause.clause * thm) Array.array * int
   1.124 +     val write_out_clasimp : string -> theory -> term -> 
   1.125 +                             (ResClause.clause * thm) Array.array * int
   1.126  val write_out_clasimp_small :string -> theory -> (ResClause.clause * thm) Array.array * int
   1.127    end;
   1.128  
   1.129 @@ -72,14 +187,17 @@
   1.130  	(multi_name)
   1.131      end;
   1.132  
   1.133 -(*Write out the claset and simpset rules of the supplied theory.*)
   1.134 -fun write_out_clasimp filename thy = 
   1.135 -    let val claset_rules = ResAxioms.claset_rules_of_thy thy;
   1.136 +(*Write out the claset and simpset rules of the supplied theory.
   1.137 +  FIXME: argument "goal" is a hack to allow relevance filtering.*)
   1.138 +fun write_out_clasimp filename thy goal = 
   1.139 +    let val claset_rules = ReduceAxiomsN.relevant_filter 1 goal 
   1.140 +                              (ResAxioms.claset_rules_of_thy thy);
   1.141  	val named_claset = List.filter has_name_pair claset_rules;
   1.142  	val claset_names = map remove_spaces_pair (named_claset)
   1.143  	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
   1.144  
   1.145 -	val simpset_rules = ResAxioms.simpset_rules_of_thy thy;
   1.146 +	val simpset_rules = ReduceAxiomsN.relevant_filter 1 goal 
   1.147 +	                       (ResAxioms.simpset_rules_of_thy thy);
   1.148  	val named_simpset = 
   1.149  	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
   1.150  	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
     2.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jul 07 18:24:20 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jul 07 18:25:02 2005 +0200
     2.3 @@ -287,10 +287,13 @@
     2.4  (******************************************************************)
     2.5  (*FIX changed to clasimp_file *)
     2.6  fun isar_atp' (ctxt,thms, thm) =
     2.7 + if null (prems_of thm) then () 
     2.8 + else
     2.9      let 
    2.10 -	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    2.11 +	val _= (print_mode := (Library.gen_rems (op =) 
    2.12 +	                       (! print_mode, ["xsymbols", "symbols"])))
    2.13          val _= (warning ("in isar_atp'"))
    2.14 -        val prems  = prems_of thm
    2.15 +        val prems = prems_of thm
    2.16          val sign = sign_of_thm thm
    2.17          val thms_string = Meson.concat_with_and (map string_of_thm thms) 
    2.18          val thmstring = string_of_thm thm
    2.19 @@ -298,22 +301,21 @@
    2.20          
    2.21  	(* set up variables for writing out the clasimps to a tptp file *)
    2.22  	val (clause_arr, num_of_clauses) =
    2.23 -	    ResClasimp.write_out_clasimp(*_small*) (File.platform_path clasimp_file) 
    2.24 +	    ResClasimp.write_out_clasimp (File.platform_path clasimp_file) 
    2.25  	                                 (ProofContext.theory_of ctxt)
    2.26 -        val _ = (warning ("clasimp_file is this: "^(File.platform_path clasimp_file)) )  
    2.27 -           
    2.28 -        
    2.29 +	                                 (hd prems) (*FIXME: hack!! need to do all prems*)
    2.30 +        val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file) 
    2.31          val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses)
    2.32 -        val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
    2.33 +        val pidstring = string_of_int(Word.toInt
    2.34 +                           (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
    2.35      in
    2.36 -	case prems of [] => () 
    2.37 -		    | _ => ((warning ("initial thms: "^thms_string)); 
    2.38 -                           (warning ("initial thm: "^thmstring));
    2.39 -                           (warning ("subgoals: "^prems_string));
    2.40 -                           (warning ("pid: "^ pidstring))); 
    2.41 -                            isar_atp_aux thms thm (length prems) (childin, childout, pid) ;
    2.42 -                           (warning("turning xsymbol back on!"));
    2.43 -                           print_mode := (["xsymbols", "symbols"] @ ! print_mode)
    2.44 +       warning ("initial thms: "^thms_string); 
    2.45 +       warning ("initial thm: "^thmstring);
    2.46 +       warning ("subgoals: "^prems_string);
    2.47 +       warning ("pid: "^ pidstring); 
    2.48 +       isar_atp_aux thms thm (length prems) (childin, childout, pid);
    2.49 +       warning("turning xsymbol back on!");
    2.50 +       print_mode := (["xsymbols", "symbols"] @ ! print_mode)
    2.51      end;
    2.52  
    2.53  
     3.1 --- a/src/HOL/Tools/res_clause.ML	Thu Jul 07 18:24:20 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Jul 07 18:25:02 2005 +0200
     3.3 @@ -577,7 +577,7 @@
     3.4    | string_of_term (Fun (name,typ,terms)) = 
     3.5      let val terms' = map string_of_term terms
     3.6      in
     3.7 -        if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms'))
     3.8 +        if (!keep_types) then name ^ (ResLib.list_to_string (terms' @ [typ]))
     3.9          else name ^ (ResLib.list_to_string terms')
    3.10      end;
    3.11  
    3.12 @@ -590,7 +590,8 @@
    3.13    | string_of_predicate (Predicate(name,typ,terms)) = 
    3.14      let val terms_as_strings = map string_of_term terms
    3.15      in
    3.16 -        if (!keep_types) then name ^ (ResLib.list_to_string  (typ :: terms_as_strings))
    3.17 +        if (!keep_types) 
    3.18 +        then name ^ (ResLib.list_to_string  (terms_as_strings @ [typ]))
    3.19          else name ^ (ResLib.list_to_string terms_as_strings) 
    3.20      end;
    3.21