--- 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;