equal
deleted
inserted
replaced
46 definition of @{term"sep"}. |
46 definition of @{term"sep"}. |
47 |
47 |
48 In general, the format of invoking recursion induction is |
48 In general, the format of invoking recursion induction is |
49 \begin{quote} |
49 \begin{quote} |
50 \isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"} |
50 \isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"} |
51 \end{quote}\index{*induct_tac}% |
51 \end{quote}\index{*induct_tac (method)}% |
52 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
52 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
53 name of a function that takes an $n$-tuple. Usually the subgoal will |
53 name of a function that takes an $n$-tuple. Usually the subgoal will |
54 contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The |
54 contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The |
55 induction rules do not mention $f$ at all. For example @{thm[source]sep.induct} |
55 induction rules do not mention $f$ at all. For example @{thm[source]sep.induct} |
56 \begin{isabelle} |
56 \begin{isabelle} |