Re: [isabelle] op =simp=> in congruence rules

Hi Tobias,

Here is the summary of =simp=> vs. ==> in the congruence rule for map. I replaced map_cong by map_cong' in List.thy and ran all of the Isabelle distribution (isabelle makeall) and the AFP, thereby fixing what was broken.

1. Whenenver map_cong was used as a congruence rule, map_cong' also works, without looping.

2. I found three occurrences where map_cong was not used as [cong] that fail with map_cong'.

a) In HOL/Word/Word.thy, it is used with rule. Using it as a congruence rule causes the simplifier to loop, but this is independent of whether ==> or =simp=> is used.

b) In the AFP entry Affine_Arithmetic is used with subst followed by auto.
  (simp cong: map_cong') does not solve the goal, either.

c) In the AFP entry Matrix, there is an instance of the pattern
  by(rule map_cong)(auto ...)
Both (simp cong: map_cong) and (simp cong: map_cong') solve the goal, too.

In conclusion, =simp=> does not break anything in the tested theories when map_cong is used as a congruence rule. Since [fundef_cong] does not handle =simp=> and map_cong seems to be useful in some cases (2a,b), we should keep the version with ==>. Possibly, BNF could also generate the congruence rule list.strong_map_cong with =simp=>. The name follow the existing naming convention for ball, bex, SUP, INF, ... (Although I would prefer map_cong_strong because the main operator does not hide somewhere in the middle of the theorem name.)


On 11/08/14 14:42, Tobias Nipkow wrote:
Dear Andres,

It is what it is mostly for historical reasons, but I also seem to recall that
=simp=> lead to nontermination in same cases (unsurprisingly) and that therefore
we restricted its usage. You could try to replace map_cong by your map_cong' and
see if anything breaks. If not, that would be a strong indication that the
map-congruence rules generated by datatype should always use =simp=>.


On 07/08/2014 10:04, Andreas Lochbihler wrote:
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.


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