rationalized redundant code

--- a/src/HOL/Tools/cnf_funcs.ML	Thu Oct 11 15:57:29 2007 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Thu Oct 11 15:59:31 2007 +0200
@@ -4,6 +4,8 @@
     Author:     Tjark Weber
     Copyright   2005-2006
 
+  FIXME: major overlaps with the code in meson.ML
+
   Description:
   This file contains functions and tactics to transform a formula into
   Conjunctive Normal Form (CNF).
@@ -122,9 +124,6 @@
 
 fun clause_is_trivial c =
 	let
-		(* Term.term -> Term.term list -> Term.term list *)
-		fun collect_literals (Const ("op |", _) $ x $ y) ls = collect_literals x (collect_literals y ls)
-		  | collect_literals x                           ls = x :: ls
 		(* Term.term -> Term.term *)
 		fun dual (Const ("Not", _) $ x) = x
 		  | dual x                      = HOLogic.Not $ x
@@ -132,7 +131,7 @@
 		fun has_duals []      = false
 		  | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs
 	in
-		has_duals (collect_literals c [])
+		has_duals (HOLogic.disjuncts c)
 	end;
 
 (* ------------------------------------------------------------------------- *)

--- a/src/HOL/Tools/metis_tools.ML	Thu Oct 11 15:57:29 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Thu Oct 11 15:59:31 2007 +0200
@@ -529,9 +529,11 @@
         tfrees = tfrees};
         
   (* Function to generate metis clauses, including comb and type clauses *)
-  fun build_map mode thy ctxt cls ths =
-    let val isFO = (mode = ResAtp.Fol) orelse
-                    (mode <> ResAtp.Hol andalso ResAtp.is_fol_thms (cls @ ths))
+  fun build_map mode ctxt cls ths =
+    let val thy = ProofContext.theory_of ctxt
+        val all_thms_FO = forall (Meson.is_fol_term thy o prop_of)
+        val isFO = (mode = ResAtp.Fol) orelse
+                   (mode <> ResAtp.Hol andalso all_thms_FO (cls @ ths))
         val lmap0 = foldl (add_thm true ctxt) 
                           {isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls
         val lmap = foldl (add_thm false ctxt) (add_tfrees lmap0) ths
@@ -559,8 +561,7 @@
 
   (* Main function to start metis prove and reconstruction *)
   fun FOL_SOLVE mode ctxt cls ths0 =
-    let val thy = ProofContext.theory_of ctxt
-        val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0
+    let val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0
         val ths = List.concat (map #2 th_cls_pairs)
         val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
                 else ();
@@ -568,7 +569,7 @@
         val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls
         val _ = Output.debug (fn () => "THEOREM CLAUSES")
         val _ = app (fn th => Output.debug (fn () => string_of_thm th)) ths
-        val {isFO,axioms,tfrees} = build_map mode thy ctxt cls ths
+        val {isFO,axioms,tfrees} = build_map mode ctxt cls ths
         val _ = if null tfrees then ()
                 else (Output.debug (fn () => "TFREE CLAUSES");
                       app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)

--- a/src/HOL/Tools/res_atp.ML	Thu Oct 11 15:57:29 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Oct 11 15:59:31 2007 +0200
@@ -36,7 +36,6 @@
   val rm_simpset : unit -> unit
   val rm_atpset : unit -> unit
   val rm_clasimp : unit -> unit
-  val is_fol_thms : thm list -> bool
   val tvar_classes_of_terms : term list -> string list
   val tfree_classes_of_terms : term list -> string list
   val type_consts_of_terms : theory -> term list -> string list
@@ -137,128 +136,9 @@
 fun add_atpset() = include_atpset:=true;
 fun rm_atpset() = include_atpset:=false;
 
-
-(******************************************************************)
-(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
-(******************************************************************)
-
-datatype logic = FOL | HOL | HOLC | HOLCS;
-
-fun string_of_logic FOL = "FOL"
-  | string_of_logic HOL = "HOL"
-  | string_of_logic HOLC = "HOLC"
-  | string_of_logic HOLCS = "HOLCS";
-
-fun is_fol_logic FOL = true
-  | is_fol_logic  _ = false
-
-(*HOLCS will not occur here*)
-fun upgrade_lg HOLC _ = HOLC
-  | upgrade_lg HOL HOLC = HOLC
-  | upgrade_lg HOL _ = HOL
-  | upgrade_lg FOL lg = lg;
-
-(* check types *)
-fun has_bool_hfn (Type("bool",_)) = true
-  | has_bool_hfn (Type("fun",_)) = true
-  | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
-  | has_bool_hfn _ = false;
-
-fun is_hol_fn tp =
-    let val (targs,tr) = strip_type tp
-    in
-        exists (has_bool_hfn) (tr::targs)
-    end;
-
-fun is_hol_pred tp =
-    let val (targs,tr) = strip_type tp
-    in
-        exists (has_bool_hfn) targs
-    end;
-
-exception FN_LG of term;
-
-fun fn_lg (t as Const(f,tp)) (lg,seen) =
-    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
-  | fn_lg (t as Free(f,tp)) (lg,seen) =
-    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
-  | fn_lg (t as Var(f,tp)) (lg,seen) =
-    if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen)
-  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen)
-  | fn_lg f _ = raise FN_LG(f);
-
+fun strip_Trueprop (Const("Trueprop",_) $ t) = t
+  | strip_Trueprop t = t;
 
-fun term_lg [] (lg,seen) = (lg,seen)
-  | term_lg (tm::tms) (FOL,seen) =
-      let val (f,args) = strip_comb tm
-          val (lg',seen') = if f mem seen then (FOL,seen)
-                            else fn_lg f (FOL,seen)
-      in
-        if is_fol_logic lg' then ()
-        else Output.debug (fn () => ("Found a HOL term: " ^ Display.raw_string_of_term f));
-        term_lg (args@tms) (lg',seen')
-      end
-  | term_lg _ (lg,seen) = (lg,seen)
-
-exception PRED_LG of term;
-
-fun pred_lg (t as Const(P,tp)) (lg,seen)=
-      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen)
-      else (lg,insert (op =) t seen)
-  | pred_lg (t as Free(P,tp)) (lg,seen) =
-      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen)
-      else (lg,insert (op =) t seen)
-  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
-  | pred_lg P _ = raise PRED_LG(P);
-
-
-fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
-  | lit_lg P (lg,seen) =
-      let val (pred,args) = strip_comb P
-          val (lg',seen') = if pred mem seen then (lg,seen)
-                            else pred_lg pred (lg,seen)
-      in
-        if is_fol_logic lg' then ()
-        else Output.debug (fn () => ("Found a HOL predicate: " ^ Display.raw_string_of_term pred));
-        term_lg args (lg',seen')
-      end;
-
-fun lits_lg [] (lg,seen) = (lg,seen)
-  | lits_lg (lit::lits) (FOL,seen) =
-      let val (lg,seen') = lit_lg lit (FOL,seen)
-      in
-        if is_fol_logic lg then ()
-        else Output.debug (fn () => ("Found a HOL literal: " ^ Display.raw_string_of_term lit));
-        lits_lg lits (lg,seen')
-      end
-  | lits_lg lits (lg,seen) = (lg,seen);
-
-fun dest_disj_aux (Const("Trueprop",_) $ t) disjs = dest_disj_aux t disjs
-  | dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
-  | dest_disj_aux t disjs = t::disjs;
-
-fun dest_disj t = dest_disj_aux t [];
-
-fun logic_of_clause tm = lits_lg (dest_disj tm);
-
-fun logic_of_clauses [] (lg,seen) = (lg,seen)
-  | logic_of_clauses (cls::clss) (FOL,seen) =
-    let val (lg,seen') = logic_of_clause cls (FOL,seen)
-        val _ =
-          if is_fol_logic lg then ()
-          else Output.debug (fn () => ("Found a HOL clause: " ^ Display.raw_string_of_term cls))
-    in
-        logic_of_clauses clss (lg,seen')
-    end
-  | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
-
-fun problem_logic_goals_aux [] (lg,seen) = lg
-  | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) =
-    problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
-
-fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
-
-fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL);
 
 (***************************************************************)
 (* Relevance Filtering                                         *)
@@ -544,7 +424,7 @@
 fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
   | hash_literal P = hashw_term(P,0w0);
 
-fun hash_term t = Word.toIntX (xor_words (map hash_literal (dest_disj t)));
+fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t))));
 
 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
 
@@ -705,9 +585,8 @@
 val linkup_logic_mode = ref Auto;
 
 (*Ensures that no higher-order theorems "leak out"*)
-fun restrict_to_logic thy logic cls =
-  if is_fol_logic logic then filter (Meson.is_fol_term thy o prop_of o fst) cls
-                        else cls;
+fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
+  | restrict_to_logic thy false cls = cls;
 
 (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
 
@@ -752,17 +631,13 @@
 val unwanted_types = ["Product_Type.unit","bool"];
 
 fun unwanted t =
-    is_taut t orelse has_typed_var unwanted_types t orelse
-    forall too_general_equality (dest_disj t);
+  is_taut t orelse has_typed_var unwanted_types t orelse
+  forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
 
 (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   likely to lead to unsound proofs.*)
 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
 
-fun tptp_writer thy logic = ResHolClause.tptp_write_file thy (logic=FOL);
-
-fun dfg_writer thy logic = ResHolClause.dfg_write_file thy (logic=FOL);
-
 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
     let val conj_cls = Meson.make_clauses conjectures
@@ -771,14 +646,14 @@
         val goal_cls = conj_cls@hyp_cls
         val goal_tms = map prop_of goal_cls
         val thy = ProofContext.theory_of ctxt
-        val logic = case mode of
-                            Auto => problem_logic_goals [goal_tms]
-                          | Fol => FOL
-                          | Hol => HOL
+        val isFO = case mode of
+                            Auto => forall (Meson.is_fol_term thy) goal_tms
+                          | Fol => true
+                          | Hol => false
         val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
         val cla_simp_atp_clauses = included_thms
                                      |> ResAxioms.cnf_rules_pairs |> make_unique
-                                     |> restrict_to_logic thy logic
+                                     |> restrict_to_logic thy isFO
                                      |> remove_unwanted_clauses
         val user_cls = ResAxioms.cnf_rules_pairs user_rules
         val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
@@ -789,11 +664,11 @@
         (*TFrees in conjecture clauses; TVars in axiom clauses*)
         val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
         val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
-        val writer = if dfg then dfg_writer else tptp_writer
+        val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
         and file = atp_input_file()
         and user_lemmas_names = map #1 user_rules
     in
-        writer thy logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
+        writer thy isFO goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
         Output.debug (fn () => "Writing to " ^ file);
         file
     end;
@@ -866,13 +741,13 @@
         | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
                                          get_neg_subgoals gls (n+1)
       val goal_cls = get_neg_subgoals goals 1
-      val logic = case !linkup_logic_mode of
-                Auto => problem_logic_goals (map (map prop_of) goal_cls)
-              | Fol => FOL
-              | Hol => HOL
+      val isFO = case !linkup_logic_mode of
+			  Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
+			| Fol => true
+			| Hol => false
       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
       val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
-                                       |> restrict_to_logic thy logic
+                                       |> restrict_to_logic thy isFO
                                        |> remove_unwanted_clauses
       val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
       val white_cls = ResAxioms.cnf_rules_pairs white_thms
@@ -880,7 +755,7 @@
       val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
       val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
                   axcls_list
-      val writer = if !prover = Recon.SPASS then dfg_writer else tptp_writer
+      val writer = if !prover = Recon.SPASS then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
       fun write_all [] [] _ = []
         | write_all (ccls::ccls_list) (axcls::axcls_list) k =
             let val fname = probfile k
@@ -901,7 +776,7 @@
                 val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
                 val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
                 val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
-                val clnames = writer thy logic ccls fname (axcls,classrel_clauses,arity_clauses) []
+                val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) []
                 val thm_names = Vector.fromList clnames
                 val _ = if !Output.debugging then trace_vector fname thm_names else ()
             in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end

--- a/src/HOL/Tools/res_reconstruct.ML	Thu Oct 11 15:57:29 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Thu Oct 11 15:59:31 2007 +0200
@@ -282,12 +282,6 @@
   let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples)
   in  map (decode_tstp ctxt vt0) tuples  end;
 
-(*FIXME: simmilar function in res_atp. Move to HOLogic?*)
-fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
-  | dest_disj_aux t disjs = t::disjs;
-
-fun dest_disj t = dest_disj_aux t [];
-
 (** Finding a matching assumption. The literals may be permuted, and variable names
     may disagree. We have to try all combinations of literals (quadratic!) and 
     match up the variable names consistently. **)
@@ -339,10 +333,10 @@
   matches_aux [] (map Envir.eta_contract lits1) (map Envir.eta_contract lits2);
 
 fun permuted_clause t =
-  let val lits = dest_disj t
+  let val lits = HOLogic.disjuncts t
       fun perm [] = NONE
         | perm (ctm::ctms) =
-            if matches (lits, dest_disj (HOLogic.dest_Trueprop (strip_alls ctm)))
+            if matches (lits, HOLogic.disjuncts (HOLogic.dest_Trueprop (strip_alls ctm)))
             then SOME ctm else perm ctms
   in perm end;
 

--- a/src/HOL/hologic.ML	Thu Oct 11 15:57:29 2007 +0200
+++ b/src/HOL/hologic.ML	Thu Oct 11 15:59:31 2007 +0200
@@ -31,6 +31,7 @@
   val mk_not: term -> term
   val dest_conj: term -> term list
   val dest_disj: term -> term list
+  val disjuncts: term -> term list
   val dest_imp: term -> term * term
   val dest_not: term -> term
   val dest_concls: term -> term list
@@ -184,6 +185,12 @@
 fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t'
   | dest_disj t = [t];
 
+(*Like dest_disj, but flattens disjunctions however nested*)
+fun disjuncts_aux (Const ("op |", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
+  | disjuncts_aux t disjs = t::disjs;
+
+fun disjuncts t = disjuncts_aux t [];
+
 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);