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