--- a/src/HOL/Tools/function_package/pattern_split.ML Wed Sep 20 07:44:34 2006 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML Wed Sep 20 09:08:35 2006 +0200
@@ -45,38 +45,57 @@
-fun pattern_subtract_subst ctx vs _ (Free v2) = []
- | pattern_subtract_subst ctx vs (v as (Free (_, T))) t' =
+
+fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
+fun join_product (xs, ys) = map join (product xs ys)
+
+fun join_list [] = []
+ | join_list xs = foldr1 (join_product) xs
+
+
+exception DISJ
+
+fun pattern_subtract_subst ctx vs t t' =
let
- fun foo constr =
+ exception DISJ
+ fun pattern_subtract_subst_aux vs _ (Free v2) = []
+ | pattern_subtract_subst_aux vs (v as (Free (_, T))) t' =
let
- val (vs', t) = saturate ctx vs constr
- val substs = pattern_subtract_subst ctx vs' t t'
+ fun foo constr =
+ let
+ val (vs', t) = saturate ctx vs constr
+ val substs = pattern_subtract_subst ctx vs' t t'
+ in
+ map (fn (vs, subst) => (vs, (v,t)::subst)) substs
+ end
in
- map (fn (vs, subst) => (vs, (v,t)::subst)) substs
+ flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T))
+ end
+ | pattern_subtract_subst_aux vs t t' =
+ let
+ val (C, ps) = strip_comb t
+ val (C', qs) = strip_comb t'
+ in
+ if C = C'
+ then flat (map2 (pattern_subtract_subst_aux vs) ps qs)
+ else raise DISJ
end
in
- flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T))
- end
- | pattern_subtract_subst ctx vs t t' =
- let
- val (C, ps) = strip_comb t
- val (C', qs) = strip_comb t'
- in
- if C = C'
- then flat (map2 (pattern_subtract_subst ctx vs) ps qs)
- else [(vs, [])]
+ pattern_subtract_subst_aux vs t t'
+ handle DISJ => [(vs, [])]
end
(* p - q *)
fun pattern_subtract ctx eq2 eq1 =
let
+ val thy = ProofContext.theory_of ctx
val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
val (_, _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
- val thy = ProofContext.theory_of ctx
+ val _ = print (cterm_of thy eq1)
+ val _ = print (cterm_of thy eq2)
val substs = pattern_subtract_subst ctx vs lhs1 lhs2
@@ -86,8 +105,10 @@
in
fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
end
+
+ fun prtrm t = let val _ = print (map (cterm_of thy) t) in t end
in
- map instantiate substs
+ prtrm (map instantiate substs)
end