relevance_filter takes input axioms as Term.term.
authormengj
Tue Mar 07 04:04:21 2006 +0100 (2006-03-07)
changeset 192001da6b9a1575d
parent 19199 b338c218cc6e
child 19201 294448903a66
relevance_filter takes input axioms as Term.term.
src/HOL/Tools/ATP/reduce_axiomsN.ML
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Tue Mar 07 04:01:25 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Tue Mar 07 04:04:21 2006 +0100
     1.3 @@ -75,11 +75,11 @@
     1.4  
     1.5  
     1.6  fun relevant_clauses_ax_g_1 _ []  _ (ax,r) = (ax,r)
     1.7 -  | relevant_clauses_ax_g_1 gconsts  ((clsthm,(consts,_))::y) P (ax,r) =
     1.8 +  | relevant_clauses_ax_g_1 gconsts  ((clstm,(consts,_))::y) P (ax,r) =
     1.9      let val weight = find_clause_weight_s_1 gconsts consts 1.0
    1.10      in
    1.11 -	if  P <= weight then relevant_clauses_ax_g_1 gconsts y P ((clsthm,(consts,weight))::ax,r)
    1.12 -	else relevant_clauses_ax_g_1 gconsts y P (ax,(clsthm,(consts,weight))::r)
    1.13 +	if  P <= weight then relevant_clauses_ax_g_1 gconsts y P ((clstm,(consts,weight))::ax,r)
    1.14 +	else relevant_clauses_ax_g_1 gconsts y P (ax,(clstm,(consts,weight))::r)
    1.15      end;
    1.16  
    1.17  
    1.18 @@ -87,22 +87,21 @@
    1.19      (case addc of [] => rel_axs @ keep
    1.20  		| _ => case tmpc of [] => addc @ rel_axs @ keep
    1.21  				  | _ => relevant_clauses_ax_1 addc tmpc P ([],[]) (rel_axs @ keep))
    1.22 -  | relevant_clauses_ax_1 rel_axs ((clsthm,(consts,weight))::e_axs) P (addc,tmpc) keep = 
    1.23 +  | relevant_clauses_ax_1 rel_axs ((clstm,(consts,weight))::e_axs) P (addc,tmpc) keep = 
    1.24      let val weight' = find_clause_weight_m_1 rel_axs (consts,weight) 
    1.25 -	val e_ax' = (clsthm,(consts, weight'))
    1.26 +	val e_ax' = (clstm,(consts, weight'))
    1.27      in
    1.28  	
    1.29 -	if P <= weight' then relevant_clauses_ax_1 rel_axs e_axs P ((clsthm,(consts,weight'))::addc,tmpc) keep
    1.30 -	else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clsthm,(consts,weight'))::tmpc) keep 
    1.31 +	if P <= weight' then relevant_clauses_ax_1 rel_axs e_axs P ((clstm,(consts,weight'))::addc,tmpc) keep
    1.32 +	else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clstm,(consts,weight'))::tmpc) keep 
    1.33      end;
    1.34  
    1.35  
    1.36  fun initialize [] ax_weights = ax_weights
    1.37 -  | initialize ((cls,thm)::clss_thms) ax_weights =
    1.38 -    let val tm = prop_of thm
    1.39 -	val consts = consts_of_term tm
    1.40 +  | initialize ((tm,name)::tms_names) ax_weights =
    1.41 +    let val consts = consts_of_term tm
    1.42      in
    1.43 -	initialize clss_thms (((cls,thm),(consts,0.0))::ax_weights)
    1.44 +	initialize tms_names (((tm,name),(consts,0.0))::ax_weights)
    1.45      end;
    1.46  
    1.47  fun relevance_filter1_aux axioms goals = 
    1.48 @@ -139,11 +138,11 @@
    1.49  
    1.50  
    1.51  fun relevant_clauses_ax_g_2 _ []  _ (ax,r) = (ax,r)
    1.52 -  | relevant_clauses_ax_g_2 gpconsts  ((clsthm,(pconsts,_))::y) P (ax,r) =
    1.53 +  | relevant_clauses_ax_g_2 gpconsts  ((clstm,(pconsts,_))::y) P (ax,r) =
    1.54      let val weight = find_clause_weight_s_2 gpconsts pconsts 1.0
    1.55      in
    1.56 -	if  P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clsthm,(pconsts,weight))::ax,r)
    1.57 -	else relevant_clauses_ax_g_2 gpconsts y P (ax,(clsthm,(pconsts,weight))::r)
    1.58 +	if  P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clstm,(pconsts,weight))::ax,r)
    1.59 +	else relevant_clauses_ax_g_2 gpconsts y P (ax,(clstm,(pconsts,weight))::r)
    1.60      end;
    1.61  
    1.62  
    1.63 @@ -151,22 +150,21 @@
    1.64      (case addc of [] => rel_axs @ keep
    1.65  		| _ => case tmpc of [] => addc @ rel_axs @ keep
    1.66  				  | _ => relevant_clauses_ax_2 addc tmpc P ([],[]) (rel_axs @ keep))
    1.67 -  | relevant_clauses_ax_2 rel_axs ((clsthm,(pconsts,weight))::e_axs) P (addc,tmpc) keep = 
    1.68 +  | relevant_clauses_ax_2 rel_axs ((clstm,(pconsts,weight))::e_axs) P (addc,tmpc) keep = 
    1.69      let val weight' = find_clause_weight_m_2 rel_axs (pconsts,weight) 
    1.70 -	val e_ax' = (clsthm,(pconsts, weight'))
    1.71 +	val e_ax' = (clstm,(pconsts, weight'))
    1.72      in
    1.73  	
    1.74 -	if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clsthm,(pconsts,weight'))::addc,tmpc) keep
    1.75 -	else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clsthm,(pconsts,weight'))::tmpc) keep 
    1.76 +	if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clstm,(pconsts,weight'))::addc,tmpc) keep
    1.77 +	else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clstm,(pconsts,weight'))::tmpc) keep 
    1.78      end;
    1.79  
    1.80  
    1.81  fun initialize_w_pol [] ax_weights = ax_weights
    1.82 -  | initialize_w_pol ((cls,thm)::clss_thms) ax_weights =
    1.83 -    let val tm = prop_of thm
    1.84 -	val consts = pconsts_of_term tm
    1.85 +  | initialize_w_pol ((tm,name)::tms_names) ax_weights =
    1.86 +    let val consts = pconsts_of_term tm
    1.87      in
    1.88 -	initialize_w_pol clss_thms (((cls,thm),(consts,0.0))::ax_weights)
    1.89 +	initialize_w_pol tms_names (((tm,name),(consts,0.0))::ax_weights)
    1.90      end;
    1.91  
    1.92  
    1.93 @@ -286,32 +284,31 @@
    1.94  
    1.95  
    1.96  fun relevant_clauses_ax_g_3 _ [] _ (ax,r) = (ax,r)
    1.97 -  | relevant_clauses_ax_g_3 gctyps ((cls_typ,(clsthm,(consts_typs,_)))::y) P (ax,r) =
    1.98 +  | relevant_clauses_ax_g_3 gctyps ((cls_typ,(clstm,(consts_typs,_)))::y) P (ax,r) =
    1.99      let val weight = find_clause_weight_s_3 gctyps consts_typs 1.0
   1.100      in
   1.101 -	if P <= weight then relevant_clauses_ax_g_3 gctyps y P ((cls_typ,(clsthm,(consts_typs,weight)))::ax,r)
   1.102 -	else relevant_clauses_ax_g_3 gctyps y P (ax,(cls_typ,(clsthm,(consts_typs,weight)))::r)
   1.103 +	if P <= weight then relevant_clauses_ax_g_3 gctyps y P ((cls_typ,(clstm,(consts_typs,weight)))::ax,r)
   1.104 +	else relevant_clauses_ax_g_3 gctyps y P (ax,(cls_typ,(clstm,(consts_typs,weight)))::r)
   1.105      end;
   1.106  
   1.107  fun relevant_clauses_ax_3 rel_axs [] P (addc,tmpc) keep =
   1.108      (case addc of [] => (rel_axs @ keep,tmpc)
   1.109  		| _ => case tmpc of [] => (addc @ rel_axs @ keep,[])
   1.110  				  | _ => relevant_clauses_ax_3 addc tmpc P ([],[]) (rel_axs @ keep))
   1.111 -  | relevant_clauses_ax_3 rel_axs ((cls_typ,(clsthm,(consts_typs,weight)))::e_axs) P (addc,tmpc) keep =
   1.112 +  | relevant_clauses_ax_3 rel_axs ((cls_typ,(clstm,(consts_typs,weight)))::e_axs) P (addc,tmpc) keep =
   1.113      let val weight' = find_clause_weight_m_3 rel_axs (consts_typs,weight)
   1.114 -	val e_ax' = (cls_typ,(clsthm,(consts_typs,weight')))
   1.115 +	val e_ax' = (cls_typ,(clstm,(consts_typs,weight')))
   1.116      in
   1.117  	if P <= weight' then relevant_clauses_ax_3 rel_axs e_axs P (e_ax'::addc,tmpc) keep
   1.118  	else relevant_clauses_ax_3 rel_axs e_axs P (addc,e_ax'::tmpc) keep
   1.119      end;
   1.120  
   1.121  fun initialize3 thy [] ax_weights = ax_weights
   1.122 -  | initialize3 thy ((cls,thm)::clss_thms) ax_weights =
   1.123 -    let val tm = prop_of thm
   1.124 -	val cls_type = clause_type tm
   1.125 +  | initialize3 thy ((tm,name)::tms_names) ax_weights =
   1.126 +    let val cls_type = clause_type tm
   1.127  	val consts = consts_typs_of_term thy tm
   1.128      in
   1.129 -	initialize3 thy clss_thms ((cls_type,((cls,thm),(consts,0.0)))::ax_weights)
   1.130 +	initialize3 thy tms_names ((cls_type,((tm,name),(consts,0.0)))::ax_weights)
   1.131      end;
   1.132  
   1.133  fun add_unit_clauses ax [] = ax