Isabelle: Напротив «интро Impi»

Question

Если моя цель состояние foo ==> bar --> qux, я знаю, что я могу использовать оператор

apply (intro impI) 

с получением целевого состояния foo ==> bar ==> qux. Как насчет другого направления? Какая команда вернет меня в состояние цели foo ==> bar --> qux?

---

Лучшее, что я придумал до сих пор

apply (rule_tac P="bar" in rev_mp, assumption, thin_tac "bar") 

, но это довольно неуклюжим, и я хотел бы узнать, есть ли лучше способ.

Answer 1

Вместо

apply (rule_tac P="bar" in rev_mp, assumption, thin_tac "bar") 

вы можете написать

apply (erule_tac P="bar" in rev_mp) 

где erule_tac исключает совпадающую предположение для вас, так что вам не нужно thin_tac больше.

Answer 2

Я предполагаю, что вы хотите остаться в apply-style. Тогда это всего лишь головоломка, возможно, с множеством возможных решений. Вот один:

apply (unfold atomize_imp, rule) 

или немного более явным

apply (unfold atomize_imp, rule impI) 

где unfold atomize_impзаменяет все вхождения==> на -->. Затем, в общем, вы можете указать номер -->, который должен быть заменен на ==> (начиная слева), соответствующим номером rule (или rule impI).

В любом случае, если вы использовали бы Isar-style, то вы просто указали, что хотите, чтобы явным образом и почти любой автоматический инструмент сможет заполнить остальные.