author mengj Tue Mar 07 04:04:21 2006 +0100 (2006-03-07) changeset 19200 1da6b9a1575d parent 19199 b338c218cc6e child 19201 294448903a66
relevance_filter takes input axioms as Term.term.
```     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
```