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