Почему симулятор не обрабатывает этот термин внутри выражения лямбда?

Question

Я доказал это простофиля правило:

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

правило не используется для упрощения следующее:

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)" 

Я знаю, что я могу применить авто или (правило вн) с последующим по simp, чтобы доказать эту лемму, но моя конечная цель - это нечто более неприятное, чем функция. Я считаю, что точкой приклеивания является использование функциональной переменной A в условии if. Я хотел бы понять, почему simp не упрощает термин в этом случае.

Следующая иллюстрируют, почему я считаю, что это камень преткновения (оба доказаны):

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 

Спасибо за любые советы.

Answer 1

В настройках по умолчанию для упрощения правила конгруэнтности предотвращают переписывание в определенных частях термина. Такие правила объявляются по умолчанию для большинства управляющих операторов, таких как if x then ... else ... и case case (например, case x of None => ... | Some y => ...). Они ограничивают упрощение термина, который решает, какую ветвь взять, т. Е. x в приведенных выше примерах. Это мотивируется идеей о том, что нет смысла упрощать термин, который не будет иметь значения, поскольку принимается какая-либо другая ветвь. В вашем случае термин the_sector ..., который будет переписан, происходит внутри ветки then, поэтому упрощение даже не смотрит на него.

Соответствующие правила конгруэнции: if_weak_cong и option.weak_case_cong (и аналогичные по другим типам данных). Вы можете удалить их по всему миру с помощью declare if_weak_cong[cong del] или локально с (simp cong del: if_weak_cong). Я рекомендую оставить их на месте во всем мире, потому что некоторые из стандартных правил simp предполагают, что существуют правила слабой конгруэнтности для разграничений случаев. В противном случае упрощение может не завершиться.

Существует также другой набор правил конгруэнтности (if_cong и option.case_cong), которые используют знания о x при упрощении ветвей. Если вы объявите их как правила сопоставления (if_cong[cong] или cong: if_cong), то ветвь then будет упрощена, зная, что условие выполнено, а ветвь else - соответственно. Аналогично, в ветвях разграничения случая упрощение знает, что рассматриваемый термин имеет соответствующую форму.

Дополнительную информацию о правилах соответствия в разделе Tutorial on Isabelle/HOL вы найдете в разделе 9.1.1.