# HG changeset patch
# User mengj
# Date 1145678799 -7200
# Node ID ef0ed2fe7bf2c15ae84b000d41cd172e116fcc66
# Parent  c7a25c05986cd5fda26b9773684c4a81132ef33e
Changed the treatment of equalities.

diff -r c7a25c05986c -r ef0ed2fe7bf2 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Thu Apr 20 04:20:06 2006 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Sat Apr 22 06:06:39 2006 +0200
@@ -196,8 +196,7 @@
 		  | CombFree of string * ctyp
 		  | CombVar of string * ctyp
 		  | CombApp of combterm * combterm * ctyp
-		  | Bool of combterm
-		  | Equal of combterm * combterm;
+		  | Bool of combterm;
 datatype literal = Literal of polarity * combterm;
 
 
@@ -243,7 +242,6 @@
     end
   | term_ord (CombConst(_,_,_),_) = LESS
   | term_ord (CombApp(_,_,_),Bool(_)) = raise TERM_ORD("bool")
-  | term_ord (CombApp(_,_,_),Equal(_,_)) = LESS
   | term_ord (CombApp(f1,arg1,tp1),CombApp(f2,arg2,tp2)) =
     let val ord1 = term_ord (f1,f2)
 	val ord2 = case ord1 of EQUAL => term_ord (arg1,arg2)
@@ -253,15 +251,9 @@
 		   | _ => ord2
     end
   | term_ord (CombApp(_,_,_),_) = GREATER
-  | term_ord (Bool(_),_) = raise TERM_ORD("bool")
-  | term_ord (Equal(t1,t2),Equal(t3,t4)) = ResClause.list_ord term_ord ([t1,t2],[t3,t4])
-  | term_ord (Equal(_,_),_) = GREATER;
+  | term_ord (Bool(_),_) = raise TERM_ORD("bool");
 
-fun predicate_ord (Equal(_,_),Bool(_)) = LESS
-  | predicate_ord (Equal(t1,t2),Equal(t3,t4)) = 
-    ResClause.list_ord term_ord ([t1,t2],[t3,t4])
-  | predicate_ord (Bool(_),Equal(_,_)) = GREATER
-  | predicate_ord (Bool(t1),Bool(t2)) = term_ord (t1,t2)
+fun predicate_ord (Bool(t1),Bool(t2)) = term_ord (t1,t2)
 
 
 fun literal_ord (Literal(false,_),Literal(true,_)) = LESS
@@ -437,12 +429,6 @@
     in
 	(v'',ts)
     end
-  | combterm_of (Const("op =",T) $ P $ Q) = (*FIXME: allow equal between bools?*)
-    let val (P',tsP) = combterm_of P        
-	val (Q',tsQ) = combterm_of Q
-    in
-	(Equal(P',Q'),tsP union tsQ)
-    end
   | combterm_of (t as (P $ Q)) =
     let val (P',tsP) = combterm_of P
 	val (Q',tsQ) = combterm_of Q
@@ -551,8 +537,9 @@
 (* convert literals of clauses into strings *)
 fun string_of_combterm1_aux _ (CombConst(c,tp,_)) = 
     let val tp' = string_of_ctyp tp
+	val c' = if c = "equal" then "fequal" else c
     in
-	(wrap_type (c,tp'),tp')
+	(wrap_type (c',tp'),tp')
     end
   | string_of_combterm1_aux _ (CombFree(v,tp)) = 
     let val tp' = string_of_ctyp tp
@@ -575,26 +562,33 @@
     in	(r,tp')
 
     end
+  | string_of_combterm1_aux is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
+    if is_pred then 
+	let val (s1,_) = string_of_combterm1_aux false t1
+	    val (s2,_) = string_of_combterm1_aux false t2
+	in
+	    ("equal" ^ (ResClause.paren_pack [s1,s2]),bool_tp)
+	end
+    else
+	let val (t,_) = string_of_combterm1_aux false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
+	in
+	    (t,bool_tp)
+	end
   | string_of_combterm1_aux is_pred (Bool(t)) = 
     let val (t',_) = string_of_combterm1_aux false t
 	val r = if is_pred then bool_str ^ (ResClause.paren_pack [t'])
 		else t'
     in
 	(r,bool_tp)
-    end
-  | string_of_combterm1_aux _ (Equal(t1,t2)) =
-    let val (s1,_) = string_of_combterm1_aux false t1
-	val (s2,_) = string_of_combterm1_aux false t2
-    in
-	("equal" ^ (ResClause.paren_pack [s1,s2]),bool_tp) 
     end;
 
 fun string_of_combterm1 is_pred term = fst (string_of_combterm1_aux is_pred term);
 
 fun string_of_combterm2 _ (CombConst(c,tp,tvars)) = 
     let val tvars' = map string_of_ctyp tvars
+	val c' = if c = "equal" then "fequal" else c
     in
-	c ^ (ResClause.paren_pack tvars')
+	c' ^ (ResClause.paren_pack tvars')
     end
   | string_of_combterm2 _ (CombFree(v,tp)) = v
   | string_of_combterm2 _ (CombVar(v,tp)) = v
@@ -604,17 +598,21 @@
     in
 	app_str ^ (ResClause.paren_pack [s1,s2])
     end
+  | string_of_combterm2 is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
+    if is_pred then 
+	let val s1 = string_of_combterm2 false t1
+	    val s2 = string_of_combterm2 false t2
+	in
+	    ("equal" ^ (ResClause.paren_pack [s1,s2]))
+	end
+    else
+	string_of_combterm2 false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
+ 
   | string_of_combterm2 is_pred (Bool(t)) = 
     let val t' = string_of_combterm2 false t
     in
 	if is_pred then bool_str ^ (ResClause.paren_pack [t'])
 	else t'
-    end
-  | string_of_combterm2 _ (Equal(t1,t2)) =
-    let val s1 = string_of_combterm2 false t1
-	val s2 = string_of_combterm2 false t2
-    in
-	("equal" ^ (ResClause.paren_pack [s1,s2])) 
     end;
 
 
@@ -696,14 +694,7 @@
     end
   | combterm_eq (CombApp(_,_,_),_) vtvars = (false,vtvars)
   | combterm_eq (Bool(t1),Bool(t2)) vtvars = combterm_eq (t1,t2) vtvars
-  | combterm_eq (Bool(_),_) vtvars = (false,vtvars)
-  | combterm_eq (Equal(t1,t2),Equal(t3,t4)) vtvars =
-    let val (eq1,vtvars1) = combterm_eq (t1,t3) vtvars
-    in
-	if eq1 then combterm_eq (t2,t4) vtvars1
-	else (eq1,vtvars1)
-    end
-  | combterm_eq (Equal(t1,t2),_) vtvars = (false,vtvars);
+  | combterm_eq (Bool(_),_) vtvars = (false,vtvars);
 
 fun lit_eq (Literal(pol1,pred1),Literal(pol2,pred2)) vtvars =
     if (pol1 = pol2) then combterm_eq (pred1,pred2) vtvars
@@ -730,9 +721,7 @@
   | hash_combterm (CombFree(f,_),w) = Polyhash.hashw_string(f,w)
   | hash_combterm (CombConst(c,tp,tps),w) = Polyhash.hashw_string(c,w)
   | hash_combterm (CombApp(f,arg,tp),w) = hash_combterm (arg, hash_combterm (f,w))
-  | hash_combterm (Bool(t),w) = hash_combterm (t,w)
-  | hash_combterm (Equal(t1,t2),w) = 
-    List.foldl hash_combterm (Polyhash.hashw_string ("equal",w)) [t1,t2]
+  | hash_combterm (Bool(t),w) = hash_combterm (t,w);
 
 fun hash_literal (Literal(true,pred)) = hash_combterm(pred,0w0)
   | hash_literal (Literal(false,pred)) = Word.notb(hash_combterm(pred,0w0));