*To*: Tobias Nipkow <nipkow at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] op =simp=> in congruence rules*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 11 Aug 2014 16:44:11 +0200*In-reply-to*: <53E8BA2E.5090408@in.tum.de>*References*: <53E33319.10405@inf.ethz.ch> <53E8BA2E.5090408@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.0

Dear Tobias,

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

- Previous by Date: Re: [isabelle] monadic function definition
- Next by Date: Re: [isabelle] monadic function definition
- Previous by Thread: Re: [isabelle] op =simp=> in congruence rules
- Next by Thread: Re: [isabelle] op =simp=> in congruence rules
- 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