src/HOL/Tools/ATP/res_clasimpset.ML
changeset 16741 7a6c17b826c0
parent 16357 f1275d2a1dee
child 16795 b400b53d8f7d
     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 []);