From a 'value' to a 'lemma'

Question

I have a rather large term foo. When I type

value "foo"

then Isabelle evaluates foo to a value, say foo_value. I would now like to prove the following lemma.

lemma "foo = foo_value"

What proof method should I use? I tried try, but that timed out. I guess I could proceed manually by unfolding the various definitions that occur in foo, but surely I should be able to tap into whatever mechanism the value command is using, right?

Answer 1

There are three proof methods that correspond to the different evaluation mechanisms of value:

• eval uses the code generator; it corresponds to value [code]. The proof succeeds if the generated ML code evaluates to True.
• normalization compiles the statement to a symbolic normalisation engine in ML. It mimicks value [nbe].
• code_simp uses Isabelle's simplifier as an evaluator. It corresponds to value [simp].

The tutorial on code generation describes these proof methods in more detail. eval and normalization act like oracles, i.e., they bypass Isabelle's kernel whereas every evaluation step of code_simp goes through the kernel. Usually, eval is faster than normalization and normalization is faster than code_simp.

Answer 2

I am not sure whether it works in all cases, but you could try:

lemma "foo = foo_value"
  by eval

In many cases, by simp should also work and I guess eval is kind of an oracle (in the sense that it is not fully verified by the kernel; please somebody correct me if I am wrong).