Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Finite product simplification

Email Gateway (Aug 19 2022 at 15:31):

From: Holden Lee <hl422@cam.ac.uk>
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

Email Gateway (Aug 19 2022 at 15:35):

From: Johannes Hölzl <hoelzl@in.tum.de>
I'm not sure but you might try an even stronger form of your cong rule:

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

then i : {x. P x /\ Q x} is rewritten into P i /\ Q i when applying the
congruence rule.

I don't know what simp_if is but I don't think you need if_splits and
simp_if.

• Johannes

Email Gateway (Aug 19 2022 at 15:35):

From: Holden Lee <hl422@cam.ac.uk>
Thanks, this works - what's the difference between ==> and =simp=>?

-Holden

2014-08-26 9:46 GMT+01:00 Johannes Hölzl <hoelzl@in.tum.de>:

Email Gateway (Aug 19 2022 at 15:36):

From: Johannes Hölzl <hoelzl@in.tum.de>
Lets assume we have a cong rule of the form:

[| A = B ; !!x. x : B =simp=> f x = g x |] ==> OP A f = OP B g

The =simp=> tells the simplifier to simplify x : B before it is used.
When ==>
is used this does not happen.

Recently there was a discussion about the usage of =simp=> = :

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-August/msg00069.html

• Johannes

Last updated: Apr 25 2024 at 16:19 UTC