doc-src/TutorialI/Rules/rules.tex

 the form of a conjunction; the proof step makes this conjunction symbol
 disappear. 
 
 In Isabelle notation, the rule looks like this:
 \begin{isabelle}
-\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulename{conjI}
+\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulenamedx{conjI}
 \end{isabelle}
 Carefully examine the syntax.  The premises appear to the
 left of the arrow and the conclusion to the right.  The premises (if 
 more than one) are grouped using the fat brackets.  The question marks
 indicate \textbf{schematic variables} (also called

 The assumptions $[P]$ and $[Q]$ are bracketed 
 to emphasize that they are local to their subproofs.  In Isabelle 
 notation, the already-familiar \isa{\isasymLongrightarrow} syntax serves the
 same  purpose:
 \begin{isabelle}
-\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE}
+\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{disjE}
 \end{isabelle}
 When we use this sort of elimination rule backwards, it produces 
 a case split.  (We have seen this before, in proofs by induction.)  The following  proof
 illustrates the use of disjunction elimination.  
 \begin{isabelle}

 of the formula, when usually we want to take both parts of the conjunction as new
 assumptions.  The easiest way to do so is by using an 
 alternative conjunction elimination rule that resembles \isa{disjE}\@.  It is
 seldom, if ever, seen in logic books.  In Isabelle syntax it looks like this: 
 \begin{isabelle}
-\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{conjE}
+\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{conjE}
 \end{isabelle}
 \index{destruction rules|)}
 
 \begin{exercise}
 Use the rule \isa{conjE} to shorten the proof above. 

 At the start of this chapter, we saw the rule \emph{modus ponens}.  It is, in fact,
 a destruction rule. The matching introduction rule looks like this 
 in Isabelle: 
 \begin{isabelle}
 (?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\
-\isasymlongrightarrow\ ?Q\rulename{impI}
+\isasymlongrightarrow\ ?Q\rulenamedx{impI}
 \end{isabelle}
 And this is \emph{modus ponens}\index{modus ponens@\emph{modus ponens}} :
 \begin{isabelle}
 \isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\
 \isasymLongrightarrow\ ?Q
-\rulename{mp}
+\rulenamedx{mp}
 \end{isabelle}
 
 Here is a proof using the implication rules.  This 
 lemma performs a sort of uncurrying, replacing the two antecedents 
 of a nested implication by a conjunction.  The proof illustrates

 Negation introduction deduces $\neg P$ if assuming $P$ leads to a 
 contradiction. Negation elimination deduces any formula in the 
 presence of $\neg P$ together with~$P$: 
 \begin{isabelle}
 (?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P%
-\rulename{notI}\isanewline
+\rulenamedx{notI}\isanewline
 \isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R%
-\rulename{notE}
+\rulenamedx{notE}
 \end{isabelle}
 %
 Classical logic allows us to assume $\neg P$ 
 when attempting to prove~$P$: 
 \begin{isabelle}
 (\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P%
-\rulename{classical}
+\rulenamedx{classical}
 \end{isabelle}
 
 \index{contrapositives|(}%
 The implications $P\imp Q$ and $\neg Q\imp\neg P$ are logically
 equivalent, and each is called the

 
 The following example may be skipped on a first reading.  It involves a
 peculiar but important rule, a form of disjunction introduction:
 \begin{isabelle}
 (\isasymnot \ ?Q\ \isasymLongrightarrow \ ?P)\ \isasymLongrightarrow \ ?P\ \isasymor \ ?Q%
-\rulename{disjCI}
+\rulenamedx{disjCI}
 \end{isabelle}
 This rule combines the effects of \isa{disjI1} and \isa{disjI2}.  Its great
 advantage is that we can remove the disjunction symbol without deciding
 which disjunction to prove.  This treatment of disjunction is standard in sequent
 and tableau calculi.

 
 The Isabelle version of the substitution rule looks like this: 
 \begin{isabelle}
 \isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\
 ?t
-\rulename{ssubst}
+\rulenamedx{ssubst}
 \end{isabelle}
 Crucially, \isa{?P} is a function 
 variable.  It can be replaced by a $\lambda$-term 
 with one bound variable, whose occurrences identify the places 
 in which $s$ will be replaced by~$t$.  The proof above requires

 \subsection{The Universal Introduction Rule}
 
 Returning to the universal quantifier, we find that having a similar quantifier
 as part of the meta-logic makes the introduction rule trivial to express:
 \begin{isabelle}
-(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI}
+(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulenamedx{allI}
 \end{isabelle}
 
 
 The following trivial proof demonstrates how the universal introduction 
 rule works. 

 the rule looks like this: 
 \[ \infer{P[t/x]}{\forall x.\,P} \]
 The conclusion is $P$ with $t$ substituted for the variable~$x$.  
 Isabelle expresses substitution using a function variable: 
 \begin{isabelle}
-{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulename{spec}
+{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulenamedx{spec}
 \end{isabelle}
 This destruction rule takes a 
 universally quantified formula and removes the quantifier, replacing 
 the bound variable \isa{x} by the schematic variable \isa{?x}.  Recall that a
 schematic variable starts with a question mark and acts as a

 The universal elimination rule is also
 available in the standard elimination format.  Like \isa{conjE}, it never
 appears in logic books:
 \begin{isabelle}
 \isasymlbrakk \isasymforall x.\ ?P\ x;\ ?P\ ?x\ \isasymLongrightarrow \ ?R\isasymrbrakk \ \isasymLongrightarrow \ ?R%
-\rulename{allE}
+\rulenamedx{allE}
 \end{isabelle}
 The methods \isa{drule~spec} and \isa{erule~allE} do precisely the
 same inference.
 
 To see how $\forall$-elimination works, let us derive a rule about reducing 

 \index{quantifiers!existential|(}%
 The concepts just presented also apply
 to the existential quantifier, whose introduction rule looks like this in
 Isabelle: 
 \begin{isabelle}
-?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI}
+?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulenamedx{exI}
 \end{isabelle}
 If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
 P(x)$ is also true.  It is a dual of the universal elimination rule, and
 logic texts present it using the same notation for substitution.
 

 in a logic text: 
 \[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \]
 %
 It looks like this in Isabelle: 
 \begin{isabelle}
-\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
+\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulenamedx{exE}
 \end{isabelle}
 %
 Given an existentially quantified theorem and some
 formula $Q$ to prove, it creates a new assumption by removing the quantifier.  As with
 the universal introduction  rule, the textbook version imposes a proviso on the

 \end{isabelle}
 We have forced the desired instantiation.
 
 \medskip
 Existential formulas can be instantiated too.  The next example uses the 
-\textbf{divides} relation\indexbold{divides relation}
+\textbf{divides} relation\index{divides relation}
 of number theory: 
 \begin{isabelle}
 ?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
 \rulename{dvd_def}
 \end{isabelle}

 description}: when \isa{P} is satisfied by a unique value,~\isa{a}. 
 We reason using this rule:\REMARK{update if we add iota}
 \begin{isabelle}
 \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \ 
 \isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a%
-\rulename{some_equality}
+\rulenamedx{some_equality}
 \end{isabelle}
 For instance, we can define the
 cardinality of a finite set~$A$ to be that
 $n$ such that $A$ is in one-to-one correspondence with $\{1,\ldots,n\}$.  We can then
 prove that the cardinality of the empty set is zero (since $n=0$ satisfies the

 
 \index{descriptions!indefinite}%
 Occasionally, \hbox{\isa{SOME\ x.\ P\ x}} serves as an \textbf{indefinite
 description}, when it makes an arbitrary selection from the values
 satisfying~\isa{P}\@.  Here is the definition
-of~\isa{inv},\index{*inv (constant)} which expresses inverses of functions:
+of~\cdx{inv}, which expresses inverses of
+functions:
 \begin{isabelle}
 inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
 \rulename{inv_def}
 \end{isabelle}
 The inverse of \isa{f}, when applied to \isa{y}, returns some~\isa{x} such that

 \isa{SOME} as a definite description, since it only reasons about
 situations in which the value is  described uniquely.  To go further is
 tricky and requires rules such as these:
 \begin{isabelle}
 P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x)
-\rulename{someI}\isanewline
+\rulenamedx{someI}\isanewline
 \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ Q\
 x\isasymrbrakk \ \isasymLongrightarrow \ Q\ (SOME\ x.\ P\ x)
-\rulename{someI2}
+\rulenamedx{someI2}
 \end{isabelle}
 Rule \isa{someI} is basic: if anything satisfies \isa{P} then so does
 \hbox{\isa{SOME\ x.\ P\ x}}.  The repetition of~\isa{P} in the conclusion makes it
 difficult to apply in a backward proof, so the derived rule \isa{someI2} is
 also provided. 

 To re-orient the equation requires the symmetry rule:
 \begin{isabelle}
 ?s\ =\ ?t\
 \isasymLongrightarrow\ ?t\ =\
 ?s%
-\rulename{sym}
+\rulenamedx{sym}
 \end{isabelle}
 The following declaration gives our equation to \isa{sym}:
 \begin{isabelle}
 \ \ \ \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_1\ [THEN\ sym]
 \end{isabelle}

 which converts the implication $P\imp Q$ into the rule
 $\vcenter{\infer{Q}{P}}$. Similar to \isa{mp} are the following two rules,
 which extract  the two directions of reasoning about a boolean equivalence:
 \begin{isabelle}
 \isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
-\rulename{iffD1}%
+\rulenamedx{iffD1}%
 \isanewline
 \isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
-\rulename{iffD2}
+\rulenamedx{iffD2}
 \end{isabelle}
 %
 Normally we would never name the intermediate theorems
 such as \isa{gcd_mult_0} and
 \isa{gcd_mult_1} but would combine

 \isa{mp} and
 \isa{spec} to operate on formulae.  They can also operate on terms, using rules
 such as these:
 \begin{isabelle}
 x\ =\ y\ \isasymLongrightarrow \ f\ x\ =\ f\ y%
-\rulename{arg_cong}\isanewline
+\rulenamedx{arg_cong}\isanewline
 i\ \isasymle \ j\ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ k%
 \rulename{mult_le_mono1}
 \end{isabelle}
 
 For example, let us prove a fact about divisibility in the natural numbers:

 \end{isabelle}
 Simplification has yielded an equation for~\isa{m}.  The rest of the proof
 is omitted.
 
 \medskip
-Here is another demonstration of \isa{insert}.  \REMARK{Effect with
-unknowns?} Division  and remainder obey a well-known law: 
+Here is another demonstration of \isa{insert}.  Division and
+remainder obey a well-known law: 
 \begin{isabelle}
 (?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m
 \rulename{mod_div_equality}
 \end{isabelle}