CODEWITHSUNDEEP
isabelletheorem-proving
TFuto
TFuto

Reputation: 1452

Isabelle - Nitpick - using witness values automatically

How can I automatically use the values found by nitpick, instead of using rule exI's and manually typing in the witness values?

  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

Upvotes: 0

Views: 96

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8248

I don't think that functionality exists, since I'd say this is not a typical use case.

One could probably add something like this to the nitpick command with a relatively small amount of effort or create a new command to do it.

Upvotes: 2

Related Questions