Tue, 11 Apr 2017 10:29:25 +0200
changeset 65438 f556a7a9080c
parent 65436 1fd2dca8eb60 (current diff)
parent 65437 b8fc7e2e1b35 (diff)
child 65464 f3cd78ba687c
--- a/src/Doc/Prog_Prove/Isar.thy	Mon Apr 10 18:01:46 2017 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy	Tue Apr 11 10:29:25 2017 +0200
@@ -881,6 +881,45 @@
 \index{structural induction|)}
+\subsection{Computation Induction}
+\index{rule induction}
+In \autoref{sec:recursive-funs} we introduced computation induction and
+its realization in Isabelle: the definition
+of a recursive function \<open>f\<close> via \isacom{fun} proves the corresponding computation
+induction rule called \<open>f.induct\<close>. Induction with this rule looks like in
+\autoref{sec:recursive-funs}, but now with \isacom{proof} instead of \isacom{apply}:
+\isacom{proof} (\<open>induction x\<^sub>1 \<dots> x\<^sub>k rule: f.induct\<close>)
+Just as for structural induction, this creates several cases, one for each
+defining equation for \<open>f\<close>. By default (if the equations have not been named
+by the user), the cases are numbered. That is, they are started by
+\isacom{case} (\<open>i x y ...\<close>)
+where \<open>i = 1,...,n\<close>, \<open>n\<close> is the number of equations defining \<open>f\<close>,
+and \<open>x y ...\<close> are the variables in equation \<open>i\<close>. Note the following:
+Although \<open>i\<close> is an Isar name, \<open>i.IH\<close> (or similar) is not. You need
+double quotes: "\<open>i.IH\<close>". When indexing the name, write "\<open>i.IH\<close>"(1),
+not "\<open>i.IH\<close>(1)".
+If defining equations for \<open>f\<close> overlap, \isacom{fun} instantiates them to make
+them nonoverlapping. This means that one user-provided equation may lead to
+several equations and thus to several cases in the induction rule.
+These have names of the form "\<open>i_j\<close>", where \<open>i\<close> is the number of the original
+equation and the system-generated \<open>j\<close> indicates the subcase.
+In Isabelle/jEdit, the \<open>induction\<close> proof method displays a proof skeleton
+with all \isacom{case}s. This is particularly useful for computation induction
+and the following rule induction.
 \subsection{Rule Induction}
 \index{rule induction|(}