Можно ли "освободить" универсально количественно определенные переменные верхнего уровня, используя тактику в Изабель?

Question

Короче говоря, я бы хотел перейти от этого:

 proof (prove)
 goal (1 subgoal):
  1. ⋀ myVar . somePredicate myVar

к этому:

 proof (prove)
 goal (1 subgoal):
  1. somePredicate myVar

, используя тактику. Единственное решение, которое я могу найти, это написать новый lemma, например:

 lemma myPredicateHolds_aux : "somePredicate myVar"
   sorry

, а затем исходный ⋀ myVar . somePredicate myVar обычно можно решить, написав:

 using myPredicateHolds_aux by blast

, ноИнтересно, есть ли лучший способ (с использованием тактики) для удобства и потому, что, если свойство очень сложное, blast может дать сбой.

Answer 1

proof (prove) предполагает, что вы пишете сценарий проверки, в этом случае вы можете использовать subgoal for myVar. Думаю, в руководстве «isar-ref» об этом сказано немного больше (хотя оно может быть немного плотным).

Вы также можете, и я считаю, что обычно это «предпочтительный» способ сделать это. , перейдите в структурированный режим защиты Isar и используйте fix:

proof -
  fix myVar
  show "somePredicate myVar"
  proof ...