1.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Sep 01 18:29:52 2000 +0200
1.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Sep 01 19:09:44 2000 +0200
1.3 @@ -21,7 +21,7 @@
1.4 apply(induct_tac xs);
1.5
1.6 txt{*\noindent
1.7 -(where \isa{hd} and \isa{last} return the first and last element of a
1.8 +(where @{term"hd"} and @{term"last"} return the first and last element of a
1.9 non-empty list)
1.10 produces the warning
1.11 \begin{quote}\tt
1.12 @@ -35,16 +35,16 @@
1.13 \begin{isabelle}
1.14 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
1.15 \end{isabelle}
1.16 -We cannot prove this equality because we do not know what \isa{hd} and
1.17 -\isa{last} return when applied to \isa{[]}.
1.18 +We cannot prove this equality because we do not know what @{term"hd"} and
1.19 +@{term"last"} return when applied to @{term"[]"}.
1.20
1.21 The point is that we have violated the above warning. Because the induction
1.22 -formula is only the conclusion, the occurrence of \isa{xs} in the premises is
1.23 +formula is only the conclusion, the occurrence of @{term"xs"} in the premises is
1.24 not modified by induction. Thus the case that should have been trivial
1.25 becomes unprovable. Fortunately, the solution is easy:
1.26 \begin{quote}
1.27 \emph{Pull all occurrences of the induction variable into the conclusion
1.28 -using \isa{\isasymlongrightarrow}.}
1.29 +using @{text"\<longrightarrow>"}.}
1.30 \end{quote}
1.31 This means we should prove
1.32 *};
1.33 @@ -59,12 +59,13 @@
1.34 \begin{isabelle}
1.35 \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
1.36 \end{isabelle}
1.37 -which is trivial, and \isa{auto} finishes the whole proof.
1.38 +which is trivial, and @{text"auto"} finishes the whole proof.
1.39
1.40 -If \isa{hd\_rev} is meant to be a simplification rule, you are done. But if you
1.41 -really need the \isa{\isasymLongrightarrow}-version of \isa{hd\_rev}, for
1.42 -example because you want to apply it as an introduction rule, you need to
1.43 -derive it separately, by combining it with modus ponens:
1.44 +If @{thm[source]hd_rev} is meant to be a simplification rule, you are
1.45 +done. But if you really need the @{text"\<Longrightarrow>"}-version of
1.46 +@{thm[source]hd_rev}, for example because you want to apply it as an
1.47 +introduction rule, you need to derive it separately, by combining it with
1.48 +modus ponens:
1.49 *};
1.50
1.51 lemmas hd_revI = hd_rev[THEN mp];
1.52 @@ -78,7 +79,7 @@
1.53 (see the remark?? in \S\ref{??}).
1.54 Additionally, you may also have to universally quantify some other variables,
1.55 which can yield a fairly complex conclusion.
1.56 -Here is a simple example (which is proved by \isa{blast}):
1.57 +Here is a simple example (which is proved by @{text"blast"}):
1.58 *};
1.59
1.60 lemma simple: "\\<forall>y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y";
1.61 @@ -86,14 +87,14 @@
1.62
1.63 text{*\noindent
1.64 You can get the desired lemma by explicit
1.65 -application of modus ponens and \isa{spec}:
1.66 +application of modus ponens and @{thm[source]spec}:
1.67 *};
1.68
1.69 lemmas myrule = simple[THEN spec, THEN mp, THEN mp];
1.70
1.71 text{*\noindent
1.72 -or the wholesale stripping of \isa{\isasymforall} and
1.73 -\isa{\isasymlongrightarrow} in the conclusion via \isa{rulify}
1.74 +or the wholesale stripping of @{text"\<forall>"} and
1.75 +@{text"\<longrightarrow>"} in the conclusion via @{text"rulify"}
1.76 *};
1.77
1.78 lemmas myrule = simple[rulify];
1.79 @@ -130,10 +131,10 @@
1.80 induction schema. In such cases some existing standard induction schema can
1.81 be helpful. We show how to apply such induction schemas by an example.
1.82
1.83 -Structural induction on \isa{nat} is
1.84 +Structural induction on @{typ"nat"} is
1.85 usually known as ``mathematical induction''. There is also ``complete
1.86 induction'', where you must prove $P(n)$ under the assumption that $P(m)$
1.87 -holds for all $m<n$. In Isabelle, this is the theorem \isa{less\_induct}:
1.88 +holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]less_induct}:
1.89 \begin{quote}
1.90 @{thm[display]"less_induct"[no_vars]}
1.91 \end{quote}
1.92 @@ -148,7 +149,7 @@
1.93 discouraged, because of the danger of inconsistencies. The above axiom does
1.94 not introduce an inconsistency because, for example, the identity function
1.95 satisfies it.}
1.96 -for \isa{f} it follows that @{term"n <= f n"}, which can
1.97 +for @{term"f"} it follows that @{prop"n <= f n"}, which can
1.98 be proved by induction on @{term"f n"}. Following the recipy outlined
1.99 above, we have to phrase the proposition as follows to allow induction:
1.100 *};
1.101 @@ -156,7 +157,7 @@
1.102 lemma f_incr_lem: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
1.103
1.104 txt{*\noindent
1.105 -To perform induction on \isa{k} using \isa{less\_induct}, we use the same
1.106 +To perform induction on @{term"k"} using @{thm[source]less_induct}, we use the same
1.107 general induction method as for recursion induction (see
1.108 \S\ref{sec:recdef-induction}):
1.109 *};
1.110 @@ -173,9 +174,9 @@
1.111 \ 1.\ {\isasymAnd}\mbox{n}.\ {\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i})\isanewline
1.112 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
1.113 \end{isabelle}
1.114 -After stripping the \isa{\isasymforall i}, the proof continues with a case
1.115 -distinction on \isa{i}. The case \isa{i = 0} is trivial and we focus on the
1.116 -other case:
1.117 +After stripping the @{text"\<forall>i"}, the proof continues with a case
1.118 +distinction on @{term"i"}. The case @{prop"i = 0"} is trivial and we focus on
1.119 +the other case:
1.120 \begin{isabelle}
1.121 \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline
1.122 \ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i});\ \mbox{i}\ =\ Suc\ \mbox{nat}{\isasymrbrakk}\isanewline
1.123 @@ -187,16 +188,16 @@
1.124
1.125 text{*\noindent
1.126 It is not surprising if you find the last step puzzling.
1.127 -The proof goes like this (writing \isa{j} instead of \isa{nat}).
1.128 -Since @{term"i = Suc j"} it suffices to show
1.129 -@{term"j < f(Suc j)"} (by \isa{Suc\_leI}: @{thm"Suc_leI"[no_vars]}). This is
1.130 -proved as follows. From \isa{f\_ax} we have @{term"f (f j) < f (Suc j)"}
1.131 -(1) which implies @{term"f j <= f (f j)"} (by the induction hypothesis).
1.132 -Using (1) once more we obtain @{term"f j < f(Suc j)"} (2) by transitivity
1.133 -(\isa{le_less_trans}: @{thm"le_less_trans"[no_vars]}).
1.134 -Using the induction hypothesis once more we obtain @{term"j <= f j"}
1.135 -which, together with (2) yields @{term"j < f (Suc j)"} (again by
1.136 -\isa{le_less_trans}).
1.137 +The proof goes like this (writing @{term"j"} instead of @{typ"nat"}).
1.138 +Since @{prop"i = Suc j"} it suffices to show
1.139 +@{prop"j < f(Suc j)"} (by @{thm[source]Suc_leI}: @{thm"Suc_leI"[no_vars]}). This is
1.140 +proved as follows. From @{thm[source]f_ax} we have @{prop"f (f j) < f (Suc j)"}
1.141 +(1) which implies @{prop"f j <= f (f j)"} (by the induction hypothesis).
1.142 +Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by transitivity
1.143 +(@{thm[source]le_less_trans}: @{thm"le_less_trans"[no_vars]}).
1.144 +Using the induction hypothesis once more we obtain @{prop"j <= f j"}
1.145 +which, together with (2) yields @{prop"j < f (Suc j)"} (again by
1.146 +@{thm[source]le_less_trans}).
1.147
1.148 This last step shows both the power and the danger of automatic proofs: they
1.149 will usually not tell you how the proof goes, because it can be very hard to
1.150 @@ -204,14 +205,14 @@
1.151 \S\ref{sec:part2?} introduces a language for writing readable yet concise
1.152 proofs.
1.153
1.154 -We can now derive the desired @{term"i <= f i"} from \isa{f\_incr}:
1.155 +We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}:
1.156 *};
1.157
1.158 lemmas f_incr = f_incr_lem[rulify, OF refl];
1.159
1.160 text{*\noindent
1.161 -The final \isa{refl} gets rid of the premise \isa{?k = f ?i}. Again, we could
1.162 -have included this derivation in the original statement of the lemma:
1.163 +The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. Again,
1.164 +we could have included this derivation in the original statement of the lemma:
1.165 *};
1.166
1.167 lemma f_incr[rulify, OF refl]: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
1.168 @@ -219,22 +220,23 @@
1.169
1.170 text{*
1.171 \begin{exercise}
1.172 -From the above axiom and lemma for \isa{f} show that \isa{f} is the identity.
1.173 +From the above axiom and lemma for @{term"f"} show that @{term"f"} is the
1.174 +identity.
1.175 \end{exercise}
1.176
1.177 -In general, \isa{induct\_tac} can be applied with any rule \isa{r}
1.178 -whose conclusion is of the form \isa{?P ?x1 \dots ?xn}, in which case the
1.179 +In general, @{text"induct_tac"} can be applied with any rule $r$
1.180 +whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
1.181 format is
1.182 -\begin{ttbox}
1.183 -apply(induct_tac y1 ... yn rule: r)
1.184 -\end{ttbox}\index{*induct_tac}%
1.185 -where \isa{y1}, \dots, \isa{yn} are variables in the first subgoal.
1.186 -In fact, \isa{induct\_tac} even allows the conclusion of
1.187 -\isa{r} to be an (iterated) conjunction of formulae of the above form, in
1.188 +\begin{quote}
1.189 +\isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
1.190 +\end{quote}\index{*induct_tac}%
1.191 +where $y@1, \dots, y@n$ are variables in the first subgoal.
1.192 +In fact, @{text"induct_tac"} even allows the conclusion of
1.193 +$r$ to be an (iterated) conjunction of formulae of the above form, in
1.194 which case the application is
1.195 -\begin{ttbox}
1.196 -apply(induct_tac y1 ... yn and ... and z1 ... zm rule: r)
1.197 -\end{ttbox}
1.198 +\begin{quote}
1.199 +\isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"and"} \dots\ @{text"and"} $z@1 \dots z@m$ @{text"rule:"} $r$@{text")"}
1.200 +\end{quote}
1.201 *};
1.202
1.203 subsection{*Derivation of new induction schemas*};
1.204 @@ -242,18 +244,18 @@
1.205 text{*\label{sec:derive-ind}
1.206 Induction schemas are ordinary theorems and you can derive new ones
1.207 whenever you wish. This section shows you how to, using the example
1.208 -of \isa{less\_induct}. Assume we only have structural induction
1.209 +of @{thm[source]less_induct}. Assume we only have structural induction
1.210 available for @{typ"nat"} and want to derive complete induction. This
1.211 requires us to generalize the statement first:
1.212 *};
1.213
1.214 -lemma induct_lem: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) ==> \\<forall>m<n. P m";
1.215 +lemma induct_lem: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) \\<Longrightarrow> \\<forall>m<n. P m";
1.216 apply(induct_tac n);
1.217
1.218 txt{*\noindent
1.219 -The base case is trivially true. For the induction step (@{term"m <
1.220 -Suc n"}) we distinguish two cases: @{term"m < n"} is true by induction
1.221 -hypothesis and @{term"m = n"} follow from the assumption again using
1.222 +The base case is trivially true. For the induction step (@{prop"m <
1.223 +Suc n"}) we distinguish two cases: @{prop"m < n"} is true by induction
1.224 +hypothesis and @{prop"m = n"} follow from the assumption again using
1.225 the induction hypothesis:
1.226 *};
1.227
1.228 @@ -264,31 +266,31 @@
1.229 ML"reset quick_and_dirty"
1.230
1.231 text{*\noindent
1.232 -The elimination rule \isa{less_SucE} expresses the case distinction:
1.233 +The elimination rule @{thm[source]less_SucE} expresses the case distinction:
1.234 \begin{quote}
1.235 @{thm[display]"less_SucE"[no_vars]}
1.236 \end{quote}
1.237
1.238 Now it is straightforward to derive the original version of
1.239 -\isa{less\_induct} by manipulting the conclusion of the above lemma:
1.240 -instantiate \isa{n} by @{term"Suc n"} and \isa{m} by \isa{n} and
1.241 -remove the trivial condition @{term"n < Sc n"}. Fortunately, this
1.242 +@{thm[source]less_induct} by manipulting the conclusion of the above lemma:
1.243 +instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and
1.244 +remove the trivial condition @{prop"n < Sc n"}. Fortunately, this
1.245 happens automatically when we add the lemma as a new premise to the
1.246 desired goal:
1.247 *};
1.248
1.249 -theorem less_induct: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) ==> P n";
1.250 +theorem less_induct: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) \\<Longrightarrow> P n";
1.251 by(insert induct_lem, blast);
1.252
1.253 text{*\noindent
1.254 Finally we should mention that HOL already provides the mother of all
1.255 -inductions, \emph{wellfounded induction} (\isa{wf\_induct}):
1.256 +inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):
1.257 \begin{quote}
1.258 @{thm[display]"wf_induct"[no_vars]}
1.259 \end{quote}
1.260 -where @{term"wf r"} means that the relation \isa{r} is wellfounded.
1.261 -For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on @{typ"nat"}.
1.262 -For details see the library.
1.263 +where @{term"wf r"} means that the relation @{term"r"} is wellfounded.
1.264 +For example @{thm[source]less_induct} is the special case where @{term"r"} is
1.265 +@{text"<"} on @{typ"nat"}. For details see the library.
1.266 *};
1.267
1.268 (*<*)