src/Doc/Codegen/Inductive_Predicate.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 66453 cc19f7ca2ed6
child 69422 472af2d7835d
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
haftmann@37613
     1
theory Inductive_Predicate
wenzelm@66453
     2
imports Codegen_Basics.Setup
haftmann@37613
     3
begin
haftmann@37613
     4
haftmann@37613
     5
(*<*)
haftmann@38441
     6
hide_const %invisible append
haftmann@37613
     7
haftmann@38441
     8
inductive %invisible append where
haftmann@37613
     9
  "append [] ys ys"
haftmann@38811
    10
| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
haftmann@38441
    11
haftmann@38441
    12
lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"
haftmann@38441
    13
  by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
haftmann@46515
    14
haftmann@46515
    15
lemmas lexordp_def = 
haftmann@46515
    16
  lexordp_def [unfolded lexord_def mem_Collect_eq split]
haftmann@37613
    17
(*>*)
haftmann@38441
    18
haftmann@59377
    19
section \<open>Inductive Predicates \label{sec:inductive}\<close>
haftmann@38441
    20
haftmann@59377
    21
text \<open>
haftmann@38508
    22
  The @{text "predicate compiler"} is an extension of the code generator
haftmann@38441
    23
  which turns inductive specifications into equational ones, from
haftmann@38441
    24
  which in turn executable code can be generated.  The mechanisms of
haftmann@38441
    25
  this compiler are described in detail in
wenzelm@58620
    26
  @{cite "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}.
haftmann@38441
    27
haftmann@38441
    28
  Consider the simple predicate @{const append} given by these two
haftmann@38441
    29
  introduction rules:
haftmann@59377
    30
\<close>
haftmann@38441
    31
haftmann@59377
    32
text %quote \<open>
haftmann@38441
    33
  @{thm append.intros(1)[of ys]} \\
haftmann@38441
    34
  @{thm append.intros(2)[of xs ys zs x]}
haftmann@59377
    35
\<close>
haftmann@38441
    36
haftmann@59377
    37
text \<open>
haftmann@38441
    38
  \noindent To invoke the compiler, simply use @{command_def "code_pred"}:
haftmann@59377
    39
\<close>
haftmann@37613
    40
haftmann@38441
    41
code_pred %quote append .
haftmann@38441
    42
haftmann@59377
    43
text \<open>
haftmann@38441
    44
  \noindent The @{command "code_pred"} command takes the name of the
haftmann@38441
    45
  inductive predicate and then you put a period to discharge a trivial
haftmann@38441
    46
  correctness proof.  The compiler infers possible modes for the
haftmann@38441
    47
  predicate and produces the derived code equations.  Modes annotate
haftmann@38441
    48
  which (parts of the) arguments are to be taken as input, and which
haftmann@38441
    49
  output. Modes are similar to types, but use the notation @{text "i"}
haftmann@38441
    50
  for input and @{text "o"} for output.
haftmann@38441
    51
 
haftmann@38441
    52
  For @{term "append"}, the compiler can infer the following modes:
haftmann@38441
    53
  \begin{itemize}
haftmann@38441
    54
    \item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
haftmann@38441
    55
    \item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
haftmann@38441
    56
    \item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
haftmann@38441
    57
  \end{itemize}
haftmann@38441
    58
  You can compute sets of predicates using @{command_def "values"}:
haftmann@59377
    59
\<close>
haftmann@38441
    60
haftmann@38441
    61
values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
haftmann@38441
    62
haftmann@59377
    63
text \<open>\noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and\<close>
haftmann@38441
    64
haftmann@38441
    65
values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
haftmann@38441
    66
haftmann@59377
    67
text \<open>\noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}.\<close>
haftmann@37613
    68
haftmann@59377
    69
text \<open>
haftmann@38441
    70
  \noindent If you are only interested in the first elements of the
haftmann@38441
    71
  set comprehension (with respect to a depth-first search on the
haftmann@38441
    72
  introduction rules), you can pass an argument to @{command "values"}
haftmann@38441
    73
  to specify the number of elements you want:
haftmann@59377
    74
\<close>
haftmann@37613
    75
haftmann@38441
    76
values %quote 1 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
haftmann@38441
    77
values %quote 3 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
haftmann@38441
    78
haftmann@59377
    79
text \<open>
haftmann@38441
    80
  \noindent The @{command "values"} command can only compute set
haftmann@38441
    81
  comprehensions for which a mode has been inferred.
haftmann@38441
    82
haftmann@38441
    83
  The code equations for a predicate are made available as theorems with
haftmann@38441
    84
  the suffix @{text "equation"}, and can be inspected with:
haftmann@59377
    85
\<close>
haftmann@38441
    86
haftmann@38441
    87
thm %quote append.equation
haftmann@38441
    88
haftmann@59377
    89
text \<open>
haftmann@38441
    90
  \noindent More advanced options are described in the following subsections.
haftmann@59377
    91
\<close>
haftmann@38441
    92
haftmann@59377
    93
subsection \<open>Alternative names for functions\<close>
haftmann@38441
    94
haftmann@59377
    95
text \<open>
haftmann@38441
    96
  By default, the functions generated from a predicate are named after
haftmann@38441
    97
  the predicate with the mode mangled into the name (e.g., @{text
haftmann@38441
    98
  "append_i_i_o"}).  You can specify your own names as follows:
haftmann@59377
    99
\<close>
haftmann@38441
   100
haftmann@38811
   101
code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat,
haftmann@38811
   102
  o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split,
haftmann@38811
   103
  i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append .
haftmann@37613
   104
haftmann@59377
   105
subsection \<open>Alternative introduction rules\<close>
haftmann@38441
   106
haftmann@59377
   107
text \<open>
haftmann@38441
   108
  Sometimes the introduction rules of an predicate are not executable
haftmann@38441
   109
  because they contain non-executable constants or specific modes
haftmann@38441
   110
  could not be inferred.  It is also possible that the introduction
haftmann@38441
   111
  rules yield a function that loops forever due to the execution in a
haftmann@38441
   112
  depth-first search manner.  Therefore, you can declare alternative
haftmann@38441
   113
  introduction rules for predicates with the attribute @{attribute
haftmann@38441
   114
  "code_pred_intro"}.  For example, the transitive closure is defined
haftmann@38441
   115
  by:
haftmann@59377
   116
\<close>
haftmann@38441
   117
haftmann@59377
   118
text %quote \<open>
haftmann@39682
   119
  @{lemma [source] "r a b \<Longrightarrow> tranclp r a b" by (fact tranclp.intros(1))}\\
haftmann@39682
   120
  @{lemma [source] "tranclp r a b \<Longrightarrow> r b c \<Longrightarrow> tranclp r a c" by (fact tranclp.intros(2))}
haftmann@59377
   121
\<close>
haftmann@38441
   122
haftmann@59377
   123
text \<open>
haftmann@38441
   124
  \noindent These rules do not suit well for executing the transitive
haftmann@38441
   125
  closure with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as
haftmann@38441
   126
  the second rule will cause an infinite loop in the recursive call.
haftmann@38441
   127
  This can be avoided using the following alternative rules which are
haftmann@38441
   128
  declared to the predicate compiler by the attribute @{attribute
haftmann@38441
   129
  "code_pred_intro"}:
haftmann@59377
   130
\<close>
haftmann@38441
   131
haftmann@37613
   132
lemma %quote [code_pred_intro]:
haftmann@39682
   133
  "r a b \<Longrightarrow> tranclp r a b"
haftmann@39682
   134
  "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
haftmann@37613
   135
by auto
haftmann@38441
   136
haftmann@59377
   137
text \<open>
haftmann@38441
   138
  \noindent After declaring all alternative rules for the transitive
haftmann@38441
   139
  closure, you invoke @{command "code_pred"} as usual.  As you have
haftmann@38441
   140
  declared alternative rules for the predicate, you are urged to prove
haftmann@38441
   141
  that these introduction rules are complete, i.e., that you can
haftmann@38441
   142
  derive an elimination rule for the alternative rules:
haftmann@59377
   143
\<close>
haftmann@38441
   144
haftmann@37613
   145
code_pred %quote tranclp
haftmann@37613
   146
proof -
haftmann@37613
   147
  case tranclp
haftmann@39682
   148
  from this converse_tranclpE [OF tranclp.prems] show thesis by metis
haftmann@37613
   149
qed
haftmann@38441
   150
haftmann@59377
   151
text \<open>
haftmann@38441
   152
  \noindent Alternative rules can also be used for constants that have
haftmann@38441
   153
  not been defined inductively. For example, the lexicographic order
haftmann@38441
   154
  which is defined as:
haftmann@59377
   155
\<close>
haftmann@38441
   156
haftmann@59377
   157
text %quote \<open>
haftmann@46515
   158
  @{thm [display] lexordp_def [of r]}
haftmann@59377
   159
\<close>
haftmann@38441
   160
haftmann@59377
   161
text \<open>
haftmann@38441
   162
  \noindent To make it executable, you can derive the following two
haftmann@38441
   163
  rules and prove the elimination rule:
haftmann@59377
   164
\<close>
haftmann@38441
   165
haftmann@37613
   166
lemma %quote [code_pred_intro]:
haftmann@46515
   167
  "append xs (a # v) ys \<Longrightarrow> lexordp r xs ys"
haftmann@46515
   168
(*<*)unfolding lexordp_def by (auto simp add: append)(*>*)
haftmann@37613
   169
haftmann@37613
   170
lemma %quote [code_pred_intro]:
haftmann@46515
   171
  "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b
haftmann@46515
   172
  \<Longrightarrow> lexordp r xs ys"
haftmann@46515
   173
(*<*)unfolding lexordp_def append apply simp
haftmann@38441
   174
apply (rule disjI2) by auto(*>*)
haftmann@37613
   175
haftmann@46515
   176
code_pred %quote lexordp
haftmann@38441
   177
(*<*)proof -
haftmann@37613
   178
  fix r xs ys
haftmann@46515
   179
  assume lexord: "lexordp r xs ys"
haftmann@46515
   180
  assume 1: "\<And>r' xs' ys' a v. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
haftmann@46515
   181
    \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
haftmann@46515
   182
  assume 2: "\<And>r' xs' ys' u a v b w. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
haftmann@46515
   183
    \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> thesis"
haftmann@37613
   184
  {
haftmann@37613
   185
    assume "\<exists>a v. ys = xs @ a # v"
haftmann@37613
   186
    from this 1 have thesis
haftmann@46515
   187
        by (fastforce simp add: append)
haftmann@37613
   188
  } moreover
haftmann@37613
   189
  {
haftmann@46515
   190
    assume "\<exists>u a b v w. r a b \<and> xs = u @ a # v \<and> ys = u @ b # w"
haftmann@46515
   191
    from this 2 have thesis by (fastforce simp add: append)
haftmann@37613
   192
  } moreover
haftmann@37613
   193
  note lexord
haftmann@37613
   194
  ultimately show thesis
haftmann@46515
   195
    unfolding lexordp_def
haftmann@46515
   196
    by fastforce
haftmann@38441
   197
qed(*>*)
haftmann@38441
   198
haftmann@38441
   199
haftmann@59377
   200
subsection \<open>Options for values\<close>
haftmann@38441
   201
haftmann@59377
   202
text \<open>
haftmann@38441
   203
  In the presence of higher-order predicates, multiple modes for some
haftmann@38441
   204
  predicate could be inferred that are not disambiguated by the
haftmann@38441
   205
  pattern of the set comprehension.  To disambiguate the modes for the
haftmann@38441
   206
  arguments of a predicate, you can state the modes explicitly in the
haftmann@38441
   207
  @{command "values"} command.  Consider the simple predicate @{term
haftmann@38441
   208
  "succ"}:
haftmann@59377
   209
\<close>
haftmann@38441
   210
haftmann@38441
   211
inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
haftmann@37613
   212
  "succ 0 (Suc 0)"
haftmann@37613
   213
| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
haftmann@37613
   214
haftmann@38441
   215
code_pred %quote succ .
haftmann@37613
   216
haftmann@59377
   217
text \<open>
haftmann@38441
   218
  \noindent For this, the predicate compiler can infer modes @{text "o
haftmann@38441
   219
  \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"}, @{text "o \<Rightarrow> i \<Rightarrow> bool"} and
haftmann@38441
   220
  @{text "i \<Rightarrow> i \<Rightarrow> bool"}.  The invocation of @{command "values"}
haftmann@38441
   221
  @{text "{n. tranclp succ 10 n}"} loops, as multiple modes for the
haftmann@38441
   222
  predicate @{text "succ"} are possible and here the first mode @{text
haftmann@38441
   223
  "o \<Rightarrow> o \<Rightarrow> bool"} is chosen. To choose another mode for the argument,
haftmann@38441
   224
  you can declare the mode for the argument between the @{command
haftmann@38441
   225
  "values"} and the number of elements.
haftmann@59377
   226
\<close>
haftmann@38441
   227
wenzelm@61498
   228
values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIXME does not terminate for n\<ge>1*)
haftmann@39065
   229
values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}"
haftmann@37613
   230
haftmann@38441
   231
haftmann@59377
   232
subsection \<open>Embedding into functional code within Isabelle/HOL\<close>
haftmann@38441
   233
haftmann@59377
   234
text \<open>
haftmann@38441
   235
  To embed the computation of an inductive predicate into functions
haftmann@38441
   236
  that are defined in Isabelle/HOL, you have a number of options:
haftmann@38441
   237
haftmann@38441
   238
  \begin{itemize}
haftmann@38441
   239
wenzelm@61498
   240
  \item You want to use the first-order predicate with the mode
wenzelm@61498
   241
    where all arguments are input. Then you can use the predicate directly, e.g.
haftmann@38441
   242
wenzelm@61498
   243
    @{text [display]
wenzelm@61498
   244
\<open>valid_suffix ys zs =
wenzelm@61498
   245
  (if append [Suc 0, 2] ys zs then Some ys else None)\<close>}
haftmann@38441
   246
wenzelm@61498
   247
  \item If you know that the execution returns only one value (it is
wenzelm@61498
   248
    deterministic), then you can use the combinator @{term
wenzelm@61498
   249
    "Predicate.the"}, e.g., a functional concatenation of lists is
wenzelm@61498
   250
    defined with
haftmann@38441
   251
wenzelm@61498
   252
    @{term [display] "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
haftmann@38441
   253
wenzelm@61498
   254
    Note that if the evaluation does not return a unique value, it
wenzelm@61498
   255
    raises a run-time error @{term "not_unique"}.
haftmann@38441
   256
haftmann@38441
   257
  \end{itemize}
haftmann@59377
   258
\<close>
haftmann@38441
   259
haftmann@38441
   260
haftmann@59377
   261
subsection \<open>Further Examples\<close>
haftmann@38441
   262
haftmann@59377
   263
text \<open>
haftmann@38441
   264
  Further examples for compiling inductive predicates can be found in
wenzelm@63680
   265
  \<^file>\<open>~~/src/HOL/Predicate_Compile_Examples/Examples.thy\<close>.  There are
haftmann@38441
   266
  also some examples in the Archive of Formal Proofs, notably in the
haftmann@38441
   267
  @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
haftmann@38441
   268
  sessions.
haftmann@59377
   269
\<close>
haftmann@38441
   270
haftmann@37613
   271
end
haftmann@46515
   272