104

1 
\contentsline {chapter}{\numberline {1}Introduction}{1}


2 
\contentsline {section}{\numberline {1.1}Basic interaction with Isabelle}{1}


3 
\contentsline {section}{\numberline {1.2}Ending a session}{2}


4 
\contentsline {section}{\numberline {1.3}Reading files of proofs and theories}{2}


5 
\contentsline {section}{\numberline {1.4}Printing of terms and theorems}{2}


6 
\contentsline {subsection}{Printing limits}{3}


7 
\contentsline {subsection}{Printing of metalevel hypotheses}{3}


8 
\contentsline {subsection}{Printing of types and sorts}{3}


9 
\contentsline {subsection}{$\eta $contraction before printing}{3}


10 
\contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{4}


11 
\contentsline {section}{\numberline {1.6}Shell scripts}{4}


12 
\contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{6}


13 
\contentsline {section}{\numberline {2.1}Basic commands}{6}


14 
\contentsline {subsection}{Starting a backward proof}{6}


15 
\contentsline {subsection}{Applying a tactic}{7}


16 
\contentsline {subsection}{Extracting the proved theorem}{8}


17 
\contentsline {subsection}{Undoing and backtracking}{8}


18 
\contentsline {subsection}{Printing the proof state}{9}


19 
\contentsline {subsection}{Timing}{9}


20 
\contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{9}


21 
\contentsline {subsection}{Refining a given subgoal}{9}


22 
\contentsline {subsubsection}{Resolution with a list of theorems}{9}


23 
\contentsline {subsection}{Scanning shortcuts}{10}


24 
\contentsline {subsubsection}{Proof by assumption and resolution}{10}


25 
\contentsline {subsubsection}{Resolution with a list of theorems}{10}


26 
\contentsline {subsection}{Other shortcuts}{10}


27 
\contentsline {section}{\numberline {2.3}Advanced features}{11}


28 
\contentsline {subsection}{Executing batch proofs}{11}


29 
\contentsline {subsection}{Managing multiple proofs}{11}


30 
\contentsline {subsubsection}{The stack of proof states}{12}


31 
\contentsline {subsubsection}{Saving and restoring proof states}{12}


32 
\contentsline {subsection}{Debugging and inspecting}{12}


33 
\contentsline {subsubsection}{Reading and printing terms}{13}


34 
\contentsline {subsubsection}{Inspecting the proof state}{13}


35 
\contentsline {subsubsection}{Filtering lists of rules}{13}


36 
\contentsline {chapter}{\numberline {3}Tactics}{14}


37 
\contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{14}


38 
\contentsline {subsection}{Resolution tactics}{14}


39 
\contentsline {subsection}{Assumption tactics}{15}


40 
\contentsline {subsection}{Matching tactics}{15}


41 
\contentsline {subsection}{Resolution with instantiation}{15}


42 
\contentsline {section}{\numberline {3.2}Other basic tactics}{16}


43 
\contentsline {subsection}{Definitions and metalevel rewriting}{16}


44 
\contentsline {subsection}{Tactic shortcuts}{17}


45 
\contentsline {subsection}{Inserting premises and facts}{17}


46 
\contentsline {subsection}{Theorems useful with tactics}{18}


47 
\contentsline {section}{\numberline {3.3}Obscure tactics}{18}


48 
\contentsline {subsection}{Tidying the proof state}{18}


49 
\contentsline {subsection}{Renaming parameters in a goal}{18}


50 
\contentsline {subsection}{Composition: resolution without lifting}{19}


51 
\contentsline {section}{\numberline {3.4}Managing lots of rules}{19}


52 
\contentsline {subsection}{Combined resolution and elimresolution}{20}


53 
\contentsline {subsection}{Discrimination nets for fast resolution}{20}


54 
\contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{21}


55 
\contentsline {subsection}{Operations on type {\ptt tactic}}{22}


56 
\contentsline {subsection}{Tracing}{22}


57 
\contentsline {subsection}{Sequences}{23}


58 
\contentsline {subsubsection}{Basic operations on sequences}{23}


59 
\contentsline {subsubsection}{Converting between sequences and lists}{23}


60 
\contentsline {subsubsection}{Combining sequences}{23}


61 
\contentsline {chapter}{\numberline {4}Tacticals}{25}


62 
\contentsline {section}{\numberline {4.1}The basic tacticals}{25}


63 
\contentsline {subsection}{Joining two tactics}{25}


64 
\contentsline {subsection}{Joining a list of tactics}{25}


65 
\contentsline {subsection}{Repetition tacticals}{26}


66 
\contentsline {subsection}{Identities for tacticals}{26}


67 
\contentsline {section}{\numberline {4.2}Control and search tacticals}{27}


68 
\contentsline {subsection}{Filtering a tactic's results}{27}


69 
\contentsline {subsection}{Depthfirst search}{28}


70 
\contentsline {subsection}{Other search strategies}{28}


71 
\contentsline {subsection}{Auxiliary tacticals for searching}{29}


72 
\contentsline {subsection}{Predicates and functions useful for searching}{29}


73 
\contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{29}


74 
\contentsline {subsection}{Restricting a tactic to one subgoal}{30}


75 
\contentsline {subsection}{Scanning for a subgoal by number}{31}


76 
\contentsline {subsection}{Joining tactic functions}{32}


77 
\contentsline {subsection}{Applying a list of tactics to 1}{32}


78 
\contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{33}


79 
\contentsline {section}{\numberline {5.1}Basic operations on theorems}{33}


80 
\contentsline {subsection}{Prettyprinting a theorem}{33}


81 
\contentsline {subsubsection}{Toplevel commands}{33}


82 
\contentsline {subsubsection}{Operations for programming}{34}


83 
\contentsline {subsection}{Forwards proof: joining rules by resolution}{34}


84 
\contentsline {subsection}{Expanding definitions in theorems}{35}


85 
\contentsline {subsection}{Instantiating a theorem}{35}


86 
\contentsline {subsection}{Miscellaneous forward rules}{35}


87 
\contentsline {subsection}{Taking a theorem apart}{36}


88 
\contentsline {subsection}{Tracing flags for unification}{36}


89 
\contentsline {section}{\numberline {5.2}Primitive metalevel inference rules}{37}


90 
\contentsline {subsection}{Propositional rules}{38}


91 
\contentsline {subsubsection}{Assumption}{38}


92 
\contentsline {subsubsection}{Implication}{38}


93 
\contentsline {subsubsection}{Logical equivalence (equality)}{39}


94 
\contentsline {subsection}{Equality rules}{39}


95 
\contentsline {subsection}{The $\lambda $conversion rules}{39}


96 
\contentsline {subsection}{Universal quantifier rules}{40}


97 
\contentsline {subsubsection}{Forall introduction}{40}


98 
\contentsline {subsubsection}{Forall elimination}{40}


99 
\contentsline {subsubsection}{Instantiation of unknowns}{41}


100 
\contentsline {subsection}{Freezing/thawing type variables}{41}


101 
\contentsline {section}{\numberline {5.3}Derived rules for goaldirected proof}{41}


102 
\contentsline {subsection}{Proof by assumption}{41}


103 
\contentsline {subsection}{Resolution}{41}


104 
\contentsline {subsection}{Composition: resolution without lifting}{42}


105 
\contentsline {subsection}{Other metarules}{42}


106 
\contentsline {chapter}{\numberline {6}Theories, Terms and Types}{44}


107 
\contentsline {section}{\numberline {6.1}Defining Theories}{44}


108 
\contentsline {section}{\numberline {6.2}Basic operations on theories}{47}


109 
\contentsline {subsection}{Extracting an axiom from a theory}{47}


110 
\contentsline {subsection}{Building a theory}{47}


111 
\contentsline {subsection}{Inspecting a theory}{48}


112 
\contentsline {section}{\numberline {6.3}Terms}{49}


113 
\contentsline {section}{\numberline {6.4}Certified terms}{50}


114 
\contentsline {subsection}{Printing terms}{50}


115 
\contentsline {subsection}{Making and inspecting certified terms}{50}


116 
\contentsline {section}{\numberline {6.5}Types}{51}


117 
\contentsline {section}{\numberline {6.6}Certified types}{51}


118 
\contentsline {subsection}{Printing types}{51}


119 
\contentsline {subsection}{Making and inspecting certified types}{51}


120 
\contentsline {chapter}{\numberline {7}Substitution Tactics}{53}


121 
\contentsline {section}{\numberline {7.1}Simple substitution}{53}


122 
\contentsline {section}{\numberline {7.2}Substitution in the hypotheses}{54}


123 
\contentsline {section}{\numberline {7.3}Setting up {\ptt hyp_subst_tac}}{54}


124 
\contentsline {chapter}{\numberline {8}Simplification}{57}


125 
\contentsline {section}{\numberline {8.1}Simplification sets}{57}


126 
\contentsline {subsection}{Rewrite rules}{57}


127 
\contentsline {subsection}{Congruence rules}{58}


128 
\contentsline {subsection}{The subgoaler}{58}


129 
\contentsline {subsection}{The solver}{59}


130 
\contentsline {subsection}{The looper}{59}


131 
\contentsline {section}{\numberline {8.2}The simplification tactics}{59}


132 
\contentsline {section}{\numberline {8.3}Example: using the simplifier}{60}


133 
\contentsline {chapter}{\numberline {9}The classical theorem prover}{64}


134 
\contentsline {section}{\numberline {9.1}The sequent calculus}{64}


135 
\contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{65}


136 
\contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{66}


137 
\contentsline {section}{\numberline {9.4}Classical rule sets}{67}


138 
\contentsline {section}{\numberline {9.5}The classical tactics}{68}


139 
\contentsline {subsection}{Singlestep tactics}{69}


140 
\contentsline {subsection}{The automatic tactics}{69}


141 
\contentsline {subsection}{Other useful tactics}{69}


142 
\contentsline {subsection}{Creating swapped rules}{70}


143 
\contentsline {section}{\numberline {9.6}Setting up the classical prover}{70}
