doc-src/Intro/advanced.tex
changeset 331 13660d5f6a77
parent 310 66fc71f3a347
child 348 1f5a94209c97
equal deleted inserted replaced
330:2fda15dd1e0f 331:13660d5f6a77
     7 theorems.  You probably should begin with first-order logic ({\tt FOL}
     7 theorems.  You probably should begin with first-order logic ({\tt FOL}
     8 or~{\tt LK}).  Try working some of the examples provided, and others from
     8 or~{\tt LK}).  Try working some of the examples provided, and others from
     9 the literature.  Set theory~({\tt ZF}) and Constructive Type Theory~({\tt
     9 the literature.  Set theory~({\tt ZF}) and Constructive Type Theory~({\tt
    10   CTT}) form a richer world for mathematical reasoning and, again, many
    10   CTT}) form a richer world for mathematical reasoning and, again, many
    11 examples are in the literature.  Higher-order logic~({\tt HOL}) is
    11 examples are in the literature.  Higher-order logic~({\tt HOL}) is
    12 Isabelle's most sophisticated logic, because its types and functions are
    12 Isabelle's most sophisticated logic because its types and functions are
    13 identified with those of the meta-logic; this may cause difficulties for
    13 identified with those of the meta-logic.
    14 beginners.
       
    15 
    14 
    16 Choose a logic that you already understand.  Isabelle is a proof
    15 Choose a logic that you already understand.  Isabelle is a proof
    17 tool, not a teaching tool; if you do not know how to do a particular proof
    16 tool, not a teaching tool; if you do not know how to do a particular proof
    18 on paper, then you certainly will not be able to do it on the machine.
    17 on paper, then you certainly will not be able to do it on the machine.
    19 Even experienced users plan large proofs on paper.
    18 Even experienced users plan large proofs on paper.
   111 \begin{eqnarray*}
   110 \begin{eqnarray*}
   112   \neg \Var{P}          & \equiv & \Var{P}\imp\bot \\
   111   \neg \Var{P}          & \equiv & \Var{P}\imp\bot \\
   113   \Var{P}\bimp \Var{Q}  & \equiv & 
   112   \Var{P}\bimp \Var{Q}  & \equiv & 
   114                 (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
   113                 (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
   115 \end{eqnarray*}
   114 \end{eqnarray*}
   116 \index{meta-rewriting}
   115 \index{meta-rewriting}%
   117 Isabelle permits {\bf meta-level rewriting} using definitions such as
   116 Isabelle permits {\bf meta-level rewriting} using definitions such as
   118 these.  {\bf Unfolding} replaces every instance
   117 these.  {\bf Unfolding} replaces every instance
   119 of $\neg \Var{P}$ by the corresponding instance of $\Var{P}\imp\bot$.  For
   118 of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$.  For
   120 example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to
   119 example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to
   121 \[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot.  \]
   120 \[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot.  \]
   122 {\bf Folding} a definition replaces occurrences of the right-hand side by
   121 {\bf Folding} a definition replaces occurrences of the right-hand side by
   123 the left.  The occurrences need not be free in the entire formula.
   122 the left.  The occurrences need not be free in the entire formula.
   124 
   123 
   125 When you define new concepts, you should derive rules asserting their
   124 When you define new concepts, you should derive rules asserting their
   126 abstract properties, and then forget their definitions.  This supports
   125 abstract properties, and then forget their definitions.  This supports
   127 modularity: if you later change the definitions, without affecting their
   126 modularity: if you later change the definitions without affecting their
   128 abstract properties, then most of your proofs will carry through without
   127 abstract properties, then most of your proofs will carry through without
   129 change.  Indiscriminate unfolding makes a subgoal grow exponentially,
   128 change.  Indiscriminate unfolding makes a subgoal grow exponentially,
   130 becoming unreadable.
   129 becoming unreadable.
   131 
   130 
   132 Taking this point of view, Isabelle does not unfold definitions
   131 Taking this point of view, Isabelle does not unfold definitions
   334 an entire logic.  A theory definition has the form
   333 an entire logic.  A theory definition has the form
   335 \begin{ttbox}
   334 \begin{ttbox}
   336 \(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
   335 \(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
   337 classes      {\it class declarations}
   336 classes      {\it class declarations}
   338 default      {\it sort}
   337 default      {\it sort}
   339 types        {\it type declarations}
   338 types        {\it type declarations and synonyms}
   340 arities      {\it arity declarations}
   339 arities      {\it arity declarations}
   341 consts       {\it constant declarations}
   340 consts       {\it constant declarations}
   342 rules        {\it rule declarations}
   341 rules        {\it rule declarations}
   343 translations {\it translation declarations}
   342 translations {\it translation declarations}
   344 end
   343 end
   359 All the declaration parts can be omitted.  In the simplest case, $T$ is
   358 All the declaration parts can be omitted.  In the simplest case, $T$ is
   360 just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
   359 just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
   361 or more other theories, inheriting their types, constants, syntax, etc.
   360 or more other theories, inheriting their types, constants, syntax, etc.
   362 The theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
   361 The theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
   363 
   362 
   364 Each theory definition must reside in a separate file, whose name is
   363 Each theory definition must reside in a separate file, whose name is the
   365 determined as follows: the theory name, say {\tt ListFn}, is converted to
   364 theory's with {\tt.thy} appended.  For example, theory {\tt ListFn} resides
   366 lower case and {\tt.thy} is appended, yielding the filename {\tt
   365 on a file named {\tt ListFn.thy}.  Isabelle uses this convention to locate the
   367   listfn.thy}.  Isabelle uses this convention to locate the file containing
   366 file containing a given theory; \ttindexbold{use_thy} automatically loads a
   368 a given theory; \ttindexbold{use_thy} automatically loads a theory's
   367 theory's parents before loading the theory itself.
   369 parents before loading the theory itself.
   368 
   370 
   369 Calling \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads a theory from the
   371 Calling \ttindexbold{use_thy}~{\tt"}{\it T\/}{\tt"} reads a theory from the
   370 file {\it T}{\tt.thy}, writes the corresponding {\ML} code to the file
   372 file {\it t}{\tt.thy}, writes the corresponding {\ML} code to the file
   371 {\tt.{\it T}.thy.ML}, reads the latter file, and deletes it if no errors
   373 {\tt.}{\it t}{\tt.thy.ML}, reads the latter file, and deletes it if no errors
   372 occurred.  This declares the {\ML} structure~$T$, which contains a component
   374 occured.  This declares the {\ML} structure~$T$, which contains a component
       
   375 {\tt thy} denoting the new theory, a component for each rule, and everything
   373 {\tt thy} denoting the new theory, a component for each rule, and everything
   376 declared in {\it ML code}.
   374 declared in {\it ML code}.
   377 
   375 
   378 Errors may arise during the translation to {\ML} (say, a misspelled keyword)
   376 Errors may arise during the translation to {\ML} (say, a misspelled keyword)
   379 or during creation of the new theory (say, a type error in a rule).  But if
   377 or during creation of the new theory (say, a type error in a rule).  But if
   380 all goes well, {\tt use_thy} will finally read the file {\it t}{\tt.ML}, if
   378 all goes well, {\tt use_thy} will finally read the file {\it T}{\tt.ML}, if
   381 it exists.  This file typically begins with the {\ML} declaration {\tt
   379 it exists.  This file typically begins with the {\ML} declaration {\tt
   382 open}~$T$ and contains proofs that refer to the components of~$T$.
   380 open}~$T$ and contains proofs that refer to the components of~$T$.
   383 
   381 
   384 When a theory file is modified, many theories may have to be reloaded.
   382 When a theory file is modified, many theories may have to be reloaded.
   385 Isabelle records the modification times and dependencies of theory files.
   383 Isabelle records the modification times and dependencies of theory files.
   386 See the {\em Reference Manual\/}
   384 See 
   387 \iflabelundefined{sec:reloading-theories}{}{(\S\ref{sec:reloading-theories})}
   385 \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
       
   386                  {\S\ref{sec:reloading-theories}}
   388 for more details.
   387 for more details.
   389 
   388 
   390 
   389 
   391 \subsection{Declaring constants and rules}
   390 \subsection{Declaring constants and rules}
   392 \indexbold{constants!declaring}\index{rules!declaring}
   391 \indexbold{constants!declaring}\index{rules!declaring}
   489 $(term)term$ is short for $(\{term\})term$.  Recall the discussion in
   488 $(term)term$ is short for $(\{term\})term$.  Recall the discussion in
   490 \S\ref{polymorphic}.
   489 \S\ref{polymorphic}.
   491 
   490 
   492 A type constructor may be overloaded (subject to certain conditions) by
   491 A type constructor may be overloaded (subject to certain conditions) by
   493 appearing in several arity declarations.  For instance, the function type
   492 appearing in several arity declarations.  For instance, the function type
   494 constructor~$\To$ has the arity $(logic,logic)logic$; in higher-order
   493 constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order
   495 logic, it is declared also to have arity $(term,term)term$.
   494 logic, it is declared also to have arity $(term,term)term$.
   496 
   495 
   497 Theory {\tt List} declares the 1-place type constructor $list$, gives
   496 Theory {\tt List} declares the 1-place type constructor $list$, gives
   498 it arity $(term)term$, and declares constants $Nil$ and $Cons$ with
   497 it arity $(term)term$, and declares constants $Nil$ and $Cons$ with
   499 polymorphic types:%
   498 polymorphic types:%
   519 Arity declarations resemble constant declarations, but there are {\it no\/}
   518 Arity declarations resemble constant declarations, but there are {\it no\/}
   520 quotation marks!  Types and rules must be quoted because the theory
   519 quotation marks!  Types and rules must be quoted because the theory
   521 translator passes them verbatim to the {\ML} output file.
   520 translator passes them verbatim to the {\ML} output file.
   522 \end{warn}
   521 \end{warn}
   523 
   522 
   524 \subsection{Type synonyms}\indexbold{types!synonyms}
   523 \subsection{Type synonyms}\indexbold{type synonyms}
   525 Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
   524 Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
   526 to those found in \ML.  Such synonyms are defined in the type declaration part
   525 to those found in \ML.  Such synonyms are defined in the type declaration part
   527 and are fairly self explanatory:
   526 and are fairly self explanatory:
   528 \begin{ttbox}
   527 \begin{ttbox}
   529 types gate       = "[o,o] => o"
   528 types gate       = "[o,o] => o"
   789 \begin{ttbox}
   788 \begin{ttbox}
   790 open Nat;
   789 open Nat;
   791 \end{ttbox}
   790 \end{ttbox}
   792 
   791 
   793 \subsection{Proving some recursion equations}
   792 \subsection{Proving some recursion equations}
   794 File {\tt FOL/ex/nat.ML} contains proofs involving this theory of the
   793 File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the
   795 natural numbers.  As a trivial example, let us derive recursion equations
   794 natural numbers.  As a trivial example, let us derive recursion equations
   796 for \verb$+$.  Here is the zero case:
   795 for \verb$+$.  Here is the zero case:
   797 \begin{ttbox}
   796 \begin{ttbox}
   798 goalw Nat.thy [add_def] "0+n = n";
   797 goalw Nat.thy [add_def] "0+n = n";
   799 {\out Level 0}
   798 {\out Level 0}
   967 
   966 
   968 The main goal admits fourteen different applications of induction.  The
   967 The main goal admits fourteen different applications of induction.  The
   969 number is exponential in the size of the formula.
   968 number is exponential in the size of the formula.
   970 
   969 
   971 \subsection{Proving that addition is associative}
   970 \subsection{Proving that addition is associative}
   972 Let us invoke the induction rule properly properly, using~{\tt
   971 Let us invoke the induction rule properly, using~{\tt
   973   res_inst_tac}.  At the same time, we shall have a glimpse at Isabelle's
   972   res_inst_tac}.  At the same time, we shall have a glimpse at Isabelle's
   974 simplification tactics, which are described in 
   973 simplification tactics, which are described in 
   975 \iflabelundefined{simp-chap}%
   974 \iflabelundefined{simp-chap}%
   976     {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.
   975     {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.
   977 
   976 
   979 
   978 
   980 Isabelle's simplification tactics repeatedly apply equations to a subgoal,
   979 Isabelle's simplification tactics repeatedly apply equations to a subgoal,
   981 perhaps proving it.  For efficiency, the rewrite rules must be
   980 perhaps proving it.  For efficiency, the rewrite rules must be
   982 packaged into a {\bf simplification set},\index{simplification sets} 
   981 packaged into a {\bf simplification set},\index{simplification sets} 
   983 or {\bf simpset}.  We take the standard simpset for first-order logic and
   982 or {\bf simpset}.  We take the standard simpset for first-order logic and
   984 insert the equations for~{\tt add} proved in the previous section, namely
   983 insert the equations proved in the previous section, namely
   985 $0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
   984 $0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
   986 \begin{ttbox}
   985 \begin{ttbox}
   987 val add_ss = FOL_ss addrews [add_0, add_Suc];
   986 val add_ss = FOL_ss addrews [add_0, add_Suc];
   988 \end{ttbox}
   987 \end{ttbox}
   989 We state the goal for associativity of addition, and
   988 We state the goal for associativity of addition, and
  1001 {\out  2. !!x. x + m + n = x + (m + n) ==>}
  1000 {\out  2. !!x. x + m + n = x + (m + n) ==>}
  1002 {\out          Suc(x) + m + n = Suc(x) + (m + n)}
  1001 {\out          Suc(x) + m + n = Suc(x) + (m + n)}
  1003 \end{ttbox}
  1002 \end{ttbox}
  1004 The base case holds easily; both sides reduce to $m+n$.  The
  1003 The base case holds easily; both sides reduce to $m+n$.  The
  1005 tactic~\ttindex{simp_tac} rewrites with respect to the given simplification
  1004 tactic~\ttindex{simp_tac} rewrites with respect to the given simplification
  1006 set, applying the rewrite rules for~{\tt +}:
  1005 set, applying the rewrite rules for addition:
  1007 \begin{ttbox}
  1006 \begin{ttbox}
  1008 by (simp_tac add_ss 1);
  1007 by (simp_tac add_ss 1);
  1009 {\out Level 2}
  1008 {\out Level 2}
  1010 {\out k + m + n = k + (m + n)}
  1009 {\out k + m + n = k + (m + n)}
  1011 {\out  1. !!x. x + m + n = x + (m + n) ==>}
  1010 {\out  1. !!x. x + m + n = x + (m + n) ==>}
  1012 {\out          Suc(x) + m + n = Suc(x) + (m + n)}
  1011 {\out          Suc(x) + m + n = Suc(x) + (m + n)}
  1013 \end{ttbox}
  1012 \end{ttbox}
  1014 The inductive step requires rewriting by the equations for~{\tt add}
  1013 The inductive step requires rewriting by the equations for addition
  1015 together the induction hypothesis, which is also an equation.  The
  1014 together the induction hypothesis, which is also an equation.  The
  1016 tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any
  1015 tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any
  1017 useful assumptions:
  1016 useful assumptions:
  1018 \begin{ttbox}
  1017 \begin{ttbox}
  1019 by (asm_simp_tac add_ss 1);
  1018 by (asm_simp_tac add_ss 1);
  1026 
  1025 
  1027 \section{A Prolog interpreter}
  1026 \section{A Prolog interpreter}
  1028 \index{Prolog interpreter|bold}
  1027 \index{Prolog interpreter|bold}
  1029 To demonstrate the power of tacticals, let us construct a Prolog
  1028 To demonstrate the power of tacticals, let us construct a Prolog
  1030 interpreter and execute programs involving lists.\footnote{To run these
  1029 interpreter and execute programs involving lists.\footnote{To run these
  1031 examples, see the file {\tt FOL/ex/prolog.ML}.} The Prolog program
  1030 examples, see the file {\tt FOL/ex/Prolog.ML}.} The Prolog program
  1032 consists of a theory.  We declare a type constructor for lists, with an
  1031 consists of a theory.  We declare a type constructor for lists, with an
  1033 arity declaration to say that $(\tau)list$ is of class~$term$
  1032 arity declaration to say that $(\tau)list$ is of class~$term$
  1034 provided~$\tau$ is:
  1033 provided~$\tau$ is:
  1035 \begin{eqnarray*}
  1034 \begin{eqnarray*}
  1036   list  & :: & (term)term
  1035   list  & :: & (term)term
  1197 {\out Level 1}
  1196 {\out Level 1}
  1198 {\out rev(?x1 : Nil, a : b : c : Nil)}
  1197 {\out rev(?x1 : Nil, a : b : c : Nil)}
  1199 {\out  1. app(Nil, ?x1 : Nil, a : b : c : Nil)}
  1198 {\out  1. app(Nil, ?x1 : Nil, a : b : c : Nil)}
  1200 \end{ttbox}
  1199 \end{ttbox}
  1201 The tactic has failed to find a solution!  It reached a dead end at
  1200 The tactic has failed to find a solution!  It reached a dead end at
  1202 subgoal~1: there is no~$\Var{x1}$ such that [] appended with~$[\Var{x1}]$
  1201 subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$
  1203 equals~$[a,b,c]$.  Backtracking explores other outcomes.
  1202 equals~$[a,b,c]$.  Backtracking explores other outcomes.
  1204 \begin{ttbox}
  1203 \begin{ttbox}
  1205 back();
  1204 back();
  1206 {\out Level 1}
  1205 {\out Level 1}
  1207 {\out rev(?x1 : a : Nil, a : b : c : Nil)}
  1206 {\out rev(?x1 : a : Nil, a : b : c : Nil)}