src/HOL/Tools/ATP/res_clasimpset.ML
changeset 19209 27b91724809f
parent 19201 294448903a66
child 19317 3d383e78b6f4
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Mar 07 16:49:48 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Mar 07 16:50:33 2006 +0100
     1.3 @@ -227,8 +227,7 @@
     1.4    | hashw_term ((Var(_,_)), w) = w
     1.5    | hashw_term ((Bound _), w) = w
     1.6    | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
     1.7 -  | hashw_term ((P$Q), w) =
     1.8 -    hashw_term (Q, (hashw_term (P, w)));
     1.9 +  | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
    1.10  
    1.11  fun hashw_pred (P,w) = 
    1.12      let val (p,args) = strip_comb P
    1.13 @@ -241,8 +240,7 @@
    1.14  
    1.15  
    1.16  fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
    1.17 -  | get_literals (Const("op |",_)$P$Q) lits =
    1.18 -    get_literals Q (get_literals P lits)
    1.19 +  | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
    1.20    | get_literals lit lits = (lit::lits);
    1.21  
    1.22  
    1.23 @@ -263,14 +261,14 @@
    1.24  
    1.25  fun insert_tms [] tms_names = tms_names
    1.26    | insert_tms ((tm,name)::tms_names) tms_names' =
    1.27 -    if mem_tm tm tms_names' then insert_tms tms_names tms_names' else insert_tms tms_names ((tm,name)::tms_names');
    1.28 +      if mem_tm tm tms_names' then insert_tms tms_names tms_names' 
    1.29 +      else insert_tms tms_names ((tm,name)::tms_names');
    1.30  
    1.31  fun warning_thms [] = ()
    1.32    | warning_thms ((name,thm)::nthms) = 
    1.33 -    let val nthm = name ^ ": " ^ (string_of_thm thm)
    1.34 -    in
    1.35 -	(warning nthm; warning_thms nthms)
    1.36 -    end;
    1.37 +      let val nthm = name ^ ": " ^ (string_of_thm thm)
    1.38 +      in warning nthm; warning_thms nthms  end;
    1.39 + 
    1.40  (*Write out the claset, simpset and atpset rules of the supplied theory.*)
    1.41  (* also write supplied user rules, they are not relevance filtered *)
    1.42  fun get_clasimp_atp_lemmas ctxt goals user_thms (use_claset, use_simpset', use_atpset) run_filter =
    1.43 @@ -290,17 +288,21 @@
    1.44        val user_rules = map put_name_pair user_thms
    1.45        val banned = make_banned_test (map #1 (user_rules@atpset_thms@claset_thms@simpset_thms))
    1.46        fun ok (a,_) = not (banned a) 	   
    1.47 -      val claset_cls_tms = if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok claset_thms)
    1.48 -			   else ResAxioms.clausify_rules_pairs_abs claset_thms
    1.49 -      val simpset_cls_tms = if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok simpset_thms)
    1.50 -			    else ResAxioms.clausify_rules_pairs_abs simpset_thms
    1.51 -      val atpset_cls_tms = if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok atpset_thms)
    1.52 -			   else ResAxioms.clausify_rules_pairs_abs atpset_thms
    1.53 +      val claset_cls_tms = 
    1.54 +            if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok claset_thms)
    1.55 +            else ResAxioms.clausify_rules_pairs_abs claset_thms
    1.56 +      val simpset_cls_tms = 
    1.57 +      	    if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok simpset_thms)
    1.58 +	    else ResAxioms.clausify_rules_pairs_abs simpset_thms
    1.59 +      val atpset_cls_tms = 
    1.60 +      	    if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok atpset_thms)
    1.61 +	    else ResAxioms.clausify_rules_pairs_abs atpset_thms
    1.62        val user_cls_tms = ResAxioms.clausify_rules_pairs_abs user_rules (* no filter here, because user supplied rules *)
    1.63        val cls_tms_list = make_unique (mk_clause_table 2200) 
    1.64 -                                      (List.concat (user_cls_tms@atpset_cls_tms@simpset_cls_tms@claset_cls_tms))
    1.65 +                           (List.concat (user_cls_tms@atpset_cls_tms@simpset_cls_tms@claset_cls_tms))
    1.66        val relevant_cls_tms_list =
    1.67 -	  if run_filter then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_tms_list goals
    1.68 +	  if run_filter 
    1.69 +	  then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_tms_list goals
    1.70  	  else cls_tms_list
    1.71        val all_relevant_cls_tms_list = insert_tms (List.concat user_cls_tms) relevant_cls_tms_list (*ensure all user supplied rules are output*)	  
    1.72      in