*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*: Mon, 11 Aug 2014 14:42:22 +0200*In-reply-to*: <53E33319.10405@inf.ethz.ch>*References*: <53E33319.10405@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

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 >

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

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

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

- Previous by Date: [isabelle] Do these tactics exist?
- Next by Date: Re: [isabelle] Do these tactics exist?
- Previous by Thread: [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