Lines Matching refs:to
10 detailed, low-level proof steps. Later, we shall see how to automate such
15 transformed to yield another.
26 \textbf{Natural deduction} is an attempt to formalize logic in a way
30 The introduction rules allow us to infer this symbol (say, to
31 infer conjunctions). The elimination rules allow us to deduce
35 have to refer to other symbols as well. It is best not to be dogmatic.
39 Natural deduction generally deserves its name. It is easy to use. Each
46 definition. Natural deduction rules also lend themselves to automation.
49 rules and uses them to search for proofs automatically. Isabelle is designed around
74 Carefully examine the syntax. The premises appear to the
75 left of the arrow and the conclusion to the right. The premises (if
80 tries to unify the current subgoal with the conclusion of the rule, which
83 it yields new subgoals given by the formulas assigned to
102 us with the assumptions (\isa{P} and~\isa{Q}) and with the goal to be proved,
106 of the \isa{\isasymand} symbol. To apply a rule to a subgoal, we apply
152 there is an elimination rule that works indirectly. If we are trying to prove
153 something else, say $R$, and we know that $P\disj Q$ holds, then we have to consider
156 deduction: that of the \textbf{assumptions}. We have to prove $R$ twice, under
157 different assumptions. The assumptions are local to these subproofs and are visible
164 to emphasize that they are local to their subproofs. In Isabelle
185 method designed to work with elimination rules. It looks for an assumption that
187 regards the first premise as proved and returns subgoals corresponding to
188 the remaining premises. When we apply \isa{erule} to \isa{disjE}, only two
190 to get three subgoals, then proving the first by assumption: the other
193 Most of the time, \isa{erule} is the best way to use elimination rules, since it
204 need to show \isa{Q\ \isasymor\ P}\@. The second introduction rule
205 (\isa{disjI2}) can reduce this to \isa{P}, which matches the assumption.
223 be useful. We can use it to replace any goal of the form $Q\disj P$
275 Choosing among the methods \isa{rule}, \isa{erule} and \isa{drule} is up to
276 you. Isabelle does not attempt to work out whether a rule
280 be applied to assumptions as well as to goals; it replaces any
286 of the formula, when usually we want to take both parts of the conjunction as new
287 assumptions. The easiest way to do so is by using an
296 Use the rule \isa{conjE} to shorten the proof above.
339 which moves the conjunction to the assumptions.
371 uses \isa{\isasymLongrightarrow} to express inference rules; the symbol is
376 connectives. You will have to use \isa{\isasymlongrightarrow} in any
378 \isa{\isasymLongrightarrow} to separate a theorem's preconditions from its
386 \isacommand{apply} command, then tries to prove all remaining subgoals using
401 We could use \isacommand{by} to replace the final \isacommand{apply} and
403 to eliminate calls to \isa{assumption}. It is also a nice way of expressing a
414 necessary in order to handle negated assumptions gracefully. This section
418 Negation introduction deduces $\lnot P$ if assuming $P$ leads to a
428 Classical logic allows us to assume $\lnot P$
429 when attempting to prove~$P$:
454 their effect is to form a contrapositive from an
459 for applying introduction rules to negated assumptions. For instance,
460 the assumption $\lnot(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we
461 might want to use conjunction introduction on it.
475 There are two negated assumptions and we need to exchange the conclusion with the
489 to \isa{rule impI}.
499 Now when Isabelle selects the first assumption, it tries to prove \isa{P\
514 which disjunction to prove. This treatment of disjunction is standard in sequent
527 The first proof step to applies the introduction rules \isa{disjCI}.
543 Now we must move the formula \isa{Q\ \isasymand\ R} to be the conclusion. The
548 is robust: the \isa{conjI} forces the \isa{erule} to select a
550 conjunction introduction to
565 may be helpful to review how they work given an arbitrary rule such as this:
567 Below, we refer to $P@1$ as the \bfindex{major premise}. This concept
568 applies only to elimination and destruction rules. These rules act upon an
569 instance of their major premise, typically to replace it by subformulas of itself.
608 \methdx{frule_tac}. These methods also let us specify which subgoal to
610 methods, but we can specify that rule \isa{R} should be applied to subgoal
623 placeholders for terms. \textbf{Unification} --- well known to Prolog programmers --- is the act of
646 For example, suppose we are trying to prove this subgoal by assumption:
673 $\lambda$-terms to replace function variables,
674 which can lead to a combinatorial explosion. However, Isabelle proofs tend
675 to involve easy cases where there are few possibilities for the
677 function variable is applied only to bound variables,
678 as when we try to unify \isa{{\isasymlambda}x\ y.\ f(?h x y)} and
679 \isa{{\isasymlambda}x\ y.\ f(x+y+a)}. The only solution is to replace
694 Isabelle also uses function variables to express \textbf{substitution}.
695 A typical substitution rule allows us to replace one term by
715 to be replaced by \isa{{\isasymlambda}x.~x=s}; the second premise will then
742 \isa{ssubst} the effect is to find, use and delete an equality
751 Now we wish to apply a commutative law:
760 The simplifier notices the danger of looping and refuses to apply the
790 want to skip on your first reading:
804 By default, Isabelle tries to substitute for all the
811 command allows us to reject this possibility and demand a new one:
839 function variables. We were forced to select the right unifier using the
844 One way to constrain the inference is by joining two methods in a
866 The most general way to constrain unification is
868 similar to \isa{rule}, but it
881 u\ x} indicate that the first two arguments have to be substituted, leaving
885 An alternative to \isa{rule_tac} is to use \isa{rule} with a theorem
888 express instantiations that refer to
902 arbitrary, since it has not been assumed to satisfy any special conditions.
905 universal quantifier (\isasymAnd) to express the notion of an arbitrary value.
909 which can be used to define constants.
913 Returning to the universal quantifier, we find that having a similar quantifier
914 as part of the meta-logic makes the introduction rule trivial to express:
933 higher-order logic by Isabelle's meta-level quantifier. Our goal is to
983 which moves the \isa{P} from the conclusion to the assumptions. Then
999 Now, to reason from the universally quantified
1002 to a particular term.
1014 to the argument~\isa{x}.) This new assumption is an implication, so we can use
1031 The consequent is \isa{Q} applied to that placeholder. It may be replaced by any
1034 be identical to the conclusion, provided the two formulas are unifiable.%
1042 to the existential quantifier, whose introduction rule looks like this in
1062 formula $Q$ to prove, it creates a new assumption by removing the quantifier. As with
1065 enough to have a universal quantifier in the meta-logic; we do not need an existential
1066 quantifier to be built in as well.
1073 to the one just above for the universal quantifier.
1082 becomes a new bound variable of the new subgoal. Isabelle tries to avoid
1083 changing its name, but sometimes it has to choose a new name in order to
1102 variables, but beware of referring to variables
1103 like~\isa{xa}. A future change to your theories could change the set of names
1104 produced at top level, so that \isa{xa} changes to~\isa{xb} or reverts to~\isa{x}.
1105 It is safer to rename automatically-generated variables before mentioning them.
1107 If the subgoal has more bound variables than there are names given to
1118 universal formula has to be kept so that it can be used again. Then we use a new
1122 In this example, going from \isa{P\ a} to \isa{P(h(h~a))}
1136 assumption is still present. Next we apply \isa{mp} to the
1166 command forces Isabelle to backtrack until it finds the correct one.
1169 we could have given the entire proof to \isa{auto}.%
1179 assumption of the form $\forall x.\,P\, x$ to generate a new assumption $P\,t$ for
1218 respect to the divides relation:
1246 The term needed to instantiate the remaining quantifier is~\isa{k*ka}. But
1247 \isa{ka} is an automatically-generated name. As noted above, references to
1248 such variable names makes a proof less resilient to future changes. So,
1249 first we rename the most recent variable to~\isa{l}:
1282 requiring the solution to be unique: it uses the axiom of choice to pick any
1286 Description operators can be hard to reason about. Novices
1287 should try to avoid them. Fortunately, descriptions are seldom required.
1307 cardinality of a finite set~$A$ to be that
1308 $n$ such that $A$ is in one-to-one correspondence with $\{1,\ldots,n\}$. We can then
1310 description) and proceed to prove other facts.
1347 call to \isa{auto} does it all:
1370 \isa{inv} do assume the function to be injective.
1372 The inverse of \isa{f}, when applied to \isa{y}, returns some~\isa{x} such that
1381 The proof is a one-liner: the subgoal simplifies to a degenerate application of
1383 to \isa{SOME\ x.\ Suc\ x\ =\ Suc\ n}, then to \isa{SOME\ x.\ x\ =\ n} and
1384 finally to~\isa{n}.
1387 \isa{inv~Suc} returns when applied to zero. The proof above still treats
1407 difficult to apply in a backward proof, so the derived rule \isa{someI2} is
1422 We have applied the introduction rules; now it is time to apply the elimination
1433 \isa{f} to \hbox{\isa{\isasymlambda x.\ SOME y.\ P\ x\ y}}, which is the choice
1434 function. It also instantiates \isa{?x2\ x} to \isa{x}.
1440 The original purpose of Hilbert's $\varepsilon$-operator was to express an
1453 conjecture is true, and it can be instructive to see how
1454 proofs fail. Here we attempt to prove a distributive law involving
1461 The first steps are routine. We apply conjunction elimination to break
1477 The proviso of the existential elimination rule has forced the variables to
1478 differ: we can hardly expect two arbitrary values to be equal! There is
1479 no way to prove this subgoal. Removing the
1482 and~\isa{xa}. We need one to become \isa{x}
1483 and the other to become~\isa{xa}, but Isabelle requires all instances of a
1484 placeholder to be identical.
1514 we attempt to prove it.
1526 refuses to substitute \isa{y}, a bound variable, for~\isa{?x}; that would be
1527 a bound variable capture. We can still try to finish the proof in some
1535 Finally, we try to apply our reflexivity assumption. We obtain a
1545 \isa{?z2} to the identity function. But, just as two steps earlier,
1546 Isabelle refuses to substitute~\isa{y} for~\isa{?x}.
1553 It is hard to prove many theorems using the methods
1555 may need to search among different ways of proving certain
1557 impossible to prove. There are further complications that we have not
1563 In this section, we shall first see how to use the classical
1564 reasoner in its default mode and then how to insert additional
1565 rules, enabling it to work in new problem domains.
1569 it to be hard to prove by automatic means.
1571 converting the nested biconditionals to
1646 classical reasoner backtracks to the most recent unsafe rule application
1651 formulas, can be given to the classical
1661 will make it known to the classical reasoner (and to the simplifier).
1678 disjunctive reasoning is hard, but translating to an actual disjunction
1682 the equivalence $P=Q$ to a pair of rules: the introduction
1683 rule $Q\Imp P$ and the destruction rule $P\Imp Q$. It gives both to the
1686 replacement, since \isa{iff} gives $P=Q$ to the
1692 reasoning uses search and backtracking in order to prove a goal outright.%
1701 to a limited extent, giving the user fine control over the proof.
1726 refer to distinct bound variables. To reach this state, \isa{clarify} applied
1729 rule for \isa{\isasymand} because of its policy never to split goals.
1737 reasoner and simplifier to one goal.
1740 with simplification. The latter's purpose is to prove all the
1745 difference: \isa{force} tries harder than {\isa{auto}} to prove
1746 its goal, so it can take much longer to terminate.
1753 That makes them slower but enables them to work in the
1763 to apply. Consider this contrived example:
1785 The \methdx{best} method is similar to
1787 Accordingly, it is slower but is less susceptible to divergence.
1788 Transitivity rules usually cause \isa{fast} to loop where \isa{best}
1798 \item \methdx{force} uses classical reasoning and simplification to prove a goal;
1822 most fundamental type of proof. Backward proof, by working from goals to
1826 to the specific. For example, consider this distributive law for
1837 Re-orientation works by applying the symmetry of equality to
1853 From this definition, it is possible to prove the distributive law.
1854 That takes us to the starting point for our example.
1860 The first step in our derivation is to replace \isa{?m} by~1. We instantiate the
1862 appearance from left to right. In this case, the variables are \isa{?k}, \isa{?m}
1881 substitution for \isa{k}. One solution is to avoid giving an instantiation for
1888 An equivalent solution is to use the attribute \isa{where}.
1892 While \isa{of} refers to
1893 variables by their position, \isa{where} refers to variables by name. Multiple
1905 and returns the result of simplifying it, with respect to the default
1924 The following declaration gives our equation to \isa{sym}:
1933 \isa{THEN~sym}\indexbold{*THEN (attribute)} gives the current theorem to the
1934 rule \isa{sym} and returns the resulting conclusion. The effect is to
1939 $\vcenter{\infer{Q}{P}}$. Similar to \isa{mp} are the following two rules,
1955 The directives, or attributes, are processed from left to right. This
1956 declaration of \isa{gcd_mult} is equivalent to the
1959 Such declarations can make the proof script hard to read. Better
1960 is to state the new lemma explicitly and to prove it using a single
2016 We can use \isa{OF} to create an instance of this rule.
2025 guaranteed to terminate, and it can be slow; Isabelle
2028 give this new lemma to \isa{OF}. The expression
2056 As with \isa{of}, we can use the \isa{_} symbol to leave some positions
2067 the same idea, namely to combine two rules. They differ in the
2069 typically with a destruction rule to extract a subformula of the current
2070 theorem. We use \isa{OF} with a list of facts to generate an instance of
2076 \item \attrdx{of} instantiates the variables of a rule to a list of terms
2077 \item \attrdx{OF} applies a rule to a list of theorems
2078 \item \attrdx{THEN} gives a theorem to a named rule and returns the
2082 \item \attrdx{simplified} applies the simplifier to a theorem
2083 \item \isacommand{lemmas} assigns a name to the theorem produced by the
2091 proof. There are many ways to achieve a forward style using our existing
2098 \isa{spec} to operate on formulae. They can also operate on terms, using rules
2115 The key step is to apply the function \ldots\isa{mod\ u} to both sides of the
2125 Simplification reduces the left side to 0 and the right side to~1, yielding the
2147 be used to help prove the subgoals.
2181 We refer to this law explicitly in the following proof:
2203 Simplification reduces \isa{(m\ *\ n)\ mod\ n} to zero.
2209 Any unknowns in the theorem given to \methdx{insert} will be universally
2220 idea is to claim that the formula holds on the basis of the current
2221 assumptions, to use this claim to complete the proof, and finally
2222 to justify the claim. It gives the proof
2247 step is to claim that \isa{z} is either 34 or 36. The resulting proof
2258 The first subgoal is trivial (\isa{blast}), but for the second Isabelle needs help to eliminate
2288 Naturally you should try to divide proofs into manageable parts. Look for lemmas
2291 and you are forced to cope with a long proof involving many subgoals.
2316 concludes~\isa{S}. The final step matches the assumption \isa{S} with the goal to
2370 If each \isa{bigsubgoal} is 15 lines or so, the proof state will be too big to
2381 All methods apply to the first subgoal.
2382 Sometimes, not only in a large proof, you may want to focus on some other
2401 Now we apply \isa{blast} repeatedly to the easy subgoals:
2407 that we can devote attention to the difficult part.
2420 We decide to work on the third subgoal.
2427 If we manage to prove \isa{doubtful}, then we can work on the other
2429 proof script to remove the \isacommand{prefer} command, since we needed it only to
2433 lemma. Always seek ways to streamline your proofs.
2440 \item the \isacommand{pr} command can limit the number of subgoals to display
2442 subgoal to the last or first position
2461 \isa{case_tac} used to perform a Boolean case split.
2515 The two divides relationships it asserts are enough to prove
2524 \isa{?k~dvd~?m}) to the two premises, which
2526 and could easily loop. More sensible is to apply the rule in the forward
2533 Attaching the \attrdx{dest} attribute to \isa{dvd_mod_imp_dvd} tells
2534 \isa{blast} to use it as destruction rule; that is, in the forward direction.
2537 We have proved a conjunction. Now, let us give names to each of the
2544 used with the \attrdx{iff} attribute, which supplies the new theorems to the
2552 Isabelle renames schematic variables to prevent
2569 preconditions. The directive \isa{rule_format} tells Isabelle to replace
2574 \isa{THEN} to the rules \isa{mp} and \isa{spec}. We did not have to
2603 gcd\ m\ n} goes to~\isa{k\ dvd\ m}. The second subgoal is proved by
2614 equivalence. This step gives us a chance to see another application
2624 Isabelle can use it to remove some occurrences of \isa{gcd}.
2640 on transitivity reasoning. The rule {\isa{gcd\_greatest}} is safe to apply