3 Isabelle, reinforcing your knowledge of the basic functions.
7 (\texttt{FOL} or~\texttt{LK}).  Try working some of the examples provided,
8 and others from the literature.  Set theory~(\texttt{ZF}) and
10 mathematical reasoning and, again, many examples are in the
13 the meta-logic.
17 on paper, then you certainly will not be able to do it on the machine.
20 We have covered only the bare essentials of Isabelle, but enough to perform
21 substantial proofs.  By occasionally dipping into the {\em Reference
38 The subgoal module supports the derivation of rules, as discussed in
39 \S\ref{deriving}.  When the \ttindex{Goal} command is supplied a formula of
40 the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, there are two
43 \item If all of the premises $\theta@1$, \ldots, $\theta@k$ are simple
44   formulae{} (they do not involve the meta-connectives $\Forall$ or
45   $\Imp$) then the command sets the goal to be 
46   $\List{\theta@1; \ldots; \theta@k} \Imp \phi$ and returns the empty list.
47 \item If one or more premises involves the meta-connectives $\Forall$ or
48   $\Imp$, then the command sets the goal to be $\phi$ and returns a list
49   consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.
51   \texttt{result} (which is called by \texttt{qed}) to discharge them in the
55 premises, and the second case applies.  In this section, many of the
56 theorems are subject to meta-level assumptions, so we make them visible by by setting the 
64 returned an empty list, which we have ignored.  In this example, the list
65 contains the two premises of the rule, since one of them involves the $\Imp$
66 connective.  We bind them to the \ML\ identifiers \texttt{major} and {\tt
69   list.  Otherwise, the pattern-match will fail; ML will raise exception
80 Look at the minor premise, recalling that meta-level assumptions are
81 shown in brackets.  Using \texttt{minor}, we reduce $R$ to the subgoals
90 Deviating from~\S\ref{deriving}, we apply $({\conj}E1)$ forwards from the
91 assumption $P\conj Q$ to obtain the theorem~$P\;[P\conj Q]$.
101 Similarly, we solve the subgoal involving~$Q$.
110 Calling \ttindex{topthm} returns the current proof state as a theorem.
112 the assumptions --- both occurrences of $P\conj Q$ are discharged as
113 one --- and makes the variables schematic.
126 and the if-and-only-if connective:
135 of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$.  For
138 {\bf Folding} a definition replaces occurrences of the right-hand side by
139 the left.  The occurrences need not be free in the entire formula.
143 modularity: if you later change the definitions without affecting their
151 the \texttt{Goal} command that unfolds the conclusion and premises of the rule
154 For example, the intuitionistic definition of negation given above may seem
158 This requires proving the following meta-formulae:
163 \subsection{Deriving the $\neg$ introduction rule}
164 To derive $(\neg I)$, we may call \texttt{Goal} with the appropriate formula.
165 Again, the rule's premises involve a meta-connective, and \texttt{Goal}
166 returns one-element list.  We bind this list to the \ML\ identifier \texttt{prems}.
174 Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the
175 definition of negation, unfolds that definition in the subgoals.  It leaves
176 the main goal alone.
185 Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality:
197 The rest of the proof is routine.  Note the form of the final result.
223 \subsection{Deriving the $\neg$ elimination rule}
224 Let us derive the rule $(\neg E)$.  The proof follows that of~\texttt{conjE}
225 above, with an additional step to unfold negation in the major premise.
227 in the conclusion but the premises.
234 As the first step, we apply \tdx{FalseE}:
242 Everything follows from falsity.  And we can prove falsity using the
261 \texttt{Goalw} unfolds definitions in the premises even when it has to return
263 applying the function \ttindex{rewrite_rule}.
288 This declares the theory $T$ to extend the existing theories
290 (of existing types), constants and rules; it can specify the default
297 not presented here, the full syntax can be found in
298 \iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference
303 All the declaration parts can be omitted or repeated and may appear in
304 any order, except that the {\ML} section must be last (after the {\tt
305   end} keyword).  In the simplest case, $T$ is just the union of
309 \thydx{CPure} offers the more usual higher-order function application
313 the theory's with {\tt.thy} appended.  Calling
314 \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it
316     T}.thy.ML}, reads the latter file, and deletes it if no errors
317 occurred.  This declares the {\ML} structure~$T$, which contains a
318 component \texttt{thy} denoting the new theory, a component for each
321 Errors may arise during the translation to {\ML} (say, a misspelled
322 keyword) or during creation of the new theory (say, a type error in a
323 rule).  But if all goes well, \texttt{use_thy} will finally read the file
325 that refer to the components of~$T$.  The structure is automatically
330 loading the theory itself.  When a theory file is modified, many
331 theories may have to be reloaded.  Isabelle records the modification
333 \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
342   constant declaration part} has the form
353 the $n$ declarations may be abbreviated to a single line:
357 The {\bf rule declaration part} has the form
366 called \emph{rules} because they are mainly used to specify the inference
370 the keyword \texttt{defs} instead of \texttt{rules}.  {\bf Definitions} are
371 rules of the form $s \equiv t$, and should serve only as
374 this, where the arguments of~$f$ appear applied on the left-hand side
375 of the equation instead of abstracted on the right-hand side.
378 variables on the right-hand side and cyclic dependencies, that could
380 theorems proved on the basis of incorrect definitions are useless,
403 \texttt{constdefs} generates the names \texttt{nand_def} and \texttt{xor_def}
405 general it has the form
417 on the right-hand side as in the following fictitious definition:
421 Isabelle rejects this ``definition'' because of the extra \texttt{m} on the
443 The {\bf type declaration part} has the general form
450 are type argument lists as shown in the example above.  It declares each
451 $id@i$ as a type constructor with the specified number of argument places.
453 The {\bf arity declaration part} has the form
461 types; they do not declare the types themselves.
462 In the simplest case, for an 0-place type constructor, an arity is simply
463 the type's class.  Let us declare a type~$bool$ of class $term$, with
474 A $k$-place type constructor may have arities of the form
476 Each sort specifies a type argument; it has the form $\{c@1,\ldots,c@m\}$,
478 sorts, and may abbreviate them by dropping the braces.  The arity
479 $(term)term$ is short for $(\{term\})term$.  Recall the discussion in
483 appearing in several arity declarations.  For instance, the function type
484 constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order
487 Theory \texttt{List} declares the 1-place type constructor $list$, gives
488 it the arity $(term)term$, and declares constants $Nil$ and $Cons$ with
490 \footnote{In the \texttt{consts} part, type variable {\tt'a} has the default
491   sort, which is \texttt{term}.  See the {\em Reference Manual\/}
510 %quotation marks!  Types and rules must be quoted because the theory
511 %translator passes them verbatim to the {\ML} output file.
516 to those found in \ML.  Such synonyms are defined in the type declaration part
533 synonyms.  Their main purpose is to improve the readability of theory
543 Infix or mixfix syntax may be attached to constants.  Consider the
556 \xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$.  Note the quotation
561 \verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda
572 add a line to the constant declaration part:
580 The declaration above does not allow the \texttt{if}-\texttt{then}-{\tt
583 added to specify the layout of mixfix operators.  For details, see
585     {the {\it Reference Manual}, chapter `Defining Logics'}%
594 defines, for each argument position, the minimal priority an expression
595 at that position must have.  The final integer is the priority of the
596 construct itself.  In the example above, any argument expression is
598 appear everywhere because 1000 is the highest priority.  On the other
599 hand, the declaration
604 the form \texttt{if~$P$ then~$Q$ else~$R$} because it must have a priority
613 infix notation $\alpha*\beta$, together with the mixfix notation
629   The name of the type constructor is~\texttt{*} and not \texttt{op~*}, as
630   it would be in the case of an infix constant.  Only infix type
639 The {\bf class declaration part} has the form
647 of~$c@i$.  In the general case, an identifier may be declared to be a
653 \S\ref{polymorphic}, let us define the class $arith$ of arithmetic
654 types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::}
656 $term$ and add the three polymorphic constants of this class.
667 names without specifying properties.  On the other hand, classes
671 We can now obtain distinct versions of the constants of $arith$ by
673 declare the 0-place type constructors $bool$ and $nat$:
691 either type.  The type constraints in the axioms are vital.  Without
692 constraints, the $x$ in $1+x = 1$ (axiom \texttt{or1l})
694 and the axiom would hold for any type of class $arith$.  This would
699 \section{Theory example: the natural numbers}
702 demonstrating many of the theory extension features.
705 \subsection{Extending first-order logic with the natural numbers}
709 including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
710 Let us introduce the Peano axioms for mathematical induction and the
720 Some authors express the induction step as $\forall x. P(x)\imp P(Suc(x))$.
721 To avoid making induction require the presence of other connectives, we
726 Similarly, to avoid expressing the other rules using~$\forall$, $\imp$
727 and~$\neg$, we take advantage of the meta-logic;\footnote
728 {On the other hand, the axioms $Suc(m)=Suc(n) \bimp m=n$
739 and obeys the equations
751 function-valued expressions.  We again take advantage of the meta-logic,
753 polymorphic over any type of class~$term$, and declare the addition
761 \subsection{Declaring the theory to Isabelle}
763 Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$,
765 the 0-place type constructor $nat$ and the associated constants.  Note that
766 the constant~0 requires a mixfix annotation because~0 is not a legal
785 Loading this theory file creates the \ML\ structure \texttt{Nat}, which
786 contains the theory and axioms.
789 Theory \texttt{FOL/ex/Nat} contains proofs involving this theory of the
791 for \verb$+$.  Here is the zero case:
804 And here is the successor case:
826 the rule~$(induct)$.  The conclusion of this rule is $\Var{P}(\Var{n})$,
829 To get round this problem, we could make the induction rule conclude
834 a rule.  But it also accepts explicit instantiations for the rule's
838 instantiates the rule {\it thm} with the instantiations {\it insts}, and
846 where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule ---
849 in the context of a particular subgoal: free variables receive the same
850 types as they have in the subgoal, and parameters may appear.  Type
853 whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$.
873 is the base case, with $k$ replaced by~0.  Subgoal~2 is the inductive step,
875 The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the
889 The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
890 Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
912 If you try the example above, you may observe that \texttt{res_inst_tac} is
913 not actually needed.  Almost by chance, \ttindex{resolve_tac} finds the right
914 instantiation for~$(induct)$ to yield the desired next state.  With more
929 indicates that induction has been applied to the term~$k+(m+n)$; this
931 Isabelle can (lazily!) generate all the valid applications of induction.
933 the tactic.
951 Now induction has been applied to~$n$.  What is the next alternative?
959 Inspecting subgoal~1 reveals that induction has been applied to just the
964 number is exponential in the size of the formula.
967 Let us invoke the induction rule properly, using~{\tt
968   res_inst_tac}.  At the same time, we shall have a glimpse at Isabelle's
971     {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.
976 perhaps proving it.  For efficiency, the rewrite rules must be packaged into a
978 augment the implicit simpset of FOL with the equations proved in the previous
983 We state the goal for associativity of addition, and
999 tactic~\ttindex{Simp_tac} rewrites with respect to the current
1000 simplification set, applying the rewrite rules for addition:
1008 The inductive step requires rewriting by the equations for addition
1009 and with the induction hypothesis, which is also an equation.  The
1010 tactic~\ttindex{Asm_simp_tac} rewrites using the implicit
1023 To demonstrate the power of tacticals, let us construct a Prolog
1025 examples, see the file \texttt{FOL/ex/Prolog.ML}.} The Prolog program
1032 We declare four constants: the empty list~$Nil$; the infix list
1033 constructor~{:}; the list concatenation predicate~$app$; the list reverse
1042 The predicate $app$ should satisfy the Prolog-style rules
1045 We define the naive version of $rev$, which calls~$app$:
1053 of the class~$term$ and the type~$o$.  The interpreter does not use the
1070 Repeated application of the rules solves Prolog goals.  Let us
1071 append the lists $[a,b,c]$ and~$[d,e]$.  As the rules are applied, the
1089 At this point, the first two elements of the result are~$a$ and~$b$.
1104 Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$:
1120 Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$?  This
1121 question has five solutions.  Using \ttindex{REPEAT} to apply the rules, we
1122 quickly find the first solution, namely $x=[]$ and $y=[a,b,c,d]$:
1134 Isabelle can lazily generate all the possibilities.  The \ttindex{back}
1135 command returns the tactic's next outcome, namely $x=[a]$ and $y=[b,c,d]$:
1164 Bundle the rules together as the \ML{} identifier \texttt{rules}.  Naive
1165 reverse requires 120 inferences for this 14-element list, but the tactic
1183 is the reverse of $[a,b,c]$?
1204 This too is a dead end, but the next outcome is successful.
1215 \ttindex{has_fewer_prems} specifies that the proof state should have no
1222 Prolog interpreter.  We return to the start of the proof using

Indexes created Sun Jun 23 19:15:37 MDT 2024