author blanchet Wed, 09 Oct 2013 16:38:48 +0200 changeset 54092 1e2585f56509 parent 54091 4df62d7eae34 child 54093 4e299e2c762d
normalize more equalities
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 09 16:07:33 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 09 16:38:48 2013 +0200
@@ -348,14 +348,14 @@
end
end

-fun normalize_eq (t as @{const Trueprop}
-        \$ ((t0 as Const (@{const_name HOL.eq}, _)) \$ t1 \$ t2)) =
-    if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
-    else HOLogic.mk_Trueprop (t0 \$ t2 \$ t1)
-  | normalize_eq (t as @{const Trueprop} \$ (@{const Not}
+fun normalize_eq (@{const Trueprop} \$ (t as (t0 as Const (@{const_name HOL.eq}, _)) \$ t1 \$ t2)) =
+    if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else t0 \$ t2 \$ t1
+  | normalize_eq (@{const Trueprop} \$ (t as @{const Not}
\$ ((t0 as Const (@{const_name HOL.eq}, _)) \$ t1 \$ t2))) =
-    if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
-    else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 \$ t2 \$ t1))
+    if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 \$ t2 \$ t1)
+  | normalize_eq (Const (@{const_name "=="}, Type (_, [T, _])) \$ t1 \$ t2) =
+    (if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1))
+    |> (fn (t1, t2) => HOLogic.eq_const T \$ t1 \$ t2)
| normalize_eq t = t

fun if_thm_before th th' =
@@ -371,14 +371,11 @@

fun build_name_tables name_of facts =
let
-    fun cons_thm (_, th) =
-      Termtab.cons_list (normalize_vars (normalize_eq (prop_of th)), th)
+    fun cons_thm (_, th) = Termtab.cons_list (normalize_vars (normalize_eq (prop_of th)), th)