Isabelle - Nitpick - автоматически используя значения свидетельства

Question

Как я могу автоматически использовать значения, найденные 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 

Answer 1

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

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