Доказательство последствий с существующим в помещениях без использования Изар

Question

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

∃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?

Answer 1

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

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

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