# HG changeset patch
# User paulson
# Date 1138982883 -3600
# Node ID 7635e0060cd4199891eaff15aa5bd1af00a7f020
# Parent  340ffeaaaedebaba6f92390b2a698fc7611d6ba3
removal of case analysis clauses

diff -r 340ffeaaaede -r 7635e0060cd4 src/HOL/Tools/res_atp_setup.ML
--- a/src/HOL/Tools/res_atp_setup.ML	Fri Feb 03 17:02:33 2006 +0100
+++ b/src/HOL/Tools/res_atp_setup.ML	Fri Feb 03 17:08:03 2006 +0100
@@ -291,7 +291,9 @@
 (**** clausification ****)
 fun cls_axiom_fol _ _ [] = []
   | cls_axiom_fol name i (tm::tms) =
-   (ResClause.make_axiom_clause tm (name,i)) :: (cls_axiom_fol name (i+1) tms);
+      case ResClause.make_axiom_clause tm (name,i) of 
+          SOME cls => cls :: cls_axiom_fol name (i+1) tms
+        | NONE => cls_axiom_fol name i tms;
 
 fun cls_axiom_hol  _ _ [] = []
   | cls_axiom_hol name i (tm::tms) =
diff -r 340ffeaaaede -r 7635e0060cd4 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri Feb 03 17:02:33 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Fri Feb 03 17:08:03 2006 +0100
@@ -398,9 +398,10 @@
 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
 
 fun make_axiom_clauses _ _ [] = []
-  | make_axiom_clauses name i (cls::clss) =
-      (ResClause.make_axiom_clause (prop_of cls) (name,i), cls) ::
-      (make_axiom_clauses name (i+1) clss)
+  | make_axiom_clauses name i (th::ths) =
+      case ResClause.make_axiom_clause (prop_of th) (name,i) of 
+          SOME cls => (cls, th) :: make_axiom_clauses name (i+1) ths
+        | NONE => make_axiom_clauses name i ths;
 
 (* outputs a list of (clause,theorem) pairs *)
 fun clausify_axiom_pairs (name,th) = 
@@ -408,9 +409,9 @@
            (make_axiom_clauses name 0 (cnf_axiom (name,th)));
 
 fun make_axiom_clausesH _ _ [] = []
-  | make_axiom_clausesH name i (cls::clss) =
-      (ResHolClause.make_axiom_clause (prop_of cls) (name,i), cls) ::
-      (make_axiom_clausesH name (i+1) clss)
+  | make_axiom_clausesH name i (th::ths) =
+      (ResHolClause.make_axiom_clause (prop_of th) (name,i), th) ::
+      (make_axiom_clausesH name (i+1) ths)
 
 fun clausify_axiom_pairsH (name,th) = 
     filter (fn (c,th) => not (ResHolClause.isTaut c))
diff -r 340ffeaaaede -r 7635e0060cd4 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Fri Feb 03 17:02:33 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML	Fri Feb 03 17:08:03 2006 +0100
@@ -34,7 +34,7 @@
   val isTaut : clause -> bool
   val keep_types : bool ref
   val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order
-  val make_axiom_clause : Term.term -> string * int -> clause
+  val make_axiom_clause : Term.term -> string * int -> clause option
   val make_conjecture_clauses : term list -> clause list
   val make_fixed_const : string -> string		
   val make_fixed_type_const : string -> string   
@@ -392,14 +392,13 @@
 		      | _ => con_ord
     end
 and
-
-types_ord ([],[]) = EQUAL
+    types_ord ([],[]) = EQUAL
   | types_ord (tps1,tps2) = list_ord type_ord (tps1,tps2);
 
 
-fun term_ord (UVar(_,_),UVar(_,_)) = EQUAL
-  | term_ord (UVar(_,_),_) = LESS
-  | term_ord (Fun(_,_,_),UVar(_)) = GREATER
+fun term_ord (UVar _, UVar _) = EQUAL
+  | term_ord (UVar _, _) = LESS
+  | term_ord (Fun _, UVar _) = GREATER
   | term_ord (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) = 
      (case string_ord (f1,f2) of
          EQUAL => 
@@ -408,8 +407,7 @@
        | fn_ord => fn_ord)
 
 and
-
-  terms_ord ([],[]) = EQUAL
+      terms_ord ([],[]) = EQUAL
     | terms_ord (tms1,tms2) = list_ord term_ord (tms1,tms2);
 
 
@@ -469,7 +467,7 @@
     (case check_var_pairs (v1,v2) vars of 0 => type_eq (tp1,tp2) (((v1,v2)::vars),tvars)
 					| 1 => type_eq (tp1,tp2) (vars,tvars)
 					| 2 => (false,(vars,tvars)))
-  | term_eq (UVar(_,_),_) vtvars = (false,vtvars)
+  | term_eq (UVar _,_) vtvars = (false,vtvars)
   | term_eq (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) vtvars =
       let val (eq1,vtvars1) = 
 	      if f1 = f2 then terms_eq (tms1,tms2) vtvars
@@ -529,7 +527,7 @@
 
 val xor_words = List.foldl Word.xorb 0w0;
 
-fun hashw_term (UVar(_,_), w) = w
+fun hashw_term (UVar _, w) = w
   | hashw_term (Fun(f,tps,args), w) = 
       List.foldl hashw_term (Polyhash.hashw_string (f,w)) args;
   
@@ -579,18 +577,8 @@
 
 fun get_tvar_strs [] = []
   | get_tvar_strs ((FOLTVar indx,s)::tss) = 
-      let val vstr = make_schematic_type_var indx
-      in
-	  vstr ins (get_tvar_strs tss)
-      end
-  | get_tvar_strs((FOLTFree x,s)::tss) = distinct (get_tvar_strs tss)
-
-fun make_axiom_clause_thm thm (ax_name,cls_id) =
-    let val (lits,types_sorts) = literals_of_term (prop_of thm)
-    in 
-	make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts)
-    end;
-
+      (make_schematic_type_var indx) ins (get_tvar_strs tss)
+  | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
 
 (* check if a clause is first-order before making a conjecture clause*)
 fun make_conjecture_clause n t =
@@ -607,15 +595,32 @@
 
 val make_conjecture_clauses = make_conjecture_clauses_aux 0
 
+(** Too general means, positive equality literal with a variable X as one operand,
+  when X does not occur properly in the other operand. This rules out clearly
+  inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
+
+fun occurs a (UVar(b,_)) = a=b
+  | occurs a (Fun (_,_,ts)) = exists (occurs a) ts
+
+(*Is the first operand a variable that does not properly occur in the second operand?*)
+fun too_general_terms (UVar _, UVar _) = false
+  | too_general_terms (Fun _, _) = false
+  | too_general_terms (UVar (a,_), t) = not (occurs a t);
+
+fun too_general_lit (Literal (true,Predicate("equal",_,[x,y]),_)) =
+      too_general_terms (x,y) orelse too_general_terms(y,x)
+  | too_general_lit _ = false;
 
 (*before converting an axiom clause to "clause" format, check if it is FOL*)
 fun make_axiom_clause term (ax_name,cls_id) =
     let val _ = check_is_fol_term term 
 	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
 	val (lits,types_sorts) = literals_of_term term
-	val lits' = sort_lits lits
     in 
-	make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts)
+	if forall too_general_lit lits then
+	   (Output.debug ("Omitting " ^ ax_name ^ ": equalities are too general"); 
+	    NONE)
+	else SOME (make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts))
     end;
 
 
@@ -861,10 +866,7 @@
   | get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist)
 
 fun dfg_vars (Clause {literals,...}) =
-    let val folterms = List.concat (map dfg_folterms literals)
-    in 
-        union_all(map get_uvars folterms)
-    end
+  union_all (map get_uvars (List.concat (map dfg_folterms literals)))
 
 fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,types_sorts,...}) =
     let val (lits,tfree_lits) = dfg_clause_aux cls