*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] op =simp=> in congruence rules*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 12 Aug 2014 14:32:41 +0200*In-reply-to*: <53E9F8D3.5060101@inf.ethz.ch>*References*: <53E33319.10405@inf.ethz.ch> <53E8BA2E.5090408@in.tum.de> <53E9F8D3.5060101@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

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

**References**:**[isabelle] op =simp=> in congruence rules***From:*Andreas Lochbihler

**Re: [isabelle] op =simp=> in congruence rules***From:*Tobias Nipkow

**Re: [isabelle] op =simp=> in congruence rules***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] op =simp=> in congruence rules
- Next by Date: Re: [isabelle] op =simp=> in congruence rules
- Previous by Thread: Re: [isabelle] op =simp=> in congruence rules
- Next by Thread: [isabelle] Isabelle2014-RC2 issues: Output markup for ML-blocks
- Cl-isabelle-users August 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list