Why won't simp handle this term inside of a lambda expression?

Question

I have proven this simp rule:

lemma AAA: the_sector (log_update ?f ?s) ?p = the_sector ?s ?p

The rule is not used to simplify the following:

lemma BBB: "(λA. if A then (the_sector (log_update f s) p) else B)
   =
   (λA. if A then (the_sector s p) else B)"

I know that I can apply auto or (rule ext) followed by simp to prove this lemma, but my ultimate goal is something much nastier than a function equality. I believe the sticking point is the use of a function variable A in the if condition. I would like to understand why simp does not simplify a term in this case.

The following illustrate why I believe this to be the sticking point (both are proven):

lemma CCC: "(λf s p. the_sector (log_update f s) p) = (λf s p. the_sector s p)"
  by simp

lemma DDD: "(if A then (the_sector (log_update f s) p) else B)
       =
       (if A then (the_sector s p) else B)"
  by simp

Thanks for any advice.

Andreas Lochbihler Andreas Lochbihler · Accepted Answer · 2015-04-28T06:30:41

In the default setup for the simplifier, congruence rules prevent the rewriting in certain parts of a term. Such rules are declared by default for most control operators like if x then ... else ... and case expressions (e.g. case x of None => ... | Some y => ...). They restrict simplification to the term that decides which branch to take, i.e., the x in the above examples. This is motivated by the idea that there is no point in simplifying a term that will not be relevant because some other branch is taken. In your case, the term the_sector ... to be rewritten occurs inside the then branch, so the simplifier does not even look at it at all.

The relevant congruence rules are if_weak_cong and option.weak_case_cong (and similar for other datatypes). You can delete them globally with declare if_weak_cong[cong del] or locally with (simp cong del: if_weak_cong). I recommend to leave them in place globally because some of the default simp rules assume that the weak congruence rules for case distinctions are in place. Otherwise, the simplifier might not terminate.

There is also another set of congruence rules (if_cong and option.case_cong) which exploit knowledge about x when simplifying the branches. If you declare them as congruence rules (if_cong[cong] or cong: if_cong), the then branch will be simplified with the knowledge that the condition holds and the else branch accordingly. Similarly, in the branches of the case distinction, the simplifier knows that the scrutinised term is of the appropriate form.

You can find more information on congruence rules in the Tutorial on Isabelle/HOL in section 9.1.1.

Why won't simp handle this term inside of a lambda expression?

1 Answers