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



Hi Andreas,

Thanks for that. For me it sounds pretty conclusive that we should follow your
recommendation: let BNF generate both map_cong and map_cong_strong.

Thanks!
Tobias

On 12/08/2014 13:21, Andreas Lochbihler wrote:
> 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.)
> 
> 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.