7 theorems. You probably should begin with firstorder logic ({\tt FOL} 
7 theorems. You probably should begin with firstorder 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. Higherorder logic~({\tt HOL}) is 
11 examples are in the literature. Higherorder 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 metalogic; this may cause difficulties for 
13 identified with those of the metalogic. 
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{metarewriting} 
115 \index{metarewriting}% 
117 Isabelle permits {\bf metalevel rewriting} using definitions such as 
116 Isabelle permits {\bf metalevel 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 righthand side by 
121 {\bf Folding} a definition replaces occurrences of the righthand 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 metalogic. 
361 The theory \thydx{Pure} contains nothing but Isabelle's metalogic. 
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:reloadingtheories}{}{(\S\ref{sec:reloadingtheories})} 
385 \iflabelundefined{sec:reloadingtheories}{the {\em Reference Manual\/}}% 

386 {\S\ref{sec:reloadingtheories}} 
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 higherorder 
493 constructor~$fun$ has the arity $(logic,logic)logic$; in higherorder 
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 1place type constructor $list$, gives 
496 Theory {\tt List} declares the 1place 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" 
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{simpchap}% 
974 \iflabelundefined{simpchap}% 
976 {the {\em Reference Manual}}{Chap.\ts\ref{simpchap}}. 
975 {the {\em Reference Manual}}{Chap.\ts\ref{simpchap}}. 
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 firstorder logic and 
982 or {\bf simpset}. We take the standard simpset for firstorder 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 interpreterbold} 
1027 \index{Prolog interpreterbold} 
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)} 