removing simple equalities in introduction rules in the predicate compiler

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 29 17:30:39 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 29 17:30:40 2010 +0200
@@ -108,13 +108,15 @@
       val _ = print_intross options thy''' "Introduction rules with new constants: " intross3
       val intross4 = map_specs (maps remove_pointless_clauses) intross3
       val _ = print_intross options thy''' "After removing pointless clauses: " intross4
-      val intross5 =
-        map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4
-      val intross6 = map_specs (map (expand_tuples thy''')) intross5
-      val intross7 = map_specs (map (eta_contract_ho_arguments thy''')) intross6
-      val _ = print_intross options thy''' "introduction rules before registering: " intross7
+      val intross5 = map_specs (map (remove_equalities thy''')) intross4
+      val _ = print_intross options thy''' "After removing equality premises:" intross5
+      val intross6 =
+        map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross5
+      val intross7 = map_specs (map (expand_tuples thy''')) intross6
+      val intross8 = map_specs (map (eta_contract_ho_arguments thy''')) intross7
+      val _ = print_intross options thy''' "introduction rules before registering: " intross8
       val _ = print_step options "Registering introduction rules..."
-      val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy'''
+      val thy'''' = fold Predicate_Compile_Core.register_intros intross8 thy'''
     in
       thy''''
     end;

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 29 17:30:39 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 29 17:30:40 2010 +0200
@@ -630,7 +630,6 @@
 
 (* eta contract higher-order arguments *)
 
-
 fun eta_contract_ho_arguments thy intro =
   let
     fun f atom = list_comb (apsnd ((map o map_products) Envir.eta_contract) (strip_comb atom))
@@ -638,5 +637,42 @@
     map_term thy (map_concl f o map_atoms f) intro
   end
 
+(* remove equalities *)
+
+fun remove_equalities thy intro =
+  let
+    fun remove_eqs intro_t =
+      let
+        val (prems, concl) = Logic.strip_horn intro_t
+        fun remove_eq (prems, concl) =
+          let
+            fun removable_eq prem =
+              case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) prem of
+                SOME (lhs, rhs) => (case lhs of
+                  Var _ => true
+                  | _ => (case rhs of Var _ => true | _ => false))
+              | NONE => false
+          in
+            case find_first removable_eq prems of
+              NONE => (prems, concl)
+            | SOME eq =>
+              let
+                val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
+                val prems' = remove (op =) eq prems
+                val subst = (case lhs of
+                  (v as Var _) =>
+                    (fn t => if t = v then rhs else t)
+                | _ => (case rhs of
+                   (v as Var _) => (fn t => if t = v then lhs else t)))
+              in
+                remove_eq (map (map_aterms subst) prems', map_aterms subst concl)
+              end
+          end
+      in
+        Logic.list_implies (remove_eq (prems, concl))
+      end
+  in
+    map_term thy remove_eqs intro
+  end
 
 end;