author paulson Fri Jul 13 17:56:05 2001 +0200 (2001-07-13) changeset 11417 499435b4084e parent 11416 91886738773a child 11418 53a402c10ba9
less indexing of theorem names
     1.1 --- a/doc-src/TutorialI/Rules/rules.tex	Fri Jul 13 17:55:35 2001 +0200
1.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Fri Jul 13 17:56:05 2001 +0200
1.3 @@ -67,7 +67,7 @@
1.4
1.5  In Isabelle notation, the rule looks like this:
1.6  \begin{isabelle}
1.7 -\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulename{conjI}
1.8 +\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulenamedx{conjI}
1.9  \end{isabelle}
1.10  Carefully examine the syntax.  The premises appear to the
1.11  left of the arrow and the conclusion to the right.  The premises (if
1.12 @@ -159,7 +159,7 @@
1.13  notation, the already-familiar \isa{\isasymLongrightarrow} syntax serves the
1.14  same  purpose:
1.15  \begin{isabelle}
1.16 -\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE}
1.17 +\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{disjE}
1.18  \end{isabelle}
1.19  When we use this sort of elimination rule backwards, it produces
1.20  a case split.  (We have seen this before, in proofs by induction.)  The following  proof
1.21 @@ -281,7 +281,7 @@
1.22  alternative conjunction elimination rule that resembles \isa{disjE}\@.  It is
1.23  seldom, if ever, seen in logic books.  In Isabelle syntax it looks like this:
1.24  \begin{isabelle}
1.25 -\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{conjE}
1.26 +\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{conjE}
1.27  \end{isabelle}
1.28  \index{destruction rules|)}
1.29
1.30 @@ -298,13 +298,13 @@
1.31  in Isabelle:
1.32  \begin{isabelle}
1.33  (?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\
1.34 -\isasymlongrightarrow\ ?Q\rulename{impI}
1.35 +\isasymlongrightarrow\ ?Q\rulenamedx{impI}
1.36  \end{isabelle}
1.37  And this is \emph{modus ponens}\index{modus ponens@\emph{modus ponens}} :
1.38  \begin{isabelle}
1.39  \isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\
1.40  \isasymLongrightarrow\ ?Q
1.41 -\rulename{mp}
1.42 +\rulenamedx{mp}
1.43  \end{isabelle}
1.44
1.45  Here is a proof using the implication rules.  This
1.46 @@ -413,16 +413,16 @@
1.47  presence of $\neg P$ together with~$P$:
1.48  \begin{isabelle}
1.49  (?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P%
1.50 -\rulename{notI}\isanewline
1.51 +\rulenamedx{notI}\isanewline
1.52  \isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R%
1.53 -\rulename{notE}
1.54 +\rulenamedx{notE}
1.55  \end{isabelle}
1.56  %
1.57  Classical logic allows us to assume $\neg P$
1.58  when attempting to prove~$P$:
1.59  \begin{isabelle}
1.60  (\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P%
1.61 -\rulename{classical}
1.62 +\rulenamedx{classical}
1.63  \end{isabelle}
1.64
1.65  \index{contrapositives|(}%
1.66 @@ -500,7 +500,7 @@
1.67  peculiar but important rule, a form of disjunction introduction:
1.68  \begin{isabelle}
1.69  (\isasymnot \ ?Q\ \isasymLongrightarrow \ ?P)\ \isasymLongrightarrow \ ?P\ \isasymor \ ?Q%
1.70 -\rulename{disjCI}
1.71 +\rulenamedx{disjCI}
1.72  \end{isabelle}
1.73  This rule combines the effects of \isa{disjI1} and \isa{disjI2}.  Its great
1.74  advantage is that we can remove the disjunction symbol without deciding
1.75 @@ -680,7 +680,7 @@
1.76  \begin{isabelle}
1.77  \isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\
1.78  ?t
1.79 -\rulename{ssubst}
1.80 +\rulenamedx{ssubst}
1.81  \end{isabelle}
1.82  Crucially, \isa{?P} is a function
1.83  variable.  It can be replaced by a $\lambda$-term
1.84 @@ -876,7 +876,7 @@
1.85  Returning to the universal quantifier, we find that having a similar quantifier
1.86  as part of the meta-logic makes the introduction rule trivial to express:
1.87  \begin{isabelle}
1.88 -(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI}
1.89 +(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulenamedx{allI}
1.90  \end{isabelle}
1.91
1.92
1.93 @@ -910,7 +910,7 @@
1.94  The conclusion is $P$ with $t$ substituted for the variable~$x$.
1.95  Isabelle expresses substitution using a function variable:
1.96  \begin{isabelle}
1.97 -{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulename{spec}
1.98 +{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulenamedx{spec}
1.99  \end{isabelle}
1.100  This destruction rule takes a
1.101  universally quantified formula and removes the quantifier, replacing
1.102 @@ -923,7 +923,7 @@
1.103  appears in logic books:
1.104  \begin{isabelle}
1.105  \isasymlbrakk \isasymforall x.\ ?P\ x;\ ?P\ ?x\ \isasymLongrightarrow \ ?R\isasymrbrakk \ \isasymLongrightarrow \ ?R%
1.106 -\rulename{allE}
1.107 +\rulenamedx{allE}
1.108  \end{isabelle}
1.109  The methods \isa{drule~spec} and \isa{erule~allE} do precisely the
1.110  same inference.
1.111 @@ -1005,7 +1005,7 @@
1.112  to the existential quantifier, whose introduction rule looks like this in
1.113  Isabelle:
1.114  \begin{isabelle}
1.115 -?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI}
1.116 +?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulenamedx{exI}
1.117  \end{isabelle}
1.118  If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x. 1.119 P(x)$ is also true.  It is a dual of the universal elimination rule, and
1.120 @@ -1018,7 +1018,7 @@
1.121  %
1.122  It looks like this in Isabelle:
1.123  \begin{isabelle}
1.124 -\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
1.125 +\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulenamedx{exE}
1.126  \end{isabelle}
1.127  %
1.128  Given an existentially quantified theorem and some
1.129 @@ -1170,7 +1170,7 @@
1.130
1.131  \medskip
1.132  Existential formulas can be instantiated too.  The next example uses the
1.133 -\textbf{divides} relation\indexbold{divides relation}
1.134 +\textbf{divides} relation\index{divides relation}
1.135  of number theory:
1.136  \begin{isabelle}
1.137  ?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
1.138 @@ -1255,7 +1255,7 @@
1.139  \begin{isabelle}
1.140  \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \
1.141  \isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a%
1.142 -\rulename{some_equality}
1.143 +\rulenamedx{some_equality}
1.144  \end{isabelle}
1.145  For instance, we can define the
1.146  cardinality of a finite set~$A$ to be that
1.147 @@ -1309,7 +1309,8 @@
1.148  Occasionally, \hbox{\isa{SOME\ x.\ P\ x}} serves as an \textbf{indefinite
1.149  description}, when it makes an arbitrary selection from the values
1.150  satisfying~\isa{P}\@.  Here is the definition
1.151 -of~\isa{inv},\index{*inv (constant)} which expresses inverses of functions:
1.152 +of~\cdx{inv}, which expresses inverses of
1.153 +functions:
1.154  \begin{isabelle}
1.155  inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
1.156  \rulename{inv_def}
1.157 @@ -1335,10 +1336,10 @@
1.158  tricky and requires rules such as these:
1.159  \begin{isabelle}
1.160  P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x)
1.161 -\rulename{someI}\isanewline
1.162 +\rulenamedx{someI}\isanewline
1.163  \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ Q\
1.164  x\isasymrbrakk \ \isasymLongrightarrow \ Q\ (SOME\ x.\ P\ x)
1.165 -\rulename{someI2}
1.166 +\rulenamedx{someI2}
1.167  \end{isabelle}
1.168  Rule \isa{someI} is basic: if anything satisfies \isa{P} then so does
1.169  \hbox{\isa{SOME\ x.\ P\ x}}.  The repetition of~\isa{P} in the conclusion makes it
1.170 @@ -1838,7 +1839,7 @@
1.171  ?s\ =\ ?t\
1.172  \isasymLongrightarrow\ ?t\ =\
1.173  ?s%
1.174 -\rulename{sym}
1.175 +\rulenamedx{sym}
1.176  \end{isabelle}
1.177  The following declaration gives our equation to \isa{sym}:
1.178  \begin{isabelle}
1.179 @@ -1859,10 +1860,10 @@
1.180  which extract  the two directions of reasoning about a boolean equivalence:
1.181  \begin{isabelle}
1.182  \isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
1.183 -\rulename{iffD1}%
1.184 +\rulenamedx{iffD1}%
1.185  \isanewline
1.186  \isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
1.187 -\rulename{iffD2}
1.188 +\rulenamedx{iffD2}
1.189  \end{isabelle}
1.190  %
1.191  Normally we would never name the intermediate theorems
1.192 @@ -2017,7 +2018,7 @@
1.193  such as these:
1.194  \begin{isabelle}
1.195  x\ =\ y\ \isasymLongrightarrow \ f\ x\ =\ f\ y%
1.196 -\rulename{arg_cong}\isanewline
1.197 +\rulenamedx{arg_cong}\isanewline
1.198  i\ \isasymle \ j\ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ k%
1.199  \rulename{mult_le_mono1}
1.200  \end{isabelle}
1.201 @@ -2096,8 +2097,8 @@
1.202  is omitted.
1.203
1.204  \medskip
1.205 -Here is another demonstration of \isa{insert}.  \REMARK{Effect with
1.206 -unknowns?} Division  and remainder obey a well-known law:
1.207 +Here is another demonstration of \isa{insert}.  Division and
1.208 +remainder obey a well-known law:
1.209  \begin{isabelle}
1.210  (?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m
1.211  \rulename{mod_div_equality}

     2.1 --- a/doc-src/TutorialI/Sets/sets.tex	Fri Jul 13 17:55:35 2001 +0200
2.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Fri Jul 13 17:56:05 2001 +0200
2.3 @@ -43,11 +43,11 @@
2.4  \begin{isabelle}
2.5  \isasymlbrakk c\ \isasymin\ A;\ c\ \isasymin\ B\isasymrbrakk\
2.6  \isasymLongrightarrow\ c\ \isasymin\ A\ \isasyminter\ B%
2.7 -\rulename{IntI}\isanewline
2.8 +\rulenamedx{IntI}\isanewline
2.9  c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ A
2.10 -\rulename{IntD1}\isanewline
2.11 +\rulenamedx{IntD1}\isanewline
2.12  c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ B
2.13 -\rulename{IntD2}
2.14 +\rulenamedx{IntD2}
2.15  \end{isabelle}
2.16
2.17  Here are two of the many installed theorems concerning set
2.18 @@ -55,7 +55,7 @@
2.19  Note that it is denoted by a minus sign.
2.20  \begin{isabelle}
2.21  (c\ \isasymin\ -\ A)\ =\ (c\ \isasymnotin\ A)
2.22 -\rulename{Compl_iff}\isanewline
2.23 +\rulenamedx{Compl_iff}\isanewline
2.24  -\ (A\ \isasymunion\ B)\ =\ -\ A\ \isasyminter\ -\ B
2.25  \rulename{Compl_Un}
2.26  \end{isabelle}
2.27 @@ -75,12 +75,12 @@
2.28  are its natural deduction rules:
2.29  \begin{isabelle}
2.30  ({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ x\ \isasymin\ B)\ \isasymLongrightarrow\ A\ \isasymsubseteq\ B%
2.31 -\rulename{subsetI}%
2.32 +\rulenamedx{subsetI}%
2.33  \par\smallskip%          \isanewline didn't leave enough space
2.34  \isasymlbrakk A\ \isasymsubseteq\ B;\ c\ \isasymin\
2.35  A\isasymrbrakk\ \isasymLongrightarrow\ c\
2.36  \isasymin\ B%
2.37 -\rulename{subsetD}
2.38 +\rulenamedx{subsetD}
2.39  \end{isabelle}
2.40  In harder proofs, you may need to apply \isa{subsetD} giving a specific term
2.41  for~\isa{c}.  However, \isa{blast} can instantly prove facts such as this
2.42 @@ -88,7 +88,7 @@
2.43  \begin{isabelle}
2.44  (A\ \isasymunion\ B\ \isasymsubseteq\ C)\ =\
2.45  (A\ \isasymsubseteq\ C\ \isasymand\ B\ \isasymsubseteq\ C)
2.46 -\rulename{Un_subset_iff}
2.47 +\rulenamedx{Un_subset_iff}
2.48  \end{isabelle}
2.49  Here is another example, also proved automatically:
2.50  \begin{isabelle}
2.51 @@ -125,7 +125,7 @@
2.52  \begin{isabelle}
2.53  ({\isasymAnd}x.\ (x\ {\isasymin}\ A)\ =\ (x\ {\isasymin}\ B))\
2.54  {\isasymLongrightarrow}\ A\ =\ B
2.55 -\rulename{set_ext}
2.56 +\rulenamedx{set_ext}
2.57  \end{isabelle}
2.58  Extensionality can be expressed as
2.59  $A=B\iff (A\subseteq B)\conj (B\subseteq A)$.
2.60 @@ -135,12 +135,12 @@
2.61  \begin{isabelle}
2.62  \isasymlbrakk A\ \isasymsubseteq\ B;\ B\ \isasymsubseteq\
2.63  A\isasymrbrakk\ \isasymLongrightarrow\ A\ =\ B
2.64 -\rulename{equalityI}
2.65 +\rulenamedx{equalityI}
2.66  \par\smallskip%          \isanewline didn't leave enough space
2.67  \isasymlbrakk A\ =\ B;\ \isasymlbrakk A\ \isasymsubseteq\ B;\ B\
2.68  \isasymsubseteq\ A\isasymrbrakk\ \isasymLongrightarrow\ P\isasymrbrakk\
2.69  \isasymLongrightarrow\ P%
2.70 -\rulename{equalityE}
2.71 +\rulenamedx{equalityE}
2.72  \end{isabelle}
2.73
2.74
2.75 @@ -264,13 +264,13 @@
2.76  \begin{isabelle}
2.77  ({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ P\ x)\ \isasymLongrightarrow\ {\isasymforall}x\isasymin
2.78  A.\ P\ x%
2.79 -\rulename{ballI}%
2.80 +\rulenamedx{ballI}%
2.81  \isanewline
2.82  \isasymlbrakk{\isasymforall}x\isasymin A.\
2.83  P\ x;\ x\ \isasymin\
2.84  A\isasymrbrakk\ \isasymLongrightarrow\ P\
2.85  x%
2.86 -\rulename{bspec}
2.87 +\rulenamedx{bspec}
2.88  \end{isabelle}
2.89  %
2.90  Dually, here are the natural deduction rules for the
2.91 @@ -282,14 +282,14 @@
2.92  \isasymLongrightarrow\
2.93  \isasymexists x\isasymin A.\ P\
2.94  x%
2.95 -\rulename{bexI}%
2.96 +\rulenamedx{bexI}%
2.97  \isanewline
2.98  \isasymlbrakk\isasymexists x\isasymin A.\
2.99  P\ x;\ {\isasymAnd}x.\
2.100  {\isasymlbrakk}x\ \isasymin\ A;\
2.101  P\ x\isasymrbrakk\ \isasymLongrightarrow\
2.102  Q\isasymrbrakk\ \isasymLongrightarrow\ Q%
2.103 -\rulename{bexE}
2.104 +\rulenamedx{bexE}
2.105  \end{isabelle}
2.106  \index{quantifiers!for sets|)}
2.107
2.108 @@ -301,7 +301,7 @@
2.109  (b\ \isasymin\
2.110  (\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\
2.111  b\ \isasymin\ B\ x)
2.112 -\rulename{UN_iff}
2.113 +\rulenamedx{UN_iff}
2.114  \end{isabelle}
2.115  It has two natural deduction rules similar to those for the existential
2.116  quantifier.  Sometimes \isa{UN_I} must be applied explicitly:
2.117 @@ -312,7 +312,7 @@
2.118  b\ \isasymin\
2.119  ({\isasymUnion}x\isasymin A.\
2.120  B\ x)
2.121 -\rulename{UN_I}%
2.122 +\rulenamedx{UN_I}%
2.123  \isanewline
2.124  \isasymlbrakk b\ \isasymin\
2.125  ({\isasymUnion}x\isasymin A.\
2.126 @@ -321,7 +321,7 @@
2.127  A;\ b\ \isasymin\
2.128  B\ x\isasymrbrakk\ \isasymLongrightarrow\
2.129  R\isasymrbrakk\ \isasymLongrightarrow\ R%
2.130 -\rulename{UN_E}
2.131 +\rulenamedx{UN_E}
2.132  \end{isabelle}
2.133  %
2.134  The following built-in syntax translation (see \S\ref{sec:def-translations})
2.135 @@ -341,7 +341,7 @@
2.136  \begin{isabelle}
2.137  (A\ \isasymin\ \isasymUnion C)\ =\ (\isasymexists X\isasymin C.\ A\
2.138  \isasymin\ X)
2.139 -\rulename{Union_iff}
2.140 +\rulenamedx{Union_iff}
2.141  \end{isabelle}
2.142
2.143  \index{intersection!indexed}%
2.144 @@ -356,13 +356,13 @@
2.145  =\
2.146  ({\isasymforall}x\isasymin A.\
2.147  b\ \isasymin\ B\ x)
2.148 -\rulename{INT_iff}%
2.149 +\rulenamedx{INT_iff}%
2.150  \isanewline
2.151  (A\ \isasymin\
2.152  \isasymInter C)\ =\
2.153  ({\isasymforall}X\isasymin C.\
2.154  A\ \isasymin\ X)
2.155 -\rulename{Inter_iff}
2.156 +\rulenamedx{Inter_iff}
2.157  \end{isabelle}
2.158
2.159  Isabelle uses logical equivalences such as those above in automatic proof.
2.160 @@ -404,12 +404,12 @@
2.161  \begin{isabelle}
2.162  {\isasymlbrakk}finite\ A;\ finite\ B\isasymrbrakk\isanewline
2.163  \isasymLongrightarrow\ card\ A\ \isacharplus\ card\ B\ =\ card\ (A\ \isasymunion\ B)\ \isacharplus\ card\ (A\ \isasyminter\ B)
2.164 -\rulename{card_Un_Int}%
2.165 +\rulenamedx{card_Un_Int}%
2.166  \isanewline
2.167  \isanewline
2.168  finite\ A\ \isasymLongrightarrow\ card\
2.169  (Pow\ A)\  =\ 2\ \isacharcircum\ card\ A%
2.170 -\rulename{card_Pow}%
2.171 +\rulenamedx{card_Pow}%
2.172  \isanewline
2.173  \isanewline
2.174  finite\ A\ \isasymLongrightarrow\isanewline
2.175 @@ -449,7 +449,7 @@
2.176  functions:
2.177  \begin{isabelle}
2.178  ({\isasymAnd}x.\ f\ x\ =\ g\ x)\ {\isasymLongrightarrow}\ f\ =\ g
2.179 -\rulename{ext}
2.180 +\rulenamedx{ext}
2.181  \end{isabelle}
2.182
2.183  \indexbold{updating a function}%
2.184 @@ -478,11 +478,11 @@
2.185  defined:
2.186  \begin{isabelle}%
2.187  id\ \isasymequiv\ {\isasymlambda}x.\ x%
2.188 -\rulename{id_def}\isanewline
2.189 +\rulenamedx{id_def}\isanewline
2.190  f\ \isasymcirc\ g\ \isasymequiv\
2.191  {\isasymlambda}x.\ f\
2.192  (g\ x)%
2.193 -\rulename{o_def}
2.194 +\rulenamedx{o_def}
2.195  \end{isabelle}
2.196  %
2.197  Many familiar theorems concerning the identity and composition
2.198 @@ -500,12 +500,12 @@
2.199  inj_on\ f\ A\ \isasymequiv\ {\isasymforall}x\isasymin A.\
2.200  {\isasymforall}y\isasymin  A.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\
2.201  =\ y%
2.202 -\rulename{inj_on_def}\isanewline
2.203 +\rulenamedx{inj_on_def}\isanewline
2.204  surj\ f\ \isasymequiv\ {\isasymforall}y.\
2.205  \isasymexists x.\ y\ =\ f\ x%
2.206 -\rulename{surj_def}\isanewline
2.207 +\rulenamedx{surj_def}\isanewline
2.208  bij\ f\ \isasymequiv\ inj\ f\ \isasymand\ surj\ f
2.209 -\rulename{bij_def}
2.210 +\rulenamedx{bij_def}
2.211  \end{isabelle}
2.212  The second argument
2.213  of \isa{inj_on} lets us express that a function is injective over a
2.214 @@ -588,7 +588,7 @@
2.215  \begin{isabelle}
2.216  f\ \ A\ \isasymequiv\ \isacharbraceleft y.\ \isasymexists x\isasymin
2.217  A.\ y\ =\ f\ x\isacharbraceright
2.218 -\rulename{image_def}
2.219 +\rulenamedx{image_def}
2.220  \end{isabelle}
2.221  %
2.222  Here are some of the many facts proved about image:
2.223 @@ -637,7 +637,7 @@
2.224  It is defined as follows:
2.225  \begin{isabelle}
2.226  f\ -\ B\ \isasymequiv\ \isacharbraceleft x.\ f\ x\ \isasymin\ B\isacharbraceright
2.227 -\rulename{vimage_def}
2.228 +\rulenamedx{vimage_def}
2.229  \end{isabelle}
2.230  %
2.231  This is one of the facts proved about it:
2.232 @@ -662,7 +662,7 @@
2.233  definition:
2.234  \begin{isabelle}
2.235  Id\ \isasymequiv\ \isacharbraceleft p.\ \isasymexists x.\ p\ =\ (x,x){\isacharbraceright}%
2.236 -\rulename{Id_def}
2.237 +\rulenamedx{Id_def}
2.238  \end{isabelle}
2.239
2.240  \indexbold{composition!of relations}%
2.241 @@ -670,7 +670,7 @@
2.242  available:
2.243  \begin{isabelle}
2.244  r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright
2.245 -\rulename{comp_def}
2.246 +\rulenamedx{comp_def}
2.247  \end{isabelle}
2.248  %
2.249  This is one of the many lemmas proved about these concepts:
2.250 @@ -698,7 +698,7 @@
2.251  \begin{isabelle}
2.252  ((a,b)\ \isasymin\ r\isasyminverse)\ =\
2.253  ((b,a)\ \isasymin\ r)
2.254 -\rulename{converse_iff}
2.255 +\rulenamedx{converse_iff}
2.256  \end{isabelle}
2.257  %
2.258  Here is a typical law proved about converse and composition:
2.259 @@ -713,7 +713,7 @@
2.260  \begin{isabelle}
2.261  (b\ \isasymin\ r\ \ A)\ =\ (\isasymexists x\isasymin
2.262  A.\ (x,b)\ \isasymin\ r)
2.263 -\rulename{Image_iff}
2.264 +\rulenamedx{Image_iff}
2.265  \end{isabelle}
2.266  It satisfies many similar laws.
2.267
2.268 @@ -724,13 +724,13 @@
2.269  \begin{isabelle}
2.270  (a\ \isasymin\ Domain\ r)\ =\ (\isasymexists y.\ (a,y)\ \isasymin\
2.271  r)
2.272 -\rulename{Domain_iff}%
2.273 +\rulenamedx{Domain_iff}%
2.274  \isanewline
2.275  (a\ \isasymin\ Range\ r)\
2.276  \ =\ (\isasymexists y.\
2.277  (y,a)\
2.278  \isasymin\ r)
2.279 -\rulename{Range_iff}
2.280 +\rulenamedx{Range_iff}
2.281  \end{isabelle}
2.282
2.283  Iterated composition of a relation is available.  The notation overloads
2.284 @@ -757,13 +757,13 @@
2.285  rules:
2.286  \begin{isabelle}
2.287  (a,\ a)\ \isasymin \ r\isactrlsup *
2.288 -\rulename{rtrancl_refl}\isanewline
2.289 +\rulenamedx{rtrancl_refl}\isanewline
2.290  p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup *
2.291 -\rulename{r_into_rtrancl}\isanewline
2.292 +\rulenamedx{r_into_rtrancl}\isanewline
2.293  \isasymlbrakk (a,b)\ \isasymin \ r\isactrlsup *;\
2.294  (b,c)\ \isasymin \ r\isactrlsup *\isasymrbrakk \ \isasymLongrightarrow \
2.295  (a,c)\ \isasymin \ r\isactrlsup *
2.296 -\rulename{rtrancl_trans}
2.297 +\rulenamedx{rtrancl_trans}
2.298  \end{isabelle}
2.299  %
2.300  Induction over the reflexive transitive closure is available:
2.301 @@ -785,9 +785,9 @@
2.302  \isa{r\isacharcircum+}.  It has two  introduction rules:
2.303  \begin{isabelle}
2.304  p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup +
2.305 -\rulename{r_into_trancl}\isanewline
2.306 +\rulenamedx{r_into_trancl}\isanewline
2.307  \isasymlbrakk (a,\ b)\ \isasymin \ r\isactrlsup +;\ (b,\ c)\ \isasymin \ r\isactrlsup +\isasymrbrakk \ \isasymLongrightarrow \ (a,\ c)\ \isasymin \ r\isactrlsup +
2.308 -\rulename{trancl_trans}
2.309 +\rulenamedx{trancl_trans}
2.310  \end{isabelle}
2.311  %
2.312  The induction rule resembles the one shown above.
2.313 @@ -910,7 +910,7 @@
2.314  relation  behaves as expected and that it is well-founded:
2.315  \begin{isabelle}
2.316  ((x,y)\ \isasymin\ less_than)\ =\ (x\ <\ y)
2.317 -\rulename{less_than_iff}\isanewline
2.318 +\rulenamedx{less_than_iff}\isanewline
2.319  wf\ less_than
2.320  \rulename{wf_less_than}
2.321  \end{isabelle}
2.322 @@ -925,7 +925,7 @@
2.323  \begin{isabelle}
2.324  inv_image\ r\ f\ \isasymequiv\ \isacharbraceleft(x,y).\ (f\ x,\ f\ y)\
2.325  \isasymin\ r\isacharbraceright
2.326 -\rulename{inv_image_def}\isanewline
2.327 +\rulenamedx{inv_image_def}\isanewline
2.328  wf\ r\ \isasymLongrightarrow\ wf\ (inv_image\ r\ f)
2.329  \rulename{wf_inv_image}
2.330  \end{isabelle}
2.331 @@ -936,7 +936,7 @@
2.332  \isa{measure} as shown:
2.333  \begin{isabelle}
2.334  measure\ \isasymequiv\ inv_image\ less_than%
2.335 -\rulename{measure_def}\isanewline
2.336 +\rulenamedx{measure_def}\isanewline
2.337  wf\ (measure\ f)
2.338  \rulename{wf_measure}
2.339  \end{isabelle}
2.340 @@ -953,7 +953,7 @@
2.341  \isasymor\isanewline
2.342  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \,a=a'\ \isasymand \ (b,b')\
2.343  \isasymin \ rb\isacharbraceright
2.344 -\rulename{lex_prod_def}%
2.345 +\rulenamedx{lex_prod_def}%
2.346  \par\smallskip
2.347  \isasymlbrakk wf\ ra;\ wf\ rb\isasymrbrakk \ \isasymLongrightarrow \ wf\ (ra\ <*lex*>\ rb)
2.348  \rulename{wf_lex_prod}
2.349 @@ -986,7 +986,7 @@
2.350    {\isasymAnd}x.\ {\isasymforall}y.\ (y,x)\ \isasymin\ r\
2.351  \isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\
2.352  \isasymLongrightarrow\ P\ a
2.353 -\rulename{wf_induct}
2.354 +\rulenamedx{wf_induct}
2.355  \end{isabelle}
2.356  Here \isa{wf\ r} expresses that the relation~\isa{r} is well-founded.
2.357
2.358 @@ -1021,7 +1021,7 @@
2.359  Isabelle's definition of monotone is overloaded over all orderings:
2.360  \begin{isabelle}
2.361  mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%
2.362 -\rulename{mono_def}
2.363 +\rulenamedx{mono_def}
2.364  \end{isabelle}
2.365  %
2.366  For fixed point operators, the ordering will be the subset relation: if