# HG changeset patch
# User mengj
# Date 1130459157 -7200
# Node ID ac059afd6b8625370335528377520e441f47d5ee
# Parent  6fe9cb1da9ed07e5699b18aa13dcdc17b6cabd25
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
Also added function "repeat_RS" to the signature.

diff -r 6fe9cb1da9ed -r ac059afd6b86 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri Oct 28 02:24:58 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Fri Oct 28 02:25:57 2005 +0200
@@ -13,23 +13,30 @@
   val elimR2Fol : thm -> term
   val transform_elim : thm -> thm
   val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list
+  val clausify_axiom_pairsH : (string*thm) -> (ResHolClause.clause*thm) list
   val cnf_axiom : (string * thm) -> thm list
+  val cnf_axiomH : (string * thm) -> thm list
   val meta_cnf_axiom : thm -> thm list
+  val meta_cnf_axiomH : thm -> thm list
   val rm_Eps : (term * term) list -> thm list -> term list
   val claset_rules_of_thy : theory -> (string * thm) list
   val simpset_rules_of_thy : theory -> (string * thm) list
   val claset_rules_of_ctxt: Proof.context -> (string * thm) list
   val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
   val clausify_rules_pairs : (string*thm) list -> (ResClause.clause*thm) list list
+  val clausify_rules_pairsH : (string*thm) list -> (ResHolClause.clause*thm) list list
   val clause_setup : (theory -> theory) list
   val meson_method_setup : (theory -> theory) list
   val pairname : thm -> (string * thm)
+  val repeat_RS : thm -> thm -> thm
+
   end;
 
 structure ResAxioms : RES_AXIOMS =
  
 struct
 
+
 val tagging_enabled = false (*compile_time option*)
 
 (**** Transformation of Elimination Rules into First-Order Formulas****)
@@ -147,14 +154,20 @@
 
 (*Convert a theorem into NNF and also skolemize it. Original version, using
   Hilbert's epsilon in the resulting clauses.*)
-fun skolem_axiom th = 
-  let val th' = (skolemize o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) th
+fun skolem_axiom_g mk_nnf th = 
+  let val th' = (skolemize o mk_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) th
   in  repeat_RS th' someI_ex
   end;
 
 
+val skolem_axiom = skolem_axiom_g make_nnf;
+val skolem_axiomH = skolem_axiom_g make_nnf1;
+
+
 fun cnf_rule th = make_clauses [skolem_axiom (transform_elim th)];
 
+fun cnf_ruleH th = make_clauses [skolem_axiomH (transform_elim th)];
+
 (*Transfer a theorem into theory Reconstruction.thy if it is not already
   inside that theory -- because it's needed for Skolemization *)
 
@@ -175,9 +188,12 @@
 val rm_redundant_cls = List.filter (not o is_taut);
 
 (* transform an Isabelle theorem into CNF *)
-fun cnf_axiom_aux th =
+fun cnf_axiom_aux_g cnf_rule th =
     map zero_var_indexes
         (rm_redundant_cls (cnf_rule (transfer_to_Reconstruction th)));
+
+val cnf_axiom_aux = cnf_axiom_aux_g cnf_rule;
+val cnf_axiom_auxH = cnf_axiom_aux_g cnf_ruleH;
        
        
 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
@@ -280,7 +296,7 @@
 	| SOME _ => skolemlist nths thy) (*FIXME: check for duplicate names?*)
 
 (*Exported function to convert Isabelle theorems into axiom clauses*) 
-fun cnf_axiom (name,th) =
+fun cnf_axiom_g cnf_axiom_aux (name,th) =
     case name of
 	  "" => cnf_axiom_aux th (*no name, so can't cache*)
 	| s  => case Symtab.lookup (!clause_cache) s of
@@ -293,12 +309,20 @@
 		      let val cls = cnf_axiom_aux th
 		      in change clause_cache (Symtab.update (s, (th, cls))); cls end;
 
+
+val cnf_axiom = cnf_axiom_g cnf_axiom_aux;
+val cnf_axiomH = cnf_axiom_g cnf_axiom_auxH;
+
+
 fun pairname th = (Thm.name_of_thm th, th);
 
 fun meta_cnf_axiom th = 
     map Meson.make_meta_clause (cnf_axiom (pairname th));
 
 
+fun meta_cnf_axiomH th = 
+    map Meson.make_meta_clause (cnf_axiomH (pairname th));
+
 (* changed: with one extra case added *)
 fun univ_vars_of_aux (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,body)) vars =    
       univ_vars_of_aux body vars
@@ -405,17 +429,25 @@
 (**** Translate a set of classical/simplifier rules into CNF (still as type "thm")  ****)
 
 (* classical rules *)
-fun cnf_rules [] err_list = ([],err_list)
-  | cnf_rules ((name,th) :: ths) err_list = 
-      let val (ts,es) = cnf_rules ths err_list
+fun cnf_rules_g cnf_axiom [] err_list = ([],err_list)
+  | cnf_rules_g cnf_axiom ((name,th) :: ths) err_list = 
+      let val (ts,es) = cnf_rules_g cnf_axiom ths err_list
       in  (cnf_axiom (name,th) :: ts,es) handle  _ => (ts, (th::es))  end;  
 
 
+val cnf_rules = cnf_rules_g cnf_axiom;
+val cnf_rulesH = cnf_rules_g cnf_axiomH;
+
+
 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
 
 fun addclause (c,th) l =
   if ResClause.isTaut c then l else (c,th) :: l;
 
+fun addclauseH (c,th) l =
+    if ResHolClause.isTaut c then l else (c,th)::l;
+
+
 (* outputs a list of (clause,theorem) pairs *)
 fun clausify_axiom_pairs (thm_name,th) =
     let val isa_clauses = cnf_axiom (thm_name,th) 
@@ -429,6 +461,21 @@
 	make_axiom_clauses 0 isa_clauses' isa_clauses		
     end
 
+
+fun clausify_axiom_pairsH (thm_name,th) =
+    let val isa_clauses = cnf_axiomH (thm_name,th) 
+        val isa_clauses' = rm_Eps [] isa_clauses
+        val clauses_n = length isa_clauses
+	fun make_axiom_clauses _ [] []= []
+	  | make_axiom_clauses i (cls::clss) (cls'::clss') =
+	      addclauseH (ResHolClause.make_axiom_clause cls (thm_name,i), cls') 
+	                (make_axiom_clauses (i+1) clss clss')
+    in
+	make_axiom_clauses 0 isa_clauses' isa_clauses		
+    end
+
+
+
 fun clausify_rules_pairs_aux result [] = result
   | clausify_rules_pairs_aux result ((name,th)::ths) =
       clausify_rules_pairs_aux (clausify_axiom_pairs (name,th) :: result) ths
@@ -440,9 +487,22 @@
 		      ": " ^ TermLib.string_of_term t); 
 	       clausify_rules_pairs_aux result ths)
 
-val clausify_rules_pairs = clausify_rules_pairs_aux []
+
+fun clausify_rules_pairs_auxH result [] = result
+  | clausify_rules_pairs_auxH result ((name,th)::ths) =
+      clausify_rules_pairs_auxH (clausify_axiom_pairsH (name,th) :: result) ths
+      handle THM (msg,_,_) =>  
+	      (debug ("Cannot clausify " ^ name ^ ": " ^ msg); 
+	       clausify_rules_pairs_auxH result ths)
+	 |  ResHolClause.LAM2COMB (t) => 
+	      (debug ("Cannot clausify "  ^ TermLib.string_of_term t); 
+	       clausify_rules_pairs_auxH result ths)
 
 
+
+val clausify_rules_pairs = clausify_rules_pairs_aux [];
+
+val clausify_rules_pairsH = clausify_rules_pairs_auxH [];
 (*Setup function: takes a theory and installs ALL simprules and claset rules 
   into the clause cache*)
 fun clause_cache_setup thy =