How to use Isabelle's code_pred and values commands?

There is an example of code_pred usage in "Concrete Semantics" by Tobias Nipkow and Gerwin Klein, Section 7.2.2. I've implemented a simple language based on the examples and I try to calculate values of expressions:

theory BooLang
  imports Main
begin

type_synonym id = string
type_synonym 'a Env = "id ⇒ 'a"

datatype BooBoolExp =
  BooLiteralExp bool |
  BooLetExp id BooBoolExp BooBoolExp |
  BooVarExp id |
  BooAndExp BooBoolExp BooBoolExp

datatype BooVal = Bv bool

type_synonym BooEnv = "BooVal Env"

inductive tbooval :: "BooBoolExp × BooEnv ⇒ BooVal ⇒ bool" (infix "⇒" 55) where
  Literal: "(BooLiteralExp b, env) ⇒ Bv b" |
  And: "⟦(a, env) ⇒ Bv av; (b, env) ⇒ Bv bv⟧ ⟹ (BooAndExp a b, env) ⇒ Bv (av ∧ bv)" |
  Var: "(BooVarExp v, env) ⇒ env v" |
  Let: "⟦(val, env) ⇒ b; (body, env(v := b)) ⇒ x⟧ ⟹ (BooLetExp v val body, env) ⇒ x"

code_pred tbooval .

values "{t. True}"

values "{t. (BooLiteralExp true, λ_. Bv false) ⇒ t}"

end

But for the 1st values' invocation I get the error:

Evaluation with values is not possible because compilation with code_pred was not invoked.

And for the 2nd one I get the error:

No mode possible for comprehension {t. (BooLiteralExp true, λ_. Bv false) ⇒ t}.

What's wrong with my theory?

Solution

The first command values {t. True} cannot work as this command asks Isabelle to enumerate all values of the type of t, which is inferred to be a type variable 'a; and this cannot be done.

For the second command, you just misspelled True and False. As is, true and false are inferred to be boolean variables instead of boolean constants. Unlike value, the command values does not support symbolic execution in Isabelle2016-1. That is, all input arguments to the inductive predicate must be ground values without variables. In your example, code_pred infers two execution modes: One in which everything is given as input and one in which only the first argument is given as input. You can see the inferred modes by passing the [show_modes] option as in

 code_pred [show_modes] tboolval .

You can find some further documentation on code_pred and values in the code generator tutorial.