Подтверждение наличия в помещении без использования isar

У меня есть следующая цель, извлеченная из одной из теорем, которую я должен доказать:

∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ P [] [x] ∨ P [x] []

Здесь я хотел применить правило экзистенциального исключения, но оно дает две странные подцели:

 1. ∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ ∃x. ?P25 x
 2. ⋀xa. ∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ ?P25 xa ⟹ P [] [x] ∨ P [x] []

Идея состоит в том, что если бы я мог удалить кванторы, доказательство действительно было бы довольно простым. Если [x] = ys @ zs, тогда есть две возможности. Либо ys = [x], zs = [], либо наоборот. Таким образом, мы могли бы P [x] [] или P [] [x].

Как я могу доказать это без использования Isar, а только с помощью команд apply?

2
0
57
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Я не знаю, почему в вашем случае не работает тактика исключения существующих, но следующая строка работает успешно.

by (elim exE, rename_tac ys zs, case_tac ys, auto)

Здесь rename_tac переименовывает вновь полученные списки в выбранные пользователем имена ys и zs, так что впоследствии возможен анализ случая на ys (пустой или нет).

большое спасибо за ваш ответ. чтобы объяснить, почему мой подход не работает, вы можете добавить эту команду im using rule, и эта команда вернет объединенные помещения. для устранения экзистенциального, вероятно, я мог бы использовать erule. (я говорю это только для полноты вашего ответа). Спасибо еще раз!

Rodrigo 01.11.2018 10:56

на самом деле комбинация erule exE с case_tac ys и auto решает цельç

Rodrigo 01.11.2018 10:58

Другие вопросы по теме