[isabelle] op =simp=> in congruence rules



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.