Intro/document/advanced.tex

25 \section{Deriving rules in Isabelle}
26 \index{rules!derived}
28 stage defines some concepts and derives rules about them.  We shall see how
29 to derive rules, perhaps involving definitions, using Isabelle.  The
30 following section will explain how to declare types, constants, rules and
36 \index{examples!of deriving rules}\index{assumptions!of main goal}
38 The subgoal module supports the derivation of rules, as discussed in
122 \subsection{Definitions and derived rules} \label{definitions}
123 \index{rules!derived}\index{definitions!and derived rules|(}
141 When you define new concepts, you should derive rules asserting their
150 Isabelle provides tactics and meta-rules for rewriting, and a version of
155 peculiar.  Using Isabelle, we shall derive pleasanter negation rules:
265 \index{definitions!and derived rules|)}
282 translations {\it ast translation rules}
284 rules        {\it rule declarations}
290 (of existing types), constants and rules; it can specify the default
293 rewrite rules on abstract syntax trees, handling notations and
338 \subsection{Declaring constants, definitions and rules}
339 \indexbold{constants!declaring}\index{rules!declaring}
341 Most theories simply declare constants, definitions and rules.  The {\bf
359 rules   \(id@1\) "\(rule@1\)"
366 called \emph{rules} because they are mainly used to specify the inference
367 rules when defining a new logic.
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
510 %quotation marks!  Types and rules must be quoted because the theory
623 rules   fst     "fst(<a,b>) = a"
666 No rules are declared for these constants: we merely introduce their
668 with rules make it possible to prove {\bf generic} theorems.  Such
681 rules   add0        "0 + n = n::nat"
726 Similarly, to avoid expressing the other rules using~$\forall$, $\imp$
776 rules   Suc_inject  "Suc(m)=Suc(n) ==> m=n"
876 other rules of theory \texttt{Nat}.  The base case holds by~\ttindex{Suc_neq_0}:
890 Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
976 perhaps proving it.  For efficiency, the rewrite rules must be packaged into a
1000 simplification set, applying the rewrite rules for addition:
1042 The predicate $app$ should satisfy the Prolog-style rules
1054 rules of~\texttt{FOL}.
1063 rules   appNil  "app(Nil,ys,ys)"
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
1121 question has five solutions.  Using \ttindex{REPEAT} to apply the rules, we
1164 Bundle the rules together as the \ML{} identifier \texttt{rules}.  Naive
1174 val rules = [appNil,appCons,revNil,revCons];
1176 by (REPEAT (resolve_tac rules 1));
1190 by (REPEAT (resolve_tac rules 1));
1219                              (resolve_tac rules 1);