There are three proof methods that correspond to the different evaluation mechanisms of value
:
eval
uses the code generator; it corresponds tovalue [code]
. The proof succeeds if the generated ML code evaluates toTrue
.normalization
compiles the statement to a symbolic normalisation engine in ML. It mimicksvalue [nbe]
.code_simp
uses Isabelle's simplifier as an evaluator. It corresponds tovalue [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
.