Fixed error in pattern splitting algorithm
authorkrauss
Wed Sep 20 09:08:35 2006 +0200 (2006-09-20)
changeset 20636ddddf0b7d322
parent 20635 e95db20977c5
child 20637 d883e0fc1c51
Fixed error in pattern splitting algorithm
src/HOL/Tools/function_package/pattern_split.ML
     1.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Wed Sep 20 07:44:34 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Wed Sep 20 09:08:35 2006 +0200
     1.3 @@ -45,38 +45,57 @@
     1.4  
     1.5  
     1.6  
     1.7 -fun pattern_subtract_subst ctx vs _ (Free v2) = []
     1.8 -  | pattern_subtract_subst ctx vs (v as (Free (_, T))) t' =
     1.9 +
    1.10 +fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
    1.11 +fun join_product (xs, ys) = map join (product xs ys)
    1.12 +
    1.13 +fun join_list [] = []
    1.14 +  | join_list xs = foldr1 (join_product) xs
    1.15 +
    1.16 +
    1.17 +exception DISJ
    1.18 +
    1.19 +fun pattern_subtract_subst ctx vs t t' =
    1.20      let
    1.21 -      fun foo constr =
    1.22 +      exception DISJ
    1.23 +      fun pattern_subtract_subst_aux vs _ (Free v2) = []
    1.24 +        | pattern_subtract_subst_aux vs (v as (Free (_, T))) t' =
    1.25            let
    1.26 -            val (vs', t) = saturate ctx vs constr
    1.27 -            val substs = pattern_subtract_subst ctx vs' t t'
    1.28 +            fun foo constr =
    1.29 +                let
    1.30 +                  val (vs', t) = saturate ctx vs constr
    1.31 +                  val substs = pattern_subtract_subst ctx vs' t t'
    1.32 +                in
    1.33 +                  map (fn (vs, subst) => (vs, (v,t)::subst)) substs
    1.34 +                end
    1.35            in
    1.36 -            map (fn (vs, subst) => (vs, (v,t)::subst)) substs
    1.37 +            flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T))
    1.38 +          end
    1.39 +        | pattern_subtract_subst_aux vs t t' =
    1.40 +          let
    1.41 +            val (C, ps) = strip_comb t
    1.42 +            val (C', qs) = strip_comb t'
    1.43 +          in
    1.44 +            if C = C'
    1.45 +            then flat (map2 (pattern_subtract_subst_aux vs) ps qs)
    1.46 +            else raise DISJ
    1.47            end
    1.48      in
    1.49 -      flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T))
    1.50 -    end
    1.51 -  | pattern_subtract_subst ctx vs t t' =
    1.52 -    let
    1.53 -      val (C, ps) = strip_comb t
    1.54 -      val (C', qs) = strip_comb t'
    1.55 -    in
    1.56 -      if C = C'
    1.57 -      then flat (map2 (pattern_subtract_subst ctx vs) ps qs)
    1.58 -      else [(vs, [])]
    1.59 +      pattern_subtract_subst_aux vs t t'
    1.60 +      handle DISJ => [(vs, [])]
    1.61      end
    1.62  
    1.63  
    1.64  (* p - q *)
    1.65  fun pattern_subtract ctx eq2 eq1 =
    1.66      let
    1.67 +      val thy = ProofContext.theory_of ctx
    1.68        
    1.69        val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
    1.70        val (_,  _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
    1.71  
    1.72 -      val thy = ProofContext.theory_of ctx
    1.73 +      val _ = print (cterm_of thy eq1)
    1.74 +      val _ = print (cterm_of thy eq2)
    1.75  
    1.76        val substs = pattern_subtract_subst ctx vs lhs1 lhs2
    1.77  
    1.78 @@ -86,8 +105,10 @@
    1.79            in
    1.80              fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
    1.81            end
    1.82 +
    1.83 +      fun prtrm t = let val _ = print (map (cterm_of thy) t) in t end
    1.84      in
    1.85 -      map instantiate substs
    1.86 +      prtrm (map instantiate substs)
    1.87      end
    1.88  
    1.89