Изабель - Нитпик - автоматическое использование значений свидетелей

Как я могу автоматически использовать значения, найденные nitpick, вместо того, чтобы использовать rule exI и вручную вводить значения свидетелей?

  theorem "EX a b. a + b = 5 & a - b = (1 :: int)"
    nitpick [falsify=false]

    (* Nitpicking formula... 
       Nitpick found a model:

       Skolem constants:
       a = 3
       b = 2
    *)

    apply (rule exI[where x="3"])
    apply (rule exI[where x="2"])
    apply (simp)
  done

theorem-proving isabelle
person TFuto    schedule 13.10.2015    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Я не думаю, что такая функциональность существует, поскольку я бы сказал, что это нетипичный вариант использования.

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

person Manuel Eberl    schedule 14.10.2015