src/Doc/Codegen/Computations.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 66453 cc19f7ca2ed6
child 67299 ba52a058942f
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 theory Computations
     2   imports Codegen_Basics.Setup
     3     "HOL-Library.Code_Target_Int"
     4     "HOL-Library.Code_Char"
     5 begin
     6 
     7 section \<open>Computations \label{sec:computations}\<close>
     8 
     9 subsection \<open>Prelude -- The @{text code} antiquotation \label{sec:code_antiq}\<close>
    10 
    11 text \<open>
    12   The @{ML_antiquotation_def code} antiquotation allows to include constants
    13   from
    14   generated code directly into ML system code, as in the following toy
    15   example:
    16 \<close>
    17 
    18 datatype %quote form = T | F | And form form | Or form form (*<*)
    19 
    20 (*>*) ML %quotetypewriter \<open>
    21   fun eval_form @{code T} = true
    22     | eval_form @{code F} = false
    23     | eval_form (@{code And} (p, q)) =
    24         eval_form p andalso eval_form q
    25     | eval_form (@{code Or} (p, q)) =
    26         eval_form p orelse eval_form q;
    27 \<close>
    28 
    29 text \<open>
    30   \noindent The antiquotation @{ML_antiquotation code} takes
    31   the name of a constant as argument;
    32   the required code is generated
    33   transparently and the corresponding constant names are inserted
    34   for the given antiquotations.  This technique allows to use pattern
    35   matching on constructors stemming from compiled datatypes.
    36   Note that the @{ML_antiquotation code}
    37   antiquotation may not refer to constants which carry adaptations;
    38   here you have to refer to the corresponding adapted code directly.
    39 \<close>
    40 
    41   
    42 subsection \<open>The concept of computations\<close>
    43 
    44 text \<open>
    45   Computations embody the simple idea that for each
    46   monomorphic Isabelle/HOL term of type @{text \<tau>} by virtue of
    47   code generation there exists an corresponding ML type @{text T} and
    48   a morphism @{text "\<Phi> :: \<tau> \<rightarrow> T"} satisfying
    49   @{text "\<Phi> (t\<^sub>1 \<cdot> t\<^sub>2) = \<Phi> t\<^sub>1 \<cdot> \<Phi> t\<^sub>2"}, with @{text \<cdot>} denoting
    50   term application.
    51 
    52   For a given Isabelle/HOL type @{text \<tau>}, parts of @{text \<Phi>} can be
    53   implemented by a corresponding ML function @{text "\<phi>\<^sub>\<tau> :: term \<rightarrow> T"}.
    54   How?
    55 
    56     \<^descr> \<open>Let input be a constant C :: \<tau>.\<close> \\
    57       Then @{text "\<phi>\<^sub>\<tau> C = f\<^sub>C"} with @{text "f\<^sub>C"} being
    58       the image of @{text C} under code generation.
    59 
    60     \<^descr> \<open>Let input be an application (t\<^sub>1 \<cdot> t\<^sub>2) :: \<tau>.\<close> \\
    61       Then @{text "\<phi>\<^sub>\<tau> (t\<^sub>1 \<cdot> t\<^sub>2) = \<phi>\<^sub>\<tau> t\<^sub>1 (\<phi>\<^sub>\<tau> t\<^sub>2)"}.
    62 
    63   \noindent Using these trivial properties, each monomorphic constant
    64   @{text "C : \<^vec>\<tau>\<^sub>n \<rightarrow> \<tau>"} yields the following
    65   equations:
    66 \<close>
    67 
    68 text %quote \<open>
    69   @{text "\<phi>\<^bsub>(\<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>)\<^esub> C = f\<^sub>C"} \\
    70   @{text "\<phi>\<^bsub>(\<tau>\<^sub>2 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>)\<^esub> (C \<cdot> t\<^sub>1) = f\<^sub>C (\<phi>\<^bsub>\<tau>\<^sub>1\<^esub> t\<^sub>1)"} \\
    71   @{text "\<dots>"} \\
    72   @{text "\<phi>\<^bsub>\<tau>\<^esub> (C \<cdot> t\<^sub>1 \<cdot> \<dots> \<cdot> t\<^sub>n) = f\<^sub>C (\<phi>\<^bsub>\<tau>\<^sub>1\<^esub> t\<^sub>1) \<dots> (\<phi>\<^bsub>\<tau>\<^sub>n\<^esub> t\<^sub>n)"}
    73 \<close>
    74   
    75 text \<open>
    76   \noindent Hence a computation is characterized as follows:
    77 
    78     \<^item> Let @{text "input constants"} denote a set of monomorphic constants.
    79 
    80     \<^item> Let @{text \<tau>} denote a monomorphic type and @{text "'ml"} be a schematic
    81       placeholder for its corresponding type in ML under code generation.
    82 
    83     \<^item> Then the corresponding computation is an ML function of type
    84       @{ML_type "Proof.context -> term -> 'ml"}
    85       partially implementing the morphism @{text "\<Phi> :: \<tau> \<rightarrow> T"} for all
    86       \<^emph>\<open>input terms\<close> consisting only of input constants and applications.
    87 
    88   \noindent The charming idea is that all required code is automatically generated
    89   by the code generator for givens input constants and types;
    90   that code is directly inserted into the Isabelle/ML runtime system
    91   by means of antiquotations.
    92 \<close>
    93 
    94 
    95 subsection \<open>The @{text computation} antiquotation\<close>
    96 
    97 text \<open>
    98   The following example illustrates its basic usage:
    99 \<close>
   100 
   101 ML %quotetypewriter \<open>
   102   local
   103 
   104   fun int_of_nat @{code "0 :: nat"} = 0
   105     | int_of_nat (@{code Suc} n) = int_of_nat n + 1;
   106 
   107   in
   108 
   109   val comp_nat = @{computation nat terms:
   110     "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
   111     "sum_list :: nat list \<Rightarrow> nat" "prod_list :: nat list \<Rightarrow> nat"
   112     datatypes: nat "nat list"}
   113     (fn post => post o HOLogic.mk_nat o int_of_nat o the);
   114 
   115   end
   116 \<close>
   117 
   118 text \<open>
   119     \<^item> Antiquotations occurring in the
   120       same ML block always refer to the same transparently generated code;
   121       particularly, they share the same transparently generated datatype
   122       declarations.
   123 
   124     \<^item> The type of a computation is specified as first argument.
   125 
   126     \<^item> Input constants are specified the following ways:
   127 
   128         \<^item> Each term following @{text "terms:"} specifies all constants
   129           it contains as input constants.
   130 
   131         \<^item> Each type following @{text "datatypes:"} specifies all constructors
   132           of the corresponding code datatype as input constants.  Note that
   133           this does not increase expressiveness but succinctness for datatypes
   134           with many constructors.
   135 
   136     \<^item> The code generated by a @{text computation} antiquotation takes a functional argument
   137       which describes how to conclude the computation.  What's the rationale
   138       behind this?
   139 
   140         \<^item> There is no automated way to generate a reconstruction function
   141           from the resulting ML type to a Isabelle term -- this is in the
   142           responsibility of the implementor.  One possible approach
   143           for robust term reconstruction is the @{text code} antiquotation.
   144 
   145         \<^item> Both statically specified input constants and dynamically provided input
   146           terms are subject to preprocessing.  Likewise the result
   147           is supposed to be subject to postprocessing; the implementor
   148           is expected to take care for this explicitly.
   149 
   150         \<^item> Computations follow the partiality principle (cf.~\secref{sec:partiality_principle}):
   151           failures due to pattern matching or unspecified functions
   152           are interpreted as partiality; therefore resulting ML values
   153           are optional. 
   154 
   155       Hence the functional argument accepts the following parameters
   156 
   157         \<^item> A postprocessor function @{ML_type "term -> term"}.
   158 
   159         \<^item> The resulting value as optional argument.
   160 
   161       The functional argument is supposed to compose the final result
   162       from these in a suitable manner.
   163 
   164   \noindent A simple application:
   165 \<close>
   166 
   167 ML_val %quotetypewriter \<open>
   168   comp_nat @{context} @{term "sum_list [Suc 0, Suc (Suc 0)] * Suc (Suc 0)"}
   169 \<close>
   170 
   171 text \<open>
   172   \noindent A single ML block may contain an arbitrary number of computation
   173   antiquotations.  These share the \<^emph>\<open>same\<close> set of possible
   174   input constants.  In other words, it does not matter in which
   175   antiquotation constants are specified;  in the following example,
   176   \<^emph>\<open>all\<close> constants are specified by the first antiquotation once
   177   and for all:
   178 \<close>
   179 
   180 ML %quotetypewriter \<open>
   181   local
   182 
   183   fun int_of_nat @{code "0 :: nat"} = 0
   184     | int_of_nat (@{code Suc} n) = int_of_nat n + 1;
   185 
   186   in
   187 
   188   val comp_nat = @{computation nat terms:
   189     "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
   190     "sum_list :: nat list \<Rightarrow> nat" "prod_list :: nat list \<Rightarrow> nat"
   191     "replicate :: nat \<Rightarrow> nat \<Rightarrow> nat list"
   192     datatypes: nat "nat list"}
   193     (fn post => post o HOLogic.mk_nat o int_of_nat o the);
   194 
   195   val comp_nat_list = @{computation "nat list"}
   196     (fn post => post o HOLogic.mk_list @{typ nat} o
   197       map (HOLogic.mk_nat o int_of_nat) o the);
   198 
   199   end
   200 \<close>
   201 
   202   
   203 subsection \<open>Pitfalls when specifying input constants \label{sec:input_constants_pitfalls}\<close>
   204 
   205 text \<open>
   206     \<^descr> \<open>Complete type coverage.\<close> Specified input constants must
   207       be \<^emph>\<open>complete\<close> in the sense that for each
   208       required type @{text \<tau>} there is at least one corresponding
   209       input constant which can actually \<^emph>\<open>construct\<close> a concrete
   210       value of type @{text \<tau>}, potentially requiring more types recursively;
   211       otherwise the system of equations cannot be generated properly.
   212       Hence such incomplete input constants sets are rejected immediately.
   213 
   214     \<^descr> \<open>Unsuitful right hand sides.\<close> The generated code for a computation
   215       must compile in the strict ML runtime environment.  This imposes
   216       the technical restriction that each compiled input constant
   217       @{text f\<^sub>C} on the right hand side of a generated equations
   218       must compile without throwing an exception.  That rules
   219       out pathological examples like @{term [source] "undefined :: nat"}
   220       as input constants, as well as abstract constructors (cf. \secref{sec:invariant}).
   221 
   222     \<^descr> \<open>Preprocessing.\<close> For consistency, input constants are subject
   223       to preprocessing;  however, the overall approach requires
   224       to operate on constants @{text C} and their respective compiled images
   225       @{text f\<^sub>C}.\footnote{Technical restrictions of the implementation
   226       enforce this, although those could be lifted in the future.}
   227       This is a problem whenever preprocessing maps an input constant
   228       to a non-constant.
   229 
   230       To circumvent these situations, the computation machinery
   231       has a dedicated preprocessor which is applied \<^emph>\<open>before\<close>
   232       the regular preprocessing, both to input constants as well as
   233       input terms.  This can be used to map problematic constants
   234       to other ones that are not subject to regular preprocessing. 
   235       Rewrite rules are added using attribute @{attribute code_computation_unfold}.
   236       There should rarely be a need to use this beyond the few default
   237       setups in HOL, which deal with literals (see also \secref{sec:literal_input}).
   238 \<close>
   239 
   240   
   241 subsection \<open>Pitfalls concerning input terms\<close>
   242 
   243 text \<open>
   244     \<^descr> \<open>No polymorphims.\<close> Input terms must be monomorphic: compilation
   245       to ML requires dedicated choice of monomorphic types.
   246 
   247     \<^descr> \<open>No abstractions.\<close> Only constants and applications are admissible
   248       as input; abstractions are not possible.  In theory, the
   249       compilation schema could be extended to cover abstractions also,
   250       but this would increase the trusted code base.  If abstractions
   251       are required, they can always be eliminated by a dedicated preprocessing
   252       step, e.g.~using combinatorial logic.
   253 
   254     \<^descr> \<open>Potential interfering of the preprocessor.\<close> As described in \secref{sec:input_constants_pitfalls}
   255       regular preprocessing can have a disruptive effect for input constants.
   256       The same also applies to input terms; however the same measures 
   257       to circumvent that problem for input constants apply to input terms also.
   258 \<close>
   259 
   260   
   261 subsection \<open>Computations using the @{text computation_conv} antiquotation\<close>
   262 
   263 text \<open>
   264   Computations are a device to implement fast proof procedures.
   265   Then results of a computation are often assumed to be trustable
   266   and thus wrapped in oracles (see \cite{isabelle-isar-ref}),
   267   as in the following example:\footnote{
   268   The technical details how numerals are dealt with are given later in
   269   \secref{sec:literal_input}.}
   270 \<close>
   271 
   272 ML %quotetypewriter \<open>
   273   local
   274 
   275   fun raw_dvd (b, ct) = Thm.mk_binop @{cterm "Pure.eq :: bool \<Rightarrow> bool \<Rightarrow> prop"}
   276     ct (if b then @{cterm True} else @{cterm False});
   277 
   278   val (_, dvd_oracle) = Context.>>> (Context.map_theory_result
   279     (Thm.add_oracle (@{binding dvd}, raw_dvd)));
   280 
   281   in
   282 
   283   val conv_dvd = @{computation_conv bool terms:
   284     "Rings.dvd :: int \<Rightarrow> int \<Rightarrow> bool"
   285     "plus :: int \<Rightarrow> int \<Rightarrow> int"
   286     "minus :: int \<Rightarrow> int \<Rightarrow> int"
   287     "times :: int \<Rightarrow> int \<Rightarrow> int"
   288     "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
   289   } (K (curry dvd_oracle))
   290 
   291   end
   292 \<close>
   293 
   294 text \<open>
   295     \<^item> Antiquotation @{ML_antiquotation computation_conv} basically yields
   296       a conversion of type @{ML_type "Proof.context -> cterm -> thm"}
   297       (see further \cite{isabelle-implementation}).
   298 
   299     \<^item> The antiquotation expects one functional argument to bridge the
   300       \qt{untrusted gap};  this can be done e.g.~using an oracle.  Since that oracle
   301       will only yield \qt{valid} results in the context of that particular
   302       computation, the implementor must make sure that it does not leave
   303       the local ML scope;  in this example, this is achieved using
   304       an explicit @{text local} ML block.  The very presence of the oracle
   305       in the code acknowledges that each computation requires explicit thinking
   306       before it can be considered trustworthy!
   307 
   308     \<^item> Postprocessing just operates as further conversion after normalization.
   309 
   310     \<^item> Partiality makes the whole conversion fall back to reflexivity.
   311 \<close> (*<*)
   312 
   313 (*>*) ML_val %quotetypewriter \<open>
   314   conv_dvd @{context} @{cterm "7 dvd ( 62437867527846782 :: int)"};
   315   conv_dvd @{context} @{cterm "7 dvd (-62437867527846783 :: int)"};
   316 \<close>
   317 
   318 text \<open>
   319   \noindent An oracle is not the only way to construct a valid theorem.
   320   A computation result can be used to construct an appropriate certificate:
   321 \<close>
   322 
   323 lemma %quote conv_div_cert:
   324   "(Code_Target_Int.positive r * Code_Target_Int.positive s)
   325      div Code_Target_Int.positive s \<equiv> (numeral r :: int)" (is "?lhs \<equiv> ?rhs")
   326 proof (rule eq_reflection)
   327   have "?lhs = numeral r * numeral s div numeral s"
   328     by simp
   329   also have "numeral r * numeral s div numeral s = ?rhs"
   330     by (rule nonzero_mult_div_cancel_right) simp
   331   finally show "?lhs = ?rhs" .
   332 qed
   333 
   334 lemma %quote positive_mult:
   335   "Code_Target_Int.positive r * Code_Target_Int.positive s = 
   336     Code_Target_Int.positive (r * s)"
   337   by simp
   338   
   339 ML %quotetypewriter \<open>
   340   local
   341 
   342   fun integer_of_int (@{code int_of_integer} k) = k
   343 
   344   val cterm_of_int = Thm.cterm_of @{context} o HOLogic.mk_numeral o integer_of_int;
   345 
   346   val divisor = Thm.dest_arg o Thm.dest_arg;
   347 
   348   val evaluate_simps = map mk_eq @{thms arith_simps positive_mult};
   349 
   350   fun evaluate ctxt = 
   351     Simplifier.rewrite_rule ctxt evaluate_simps;
   352 
   353   fun revaluate ctxt k ct =
   354     @{thm conv_div_cert}
   355     |> Thm.instantiate' [] [SOME (cterm_of_int k), SOME (divisor ct)]
   356     |> evaluate ctxt;
   357 
   358   in
   359 
   360   val conv_div = @{computation_conv int terms:
   361     "divide :: int \<Rightarrow> int \<Rightarrow> int"
   362     "0 :: int" "1 :: int" "2 :: int" "3 :: int"
   363   } revaluate
   364 
   365   end
   366 \<close>
   367 
   368 ML_val %quotetypewriter \<open>
   369   conv_div @{context}
   370     @{cterm "46782454343499999992777742432342242323423425 div (7 :: int)"}
   371 \<close>
   372 
   373 text \<open>
   374   \noindent The example is intentionally kept simple: only positive
   375   integers are covered, only remainder-free divisions are feasible,
   376   and the input term is expected to have a particular shape.
   377   This exhibits the idea more clearly:
   378   the result of the computation is used as a mere
   379   hint how to instantiate @{fact conv_div_cert}, from which the required
   380   theorem is obtained by performing multiplication using the
   381   simplifier;  hence that theorem is built of proper inferences,
   382   with no oracles involved.
   383 \<close>
   384 
   385 
   386 subsection \<open>Computations using the @{text computation_check} antiquotation\<close>
   387 
   388 text \<open>
   389   The @{text computation_check} antiquotation is convenient if
   390   only a positive checking of propositions is desired, because then
   391   the result type is fixed (@{typ prop}) and all the technical
   392   matter concerning postprocessing and oracles is done in the framework
   393   once and for all:
   394 \<close>
   395 
   396 ML %quotetypewriter \<open>
   397   val check_nat = @{computation_check terms:
   398     Trueprop "less :: nat \<Rightarrow> nat \<Rightarrow> bool" "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" 
   399     "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
   400     "0 :: nat" Suc
   401   }
   402 \<close>
   403 
   404 text \<open>
   405   \noindent The HOL judgement @{term Trueprop} embeds an expression
   406   of type @{typ bool} into @{typ prop}.
   407 \<close>
   408 
   409 ML_val %quotetypewriter \<open>
   410   check_nat @{context} @{cprop "less (Suc (Suc 0)) (Suc (Suc (Suc 0)))"}
   411 \<close>
   412 
   413 text \<open>
   414   \noindent Note that such computations can only \<^emph>\<open>check\<close>
   415   for @{typ prop}s to hold but not \<^emph>\<open>decide\<close>.
   416 \<close>
   417 
   418 
   419 subsection \<open>Some practical hints\<close>  
   420 
   421 subsubsection \<open>Inspecting generated code\<close>
   422 
   423 text \<open>
   424   The antiquotations for computations attempt to produce meaningful error
   425   messages.  If these are not sufficient, it might by useful to
   426   inspect the generated code, which can be achieved using
   427 \<close>
   428   
   429 declare %quote [[ML_source_trace]] (*<*) declare %quote [[ML_source_trace = false]] (*>*)
   430 
   431 
   432 subsubsection \<open>Literals as input constants \label{sec:literal_input}\<close>
   433 
   434 text \<open>
   435   Literals (characters, numerals) in computations cannot be processed
   436   naively: the compilation pattern for computations fails whenever
   437   target-language literals are involved; since various
   438   common code generator setups (see \secref{sec:common_adaptation})
   439   implement @{typ nat} and @{typ int} by target-language literals,
   440   this problem manifests whenever numeric types are involved.
   441   In practice, this is circumvented with a dedicated preprocessor
   442   setup for literals (see also \secref{sec:input_constants_pitfalls}).
   443 
   444   The following examples illustrate the pattern
   445   how to specify input constants when literals are involved, without going into
   446   too much detail:
   447 \<close>
   448 
   449 paragraph \<open>An example for @{typ nat}\<close>
   450 
   451 ML %quotetypewriter \<open>
   452   val check_nat = @{computation_check terms:
   453     Trueprop "even :: nat \<Rightarrow> bool" "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" 
   454     "0 :: nat" Suc "1 :: nat" "2 :: nat" "3 :: nat"
   455   }
   456 \<close>
   457 
   458 ML_val %quotetypewriter \<open>
   459   check_nat @{context} @{cprop "even (Suc 0 + 1 + 2 + 3 + 4 + 5)"}
   460 \<close>
   461   
   462 paragraph \<open>An example for @{typ int}\<close>
   463 
   464 ML %quotetypewriter \<open>
   465   val check_int = @{computation_check terms:
   466     Trueprop "even :: int \<Rightarrow> bool" "plus :: int \<Rightarrow> int \<Rightarrow> int" 
   467     "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
   468   }
   469 \<close>
   470 
   471 ML_val %quotetypewriter \<open>
   472   check_int @{context} @{cprop "even ((0::int) + 1 + 2 + 3 + -1 + -2 + -3)"}
   473 \<close>
   474   
   475 paragraph \<open>An example for @{typ char}\<close>
   476 
   477 definition %quote is_cap_letter :: "char \<Rightarrow> bool"
   478   where "is_cap_letter c \<longleftrightarrow> (let n = nat_of_char c in 65 \<le> n \<and> n \<le> 90)" (*<*)
   479 
   480 (*>*) ML %quotetypewriter \<open>
   481   val check_char = @{computation_check terms:
   482     Trueprop is_cap_letter
   483     Char datatypes: num
   484   }
   485 \<close>
   486 
   487 ML_val %quotetypewriter \<open>
   488   check_char @{context} @{cprop "is_cap_letter (CHR ''Y'')"}
   489 \<close>
   490 
   491   
   492 subsubsection \<open>Preprocessing HOL terms into evaluable shape\<close>
   493 
   494 text \<open>
   495   When integrating decision procedures developed inside HOL into HOL itself,
   496   a common approach is to use a deep embedding where operators etc.
   497   are represented by datatypes in Isabelle/HOL.  Then it is necessary
   498   to turn generic shallowly embedded statements into that particular
   499   deep embedding (\qt{reification}).
   500 
   501   One option is to hardcode using code antiquotations (see \secref{sec:code_antiq}).
   502   Another option is to use pre-existing infrastructure in HOL:
   503   @{ML "Reification.conv"} and @{ML "Reification.tac"}.
   504 
   505   A simplistic example:
   506 \<close>
   507 
   508 datatype %quote form_ord = T | F | Less nat nat
   509   | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
   510 
   511 primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
   512 where
   513   "interp T vs \<longleftrightarrow> True"
   514 | "interp F vs \<longleftrightarrow> False"
   515 | "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
   516 | "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
   517 | "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
   518 | "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
   519 
   520 text \<open>
   521   \noindent The datatype @{type form_ord} represents formulae whose semantics is given by
   522   @{const interp}.  Note that values are represented by variable indices (@{typ nat})
   523   whose concrete values are given in list @{term vs}.
   524 \<close>
   525 
   526 ML %quotetypewriter (*<*) \<open>\<close>
   527 lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> interp (And (Less (Suc 0) (Suc (Suc 0))) (Less (Suc 0) 0)) [z, x, y]"
   528 ML_prf %quotetypewriter
   529 (*>*) \<open>val thm =
   530   Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
   531 by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>)
   532 (*>*) 
   533 
   534 text \<open>
   535   \noindent By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
   536   which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
   537   to @{const interp} does not contain any free variables and can thus be evaluated
   538   using evaluation.
   539 
   540   A less meager example can be found in the AFP, session @{text "Regular-Sets"},
   541   theory @{text Regexp_Method}.
   542 \<close>
   543 
   544 end