359

1 
\contentsline {chapter}{\numberline {1}Basic Use of Isabelle}{1}

104

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


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

359

4 
\contentsline {section}{\numberline {1.3}Reading ML files}{2}


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


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


7 
\contentsline {subsection}{Printing of hypotheses, types and sorts}{3}


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


9 
\contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{3}


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


11 
\contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{5}


12 
\contentsline {section}{\numberline {2.1}Basic commands}{5}


13 
\contentsline {subsection}{Starting a backward proof}{5}


14 
\contentsline {subsection}{Applying a tactic}{6}


15 
\contentsline {subsection}{Extracting the proved theorem}{7}


16 
\contentsline {subsection}{Undoing and backtracking}{7}


17 
\contentsline {subsection}{Printing the proof state}{8}


18 
\contentsline {subsection}{Timing}{8}


19 
\contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{8}


20 
\contentsline {subsection}{Refining a given subgoal}{8}


21 
\contentsline {subsection}{Scanning shortcuts}{9}


22 
\contentsline {subsection}{Other shortcuts}{9}


23 
\contentsline {section}{\numberline {2.3}Executing batch proofs}{9}


24 
\contentsline {section}{\numberline {2.4}Managing multiple proofs}{10}


25 
\contentsline {subsection}{The stack of proof states}{11}


26 
\contentsline {subsection}{Saving and restoring proof states}{11}


27 
\contentsline {section}{\numberline {2.5}Debugging and inspecting}{11}


28 
\contentsline {subsection}{Reading and printing terms}{11}


29 
\contentsline {subsection}{Inspecting the proof state}{12}


30 
\contentsline {subsection}{Filtering lists of rules}{12}


31 
\contentsline {chapter}{\numberline {3}Tactics}{13}


32 
\contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{13}


33 
\contentsline {subsection}{Resolution tactics}{13}


34 
\contentsline {subsection}{Assumption tactics}{14}


35 
\contentsline {subsection}{Matching tactics}{14}


36 
\contentsline {subsection}{Resolution with instantiation}{14}


37 
\contentsline {section}{\numberline {3.2}Other basic tactics}{15}


38 
\contentsline {subsection}{Definitions and metalevel rewriting}{15}


39 
\contentsline {subsection}{Tactic shortcuts}{16}


40 
\contentsline {subsection}{Inserting premises and facts}{16}


41 
\contentsline {subsection}{Theorems useful with tactics}{17}


42 
\contentsline {section}{\numberline {3.3}Obscure tactics}{17}


43 
\contentsline {subsection}{Tidying the proof state}{17}


44 
\contentsline {subsection}{Renaming parameters in a goal}{17}


45 
\contentsline {subsection}{Composition: resolution without lifting}{18}


46 
\contentsline {section}{\numberline {3.4}Managing lots of rules}{18}


47 
\contentsline {subsection}{Combined resolution and elimresolution}{19}


48 
\contentsline {subsection}{Discrimination nets for fast resolution}{19}


49 
\contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{20}


50 
\contentsline {subsection}{Operations on type {\ptt tactic}}{21}


51 
\contentsline {subsection}{Tracing}{21}


52 
\contentsline {section}{\numberline {3.6}Sequences}{22}


53 
\contentsline {subsection}{Basic operations on sequences}{22}


54 
\contentsline {subsection}{Converting between sequences and lists}{22}


55 
\contentsline {subsection}{Combining sequences}{22}


56 
\contentsline {chapter}{\numberline {4}Tacticals}{24}


57 
\contentsline {section}{\numberline {4.1}The basic tacticals}{24}


58 
\contentsline {subsection}{Joining two tactics}{24}


59 
\contentsline {subsection}{Joining a list of tactics}{24}


60 
\contentsline {subsection}{Repetition tacticals}{25}


61 
\contentsline {subsection}{Identities for tacticals}{25}


62 
\contentsline {section}{\numberline {4.2}Control and search tacticals}{26}


63 
\contentsline {subsection}{Filtering a tactic's results}{26}


64 
\contentsline {subsection}{Depthfirst search}{26}


65 
\contentsline {subsection}{Other search strategies}{27}


66 
\contentsline {subsection}{Auxiliary tacticals for searching}{27}


67 
\contentsline {subsection}{Predicates and functions useful for searching}{28}


68 
\contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{28}


69 
\contentsline {subsection}{Restricting a tactic to one subgoal}{28}


70 
\contentsline {subsection}{Scanning for a subgoal by number}{29}


71 
\contentsline {subsection}{Joining tactic functions}{30}


72 
\contentsline {subsection}{Applying a list of tactics to 1}{31}


73 
\contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{32}


74 
\contentsline {section}{\numberline {5.1}Basic operations on theorems}{32}


75 
\contentsline {subsection}{Prettyprinting a theorem}{32}


76 
\contentsline {subsection}{Forward proof: joining rules by resolution}{33}


77 
\contentsline {subsection}{Expanding definitions in theorems}{33}


78 
\contentsline {subsection}{Instantiating a theorem}{34}


79 
\contentsline {subsection}{Miscellaneous forward rules}{34}


80 
\contentsline {subsection}{Taking a theorem apart}{35}


81 
\contentsline {subsection}{Tracing flags for unification}{35}


82 
\contentsline {section}{\numberline {5.2}Primitive metalevel inference rules}{36}


83 
\contentsline {subsection}{Assumption rule}{37}


84 
\contentsline {subsection}{Implication rules}{37}


85 
\contentsline {subsection}{Logical equivalence rules}{38}


86 
\contentsline {subsection}{Equality rules}{38}


87 
\contentsline {subsection}{The $\lambda $conversion rules}{38}


88 
\contentsline {subsection}{Forall introduction rules}{39}


89 
\contentsline {subsection}{Forall elimination rules}{39}


90 
\contentsline {subsection}{Instantiation of unknowns}{39}


91 
\contentsline {subsection}{Freezing/thawing type unknowns}{40}


92 
\contentsline {section}{\numberline {5.3}Derived rules for goaldirected proof}{40}


93 
\contentsline {subsection}{Proof by assumption}{40}


94 
\contentsline {subsection}{Resolution}{40}


95 
\contentsline {subsection}{Composition: resolution without lifting}{40}


96 
\contentsline {subsection}{Other metarules}{41}


97 
\contentsline {chapter}{\numberline {6}Theories, Terms and Types}{42}


98 
\contentsline {section}{\numberline {6.1}Defining theories}{42}


99 
\contentsline {subsection}{*Classes and arities}{44}


100 
\contentsline {section}{\numberline {6.2}Loading a new theory}{44}


101 
\contentsline {section}{\numberline {6.3}Reloading modified theories}{45}


102 
\contentsline {subsection}{Important note for Poly/ML users}{45}


103 
\contentsline {subsection}{*Pseudo theories}{46}


104 
\contentsline {section}{\numberline {6.4}Basic operations on theories}{47}


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


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


107 
\contentsline {subsection}{Inspecting a theory}{47}


108 
\contentsline {section}{\numberline {6.5}Terms}{48}


109 
\contentsline {section}{\numberline {6.6}Variable binding}{49}


110 
\contentsline {section}{\numberline {6.7}Certified terms}{50}


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


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


113 
\contentsline {section}{\numberline {6.8}Types}{50}


114 
\contentsline {section}{\numberline {6.9}Certified types}{51}


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


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


117 
\contentsline {chapter}{\numberline {7}Defining Logics}{52}


118 
\contentsline {section}{\numberline {7.1}Priority grammars}{52}


119 
\contentsline {section}{\numberline {7.2}The Pure syntax}{53}


120 
\contentsline {subsection}{Logical types and default syntax}{55}


121 
\contentsline {subsection}{Lexical matters}{55}


122 
\contentsline {subsection}{*Inspecting the syntax}{56}


123 
\contentsline {section}{\numberline {7.3}Mixfix declarations}{58}


124 
\contentsline {subsection}{Grammar productions}{58}


125 
\contentsline {subsection}{The general mixfix form}{59}


126 
\contentsline {subsection}{Example: arithmetic expressions}{60}


127 
\contentsline {subsection}{The mixfix template}{61}


128 
\contentsline {subsection}{Infixes}{61}


129 
\contentsline {subsection}{Binders}{62}


130 
\contentsline {section}{\numberline {7.4}Example: some minimal logics}{62}


131 
\contentsline {chapter}{\numberline {8}Syntax Transformations}{66}


132 
\contentsline {section}{\numberline {8.1}Abstract syntax trees}{66}


133 
\contentsline {section}{\numberline {8.2}Transforming parse trees to {\psc ast}{}s}{67}


134 
\contentsline {section}{\numberline {8.3}Transforming {\psc ast}{}s to terms}{69}


135 
\contentsline {section}{\numberline {8.4}Printing of terms}{69}


136 
\contentsline {section}{\numberline {8.5}Macros: Syntactic rewriting}{71}


137 
\contentsline {subsection}{Specifying macros}{72}


138 
\contentsline {subsection}{Applying rules}{73}


139 
\contentsline {subsection}{Example: the syntax of finite sets}{75}


140 
\contentsline {subsection}{Example: a parse macro for dependent types}{76}


141 
\contentsline {section}{\numberline {8.6}Translation functions}{76}


142 
\contentsline {subsection}{Declaring translation functions}{77}


143 
\contentsline {subsection}{The translation strategy}{77}


144 
\contentsline {subsection}{Example: a print translation for dependent types}{78}


145 
\contentsline {chapter}{\numberline {9}Substitution Tactics}{80}


146 
\contentsline {section}{\numberline {9.1}Substitution rules}{80}


147 
\contentsline {section}{\numberline {9.2}Substitution in the hypotheses}{81}


148 
\contentsline {section}{\numberline {9.3}Setting up {\ptt hyp_subst_tac}}{82}


149 
\contentsline {chapter}{\numberline {10}Simplification}{84}


150 
\contentsline {section}{\numberline {10.1}Simplification sets}{84}


151 
\contentsline {subsection}{Rewrite rules}{84}


152 
\contentsline {subsection}{*Congruence rules}{85}


153 
\contentsline {subsection}{*The subgoaler}{85}


154 
\contentsline {subsection}{*The solver}{86}


155 
\contentsline {subsection}{*The looper}{86}


156 
\contentsline {section}{\numberline {10.2}The simplification tactics}{87}


157 
\contentsline {section}{\numberline {10.3}Examples using the simplifier}{88}


158 
\contentsline {subsection}{A trivial example}{88}


159 
\contentsline {subsection}{An example of tracing}{89}


160 
\contentsline {subsection}{Free variables and simplification}{90}


161 
\contentsline {section}{\numberline {10.4}Permutative rewrite rules}{90}


162 
\contentsline {subsection}{Example: sums of integers}{91}


163 
\contentsline {subsection}{Reorienting equalities}{93}


164 
\contentsline {section}{\numberline {10.5}*Setting up the simplifier}{93}


165 
\contentsline {subsection}{A collection of standard rewrite rules}{94}


166 
\contentsline {subsection}{Functions for preprocessing the rewrite rules}{94}


167 
\contentsline {subsection}{Making the initial simpset}{96}


168 
\contentsline {subsection}{Case splitting}{97}


169 
\contentsline {chapter}{\numberline {11}The Classical Reasoner}{98}


170 
\contentsline {section}{\numberline {11.1}The sequent calculus}{98}


171 
\contentsline {section}{\numberline {11.2}Simulating sequents by natural deduction}{99}


172 
\contentsline {section}{\numberline {11.3}Extra rules for the sequent calculus}{100}


173 
\contentsline {section}{\numberline {11.4}Classical rule sets}{101}


174 
\contentsline {section}{\numberline {11.5}The classical tactics}{103}


175 
\contentsline {subsection}{The automatic tactics}{103}


176 
\contentsline {subsection}{Singlestep tactics}{103}


177 
\contentsline {subsection}{Other useful tactics}{104}


178 
\contentsline {subsection}{Creating swapped rules}{104}


179 
\contentsline {section}{\numberline {11.6}Setting up the classical reasoner}{104}


180 
\contentsline {chapter}{\numberline {A}Syntax of Isabelle Theories}{107}
