title: How to use Isabelle's code_pred and values commands?
body: <p>There is an example of <code>code_pred</code> 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:</p>
  
  <pre><code>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
  </code></pre>
  
  <p>But for the 1st values' invocation I get the error: </p>
  
  <blockquote>
    <p>Evaluation with values is not possible because compilation with
    code_pred was not invoked.</p>
  </blockquote>
  
  <p>And for the 2nd one I get the error: </p>
  
  <blockquote>
    <p>No mode possible for comprehension {t. (BooLiteralExp true, λ_. Bv
    false) ⇒ t}.</p>
  </blockquote>
  
  <p>What's wrong with my theory?</p>