# [isabelle] op =simp=> in congruence rules

`I wondered why the congruence rule for map does not enable the simplifier to solve
``statements such as the following. Such statements occur naturally with the induction rules
``from the new datatype package when recursion goes through a list.
`
lemma "(⋀x. x ∈ set xs ⟹ f x = g x) ⟹ h (map f (rev xs)) = h (map g (rev xs))"
apply(simp cong: list.map_cong)
Then, I found he following comment on op =simp=> in HOL.thy:
text {*
The following copy of the implication operator is useful for
fine-tuning congruence rules. It instructs the simplifier to simplify
its premise.
*}
definition simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) where
"simp_implies ≡ op ==>"

`A look at the usages of op =simp=> showed that it is only used in congruence rules for the
``big operators and bounded quantification. In particular, all of them use it in the form
`
!!x. x : ?B =simp=> ?f x = ?g x
and the same form shows up in list.map_cong. And indeed, if list.map_cong were
lemma map_cong': "⟦xs = ys; ⋀x. x ∈ set ys =simp=> f x = g x⟧ ⟹ map f xs = map g ys"
unfolding simp_implies_def by(rule list.map_cong)
then simp would be able to solve the above goal:
by(simp cong: map_cong')

`My question now is: What is the advantage of op ==> over op =simp=> in congruence rules,
``i.e., list.map_cong over map_cong'? Since the BNF package generates congruence rules with
``the structure
`
!!x. x : set_type ?A ==> f x = g x
would it be sensible to use =simp=> there?

`By the way, I noticed that [fundef_cong] cannot deal with =simp=>. But that should not be
``the only reason for having the weaker cong rule.
`
Best,
Andreas

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