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