the "all_theorems" option and some fixes
authorpaulson
Thu Jun 15 17:50:47 2006 +0200 (2006-06-15 ago)
changeset 198947c7e15b27145
parent 19893 7546dafb3fc6
child 19895 cab56c949350
the "all_theorems" option and some fixes
src/HOL/Tools/meson.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/meson.ML	Thu Jun 15 17:50:30 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Jun 15 17:50:47 2006 +0200
     1.3 @@ -123,7 +123,8 @@
     1.4    in  exists taut_poslit poslits
     1.5        orelse
     1.6        exists (fn t => mem_term (t, neglits)) (HOLogic.false_const :: poslits)
     1.7 -  end;
     1.8 +  end
     1.9 +  handle TERM _ => false;	(*probably dest_Trueprop on a weird theorem*)		      
    1.10  
    1.11  
    1.12  (*** To remove trivial negated equality literals from clauses ***)
    1.13 @@ -154,11 +155,20 @@
    1.14  (*Simplify a clause by applying reflexivity to its negated equality literals*)
    1.15  fun refl_clause th = 
    1.16    let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
    1.17 -  in  zero_var_indexes (refl_clause_aux neqs th)  end;
    1.18 +  in  zero_var_indexes (refl_clause_aux neqs th)  end
    1.19 +  handle TERM _ => th;	(*probably dest_Trueprop on a weird theorem*)		      
    1.20  
    1.21  
    1.22  (*** The basic CNF transformation ***)
    1.23  
    1.24 +(*Estimate the number of clauses in order to detect infeasible theorems*)
    1.25 +fun nclauses (Const("Trueprop",_) $ t) = nclauses t
    1.26 +  | nclauses (Const("op &",_) $ t $ u) = nclauses t + nclauses u
    1.27 +  | nclauses (Const("Ex", _) $ Abs (_,_,t)) = nclauses t
    1.28 +  | nclauses (Const("All",_) $ Abs (_,_,t)) = nclauses t
    1.29 +  | nclauses (Const("op |",_) $ t $ u) = nclauses t * nclauses u
    1.30 +  | nclauses _ = 1; (* literal *)
    1.31 +
    1.32  (*Replaces universally quantified variables by FREE variables -- because
    1.33    assumptions may not contain scheme variables.  Later, call "generalize". *)
    1.34  fun freeze_spec th =
    1.35 @@ -179,7 +189,7 @@
    1.36    Eliminates existential quantifiers using skoths: Skolemization theorems.*)
    1.37  fun cnf skoths (th,ths) =
    1.38    let fun cnf_aux (th,ths) =
    1.39 -        if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
    1.40 +  	if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
    1.41          else if not (has_consts ["All","Ex","op &"] (prop_of th))  
    1.42  	then th::ths (*no work to do, terminate*)
    1.43  	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
    1.44 @@ -199,7 +209,9 @@
    1.45  	  | _ => (*no work to do*) th::ths 
    1.46        and cnf_nil th = cnf_aux (th,[])
    1.47    in 
    1.48 -    cnf_aux (th,ths)
    1.49 +    if nclauses (concl_of th) > 20 
    1.50 +    then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths)
    1.51 +    else cnf_aux (th,ths)
    1.52    end;
    1.53  
    1.54  (*Convert all suitable free variables to schematic variables, 
    1.55 @@ -379,15 +391,18 @@
    1.56    which are needed to avoid the various one-point theorems from generating junk clauses.*)
    1.57  val tag_True = thm "tag_True";
    1.58  val tag_False = thm "tag_False";
    1.59 -val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False]
    1.60 +val nnf_simps =
    1.61 +     [simp_implies_def, Ex1_def, Ball_def, Bex_def, tag_True, tag_False, if_True, 
    1.62 +      if_False, if_cancel, if_eq_cancel, cases_simp];
    1.63 +val nnf_extra_simps =
    1.64 +      thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
    1.65  
    1.66  val nnf_ss =
    1.67 -    HOL_basic_ss addsimps
    1.68 -     (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp] @
    1.69 -      thms"split_ifs" @ ex_simps @ all_simps @ simp_thms)
    1.70 -     addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
    1.71 +    HOL_basic_ss addsimps nnf_extra_simps 
    1.72 +                 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
    1.73  
    1.74 -fun make_nnf th = th |> simplify nnf_ss
    1.75 +fun make_nnf th = th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
    1.76 +                     |> simplify nnf_ss  (*But this doesn't simplify premises...*)
    1.77                       |> make_nnf1
    1.78  
    1.79  (*Pull existential quantifiers to front. This accomplishes Skolemization for
     2.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jun 15 17:50:30 2006 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jun 15 17:50:47 2006 +0200
     2.3 @@ -39,10 +39,12 @@
     2.4    val run_relevance_filter: bool ref
     2.5    val run_blacklist_filter: bool ref
     2.6    val invoke_atp_ml : ProofContext.context * thm -> unit
     2.7 +  val add_all : unit -> unit
     2.8    val add_claset : unit -> unit
     2.9    val add_simpset : unit -> unit
    2.10    val add_clasimp : unit -> unit
    2.11    val add_atpset : unit -> unit
    2.12 +  val rm_all : unit -> unit
    2.13    val rm_claset : unit -> unit
    2.14    val rm_simpset : unit -> unit
    2.15    val rm_atpset : unit -> unit
    2.16 @@ -133,13 +135,16 @@
    2.17  	else error ("No such directory: " ^ !destdir)
    2.18      end;
    2.19  
    2.20 +val include_all = ref false;
    2.21  val include_simpset = ref false;
    2.22  val include_claset = ref false; 
    2.23  val include_atpset = ref true;
    2.24 +val add_all = (fn () => include_all:=true);
    2.25  val add_simpset = (fn () => include_simpset:=true);
    2.26  val add_claset = (fn () => include_claset:=true);
    2.27  val add_clasimp = (fn () => (include_simpset:=true;include_claset:=true));
    2.28  val add_atpset = (fn () => include_atpset:=true);
    2.29 +val rm_all = (fn () => include_all:=false);
    2.30  val rm_simpset = (fn () => include_simpset:=false);
    2.31  val rm_claset = (fn () => include_claset:=false);
    2.32  val rm_clasimp = (fn () => (include_simpset:=false;include_claset:=false));
    2.33 @@ -512,47 +517,55 @@
    2.34        in Output.debug nthm; display_thms nthms  end;
    2.35   
    2.36  
    2.37 +fun all_facts_of ctxt =
    2.38 +  FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
    2.39 +  |> maps #2 |> map (`Thm.name_of_thm);
    2.40 +
    2.41  (* get lemmas from claset, simpset, atpset and extra supplied rules *)
    2.42  fun get_clasimp_atp_lemmas ctxt user_thms = 
    2.43 -    let val claset_thms =
    2.44 -	    if !include_claset then
    2.45 -		map put_name_pair (ResAxioms.claset_rules_of_ctxt ctxt)
    2.46 -	    else []
    2.47 -	val simpset_thms = 
    2.48 -	    if !include_simpset then 
    2.49 -		map put_name_pair (ResAxioms.simpset_rules_of_ctxt ctxt)
    2.50 -	    else []
    2.51 -	val atpset_thms =
    2.52 -	    if !include_atpset then
    2.53 -		map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt)
    2.54 -	    else []
    2.55 -	val _ = if !Output.show_debug_msgs then (Output.debug "ATP theorems: "; display_thms atpset_thms) else ()		 
    2.56 -	val user_rules = 
    2.57 -	    case user_thms of  (*use whitelist if there are no user-supplied rules*)
    2.58 -		[] => map (put_name_pair o ResAxioms.pairname) (!whitelist)
    2.59 -	      | _  => map put_name_pair user_thms
    2.60 -    in
    2.61 -	(claset_thms, simpset_thms, atpset_thms, user_rules)
    2.62 -    end;
    2.63 +  let val included_thms =
    2.64 +	if !include_all 
    2.65 +	then (tap (fn ths => Output.debug ("Including all " ^ Int.toString (length ths) ^
    2.66 +	                                   " theorems")) 
    2.67 +	          (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
    2.68 +	else 
    2.69 +	let val claset_thms =
    2.70 +		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
    2.71 +		else []
    2.72 +	    val simpset_thms = 
    2.73 +		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
    2.74 +		else []
    2.75 +	    val atpset_thms =
    2.76 +		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
    2.77 +		else []
    2.78 +	    val _ = if !Output.show_debug_msgs 
    2.79 +		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
    2.80 +		    else ()		 
    2.81 +	in  claset_thms @ simpset_thms @ atpset_thms  end
    2.82 +      val user_rules = map (put_name_pair o ResAxioms.pairname)
    2.83 +			   (if null user_thms then !whitelist else user_thms)
    2.84 +  in
    2.85 +      (map put_name_pair included_thms, user_rules)
    2.86 +  end;
    2.87  
    2.88  (* remove lemmas that are banned from the backlist *)
    2.89  fun blacklist_filter thms = 
    2.90 -    if !run_blacklist_filter then 
    2.91 -	let val banned = make_banned_test (map #1 thms)
    2.92 -	    fun ok (a,_) = not (banned a)
    2.93 -	in
    2.94 -	    filter ok thms
    2.95 -	end
    2.96 -    else
    2.97 -	thms;
    2.98 +  if !run_blacklist_filter then 
    2.99 +      let val banned = make_banned_test (map #1 thms)
   2.100 +	  fun ok (a,_) = not (banned a)
   2.101 +      in  filter ok thms  end
   2.102 +  else thms;
   2.103  
   2.104  (* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
   2.105  fun get_relevant_clauses ctxt cls_thms white_cls goals =
   2.106 -    let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms))
   2.107 -	val relevant_cls_thms_list = if !run_relevance_filter then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals else cls_thms_list
   2.108 -    in
   2.109 -        insert_thms (List.concat white_cls) relevant_cls_thms_list 
   2.110 -    end;
   2.111 + let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms))
   2.112 +     val relevant_cls_thms_list = 
   2.113 +	 if !run_relevance_filter 
   2.114 +	 then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals 
   2.115 +	 else cls_thms_list
   2.116 + in
   2.117 +     insert_thms (List.concat white_cls) relevant_cls_thms_list 
   2.118 + end;
   2.119  
   2.120  (***************************************************************)
   2.121  (* ATP invocation methods setup                                *)
   2.122 @@ -587,8 +600,8 @@
   2.123      let val conj_cls = make_clauses conjectures 
   2.124  	val hyp_cls = cnf_hyps_thms ctxt
   2.125  	val goal_cls = conj_cls@hyp_cls
   2.126 -	val (cla_thms,simp_thms,atp_thms,user_rules) = get_clasimp_atp_lemmas ctxt (map ResAxioms.pairname user_thms)
   2.127 -	val rm_black_cls = blacklist_filter (cla_thms@simp_thms@atp_thms) 
   2.128 +	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   2.129 +	val rm_black_cls = blacklist_filter included_thms 
   2.130  	val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls
   2.131  	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   2.132  	val axclauses_as_thms = get_relevant_clauses ctxt cla_simp_atp_clauses user_cls (map prop_of goal_cls)
   2.133 @@ -685,8 +698,8 @@
   2.134  fun write_problem_files pf (ctxt,th)  =
   2.135    let val goals = Thm.prems_of th
   2.136        val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   2.137 -      val (cla_thms,simp_thms,atp_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   2.138 -      val rm_blacklist_cls = blacklist_filter (cla_thms@simp_thms@atp_thms)
   2.139 +      val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   2.140 +      val rm_blacklist_cls = blacklist_filter included_thms
   2.141        val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_blacklist_cls
   2.142        val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses (ResAxioms.cnf_rules_pairs white_thms) goals 
   2.143        val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ 
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Jun 15 17:50:30 2006 +0200
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Jun 15 17:50:47 2006 +0200
     3.3 @@ -44,88 +44,65 @@
     3.4  
     3.5  exception ELIMR2FOL of string;
     3.6  
     3.7 -(* functions used to construct a formula *)
     3.8 -
     3.9 -fun make_disjs [x] = x
    3.10 -  | make_disjs (x :: xs) = HOLogic.mk_disj(x, make_disjs xs)
    3.11 -
    3.12 -fun make_conjs [x] = x
    3.13 -  | make_conjs (x :: xs) =  HOLogic.mk_conj(x, make_conjs xs)
    3.14 -
    3.15  fun add_EX tm [] = tm
    3.16    | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
    3.17  
    3.18 -fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_)) = (p = q)
    3.19 +(*Checks for the premise ~P when the conclusion is P.*)
    3.20 +fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) 
    3.21 +           (Const("Trueprop",_) $ Free(q,_)) = (p = q)
    3.22    | is_neg _ _ = false;
    3.23  
    3.24 -
    3.25 -exception STRIP_CONCL;
    3.26 -
    3.27 -
    3.28 +(*FIXME: What if dest_Trueprop fails?*)
    3.29  fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
    3.30 -      let val P' = HOLogic.dest_Trueprop P
    3.31 -  	  val prems' = P'::prems
    3.32 -      in
    3.33 -	strip_concl' prems' bvs  Q
    3.34 -      end
    3.35 +      strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs  Q
    3.36    | strip_concl' prems bvs P = 
    3.37        let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P)
    3.38 -      in
    3.39 -	add_EX (make_conjs (P'::prems)) bvs
    3.40 -      end;
    3.41 -
    3.42 +      in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end;
    3.43  
    3.44  fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) = 
    3.45        strip_concl prems ((x,xtp)::bvs) concl body
    3.46    | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
    3.47        if (is_neg P concl) then (strip_concl' prems bvs Q)
    3.48        else strip_concl (HOLogic.dest_Trueprop P::prems) bvs  concl Q
    3.49 -  | strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs;
    3.50 +  | strip_concl prems bvs concl _ = add_EX (foldr1 HOLogic.mk_conj prems) bvs;
    3.51   
    3.52 -
    3.53 -fun trans_elim (main,others,concl) =
    3.54 -    let val others' = map (strip_concl [] [] concl) others
    3.55 -	val disjs = make_disjs others'
    3.56 +fun trans_elim (major,minors,concl) =
    3.57 +    let val disjs = foldr1 HOLogic.mk_disj (map (strip_concl [] [] concl) minors)
    3.58      in
    3.59 -	HOLogic.mk_imp (HOLogic.dest_Trueprop main, disjs)
    3.60 +	HOLogic.mk_imp (HOLogic.dest_Trueprop major, disjs)
    3.61      end;
    3.62  
    3.63 -
    3.64 -(* aux function of elim2Fol, take away predicate variable. *)
    3.65 -fun elimR2Fol_aux prems concl = 
    3.66 -    let val nprems = length prems
    3.67 -	val main = hd prems
    3.68 -    in
    3.69 -	if (nprems = 1) then HOLogic.Not $ (HOLogic.dest_Trueprop main)
    3.70 -        else trans_elim (main, tl prems, concl)
    3.71 -    end;
    3.72 -
    3.73 -    
    3.74  (* convert an elim rule into an equivalent formula, of type term. *)
    3.75  fun elimR2Fol elimR = 
    3.76 -    let val elimR' = Drule.freeze_all elimR
    3.77 -	val (prems,concl) = (prems_of elimR', concl_of elimR')
    3.78 -    in
    3.79 -	case concl of Const("Trueprop",_) $ Free(_,Type("bool",[])) 
    3.80 -		      => HOLogic.mk_Trueprop (elimR2Fol_aux prems concl)
    3.81 -                    | Free(x,Type("prop",[])) => HOLogic.mk_Trueprop(elimR2Fol_aux prems concl) 
    3.82 -		    | _ => raise ELIMR2FOL("Not an elimination rule!")
    3.83 -    end;
    3.84 -
    3.85 +  let val elimR' = Drule.freeze_all elimR
    3.86 +      val (prems,concl) = (prems_of elimR', concl_of elimR')
    3.87 +      val _ = case concl of 
    3.88 +		  Const("Trueprop",_) $ Free(_,Type("bool",[])) => ()
    3.89 +		| Free(_, Type("prop",[])) => ()
    3.90 +		| _ => raise ELIMR2FOL "elimR2Fol: Not an elimination rule!"
    3.91 +      val th = case prems of
    3.92 +      		  [] => raise ELIMR2FOL "elimR2Fol: No premises!"
    3.93 +      		| [major] => HOLogic.Not $ (HOLogic.dest_Trueprop major)
    3.94 +      		| major::minors => trans_elim (major, minors, concl)
    3.95 +  in HOLogic.mk_Trueprop th end
    3.96 +  handle exn => 
    3.97 +    (warning ("elimR2Fol raised exception " ^ Toplevel.exn_message exn);
    3.98 +     concl_of elimR);
    3.99  
   3.100  (* check if a rule is an elim rule *)
   3.101  fun is_elimR th = 
   3.102 -    case (concl_of th) of (Const ("Trueprop", _) $ Var (idx,_)) => true
   3.103 -			 | Var(indx,Type("prop",[])) => true
   3.104 -			 | _ => false;
   3.105 +    case concl_of th of Const ("Trueprop", _) $ Var _ => true
   3.106 +		      | Var(_,Type("prop",[])) => true
   3.107 +		      | _ => false;
   3.108  
   3.109  (* convert an elim-rule into an equivalent theorem that does not have the 
   3.110     predicate variable.  Leave other theorems unchanged.*) 
   3.111  fun transform_elim th =
   3.112    if is_elimR th then
   3.113 -    let val tm = elimR2Fol th
   3.114 -	val ctm = cterm_of (sign_of_thm th) tm	
   3.115 +    let val ctm = cterm_of (sign_of_thm th) (elimR2Fol th)
   3.116      in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end
   3.117 +    handle exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^ 
   3.118 +                            " for theorem " ^ string_of_thm th); th)
   3.119   else th;
   3.120  
   3.121  
   3.122 @@ -303,12 +280,12 @@
   3.123  
   3.124  
   3.125  (*Exported function to convert Isabelle theorems into axiom clauses*) 
   3.126 -fun cnf_axiom_g cnf (name,th) =
   3.127 +fun cnf_axiom (name,th) =
   3.128    case name of
   3.129 -	"" => cnf th (*no name, so can't cache*)
   3.130 +	"" => skolem_thm th (*no name, so can't cache*)
   3.131        | s  => case Symtab.lookup (!clause_cache) s of
   3.132  		NONE => 
   3.133 -		  let val cls = cnf th
   3.134 +		  let val cls = skolem_thm th
   3.135  		  in change clause_cache (Symtab.update (s, (th, cls))); cls end
   3.136  	      | SOME(th',cls) =>
   3.137  		  if eq_thm(th,th') then cls
   3.138 @@ -319,15 +296,10 @@
   3.139  
   3.140  fun pairname th = (Thm.name_of_thm th, th);
   3.141  
   3.142 -
   3.143 -val cnf_axiom = cnf_axiom_g skolem_thm;
   3.144 -
   3.145 -
   3.146  fun meta_cnf_axiom th = 
   3.147      map Meson.make_meta_clause (cnf_axiom (pairname th));
   3.148  
   3.149  
   3.150 -
   3.151  (**** Extract and Clausify theorems from a theory's claset and simpset ****)
   3.152  
   3.153  (*Preserve the name of "th" after the transformation "f"*)
   3.154 @@ -374,34 +346,27 @@
   3.155  
   3.156  (**** Translate a set of classical/simplifier rules into CNF (still as type "thm")  ****)
   3.157  
   3.158 -(* classical rules *)
   3.159 -fun cnf_rules_g cnf_axiom [] err_list = ([],err_list)
   3.160 -  | cnf_rules_g cnf_axiom ((name,th) :: ths) err_list = 
   3.161 -      let val (ts,es) = cnf_rules_g cnf_axiom ths err_list
   3.162 +(* classical rules: works for both FOL and HOL *)
   3.163 +fun cnf_rules [] err_list = ([],err_list)
   3.164 +  | cnf_rules ((name,th) :: ths) err_list = 
   3.165 +      let val (ts,es) = cnf_rules ths err_list
   3.166        in  (cnf_axiom (name,th) :: ts,es) handle  _ => (ts, (th::es))  end;  
   3.167  
   3.168 -
   3.169 -(*works for both FOL and HOL*)
   3.170 -val cnf_rules = cnf_rules_g cnf_axiom;
   3.171 -
   3.172 -fun cnf_rules_pairs_aux [] = []
   3.173 -  | cnf_rules_pairs_aux ((name,th)::ths) =
   3.174 -    let val ts = cnf_rules_pairs_aux ths
   3.175 -	fun pair_name_cls k (n, []) = []
   3.176 -	  | pair_name_cls k (n, cls::clss) =
   3.177 -	    (cls, (n,k))::(pair_name_cls (k+1) (n, clss))
   3.178 -    in
   3.179 -	(pair_name_cls 0 (name, cnf_axiom(name,th)))::ts
   3.180 -	handle THM _ => ts | ResClause.CLAUSE _ => ts | ResHolClause.LAM2COMB _ => ts
   3.181 -    end;
   3.182 +fun pair_name_cls k (n, []) = []
   3.183 +  | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
   3.184 + 	    
   3.185 +fun cnf_rules_pairs_aux pairs [] = pairs
   3.186 +  | cnf_rules_pairs_aux pairs ((name,th)::ths) =
   3.187 +      let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) :: pairs
   3.188 +		       handle THM _ => pairs | ResClause.CLAUSE _ => pairs
   3.189 +			    | ResHolClause.LAM2COMB _ => pairs
   3.190 +      in  cnf_rules_pairs_aux pairs' ths  end;
   3.191      
   3.192 -
   3.193 -fun cnf_rules_pairs thms = rev (cnf_rules_pairs_aux thms);
   3.194 +val cnf_rules_pairs = cnf_rules_pairs_aux [];
   3.195  
   3.196  
   3.197  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
   3.198  
   3.199 -
   3.200  (*These should include any plausibly-useful theorems, especially if they need
   3.201    Skolem functions. FIXME: this list is VERY INCOMPLETE*)
   3.202  val default_initial_thms = map pairname