1.1 --- a/doc-src/TutorialI/Inductive/Advanced.thy Wed Feb 21 12:07:00 2001 +0100
1.2 +++ b/doc-src/TutorialI/Inductive/Advanced.thy Wed Feb 21 12:57:55 2001 +0100
1.3 @@ -56,7 +56,7 @@
1.4 \rulename{gterm_Apply_elim}
1.5 *}
1.6
1.7 -lemma gterms_IntI [rule_format]:
1.8 +lemma gterms_IntI [rule_format, intro!]:
1.9 "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
1.10 apply (erule gterms.induct)
1.11 txt{*
1.12 @@ -73,10 +73,7 @@
1.13
1.14 lemma gterms_Int_eq [simp]:
1.15 "gterms (F\<inter>G) = gterms F \<inter> gterms G"
1.16 -apply (rule equalityI)
1.17 -apply (blast intro!: mono_Int monoI gterms_mono)
1.18 -apply (blast intro!: gterms_IntI)
1.19 -done
1.20 +by (blast intro!: mono_Int monoI gterms_mono)
1.21
1.22
1.23 consts integer_arity :: "integer_op \<Rightarrow> nat"
2.1 --- a/doc-src/TutorialI/Inductive/advanced-examples.tex Wed Feb 21 12:07:00 2001 +0100
2.2 +++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Wed Feb 21 12:57:55 2001 +0100
2.3 @@ -1,7 +1,11 @@
2.4 % $Id$
2.5 -This section describes advanced features of inductive definitions.
2.6 The premises of introduction rules may contain universal quantifiers and
2.7 -monotonic functions. Theorems may be proved by rule inversion.
2.8 +monotone functions. A universal quantifier lets the rule
2.9 +refer to any number of instances of
2.10 +the inductively defined set. A monotone function lets the rule refer
2.11 +to existing constructions (such as ``list of'') over the inductively defined
2.12 +set. The examples below show how to use the additional expressiveness
2.13 +and how to reason from the resulting definitions.
2.14
2.15 \subsection{Universal Quantifiers in Introduction Rules}
2.16 \label{sec:gterm-datatype}
2.17 @@ -40,7 +44,7 @@
2.18 A universal quantifier in the premise of the introduction rule
2.19 expresses that every element of \isa{args} belongs
2.20 to our inductively defined set: is a ground term
2.21 -over~\isa{F}. The function {\isa{set}} denotes the set of elements in a given
2.22 +over~\isa{F}. The function \isa{set} denotes the set of elements in a given
2.23 list.
2.24 \begin{isabelle}
2.25 \isacommand{consts}\ gterms\ ::\ "'f\ set\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
2.26 @@ -53,7 +57,7 @@
2.27
2.28 To demonstrate a proof from this definition, let us
2.29 show that the function \isa{gterms}
2.30 -is \textbf{monotonic}. We shall need this concept shortly.
2.31 +is \textbf{monotone}. We shall need this concept shortly.
2.32 \begin{isabelle}
2.33 \isacommand{lemma}\ gterms_mono:\ "F\isasymsubseteq G\ \isasymLongrightarrow \ gterms\ F\ \isasymsubseteq \ gterms\ G"\isanewline
2.34 \isacommand{apply}\ clarify\isanewline
2.35 @@ -85,162 +89,16 @@
2.36 {\isa{gterm.induct}}.
2.37 \end{warn}
2.38
2.39 -
2.40 -\subsection{Rule Inversion}\label{sec:rule-inversion}
2.41 -
2.42 -Case analysis on an inductive definition is called \textbf{rule inversion}.
2.43 -It is frequently used in proofs about operational semantics. It can be
2.44 -highly effective when it is applied automatically. Let us look at how rule
2.45 -inversion is done in Isabelle.
2.46 -
2.47 -Recall that \isa{even} is the minimal set closed under these two rules:
2.48 -\begin{isabelle}
2.49 -0\ \isasymin \ even\isanewline
2.50 -n\ \isasymin \ even\ \isasymLongrightarrow \ Suc\ (Suc\ n)\ \isasymin
2.51 -\ even
2.52 -\end{isabelle}
2.53 -Minimality means that \isa{even} contains only the elements that these
2.54 -rules force it to contain. If we are told that \isa{a}
2.55 -belongs to
2.56 -\isa{even} then there are only two possibilities. Either \isa{a} is \isa{0}
2.57 -or else \isa{a} has the form \isa{Suc(Suc~n)}, for some suitable \isa{n}
2.58 -that belongs to
2.59 -\isa{even}. That is the gist of the \isa{cases} rule, which Isabelle proves
2.60 -for us when it accepts an inductive definition:
2.61 -\begin{isabelle}
2.62 -\isasymlbrakk a\ \isasymin \ even;\isanewline
2.63 -\ a\ =\ 0\ \isasymLongrightarrow \ P;\isanewline
2.64 -\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc(Suc\ n);\ n\ \isasymin \
2.65 -even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \
2.66 -\isasymLongrightarrow \ P
2.67 -\rulename{even.cases}
2.68 -\end{isabelle}
2.69 -
2.70 -This general rule is less useful than instances of it for
2.71 -specific patterns. For example, if \isa{a} has the form
2.72 -\isa{Suc(Suc~n)} then the first case becomes irrelevant, while the second
2.73 -case tells us that \isa{n} belongs to \isa{even}. Isabelle will generate
2.74 -this instance for us:
2.75 -\begin{isabelle}
2.76 -\isacommand{inductive\_cases}\ Suc_Suc_cases\ [elim!]:
2.77 -\ "Suc(Suc\ n)\ \isasymin \ even"
2.78 -\end{isabelle}
2.79 -The \isacommand{inductive\_cases} command generates an instance of the
2.80 -\isa{cases} rule for the supplied pattern and gives it the supplied name:
2.81 -%
2.82 -\begin{isabelle}
2.83 -\isasymlbrakk Suc\ (Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\
2.84 -\isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
2.85 -\rulename{Suc_Suc_cases}
2.86 -\end{isabelle}
2.87 -%
2.88 -Applying this as an elimination rule yields one case where \isa{even.cases}
2.89 -would yield two. Rule inversion works well when the conclusions of the
2.90 -introduction rules involve datatype constructors like \isa{Suc} and \isa{\#}
2.91 -(list ``cons''); freeness reasoning discards all but one or two cases.
2.92 -
2.93 -In the \isacommand{inductive\_cases} command we supplied an
2.94 -attribute, \isa{elim!}, indicating that this elimination rule can be applied
2.95 -aggressively. The original
2.96 -\isa{cases} rule would loop if used in that manner because the
2.97 -pattern~\isa{a} matches everything.
2.98 -
2.99 -The rule \isa{Suc_Suc_cases} is equivalent to the following implication:
2.100 -\begin{isabelle}
2.101 -Suc (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \
2.102 -even
2.103 -\end{isabelle}
2.104 -%
2.105 -In {\S}\ref{sec:gen-rule-induction} we devoted some effort to proving precisely
2.106 -this result. Yet we could have obtained it by a one-line declaration.
2.107 -This example also justifies the terminology \textbf{rule inversion}: the new
2.108 -rule inverts the introduction rule \isa{even.step}.
2.109 -
2.110 -For one-off applications of rule inversion, use the \isa{ind_cases} method.
2.111 -Here is an example:
2.112 -\begin{isabelle}
2.113 -\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")
2.114 -\end{isabelle}
2.115 -The specified instance of the \isa{cases} rule is generated, applied, and
2.116 -discarded.
2.117 -
2.118 -\medskip
2.119 -Let us try rule inversion on our ground terms example:
2.120 -\begin{isabelle}
2.121 -\isacommand{inductive\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\
2.122 -\isasymin\ gterms\ F"
2.123 -\end{isabelle}
2.124 -%
2.125 -Here is the result. No cases are discarded (there was only one to begin
2.126 -with) but the rule applies specifically to the pattern \isa{Apply\ f\ args}.
2.127 -It can be applied repeatedly as an elimination rule without looping, so we
2.128 -have given the
2.129 -\isa{elim!}\ attribute.
2.130 -\begin{isabelle}
2.131 -\isasymlbrakk Apply\ f\ args\ \isasymin \ gterms\ F;\isanewline
2.132 -\ \isasymlbrakk
2.133 -\isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F;\ f\ \isasymin
2.134 -\ F\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk\isanewline
2.135 -\isasymLongrightarrow \ P%
2.136 -\rulename{gterm_Apply_elim}
2.137 -\end{isabelle}
2.138 -
2.139 -This rule replaces an assumption about \isa{Apply\ f\ args} by
2.140 -assumptions about \isa{f} and~\isa{args}. Here is a proof in which this
2.141 -inference is essential. We show that if \isa{t} is a ground term over both
2.142 -of the sets
2.143 -\isa{F} and~\isa{G} then it is also a ground term over their intersection,
2.144 -\isa{F\isasyminter G}.
2.145 -\begin{isabelle}
2.146 -\isacommand{lemma}\ gterms_IntI\ [rule_format]:\isanewline
2.147 -\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter G)"\isanewline
2.148 -\isacommand{apply}\ (erule\ gterms.induct)\isanewline
2.149 -\isacommand{apply}\ blast\isanewline
2.150 -\isacommand{done}
2.151 -\end{isabelle}
2.152 -%
2.153 -The proof begins with rule induction over the definition of
2.154 -\isa{gterms}, which leaves a single subgoal:
2.155 -\begin{isabelle}
2.156 -1.\ \isasymAnd args\ f.\isanewline
2.157 -\ \ \ \ \ \ \isasymlbrakk \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand\isanewline
2.158 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline
2.159 -\ \ \ \ \ \ \ f\ \isasymin \ F\isasymrbrakk \isanewline
2.160 -\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G)
2.161 -\end{isabelle}
2.162 -%
2.163 -The induction hypothesis states that every element of \isa{args} belongs to
2.164 -\isa{gterms\ (F\ \isasyminter \ G)} --- provided it already belongs to
2.165 -\isa{gterms\ G}. How do we meet that condition?
2.166 -
2.167 -By assuming (as we may) the formula \isa{Apply\ f\ args\ \isasymin \ gterms\
2.168 -G}. Rule inversion, in the form of \isa{gterm_Apply_elim}, infers that every
2.169 -element of \isa{args} belongs to
2.170 -\isa{gterms~G}. It also yields \isa{f\ \isasymin \ G}, which will allow us
2.171 -to conclude \isa{f\ \isasymin \ F\ \isasyminter \ G}. All of this reasoning
2.172 -is done by \isa{blast}.
2.173 -
2.174 -\medskip
2.175 -
2.176 -To summarize, every inductive definition produces a \isa{cases} rule. The
2.177 -\isacommand{inductive\_cases} command stores an instance of the \isa{cases}
2.178 -rule for a given pattern. Within a proof, the \isa{ind_cases} method
2.179 -applies an instance of the \isa{cases}
2.180 -rule.
2.181 -
2.182 -
2.183 -\subsection{Continuing the Ground Terms Example}
2.184 -
2.185 -Call a term \textbf{well-formed} if each symbol occurring in it has
2.186 -the correct number of arguments. To formalize this concept, we
2.187 -introduce a function mapping each symbol to its \textbf{arity}, a natural
2.188 -number.
2.189 -
2.190 -Let us define the set of well-formed ground terms.
2.191 -Suppose we are given a function called \isa{arity}, specifying the arities to be used.
2.192 -In the inductive step, we have a list \isa{args} of such terms and a function
2.193 -symbol~\isa{f}. If the length of the list matches the function's arity
2.194 -then applying \isa{f} to \isa{args} yields a well-formed term.
2.195 +Call a term \textbf{well-formed} if each symbol occurring in it is applied
2.196 +to the correct number of arguments. (This number is called the symbol's
2.197 +\textbf{arity}.) We can express well-formedness by
2.198 +generalizing the inductive definition of
2.199 +\isa{gterms}.
2.200 +Suppose we are given a function called \isa{arity}, specifying the arities
2.201 +of all symbols. In the inductive step, we have a list \isa{args} of such
2.202 +terms and a function symbol~\isa{f}. If the length of the list matches the
2.203 +function's arity then applying \isa{f} to \isa{args} yields a well-formed
2.204 +term.
2.205 \begin{isabelle}
2.206 \isacommand{consts}\ well_formed_gterm\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
2.207 \isacommand{inductive}\ "well_formed_gterm\ arity"\isanewline
2.208 @@ -252,14 +110,14 @@
2.209 \end{isabelle}
2.210 %
2.211 The inductive definition neatly captures the reasoning above.
2.212 -It is just an elaboration of the previous one, consisting of a single
2.213 -introduction rule. The universal quantification over the
2.214 +The universal quantification over the
2.215 \isa{set} of arguments expresses that all of them are well-formed.
2.216
2.217 -\subsection{Alternative Definition Using a Monotonic Function}
2.218 +
2.219 +\subsection{Alternative Definition Using a monotone Function}
2.220
2.221 An inductive definition may refer to the inductively defined
2.222 -set through an arbitrary monotonic function. To demonstrate this
2.223 +set through an arbitrary monotone function. To demonstrate this
2.224 powerful feature, let us
2.225 change the inductive definition above, replacing the
2.226 quantifier by a use of the function \isa{lists}. This
2.227 @@ -289,7 +147,7 @@
2.228 \ lists\ B\rulename{lists_mono}
2.229 \end{isabelle}
2.230 %
2.231 -Why must the function be monotonic? An inductive definition describes
2.232 +Why must the function be monotone? An inductive definition describes
2.233 an iterative construction: each element of the set is constructed by a
2.234 finite number of introduction rule applications. For example, the
2.235 elements of \isa{even} are constructed by finitely many applications of
2.236 @@ -321,7 +179,7 @@
2.237 \end{isabelle}
2.238 To apply the rule we construct a list \isa{args} of previously
2.239 constructed well-formed terms. We obtain a
2.240 -new term, \isa{Apply\ f\ args}. Because \isa{lists} is monotonic,
2.241 +new term, \isa{Apply\ f\ args}. Because \isa{lists} is monotone,
2.242 applications of the rule remain valid as new terms are constructed.
2.243 Further lists of well-formed
2.244 terms become available and none are taken away.
2.245 @@ -372,9 +230,9 @@
2.246 \ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm\ arity%
2.247 \end{isabelle}
2.248 The induction hypothesis contains an application of \isa{lists}. Using a
2.249 -monotonic function in the inductive definition always has this effect. The
2.250 -subgoal may look uninviting, but fortunately a useful rewrite rule concerning
2.251 -\isa{lists} is available:
2.252 +monotone function in the inductive definition always has this effect. The
2.253 +subgoal may look uninviting, but fortunately
2.254 +\isa{lists} distributes over intersection:
2.255 \begin{isabelle}
2.256 lists\ (A\ \isasyminter \ B)\ =\ lists\ A\ \isasyminter \ lists\ B
2.257 \rulename{lists_Int_eq}
2.258 @@ -390,10 +248,9 @@
2.259 call to
2.260 \isa{auto} does all this work.
2.261
2.262 -This example is typical of how monotonic functions can be used. In
2.263 -particular, a rewrite rule analogous to \isa{lists_Int_eq} holds in most
2.264 -cases. Monotonicity implies one direction of this set equality; we have
2.265 -this theorem:
2.266 +This example is typical of how monotone functions can be used. In
2.267 +particular, many of them distribute over intersection. Monotonicity
2.268 +implies one direction of this set equality; we have this theorem:
2.269 \begin{isabelle}
2.270 mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \
2.271 f\ A\ \isasyminter \ f\ B%
2.272 @@ -401,15 +258,76 @@
2.273 \end{isabelle}
2.274
2.275
2.276 -To summarize: a universal quantifier in an introduction rule
2.277 -lets it refer to any number of instances of
2.278 -the inductively defined set. A monotonic function in an introduction
2.279 -rule lets it refer to constructions over the inductively defined
2.280 -set. Each element of an inductively defined set is created
2.281 -through finitely many applications of the introduction rules. So each rule
2.282 -must be positive, and never can it refer to \textit{infinitely} many
2.283 -previous instances of the inductively defined set.
2.284 +\subsection{Another Example of Rule Inversion}
2.285
2.286 +Does \isa{gterms} distribute over intersection? We have proved that this
2.287 +function is monotone, so \isa{mono_Int} gives one of the inclusions. The
2.288 +opposite inclusion asserts that if \isa{t} is a ground term over both of the
2.289 +sets
2.290 +\isa{F} and~\isa{G} then it is also a ground term over their intersection,
2.291 +\isa{F\isasyminter G}.
2.292 +
2.293 +Attempting this proof, we get the assumption
2.294 +\isa{Apply\ f\ args\ \isasymin\ gterms\ F}, which cannot be broken down.
2.295 +It looks like a job for rule inversion:
2.296 +\begin{isabelle}
2.297 +\isacommand{inductive\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\
2.298 +\isasymin\ gterms\ F"
2.299 +\end{isabelle}
2.300 +%
2.301 +Here is the result.
2.302 +\begin{isabelle}
2.303 +\isasymlbrakk Apply\ f\ args\ \isasymin \ gterms\ F;\isanewline
2.304 +\ \isasymlbrakk
2.305 +\isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F;\ f\ \isasymin
2.306 +\ F\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk\isanewline
2.307 +\isasymLongrightarrow \ P%
2.308 +\rulename{gterm_Apply_elim}
2.309 +\end{isabelle}
2.310 +This rule replaces an assumption about \isa{Apply\ f\ args} by
2.311 +assumptions about \isa{f} and~\isa{args}.
2.312 +No cases are discarded (there was only one to begin
2.313 +with) but the rule applies specifically to the pattern \isa{Apply\ f\ args}.
2.314 +It can be applied repeatedly as an elimination rule without looping, so we
2.315 +have given the
2.316 +\isa{elim!}\ attribute.
2.317 +
2.318 +Now we can prove the other half of that distributive law.
2.319 +\begin{isabelle}
2.320 +\isacommand{lemma}\ gterms_IntI\ [rule_format,\ intro!]:\isanewline
2.321 +\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter G)"\isanewline
2.322 +\isacommand{apply}\ (erule\ gterms.induct)\isanewline
2.323 +\isacommand{apply}\ blast\isanewline
2.324 +\isacommand{done}
2.325 +\end{isabelle}
2.326 +%
2.327 +The proof begins with rule induction over the definition of
2.328 +\isa{gterms}, which leaves a single subgoal:
2.329 +\begin{isabelle}
2.330 +1.\ \isasymAnd args\ f.\isanewline
2.331 +\ \ \ \ \ \ \isasymlbrakk \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand\isanewline
2.332 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline
2.333 +\ \ \ \ \ \ \ f\ \isasymin \ F\isasymrbrakk \isanewline
2.334 +\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G)
2.335 +\end{isabelle}
2.336 +%
2.337 +To prove this, we assume \isa{Apply\ f\ args\ \isasymin \
2.338 +gterms\ G}. Rule inversion, in the form of \isa{gterm_Apply_elim}, infers
2.339 +that every element of \isa{args} belongs to
2.340 +\isa{gterms~G}; hence (by the induction hypothesis) it belongs
2.341 +to \isa{gterms\ (F\ \isasyminter \ G)}. Rule inversion also yields
2.342 +\isa{f\ \isasymin\ G} and hence \isa{f\ \isasymin \ F\ \isasyminter \ G}.
2.343 +All of this reasoning is done by \isa{blast}.
2.344 +
2.345 +\smallskip
2.346 +Our distributive law is a trivial consequence of previously-proved results:
2.347 +\begin{isabelle}
2.348 +\isacommand{theorem}\ gterms_Int_eq\ [simp]:\isanewline
2.349 +\ \ \ \ \ "gterms\ (F\isasyminter G)\ =\ gterms\ F\ \isasyminter \ gterms\ G"\isanewline
2.350 +\isacommand{by}\ (blast\ intro!:\ mono_Int\ monoI\ gterms_mono)
2.351 +\end{isabelle}
2.352 +The \isa{intro!}\ attribute of \isa{gterms_IntI} makes it available for
2.353 +this proof.
2.354
2.355
2.356 \begin{exercise}
3.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Wed Feb 21 12:07:00 2001 +0100
3.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Wed Feb 21 12:57:55 2001 +0100
3.3 @@ -1,221 +1,218 @@
3.4 %
3.5 -\begin{isabellebody}%
3.6 -\def\isabellecontext{Advanced}%
3.7 +\begin{isabelle}
3.8 +\def\isabellecontext{Advanced}
3.9 \isanewline
3.10 -\isacommand{theory}\ Advanced\ {\isacharequal}\ Even{\isacharcolon}\isanewline
3.11 +\isacommand{theory}\ Advanced\ =\ Even:\isanewline
3.12 \isanewline
3.13 \isanewline
3.14 -\isacommand{datatype}\ {\isacharprime}f\ gterm\ {\isacharequal}\ Apply\ {\isacharprime}f\ {\isachardoublequote}{\isacharprime}f\ gterm\ list{\isachardoublequote}\isanewline
3.15 +\isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list"\isanewline
3.16 \isanewline
3.17 -\isacommand{datatype}\ integer{\isacharunderscore}op\ {\isacharequal}\ Number\ int\ {\isacharbar}\ UnaryMinus\ {\isacharbar}\ Plus\isanewline
3.18 +\isacommand{datatype}\ integer_op\ =\ Number\ int\ |\ UnaryMinus\ |\ Plus\isanewline
3.19 \isanewline
3.20 -\isacommand{consts}\ gterms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
3.21 -\isacommand{inductive}\ {\isachardoublequote}gterms\ F{\isachardoublequote}\isanewline
3.22 +\isacommand{consts}\ gterms\ ::\ "'f\ set\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
3.23 +\isacommand{inductive}\ "gterms\ F"\isanewline
3.24 \isakeyword{intros}\isanewline
3.25 -step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
3.26 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ gterms\ F{\isachardoublequote}\isanewline
3.27 +step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ gterms\ F;\ \ f\ \isasymin \ F\isasymrbrakk \isanewline
3.28 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ gterms\ F"\isanewline
3.29 \isanewline
3.30 -\isacommand{lemma}\ gterms{\isacharunderscore}mono{\isacharcolon}\ {\isachardoublequote}F{\isasymsubseteq}G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G{\isachardoublequote}\isanewline
3.31 +\isacommand{lemma}\ gterms_mono:\ "F\isasymsubseteq G\ \isasymLongrightarrow \ gterms\ F\ \isasymsubseteq \ gterms\ G"\isanewline
3.32 \isacommand{apply}\ clarify\isanewline
3.33 -\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}%
3.34 -\begin{isamarkuptxt}%
3.35 -\begin{isabelle}%
3.36 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
3.37 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ t\ {\isasymin}\ gterms\ G{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
3.38 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G%
3.39 -\end{isabelle}%
3.40 -\end{isamarkuptxt}%
3.41 +\isacommand{apply}\ (erule\ gterms.induct)
3.42 +\begin{isamarkuptxt}
3.43 +\begin{isabelle}
3.44 +\ 1.\ \isasymAnd x\ args\ f.\isanewline
3.45 +\isaindent{\ 1.\ \ \ \ }\isasymlbrakk F\ \isasymsubseteq \ G;\ \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand \ t\ \isasymin \ gterms\ G;\ f\ \isasymin \ F\isasymrbrakk \isanewline
3.46 +\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G%
3.47 +\end{isabelle}
3.48 +\end{isamarkuptxt}
3.49 \isacommand{apply}\ blast\isanewline
3.50 -\isacommand{done}%
3.51 -\begin{isamarkuptext}%
3.52 -\begin{isabelle}%
3.53 -\ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
3.54 +\isacommand{done}
3.55 +\begin{isamarkuptext}
3.56 +\begin{isabelle}
3.57 +\ \ \ \ \ \isasymlbrakk a\ \isasymin \ even;\ a\ =\ 0\ \isasymLongrightarrow \ P;\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc\ (Suc\ n);\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
3.58 +\rulename{even.cases}
3.59 \end{isabelle}
3.60 -\rulename{even.cases}
3.61
3.62 Just as a demo I include
3.63 the two forms that Markus has made available. First the one for binding the
3.64 result to a name%
3.65 -\end{isamarkuptext}%
3.66 -\isacommand{inductive{\isacharunderscore}cases}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline
3.67 -\ \ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}\isanewline
3.68 +\end{isamarkuptext}
3.69 +\isacommand{inductive_cases}\ Suc_Suc_cases\ [elim!]:\isanewline
3.70 +\ \ "Suc(Suc\ n)\ \isasymin \ even"\isanewline
3.71 \isanewline
3.72 -\isacommand{thm}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases%
3.73 -\begin{isamarkuptext}%
3.74 -\begin{isabelle}%
3.75 -\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
3.76 +\isacommand{thm}\ Suc_Suc_cases%
3.77 +\begin{isamarkuptext}
3.78 +\begin{isabelle}
3.79 +\ \ \ \ \ \isasymlbrakk Suc\ (Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\ \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
3.80 +\rulename{Suc_Suc_cases}
3.81 \end{isabelle}
3.82 -\rulename{Suc_Suc_cases}
3.83
3.84 and now the one for local usage:%
3.85 -\end{isamarkuptext}%
3.86 -\isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
3.87 -\isacommand{apply}\ {\isacharparenleft}ind{\isacharunderscore}cases\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}{\isacharparenright}\isanewline
3.88 +\end{isamarkuptext}
3.89 +\isacommand{lemma}\ "Suc(Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ P\ n"\isanewline
3.90 +\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")\isanewline
3.91 \isacommand{oops}\isanewline
3.92 \isanewline
3.93 -\isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}%
3.94 -\begin{isamarkuptext}%
3.95 +\isacommand{inductive_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\ \isasymin \ gterms\ F"
3.96 +\begin{isamarkuptext}
3.97 this is what we get:
3.98
3.99 -\begin{isabelle}%
3.100 -\ \ \ \ \ {\isasymlbrakk}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
3.101 +\begin{isabelle}
3.102 +\ \ \ \ \ \isasymlbrakk Apply\ f\ args\ \isasymin \ gterms\ F;\ \isasymlbrakk \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F;\ f\ \isasymin \ F\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
3.103 +\rulename{gterm_Apply_elim}
3.104 \end{isabelle}
3.105 -\rulename{gterm_Apply_elim}%
3.106 -\end{isamarkuptext}%
3.107 -\isacommand{lemma}\ gterms{\isacharunderscore}IntI\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
3.108 -\ \ \ \ \ {\isachardoublequote}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequote}\isanewline
3.109 -\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}%
3.110 -\begin{isamarkuptxt}%
3.111 -\begin{isabelle}%
3.112 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline
3.113 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
3.114 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
3.115 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
3.116 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline
3.117 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}%
3.118 -\end{isabelle}%
3.119 -\end{isamarkuptxt}%
3.120 +\end{isamarkuptext}
3.121 +\isacommand{lemma}\ gterms_IntI\ [rule_format,\ intro!]:\isanewline
3.122 +\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter G)"\isanewline
3.123 +\isacommand{apply}\ (erule\ gterms.induct)
3.124 +\begin{isamarkuptxt}
3.125 +\begin{isabelle}
3.126 +\ 1.\ \isasymAnd args\ f.\isanewline
3.127 +\isaindent{\ 1.\ \ \ \ }\isasymlbrakk \isasymforall t\isasymin set\ args.\isanewline
3.128 +\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ gterms\ F\ \isasymand \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline
3.129 +\isaindent{\ 1.\ \ \ \ \ \ \ }f\ \isasymin \ F\isasymrbrakk \isanewline
3.130 +\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \isanewline
3.131 +\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G)
3.132 +\end{isabelle}
3.133 +\end{isamarkuptxt}
3.134 \isacommand{apply}\ blast\isanewline
3.135 -\isacommand{done}%
3.136 -\begin{isamarkuptext}%
3.137 -\begin{isabelle}%
3.138 -\ \ \ \ \ mono\ f\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymsubseteq}\ f\ A\ {\isasyminter}\ f\ B%
3.139 +\isacommand{done}
3.140 +\begin{isamarkuptext}
3.141 +\begin{isabelle}
3.142 +\ \ \ \ \ mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \ f\ A\ \isasyminter \ f\ B%
3.143 +\rulename{mono_Int}
3.144 \end{isabelle}
3.145 -\rulename{mono_Int}%
3.146 -\end{isamarkuptext}%
3.147 -\isacommand{lemma}\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
3.148 -\ \ \ \ \ {\isachardoublequote}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequote}\isanewline
3.149 -\isacommand{apply}\ {\isacharparenleft}rule\ equalityI{\isacharparenright}\isanewline
3.150 -\isacommand{apply}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isanewline
3.151 -\isacommand{apply}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ gterms{\isacharunderscore}IntI{\isacharparenright}\isanewline
3.152 -\isacommand{done}\isanewline
3.153 +\end{isamarkuptext}
3.154 +\isacommand{lemma}\ gterms_Int_eq\ [simp]:\isanewline
3.155 +\ \ \ \ \ "gterms\ (F\isasyminter G)\ =\ gterms\ F\ \isasyminter \ gterms\ G"\isanewline
3.156 +\isacommand{by}\ (blast\ intro!:\ mono_Int\ monoI\ gterms_mono)\isanewline
3.157 \isanewline
3.158 \isanewline
3.159 -\isacommand{consts}\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
3.160 +\isacommand{consts}\ integer_arity\ ::\ "integer_op\ \isasymRightarrow \ nat"\isanewline
3.161 \isacommand{primrec}\isanewline
3.162 -{\isachardoublequote}integer{\isacharunderscore}arity\ {\isacharparenleft}Number\ n{\isacharparenright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharhash}{\isadigit{0}}{\isachardoublequote}\isanewline
3.163 -{\isachardoublequote}integer{\isacharunderscore}arity\ UnaryMinus\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}\isanewline
3.164 -{\isachardoublequote}integer{\isacharunderscore}arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharhash}{\isadigit{2}}{\isachardoublequote}\isanewline
3.165 +"integer_arity\ (Number\ n)\ \ \ \ \ \ \ \ =\ \#0"\isanewline
3.166 +"integer_arity\ UnaryMinus\ \ \ \ \ \ \ \ =\ \#1"\isanewline
3.167 +"integer_arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ =\ \#2"\isanewline
3.168 \isanewline
3.169 -\isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
3.170 -\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
3.171 +\isacommand{consts}\ well_formed_gterm\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
3.172 +\isacommand{inductive}\ "well_formed_gterm\ arity"\isanewline
3.173 \isakeyword{intros}\isanewline
3.174 -step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharsemicolon}\ \ \isanewline
3.175 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
3.176 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
3.177 +step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ well_formed_gterm\ arity;\ \ \isanewline
3.178 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
3.179 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm\ arity"\isanewline
3.180 \isanewline
3.181 \isanewline
3.182 -\isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
3.183 -\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
3.184 +\isacommand{consts}\ well_formed_gterm'\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
3.185 +\isacommand{inductive}\ "well_formed_gterm'\ arity"\isanewline
3.186 \isakeyword{intros}\isanewline
3.187 -step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}{\isacharsemicolon}\ \ \isanewline
3.188 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
3.189 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
3.190 -\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline
3.191 +step[intro!]:\ "\isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity);\ \ \isanewline
3.192 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
3.193 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm'\ arity"\isanewline
3.194 +\isakeyword{monos}\ lists_mono\isanewline
3.195 \isanewline
3.196 -\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
3.197 +\isacommand{lemma}\ "well_formed_gterm\ arity\ \isasymsubseteq \ well_formed_gterm'\ arity"\isanewline
3.198 \isacommand{apply}\ clarify%
3.199 -\begin{isamarkuptxt}%
3.200 +\begin{isamarkuptxt}
3.201 The situation after clarify
3.202 -\begin{isabelle}%
3.203 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymLongrightarrow}\isanewline
3.204 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
3.205 -\end{isabelle}%
3.206 -\end{isamarkuptxt}%
3.207 -\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}%
3.208 -\begin{isamarkuptxt}%
3.209 +\begin{isabelle}
3.210 +\ 1.\ \isasymAnd x.\ x\ \isasymin \ well_formed_gterm\ arity\ \isasymLongrightarrow \isanewline
3.211 +\isaindent{\ 1.\ \isasymAnd x.\ }x\ \isasymin \ well_formed_gterm'\ arity%
3.212 +\end{isabelle}
3.213 +\end{isamarkuptxt}
3.214 +\isacommand{apply}\ (erule\ well_formed_gterm.induct)
3.215 +\begin{isamarkuptxt}
3.216 note the induction hypothesis!
3.217 -\begin{isabelle}%
3.218 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
3.219 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
3.220 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\isanewline
3.221 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
3.222 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
3.223 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
3.224 -\end{isabelle}%
3.225 -\end{isamarkuptxt}%
3.226 +\begin{isabelle}
3.227 +\ 1.\ \isasymAnd x\ args\ f.\isanewline
3.228 +\isaindent{\ 1.\ \ \ \ }\isasymlbrakk \isasymforall t\isasymin set\ args.\isanewline
3.229 +\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ well_formed_gterm\ arity\ \isasymand \isanewline
3.230 +\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ well_formed_gterm'\ arity;\isanewline
3.231 +\isaindent{\ 1.\ \ \ \ \ \ \ }length\ args\ =\ arity\ f\isasymrbrakk \isanewline
3.232 +\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm'\ arity%
3.233 +\end{isabelle}
3.234 +\end{isamarkuptxt}
3.235 \isacommand{apply}\ auto\isanewline
3.236 \isacommand{done}\isanewline
3.237 \isanewline
3.238 \isanewline
3.239 \isanewline
3.240 -\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
3.241 +\isacommand{lemma}\ "well_formed_gterm'\ arity\ \isasymsubseteq \ well_formed_gterm\ arity"\isanewline
3.242 \isacommand{apply}\ clarify%
3.243 -\begin{isamarkuptxt}%
3.244 +\begin{isamarkuptxt}
3.245 The situation after clarify
3.246 -\begin{isabelle}%
3.247 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymLongrightarrow}\isanewline
3.248 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
3.249 -\end{isabelle}%
3.250 -\end{isamarkuptxt}%
3.251 -\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}%
3.252 -\begin{isamarkuptxt}%
3.253 +\begin{isabelle}
3.254 +\ 1.\ \isasymAnd x.\ x\ \isasymin \ well_formed_gterm'\ arity\ \isasymLongrightarrow \isanewline
3.255 +\isaindent{\ 1.\ \isasymAnd x.\ }x\ \isasymin \ well_formed_gterm\ arity%
3.256 +\end{isabelle}
3.257 +\end{isamarkuptxt}
3.258 +\isacommand{apply}\ (erule\ well_formed_gterm'.induct)
3.259 +\begin{isamarkuptxt}
3.260 note the induction hypothesis!
3.261 -\begin{isabelle}%
3.262 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
3.263 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline
3.264 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline
3.265 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline
3.266 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline
3.267 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
3.268 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
3.269 -\end{isabelle}%
3.270 -\end{isamarkuptxt}%
3.271 +\begin{isabelle}
3.272 +\ 1.\ \isasymAnd x\ args\ f.\isanewline
3.273 +\isaindent{\ 1.\ \ \ \ }\isasymlbrakk args\isanewline
3.274 +\isaindent{\ 1.\ \ \ \ \isasymlbrakk }\isasymin \ lists\isanewline
3.275 +\isaindent{\ 1.\ \ \ \ \isasymlbrakk \isasymin \ \ }(well_formed_gterm'\ arity\ \isasyminter \isanewline
3.276 +\isaindent{\ 1.\ \ \ \ \isasymlbrakk \isasymin \ \ (}\isacharbraceleft x.\ x\ \isasymin \ well_formed_gterm\ arity\isacharbraceright );\isanewline
3.277 +\isaindent{\ 1.\ \ \ \ \ \ \ }length\ args\ =\ arity\ f\isasymrbrakk \isanewline
3.278 +\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm\ arity%
3.279 +\end{isabelle}
3.280 +\end{isamarkuptxt}
3.281 \isacommand{apply}\ auto\isanewline
3.282 -\isacommand{done}%
3.283 -\begin{isamarkuptext}%
3.284 -\begin{isabelle}%
3.285 -\ \ \ \ \ lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B%
3.286 -\end{isabelle}%
3.287 -\end{isamarkuptext}%
3.288 +\isacommand{done}
3.289 +\begin{isamarkuptext}
3.290 +\begin{isabelle}
3.291 +\ \ \ \ \ lists\ (A\ \isasyminter \ B)\ =\ lists\ A\ \isasyminter \ lists\ B%
3.292 +\end{isabelle}
3.293 +\end{isamarkuptext}
3.294 %
3.295 -\begin{isamarkuptext}%
3.296 +\begin{isamarkuptext}
3.297 the rest isn't used: too complicated. OK for an exercise though.%
3.298 -\end{isamarkuptext}%
3.299 -\isacommand{consts}\ integer{\isacharunderscore}signature\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}integer{\isacharunderscore}op\ {\isacharasterisk}\ {\isacharparenleft}unit\ list\ {\isacharasterisk}\ unit{\isacharparenright}{\isacharparenright}\ set{\isachardoublequote}\isanewline
3.300 -\isacommand{inductive}\ {\isachardoublequote}integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
3.301 +\end{isamarkuptext}
3.302 +\isacommand{consts}\ integer_signature\ ::\ "(integer_op\ *\ (unit\ list\ *\ unit))\ set"\isanewline
3.303 +\isacommand{inductive}\ "integer_signature"\isanewline
3.304 \isakeyword{intros}\isanewline
3.305 -Number{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isacharparenleft}Number\ n{\isacharcomma}\ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
3.306 -UnaryMinus{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}UnaryMinus{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
3.307 -Plus{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}Plus{\isacharcomma}\ \ \ \ \ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharcomma}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
3.308 +Number:\ \ \ \ \ "(Number\ n,\ \ \ ([],\ ()))\ \isasymin \ integer_signature"\isanewline
3.309 +UnaryMinus:\ "(UnaryMinus,\ ([()],\ ()))\ \isasymin \ integer_signature"\isanewline
3.310 +Plus:\ \ \ \ \ \ \ "(Plus,\ \ \ \ \ \ \ ([(),()],\ ()))\ \isasymin \ integer_signature"\isanewline
3.311 \isanewline
3.312 \isanewline
3.313 -\isacommand{consts}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequote}\isanewline
3.314 -\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
3.315 +\isacommand{consts}\ well_typed_gterm\ ::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline
3.316 +\isacommand{inductive}\ "well_typed_gterm\ sig"\isanewline
3.317 \isakeyword{intros}\isanewline
3.318 -step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline
3.319 -\ \ \ \ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}pair\ {\isasymin}\ set\ args{\isachardot}\ pair\ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isacharsemicolon}\ \isanewline
3.320 -\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline
3.321 -\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline
3.322 -\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
3.323 +step[intro!]:\ \isanewline
3.324 +\ \ \ \ "\isasymlbrakk \isasymforall pair\ \isasymin \ set\ args.\ pair\ \isasymin \ well_typed_gterm\ sig;\ \isanewline
3.325 +\ \ \ \ \ \ sig\ f\ =\ (map\ snd\ args,\ rtype)\isasymrbrakk \isanewline
3.326 +\ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ (map\ fst\ args),\ rtype)\ \isanewline
3.327 +\ \ \ \ \ \ \ \ \ \isasymin \ well_typed_gterm\ sig"\isanewline
3.328 \isanewline
3.329 -\isacommand{consts}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequote}\isanewline
3.330 -\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
3.331 +\isacommand{consts}\ well_typed_gterm'\ ::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline
3.332 +\isacommand{inductive}\ "well_typed_gterm'\ sig"\isanewline
3.333 \isakeyword{intros}\isanewline
3.334 -step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline
3.335 -\ \ \ \ {\isachardoublequote}{\isasymlbrakk}args\ {\isasymin}\ lists{\isacharparenleft}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isacharparenright}{\isacharsemicolon}\ \isanewline
3.336 -\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline
3.337 -\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline
3.338 -\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
3.339 -\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline
3.340 +step[intro!]:\ \isanewline
3.341 +\ \ \ \ "\isasymlbrakk args\ \isasymin \ lists(well_typed_gterm'\ sig);\ \isanewline
3.342 +\ \ \ \ \ \ sig\ f\ =\ (map\ snd\ args,\ rtype)\isasymrbrakk \isanewline
3.343 +\ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ (map\ fst\ args),\ rtype)\ \isanewline
3.344 +\ \ \ \ \ \ \ \ \ \isasymin \ well_typed_gterm'\ sig"\isanewline
3.345 +\isakeyword{monos}\ lists_mono\isanewline
3.346 \isanewline
3.347 \isanewline
3.348 -\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
3.349 +\isacommand{lemma}\ "well_typed_gterm\ sig\ \isasymsubseteq \ well_typed_gterm'\ sig"\isanewline
3.350 \isacommand{apply}\ clarify\isanewline
3.351 -\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isanewline
3.352 +\isacommand{apply}\ (erule\ well_typed_gterm.induct)\isanewline
3.353 \isacommand{apply}\ auto\isanewline
3.354 \isacommand{done}\isanewline
3.355 \isanewline
3.356 -\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
3.357 +\isacommand{lemma}\ "well_typed_gterm'\ sig\ \isasymsubseteq \ well_typed_gterm\ sig"\isanewline
3.358 \isacommand{apply}\ clarify\isanewline
3.359 -\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isanewline
3.360 +\isacommand{apply}\ (erule\ well_typed_gterm'.induct)\isanewline
3.361 \isacommand{apply}\ auto\isanewline
3.362 \isacommand{done}\isanewline
3.363 \isanewline
3.364 \isanewline
3.365 \isacommand{end}\isanewline
3.366 \isanewline
3.367 -\end{isabellebody}%
3.368 +\end{isabelle}
3.369 %%% Local Variables:
3.370 %%% mode: latex
3.371 %%% TeX-master: "root"
4.1 --- a/doc-src/TutorialI/Inductive/even-example.tex Wed Feb 21 12:07:00 2001 +0100
4.2 +++ b/doc-src/TutorialI/Inductive/even-example.tex Wed Feb 21 12:57:55 2001 +0100
4.3 @@ -24,12 +24,11 @@
4.4
4.5 An inductive definition consists of introduction rules. The first one
4.6 above states that 0 is even; the second states that if $n$ is even, then so
4.7 -is
4.8 -$n+2$. Given this declaration, Isabelle generates a fixed point definition
4.9 -for \isa{even} and proves theorems about it. These theorems include the
4.10 -introduction rules specified in the declaration, an elimination rule for case
4.11 -analysis and an induction rule. We can refer to these theorems by
4.12 -automatically-generated names. Here are two examples:
4.13 +is~$n+2$. Given this declaration, Isabelle generates a fixed point
4.14 +definition for \isa{even} and proves theorems about it. These theorems
4.15 +include the introduction rules specified in the declaration, an elimination
4.16 +rule for case analysis and an induction rule. We can refer to these
4.17 +theorems by automatically-generated names. Here are two examples:
4.18 %
4.19 \begin{isabelle}
4.20 0\ \isasymin \ even
4.21 @@ -217,5 +216,92 @@
4.22 \isacommand{by}\ (blast\ dest:\ Suc_Suc_even_imp_even)
4.23 \end{isabelle}
4.24
4.25 -The even numbers example has shown how inductive definitions can be used.
4.26 -Later examples will show that they are actually worth using.
4.27 +
4.28 +\subsection{Rule Inversion}\label{sec:rule-inversion}
4.29 +
4.30 +Case analysis on an inductive definition is called \textbf{rule inversion}.
4.31 +It is frequently used in proofs about operational semantics. It can be
4.32 +highly effective when it is applied automatically. Let us look at how rule
4.33 +inversion is done in Isabelle/HOL\@.
4.34 +
4.35 +Recall that \isa{even} is the minimal set closed under these two rules:
4.36 +\begin{isabelle}
4.37 +0\ \isasymin \ even\isanewline
4.38 +n\ \isasymin \ even\ \isasymLongrightarrow \ Suc\ (Suc\ n)\ \isasymin
4.39 +\ even
4.40 +\end{isabelle}
4.41 +Minimality means that \isa{even} contains only the elements that these
4.42 +rules force it to contain. If we are told that \isa{a}
4.43 +belongs to
4.44 +\isa{even} then there are only two possibilities. Either \isa{a} is \isa{0}
4.45 +or else \isa{a} has the form \isa{Suc(Suc~n)}, for some suitable \isa{n}
4.46 +that belongs to
4.47 +\isa{even}. That is the gist of the \isa{cases} rule, which Isabelle proves
4.48 +for us when it accepts an inductive definition:
4.49 +\begin{isabelle}
4.50 +\isasymlbrakk a\ \isasymin \ even;\isanewline
4.51 +\ a\ =\ 0\ \isasymLongrightarrow \ P;\isanewline
4.52 +\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc(Suc\ n);\ n\ \isasymin \
4.53 +even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \
4.54 +\isasymLongrightarrow \ P
4.55 +\rulename{even.cases}
4.56 +\end{isabelle}
4.57 +
4.58 +This general rule is less useful than instances of it for
4.59 +specific patterns. For example, if \isa{a} has the form
4.60 +\isa{Suc(Suc~n)} then the first case becomes irrelevant, while the second
4.61 +case tells us that \isa{n} belongs to \isa{even}. Isabelle will generate
4.62 +this instance for us:
4.63 +\begin{isabelle}
4.64 +\isacommand{inductive\_cases}\ Suc_Suc_cases\ [elim!]:
4.65 +\ "Suc(Suc\ n)\ \isasymin \ even"
4.66 +\end{isabelle}
4.67 +The \isacommand{inductive\_cases} command generates an instance of the
4.68 +\isa{cases} rule for the supplied pattern and gives it the supplied name:
4.69 +%
4.70 +\begin{isabelle}
4.71 +\isasymlbrakk Suc(Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\
4.72 +\isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
4.73 +\rulename{Suc_Suc_cases}
4.74 +\end{isabelle}
4.75 +%
4.76 +Applying this as an elimination rule yields one case where \isa{even.cases}
4.77 +would yield two. Rule inversion works well when the conclusions of the
4.78 +introduction rules involve datatype constructors like \isa{Suc} and \isa{\#}
4.79 +(list ``cons''); freeness reasoning discards all but one or two cases.
4.80 +
4.81 +In the \isacommand{inductive\_cases} command we supplied an
4.82 +attribute, \isa{elim!}, indicating that this elimination rule can be applied
4.83 +aggressively. The original
4.84 +\isa{cases} rule would loop if used in that manner because the
4.85 +pattern~\isa{a} matches everything.
4.86 +
4.87 +The rule \isa{Suc_Suc_cases} is equivalent to the following implication:
4.88 +\begin{isabelle}
4.89 +Suc (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \
4.90 +even
4.91 +\end{isabelle}
4.92 +%
4.93 +Just above we devoted some effort to reaching precisely
4.94 +this result. Yet we could have obtained it by a one-line declaration,
4.95 +dispensing with the lemma \isa{even_imp_even_minus_2}.
4.96 +This example also justifies the terminology
4.97 +\textbf{rule inversion}: the new rule inverts the introduction rule
4.98 +\isa{even.step}.
4.99 +
4.100 +For one-off applications of rule inversion, use the \isa{ind_cases} method.
4.101 +Here is an example:
4.102 +\begin{isabelle}
4.103 +\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")
4.104 +\end{isabelle}
4.105 +The specified instance of the \isa{cases} rule is generated, then applied
4.106 +as an elimination rule.
4.107 +
4.108 +To summarize, every inductive definition produces a \isa{cases} rule. The
4.109 +\isacommand{inductive\_cases} command stores an instance of the \isa{cases}
4.110 +rule for a given pattern. Within a proof, the \isa{ind_cases} method
4.111 +applies an instance of the \isa{cases}
4.112 +rule.
4.113 +
4.114 +The even numbers example has shown how inductive definitions can be
4.115 +used. Later examples will show that they are actually worth using.