[isabelle] Finite product simplification



I need to be able to do something like this automatically:

lemma (in comm_monoid) finprod_exp:
  "⟦A={x. P x ∧ Q x}; finite A; a∈A→carrier G⟧⟹finprod G (λx. if P x then
    a x else b x) A = finprod G a A"
using[[simp_trace, simp_trace_depth_limit=10]]
apply (auto cong: finprod_cong2' simp add:simp_if  split:if_splits)

Looking at the simp trace, it appears to fail during the congruence, when
it fails to show "a∈A→carrier G" even when this was given as a hypothesis.
(Note that apply (intro finprod_cong2') apply (auto...) works, but this is
not good enough for applications because simp doesn't call intro.)

Here finprod_cong2' is just finprod_cong' in a different (hopefully better)
order:

lemma (in comm_monoid) finprod_cong2':
  "[| A = B;
      !!i. i ∈ B ==> f i = g i ; g ∈ B -> carrier G|] ==> finprod G f A =
finprod G g B"
 apply (auto cong: finprod_cong')
done

What gives?

Thanks,
Holden



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.