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



Dear Tobias,

Thanks for the background infos. I pushed the replacement of ==> with =simp=> to testboard (see http://isabelle.in.tum.de/testboard/Isabelle/rev/1cbcd78f8d3c). I expect a few proofs in the AFP to break, because they use apply(rule map_cong), but let's see.

Even if that is the only problem, I doubt that this will be a strong indication either way. A grep over the sources revealed just a few places where map_cong is used (map_cong is not a default congruence rule); probably because the [simp] rule map_eq_conv takes already care of map equalities.

Andreas


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=>.

Tobias

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.

Best,
Andreas






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