author paulson Fri, 16 Feb 2001 18:50:09 +0100 changeset 11155 603df40ef1e9 parent 11154 042015819774 child 11156 1d1d9f60c29b
Least_def now refers to LeastM
--- a/doc-src/TutorialI/Rules/rules.tex	Fri Feb 16 13:47:06 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Feb 16 18:50:09 2001 +0100
@@ -1085,17 +1085,16 @@
A more challenging example illustrates how Isabelle/HOL defines the least-number
operator, which denotes the least \isa{x} satisfying~\isa{P}:
\begin{isabelle}
-(LEAST\ x.\ P\ x)\ \isasymequiv \ SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
+(LEAST\ x.\ P\ x)\ = \ SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)
-\rulename{Least_def}
\end{isabelle}

Let us prove the counterpart of \isa{some_equality} for this operator.
-The first step merely unfolds the definition:
+The first step merely unfolds the definitions:
\begin{isabelle}
\isacommand{theorem}\ Least_equality:\isanewline
\ \ \ \ \ "\isasymlbrakk \ P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\ \isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline
%\ \ \ \ \isasymLongrightarrow \ (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))\ =\ k%