i have proven simp rule:
lemma aaa: the_sector (log_update ?f ?s) ?p = the_sector ?s ?p the rule not used simplify following:
lemma bbb: "(λa. if (the_sector (log_update f s) p) else b) = (λa. if (the_sector s p) else b)" i know can apply auto or (rule ext) followed simp prove lemma, ultimate goal nastier function equality. believe sticking point use of function variable in if condition. understand why simp not simplify term in case.
the following illustrate why believe sticking point (both proven):
lemma ccc: "(λf s p. the_sector (log_update f s) p) = (λf s p. the_sector s p)" simp lemma ddd: "(if (the_sector (log_update f s) p) else b) = (if (the_sector s p) else b)" simp thanks advice.
in default setup simplifier, congruence rules prevent rewriting in parts of term. such rules declared default control operators if x ... else ... , case expressions (e.g. case x of none => ... | y => ...). restrict simplification term decides branch take, i.e., x in above examples. motivated idea there no point in simplifying term not relevant because other branch taken. in case, term the_sector ... rewritten occurs inside then branch, simplifier not @ at all.
the relevant congruence rules if_weak_cong , option.weak_case_cong (and similar other datatypes). can delete them globally declare if_weak_cong[cong del] or locally (simp cong del: if_weak_cong). recommend leave them in place globally because of default simp rules assume weak congruence rules case distinctions in place. otherwise, simplifier might not terminate.
there set of congruence rules (if_cong , option.case_cong) exploit knowledge x when simplifying branches. if declare them congruence rules (if_cong[cong] or cong: if_cong), branch simplified knowledge condition holds , else branch accordingly. similarly, in branches of case distinction, simplifier knows scrutinised term of appropriate form.
you can find more information on congruence rules in tutorial on isabelle/hol in section 9.1.1.
