--- a/doc-src/TutorialI/Sets/sets.tex Fri Jul 13 17:55:35 2001 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex Fri Jul 13 17:56:05 2001 +0200
@@ -43,11 +43,11 @@
\begin{isabelle}
\isasymlbrakk c\ \isasymin\ A;\ c\ \isasymin\ B\isasymrbrakk\
\isasymLongrightarrow\ c\ \isasymin\ A\ \isasyminter\ B%
-\rulename{IntI}\isanewline
+\rulenamedx{IntI}\isanewline
c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ A
-\rulename{IntD1}\isanewline
+\rulenamedx{IntD1}\isanewline
c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ B
-\rulename{IntD2}
+\rulenamedx{IntD2}
\end{isabelle}
Here are two of the many installed theorems concerning set
@@ -55,7 +55,7 @@
Note that it is denoted by a minus sign.
\begin{isabelle}
(c\ \isasymin\ -\ A)\ =\ (c\ \isasymnotin\ A)
-\rulename{Compl_iff}\isanewline
+\rulenamedx{Compl_iff}\isanewline
-\ (A\ \isasymunion\ B)\ =\ -\ A\ \isasyminter\ -\ B
\rulename{Compl_Un}
\end{isabelle}
@@ -75,12 +75,12 @@
are its natural deduction rules:
\begin{isabelle}
({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ x\ \isasymin\ B)\ \isasymLongrightarrow\ A\ \isasymsubseteq\ B%
-\rulename{subsetI}%
+\rulenamedx{subsetI}%
\par\smallskip% \isanewline didn't leave enough space
\isasymlbrakk A\ \isasymsubseteq\ B;\ c\ \isasymin\
A\isasymrbrakk\ \isasymLongrightarrow\ c\
\isasymin\ B%
-\rulename{subsetD}
+\rulenamedx{subsetD}
\end{isabelle}
In harder proofs, you may need to apply \isa{subsetD} giving a specific term
for~\isa{c}. However, \isa{blast} can instantly prove facts such as this
@@ -88,7 +88,7 @@
\begin{isabelle}
(A\ \isasymunion\ B\ \isasymsubseteq\ C)\ =\
(A\ \isasymsubseteq\ C\ \isasymand\ B\ \isasymsubseteq\ C)
-\rulename{Un_subset_iff}
+\rulenamedx{Un_subset_iff}
\end{isabelle}
Here is another example, also proved automatically:
\begin{isabelle}
@@ -125,7 +125,7 @@
\begin{isabelle}
({\isasymAnd}x.\ (x\ {\isasymin}\ A)\ =\ (x\ {\isasymin}\ B))\
{\isasymLongrightarrow}\ A\ =\ B
-\rulename{set_ext}
+\rulenamedx{set_ext}
\end{isabelle}
Extensionality can be expressed as
$A=B\iff (A\subseteq B)\conj (B\subseteq A)$.
@@ -135,12 +135,12 @@
\begin{isabelle}
\isasymlbrakk A\ \isasymsubseteq\ B;\ B\ \isasymsubseteq\
A\isasymrbrakk\ \isasymLongrightarrow\ A\ =\ B
-\rulename{equalityI}
+\rulenamedx{equalityI}
\par\smallskip% \isanewline didn't leave enough space
\isasymlbrakk A\ =\ B;\ \isasymlbrakk A\ \isasymsubseteq\ B;\ B\
\isasymsubseteq\ A\isasymrbrakk\ \isasymLongrightarrow\ P\isasymrbrakk\
\isasymLongrightarrow\ P%
-\rulename{equalityE}
+\rulenamedx{equalityE}
\end{isabelle}
@@ -264,13 +264,13 @@
\begin{isabelle}
({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ P\ x)\ \isasymLongrightarrow\ {\isasymforall}x\isasymin
A.\ P\ x%
-\rulename{ballI}%
+\rulenamedx{ballI}%
\isanewline
\isasymlbrakk{\isasymforall}x\isasymin A.\
P\ x;\ x\ \isasymin\
A\isasymrbrakk\ \isasymLongrightarrow\ P\
x%
-\rulename{bspec}
+\rulenamedx{bspec}
\end{isabelle}
%
Dually, here are the natural deduction rules for the
@@ -282,14 +282,14 @@
\isasymLongrightarrow\
\isasymexists x\isasymin A.\ P\
x%
-\rulename{bexI}%
+\rulenamedx{bexI}%
\isanewline
\isasymlbrakk\isasymexists x\isasymin A.\
P\ x;\ {\isasymAnd}x.\
{\isasymlbrakk}x\ \isasymin\ A;\
P\ x\isasymrbrakk\ \isasymLongrightarrow\
Q\isasymrbrakk\ \isasymLongrightarrow\ Q%
-\rulename{bexE}
+\rulenamedx{bexE}
\end{isabelle}
\index{quantifiers!for sets|)}
@@ -301,7 +301,7 @@
(b\ \isasymin\
(\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\
b\ \isasymin\ B\ x)
-\rulename{UN_iff}
+\rulenamedx{UN_iff}
\end{isabelle}
It has two natural deduction rules similar to those for the existential
quantifier. Sometimes \isa{UN_I} must be applied explicitly:
@@ -312,7 +312,7 @@
b\ \isasymin\
({\isasymUnion}x\isasymin A.\
B\ x)
-\rulename{UN_I}%
+\rulenamedx{UN_I}%
\isanewline
\isasymlbrakk b\ \isasymin\
({\isasymUnion}x\isasymin A.\
@@ -321,7 +321,7 @@
A;\ b\ \isasymin\
B\ x\isasymrbrakk\ \isasymLongrightarrow\
R\isasymrbrakk\ \isasymLongrightarrow\ R%
-\rulename{UN_E}
+\rulenamedx{UN_E}
\end{isabelle}
%
The following built-in syntax translation (see \S\ref{sec:def-translations})
@@ -341,7 +341,7 @@
\begin{isabelle}
(A\ \isasymin\ \isasymUnion C)\ =\ (\isasymexists X\isasymin C.\ A\
\isasymin\ X)
-\rulename{Union_iff}
+\rulenamedx{Union_iff}
\end{isabelle}
\index{intersection!indexed}%
@@ -356,13 +356,13 @@
=\
({\isasymforall}x\isasymin A.\
b\ \isasymin\ B\ x)
-\rulename{INT_iff}%
+\rulenamedx{INT_iff}%
\isanewline
(A\ \isasymin\
\isasymInter C)\ =\
({\isasymforall}X\isasymin C.\
A\ \isasymin\ X)
-\rulename{Inter_iff}
+\rulenamedx{Inter_iff}
\end{isabelle}
Isabelle uses logical equivalences such as those above in automatic proof.
@@ -404,12 +404,12 @@
\begin{isabelle}
{\isasymlbrakk}finite\ A;\ finite\ B\isasymrbrakk\isanewline
\isasymLongrightarrow\ card\ A\ \isacharplus\ card\ B\ =\ card\ (A\ \isasymunion\ B)\ \isacharplus\ card\ (A\ \isasyminter\ B)
-\rulename{card_Un_Int}%
+\rulenamedx{card_Un_Int}%
\isanewline
\isanewline
finite\ A\ \isasymLongrightarrow\ card\
(Pow\ A)\ =\ 2\ \isacharcircum\ card\ A%
-\rulename{card_Pow}%
+\rulenamedx{card_Pow}%
\isanewline
\isanewline
finite\ A\ \isasymLongrightarrow\isanewline
@@ -449,7 +449,7 @@
functions:
\begin{isabelle}
({\isasymAnd}x.\ f\ x\ =\ g\ x)\ {\isasymLongrightarrow}\ f\ =\ g
-\rulename{ext}
+\rulenamedx{ext}
\end{isabelle}
\indexbold{updating a function}%
@@ -478,11 +478,11 @@
defined:
\begin{isabelle}%
id\ \isasymequiv\ {\isasymlambda}x.\ x%
-\rulename{id_def}\isanewline
+\rulenamedx{id_def}\isanewline
f\ \isasymcirc\ g\ \isasymequiv\
{\isasymlambda}x.\ f\
(g\ x)%
-\rulename{o_def}
+\rulenamedx{o_def}
\end{isabelle}
%
Many familiar theorems concerning the identity and composition
@@ -500,12 +500,12 @@
inj_on\ f\ A\ \isasymequiv\ {\isasymforall}x\isasymin A.\
{\isasymforall}y\isasymin A.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\
=\ y%
-\rulename{inj_on_def}\isanewline
+\rulenamedx{inj_on_def}\isanewline
surj\ f\ \isasymequiv\ {\isasymforall}y.\
\isasymexists x.\ y\ =\ f\ x%
-\rulename{surj_def}\isanewline
+\rulenamedx{surj_def}\isanewline
bij\ f\ \isasymequiv\ inj\ f\ \isasymand\ surj\ f
-\rulename{bij_def}
+\rulenamedx{bij_def}
\end{isabelle}
The second argument
of \isa{inj_on} lets us express that a function is injective over a
@@ -588,7 +588,7 @@
\begin{isabelle}
f\ `\ A\ \isasymequiv\ \isacharbraceleft y.\ \isasymexists x\isasymin
A.\ y\ =\ f\ x\isacharbraceright
-\rulename{image_def}
+\rulenamedx{image_def}
\end{isabelle}
%
Here are some of the many facts proved about image:
@@ -637,7 +637,7 @@
It is defined as follows:
\begin{isabelle}
f\ -`\ B\ \isasymequiv\ \isacharbraceleft x.\ f\ x\ \isasymin\ B\isacharbraceright
-\rulename{vimage_def}
+\rulenamedx{vimage_def}
\end{isabelle}
%
This is one of the facts proved about it:
@@ -662,7 +662,7 @@
definition:
\begin{isabelle}
Id\ \isasymequiv\ \isacharbraceleft p.\ \isasymexists x.\ p\ =\ (x,x){\isacharbraceright}%
-\rulename{Id_def}
+\rulenamedx{Id_def}
\end{isabelle}
\indexbold{composition!of relations}%
@@ -670,7 +670,7 @@
available:
\begin{isabelle}
r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright
-\rulename{comp_def}
+\rulenamedx{comp_def}
\end{isabelle}
%
This is one of the many lemmas proved about these concepts:
@@ -698,7 +698,7 @@
\begin{isabelle}
((a,b)\ \isasymin\ r\isasyminverse)\ =\
((b,a)\ \isasymin\ r)
-\rulename{converse_iff}
+\rulenamedx{converse_iff}
\end{isabelle}
%
Here is a typical law proved about converse and composition:
@@ -713,7 +713,7 @@
\begin{isabelle}
(b\ \isasymin\ r\ ``\ A)\ =\ (\isasymexists x\isasymin
A.\ (x,b)\ \isasymin\ r)
-\rulename{Image_iff}
+\rulenamedx{Image_iff}
\end{isabelle}
It satisfies many similar laws.
@@ -724,13 +724,13 @@
\begin{isabelle}
(a\ \isasymin\ Domain\ r)\ =\ (\isasymexists y.\ (a,y)\ \isasymin\
r)
-\rulename{Domain_iff}%
+\rulenamedx{Domain_iff}%
\isanewline
(a\ \isasymin\ Range\ r)\
\ =\ (\isasymexists y.\
(y,a)\
\isasymin\ r)
-\rulename{Range_iff}
+\rulenamedx{Range_iff}
\end{isabelle}
Iterated composition of a relation is available. The notation overloads
@@ -757,13 +757,13 @@
rules:
\begin{isabelle}
(a,\ a)\ \isasymin \ r\isactrlsup *
-\rulename{rtrancl_refl}\isanewline
+\rulenamedx{rtrancl_refl}\isanewline
p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup *
-\rulename{r_into_rtrancl}\isanewline
+\rulenamedx{r_into_rtrancl}\isanewline
\isasymlbrakk (a,b)\ \isasymin \ r\isactrlsup *;\
(b,c)\ \isasymin \ r\isactrlsup *\isasymrbrakk \ \isasymLongrightarrow \
(a,c)\ \isasymin \ r\isactrlsup *
-\rulename{rtrancl_trans}
+\rulenamedx{rtrancl_trans}
\end{isabelle}
%
Induction over the reflexive transitive closure is available:
@@ -785,9 +785,9 @@
\isa{r\isacharcircum+}. It has two introduction rules:
\begin{isabelle}
p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup +
-\rulename{r_into_trancl}\isanewline
+\rulenamedx{r_into_trancl}\isanewline
\isasymlbrakk (a,\ b)\ \isasymin \ r\isactrlsup +;\ (b,\ c)\ \isasymin \ r\isactrlsup +\isasymrbrakk \ \isasymLongrightarrow \ (a,\ c)\ \isasymin \ r\isactrlsup +
-\rulename{trancl_trans}
+\rulenamedx{trancl_trans}
\end{isabelle}
%
The induction rule resembles the one shown above.
@@ -910,7 +910,7 @@
relation behaves as expected and that it is well-founded:
\begin{isabelle}
((x,y)\ \isasymin\ less_than)\ =\ (x\ <\ y)
-\rulename{less_than_iff}\isanewline
+\rulenamedx{less_than_iff}\isanewline
wf\ less_than
\rulename{wf_less_than}
\end{isabelle}
@@ -925,7 +925,7 @@
\begin{isabelle}
inv_image\ r\ f\ \isasymequiv\ \isacharbraceleft(x,y).\ (f\ x,\ f\ y)\
\isasymin\ r\isacharbraceright
-\rulename{inv_image_def}\isanewline
+\rulenamedx{inv_image_def}\isanewline
wf\ r\ \isasymLongrightarrow\ wf\ (inv_image\ r\ f)
\rulename{wf_inv_image}
\end{isabelle}
@@ -936,7 +936,7 @@
\isa{measure} as shown:
\begin{isabelle}
measure\ \isasymequiv\ inv_image\ less_than%
-\rulename{measure_def}\isanewline
+\rulenamedx{measure_def}\isanewline
wf\ (measure\ f)
\rulename{wf_measure}
\end{isabelle}
@@ -953,7 +953,7 @@
\isasymor\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \,a=a'\ \isasymand \ (b,b')\
\isasymin \ rb\isacharbraceright
-\rulename{lex_prod_def}%
+\rulenamedx{lex_prod_def}%
\par\smallskip
\isasymlbrakk wf\ ra;\ wf\ rb\isasymrbrakk \ \isasymLongrightarrow \ wf\ (ra\ <*lex*>\ rb)
\rulename{wf_lex_prod}
@@ -986,7 +986,7 @@
{\isasymAnd}x.\ {\isasymforall}y.\ (y,x)\ \isasymin\ r\
\isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\
\isasymLongrightarrow\ P\ a
-\rulename{wf_induct}
+\rulenamedx{wf_induct}
\end{isabelle}
Here \isa{wf\ r} expresses that the relation~\isa{r} is well-founded.
@@ -1021,7 +1021,7 @@
Isabelle's definition of monotone is overloaded over all orderings:
\begin{isabelle}
mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%
-\rulename{mono_def}
+\rulenamedx{mono_def}
\end{isabelle}
%
For fixed point operators, the ordering will be the subset relation: if