src/HOL/Tools/res_clause.ML
changeset 18920 7635e0060cd4
parent 18869 00741f7280f7
child 19155 b294c097767e
     1.1 --- a/src/HOL/Tools/res_clause.ML	Fri Feb 03 17:02:33 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Feb 03 17:08:03 2006 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4    val isTaut : clause -> bool
     1.5    val keep_types : bool ref
     1.6    val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order
     1.7 -  val make_axiom_clause : Term.term -> string * int -> clause
     1.8 +  val make_axiom_clause : Term.term -> string * int -> clause option
     1.9    val make_conjecture_clauses : term list -> clause list
    1.10    val make_fixed_const : string -> string		
    1.11    val make_fixed_type_const : string -> string   
    1.12 @@ -392,14 +392,13 @@
    1.13  		      | _ => con_ord
    1.14      end
    1.15  and
    1.16 -
    1.17 -types_ord ([],[]) = EQUAL
    1.18 +    types_ord ([],[]) = EQUAL
    1.19    | types_ord (tps1,tps2) = list_ord type_ord (tps1,tps2);
    1.20  
    1.21  
    1.22 -fun term_ord (UVar(_,_),UVar(_,_)) = EQUAL
    1.23 -  | term_ord (UVar(_,_),_) = LESS
    1.24 -  | term_ord (Fun(_,_,_),UVar(_)) = GREATER
    1.25 +fun term_ord (UVar _, UVar _) = EQUAL
    1.26 +  | term_ord (UVar _, _) = LESS
    1.27 +  | term_ord (Fun _, UVar _) = GREATER
    1.28    | term_ord (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) = 
    1.29       (case string_ord (f1,f2) of
    1.30           EQUAL => 
    1.31 @@ -408,8 +407,7 @@
    1.32         | fn_ord => fn_ord)
    1.33  
    1.34  and
    1.35 -
    1.36 -  terms_ord ([],[]) = EQUAL
    1.37 +      terms_ord ([],[]) = EQUAL
    1.38      | terms_ord (tms1,tms2) = list_ord term_ord (tms1,tms2);
    1.39  
    1.40  
    1.41 @@ -469,7 +467,7 @@
    1.42      (case check_var_pairs (v1,v2) vars of 0 => type_eq (tp1,tp2) (((v1,v2)::vars),tvars)
    1.43  					| 1 => type_eq (tp1,tp2) (vars,tvars)
    1.44  					| 2 => (false,(vars,tvars)))
    1.45 -  | term_eq (UVar(_,_),_) vtvars = (false,vtvars)
    1.46 +  | term_eq (UVar _,_) vtvars = (false,vtvars)
    1.47    | term_eq (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) vtvars =
    1.48        let val (eq1,vtvars1) = 
    1.49  	      if f1 = f2 then terms_eq (tms1,tms2) vtvars
    1.50 @@ -529,7 +527,7 @@
    1.51  
    1.52  val xor_words = List.foldl Word.xorb 0w0;
    1.53  
    1.54 -fun hashw_term (UVar(_,_), w) = w
    1.55 +fun hashw_term (UVar _, w) = w
    1.56    | hashw_term (Fun(f,tps,args), w) = 
    1.57        List.foldl hashw_term (Polyhash.hashw_string (f,w)) args;
    1.58    
    1.59 @@ -579,18 +577,8 @@
    1.60  
    1.61  fun get_tvar_strs [] = []
    1.62    | get_tvar_strs ((FOLTVar indx,s)::tss) = 
    1.63 -      let val vstr = make_schematic_type_var indx
    1.64 -      in
    1.65 -	  vstr ins (get_tvar_strs tss)
    1.66 -      end
    1.67 -  | get_tvar_strs((FOLTFree x,s)::tss) = distinct (get_tvar_strs tss)
    1.68 -
    1.69 -fun make_axiom_clause_thm thm (ax_name,cls_id) =
    1.70 -    let val (lits,types_sorts) = literals_of_term (prop_of thm)
    1.71 -    in 
    1.72 -	make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts)
    1.73 -    end;
    1.74 -
    1.75 +      (make_schematic_type_var indx) ins (get_tvar_strs tss)
    1.76 +  | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
    1.77  
    1.78  (* check if a clause is first-order before making a conjecture clause*)
    1.79  fun make_conjecture_clause n t =
    1.80 @@ -607,15 +595,32 @@
    1.81  
    1.82  val make_conjecture_clauses = make_conjecture_clauses_aux 0
    1.83  
    1.84 +(** Too general means, positive equality literal with a variable X as one operand,
    1.85 +  when X does not occur properly in the other operand. This rules out clearly
    1.86 +  inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
    1.87 +
    1.88 +fun occurs a (UVar(b,_)) = a=b
    1.89 +  | occurs a (Fun (_,_,ts)) = exists (occurs a) ts
    1.90 +
    1.91 +(*Is the first operand a variable that does not properly occur in the second operand?*)
    1.92 +fun too_general_terms (UVar _, UVar _) = false
    1.93 +  | too_general_terms (Fun _, _) = false
    1.94 +  | too_general_terms (UVar (a,_), t) = not (occurs a t);
    1.95 +
    1.96 +fun too_general_lit (Literal (true,Predicate("equal",_,[x,y]),_)) =
    1.97 +      too_general_terms (x,y) orelse too_general_terms(y,x)
    1.98 +  | too_general_lit _ = false;
    1.99  
   1.100  (*before converting an axiom clause to "clause" format, check if it is FOL*)
   1.101  fun make_axiom_clause term (ax_name,cls_id) =
   1.102      let val _ = check_is_fol_term term 
   1.103  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
   1.104  	val (lits,types_sorts) = literals_of_term term
   1.105 -	val lits' = sort_lits lits
   1.106      in 
   1.107 -	make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts)
   1.108 +	if forall too_general_lit lits then
   1.109 +	   (Output.debug ("Omitting " ^ ax_name ^ ": equalities are too general"); 
   1.110 +	    NONE)
   1.111 +	else SOME (make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts))
   1.112      end;
   1.113  
   1.114  
   1.115 @@ -861,10 +866,7 @@
   1.116    | get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist)
   1.117  
   1.118  fun dfg_vars (Clause {literals,...}) =
   1.119 -    let val folterms = List.concat (map dfg_folterms literals)
   1.120 -    in 
   1.121 -        union_all(map get_uvars folterms)
   1.122 -    end
   1.123 +  union_all (map get_uvars (List.concat (map dfg_folterms literals)))
   1.124  
   1.125  fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,types_sorts,...}) =
   1.126      let val (lits,tfree_lits) = dfg_clause_aux cls