src/HOL/Tools/ATP/reduce_axiomsN.ML
changeset 19355 3140daf6863d
parent 19337 146b25b893bb
child 19448 72dab71cb11e
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Fri Apr 07 05:12:51 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Fri Apr 07 05:14:06 2006 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4  
     1.5  structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
     1.6  
     1.7 -fun count_axiom_consts thy ((t,_), tab) = 
     1.8 +fun count_axiom_consts thy ((thm,_), tab) = 
     1.9    let fun count_const (a, T, tab) =
    1.10  	let val (c, cts) = const_with_typ thy (a,T)
    1.11  	    val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)
    1.12 @@ -101,7 +101,7 @@
    1.13  	    count_term_consts (t, count_term_consts (u, tab))
    1.14  	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
    1.15  	| count_term_consts (_, tab) = tab
    1.16 -  in  count_term_consts (t, tab)  end;
    1.17 +  in  count_term_consts (prop_of thm, tab)  end;
    1.18  
    1.19  
    1.20  (******** filter clauses ********)
    1.21 @@ -127,8 +127,8 @@
    1.22  	rel_weight / (rel_weight + real (length consts_typs - length rel))
    1.23      end;
    1.24      
    1.25 -fun pair_consts_typs_axiom thy (tm,name) =
    1.26 -    ((tm,name), (consts_typs_of_term thy tm));
    1.27 +fun pair_consts_typs_axiom thy (thm,name) =
    1.28 +    ((thm,name), (consts_typs_of_term thy (prop_of thm)));
    1.29  
    1.30  exception ConstFree;
    1.31  fun dest_ConstFree (Const aT) = aT
    1.32 @@ -136,18 +136,19 @@
    1.33    | dest_ConstFree _ = raise ConstFree;
    1.34  
    1.35  (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
    1.36 -fun defines thy (tm,(name,n)) gctypes =
    1.37 -  let fun defs hs =
    1.38 -        let val (rator,args) = strip_comb hs
    1.39 -            val ct = const_with_typ thy (dest_ConstFree rator)
    1.40 -        in  forall is_Var args andalso uni_mem ct gctypes  end
    1.41 -        handle ConstFree => false
    1.42 -  in    
    1.43 -    case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ _) => 
    1.44 -          defs lhs andalso
    1.45 -          (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
    1.46 -      | _ => false
    1.47 -  end
    1.48 +fun defines thy (thm,(name,n)) gctypes =
    1.49 +    let val tm = prop_of thm
    1.50 +	fun defs hs =
    1.51 +            let val (rator,args) = strip_comb hs
    1.52 +		val ct = const_with_typ thy (dest_ConstFree rator)
    1.53 +            in  forall is_Var args andalso uni_mem ct gctypes  end
    1.54 +		handle ConstFree => false
    1.55 +    in    
    1.56 +	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ _) => 
    1.57 +		   defs lhs andalso
    1.58 +		   (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
    1.59 +		 | _ => false
    1.60 +    end
    1.61  
    1.62  fun relevant_clauses thy ctab p rel_consts =
    1.63    let fun relevant (newrels,rejects) []  =
    1.64 @@ -159,10 +160,10 @@
    1.65  	      in Output.debug ("found relevant: " ^ Int.toString (length newrels));
    1.66                   newrels @ relevant_clauses thy ctab newp rel_consts' rejects
    1.67  	      end
    1.68 -	| relevant (newrels,rejects) ((ax as (clstm,consts_typs)) :: axs) =
    1.69 +	| relevant (newrels,rejects) ((ax as (clsthm,consts_typs)) :: axs) =
    1.70  	    let val weight = clause_weight ctab rel_consts consts_typs
    1.71  	    in
    1.72 -	      if p <= weight orelse (!follow_defs andalso defines thy clstm rel_consts)
    1.73 +	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
    1.74  	      then relevant (ax::newrels, rejects) axs
    1.75  	      else relevant (newrels, ax::rejects) axs
    1.76  	    end