이자벨 : "소개 IMPI"

Question

내 목표 상태 인 경우 foo ==> bar --> qux의 반대, 내가 목표 상태 foo ==> bar ==> qux를 산출하기 위해 문

apply (intro impI) 

를 사용할 수 있다는 것을 알고. 다른 방향은 어떨까요? 어떤 명령이 나를 목표 상태 foo ==> bar --> qux으로 보내겠습니까?

---

내가 지금까지 함께 온 가장 좋은

는

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

입니다하지만 오히려 어설픈, 그리고 내가 더 좋은 방법이 있는지 알고 싶습니다.

Answer 1

당신은 당신이 더 이상 thin_tac을 필요가 없습니다 erule_tac 당신을 위해 일치하는 가정을 제거

apply (erule_tac P="bar" in rev_mp) 

를 작성할 수 있습니다.

Answer 2

적용 스타일에 머물고 싶다고 가정합니다. 그렇다면 이것은 가능한 많은 솔루션을 갖춘 퍼즐 일뿐입니다. 여기에 하나입니다

apply (unfold atomize_imp, rule impI) 

apply (unfold atomize_imp, rule) 

또는 좀 더 노골적인 unfold atomize_imp가 -->으로 ==>의 모든 발생을 대체하는 곳. 그런 다음 일반적으로 ==> (왼쪽에서부터 시작)으로 대체해야하는 -->의 번호를 rule (또는 rule impI)의 해당 번호로 지정할 수 있습니다.

어쨌든 Isar-style을 사용한다면 명시 적으로 원하는 것을 명시하고 거의 모든 자동 도구가 나머지를 채울 수 있습니다. 대신

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

의