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



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.