doc-src/Ref/ref.toc
author paulson
Wed, 07 Oct 1998 10:31:30 +0200
changeset 5619 76a8c72e3fd4
parent 359 b5a2e9503a7a
permissions -rw-r--r--
new theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
359
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
     1
\contentsline {chapter}{\numberline {1}Basic Use of Isabelle}{1}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
\contentsline {section}{\numberline {1.1}Basic interaction with Isabelle}{1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\contentsline {section}{\numberline {1.2}Ending a session}{2}
359
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
     4
\contentsline {section}{\numberline {1.3}Reading ML files}{2}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
     5
\contentsline {section}{\numberline {1.4}Printing of terms and theorems}{2}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
     6
\contentsline {subsection}{Printing limits}{2}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
     7
\contentsline {subsection}{Printing of hypotheses, types and sorts}{3}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
     8
\contentsline {subsection}{$\eta $-contraction before printing}{3}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
     9
\contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{3}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    10
\contentsline {section}{\numberline {1.6}Shell scripts}{4}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    11
\contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{5}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    12
\contentsline {section}{\numberline {2.1}Basic commands}{5}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    13
\contentsline {subsection}{Starting a backward proof}{5}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    14
\contentsline {subsection}{Applying a tactic}{6}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    15
\contentsline {subsection}{Extracting the proved theorem}{7}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    16
\contentsline {subsection}{Undoing and backtracking}{7}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    17
\contentsline {subsection}{Printing the proof state}{8}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    18
\contentsline {subsection}{Timing}{8}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    19
\contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{8}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    20
\contentsline {subsection}{Refining a given subgoal}{8}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    21
\contentsline {subsection}{Scanning shortcuts}{9}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    22
\contentsline {subsection}{Other shortcuts}{9}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    23
\contentsline {section}{\numberline {2.3}Executing batch proofs}{9}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    24
\contentsline {section}{\numberline {2.4}Managing multiple proofs}{10}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    25
\contentsline {subsection}{The stack of proof states}{11}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    26
\contentsline {subsection}{Saving and restoring proof states}{11}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    27
\contentsline {section}{\numberline {2.5}Debugging and inspecting}{11}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    28
\contentsline {subsection}{Reading and printing terms}{11}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    29
\contentsline {subsection}{Inspecting the proof state}{12}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    30
\contentsline {subsection}{Filtering lists of rules}{12}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    31
\contentsline {chapter}{\numberline {3}Tactics}{13}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    32
\contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{13}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    33
\contentsline {subsection}{Resolution tactics}{13}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    34
\contentsline {subsection}{Assumption tactics}{14}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    35
\contentsline {subsection}{Matching tactics}{14}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    36
\contentsline {subsection}{Resolution with instantiation}{14}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    37
\contentsline {section}{\numberline {3.2}Other basic tactics}{15}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    38
\contentsline {subsection}{Definitions and meta-level rewriting}{15}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    39
\contentsline {subsection}{Tactic shortcuts}{16}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    40
\contentsline {subsection}{Inserting premises and facts}{16}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    41
\contentsline {subsection}{Theorems useful with tactics}{17}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    42
\contentsline {section}{\numberline {3.3}Obscure tactics}{17}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    43
\contentsline {subsection}{Tidying the proof state}{17}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    44
\contentsline {subsection}{Renaming parameters in a goal}{17}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    45
\contentsline {subsection}{Composition: resolution without lifting}{18}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    46
\contentsline {section}{\numberline {3.4}Managing lots of rules}{18}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    47
\contentsline {subsection}{Combined resolution and elim-resolution}{19}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    48
\contentsline {subsection}{Discrimination nets for fast resolution}{19}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    49
\contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{20}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    50
\contentsline {subsection}{Operations on type {\ptt tactic}}{21}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    51
\contentsline {subsection}{Tracing}{21}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    52
\contentsline {section}{\numberline {3.6}Sequences}{22}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    53
\contentsline {subsection}{Basic operations on sequences}{22}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    54
\contentsline {subsection}{Converting between sequences and lists}{22}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    55
\contentsline {subsection}{Combining sequences}{22}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    56
\contentsline {chapter}{\numberline {4}Tacticals}{24}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    57
\contentsline {section}{\numberline {4.1}The basic tacticals}{24}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    58
\contentsline {subsection}{Joining two tactics}{24}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    59
\contentsline {subsection}{Joining a list of tactics}{24}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    60
\contentsline {subsection}{Repetition tacticals}{25}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    61
\contentsline {subsection}{Identities for tacticals}{25}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    62
\contentsline {section}{\numberline {4.2}Control and search tacticals}{26}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    63
\contentsline {subsection}{Filtering a tactic's results}{26}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    64
\contentsline {subsection}{Depth-first search}{26}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    65
\contentsline {subsection}{Other search strategies}{27}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    66
\contentsline {subsection}{Auxiliary tacticals for searching}{27}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    67
\contentsline {subsection}{Predicates and functions useful for searching}{28}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    68
\contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{28}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    69
\contentsline {subsection}{Restricting a tactic to one subgoal}{28}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    70
\contentsline {subsection}{Scanning for a subgoal by number}{29}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    71
\contentsline {subsection}{Joining tactic functions}{30}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    72
\contentsline {subsection}{Applying a list of tactics to 1}{31}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    73
\contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{32}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    74
\contentsline {section}{\numberline {5.1}Basic operations on theorems}{32}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    75
\contentsline {subsection}{Pretty-printing a theorem}{32}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    76
\contentsline {subsection}{Forward proof: joining rules by resolution}{33}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    77
\contentsline {subsection}{Expanding definitions in theorems}{33}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    78
\contentsline {subsection}{Instantiating a theorem}{34}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    79
\contentsline {subsection}{Miscellaneous forward rules}{34}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    80
\contentsline {subsection}{Taking a theorem apart}{35}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    81
\contentsline {subsection}{Tracing flags for unification}{35}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    82
\contentsline {section}{\numberline {5.2}Primitive meta-level inference rules}{36}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    83
\contentsline {subsection}{Assumption rule}{37}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    84
\contentsline {subsection}{Implication rules}{37}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    85
\contentsline {subsection}{Logical equivalence rules}{38}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    86
\contentsline {subsection}{Equality rules}{38}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    87
\contentsline {subsection}{The $\lambda $-conversion rules}{38}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    88
\contentsline {subsection}{Forall introduction rules}{39}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    89
\contentsline {subsection}{Forall elimination rules}{39}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    90
\contentsline {subsection}{Instantiation of unknowns}{39}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    91
\contentsline {subsection}{Freezing/thawing type unknowns}{40}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    92
\contentsline {section}{\numberline {5.3}Derived rules for goal-directed proof}{40}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    93
\contentsline {subsection}{Proof by assumption}{40}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    94
\contentsline {subsection}{Resolution}{40}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    95
\contentsline {subsection}{Composition: resolution without lifting}{40}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    96
\contentsline {subsection}{Other meta-rules}{41}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    97
\contentsline {chapter}{\numberline {6}Theories, Terms and Types}{42}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    98
\contentsline {section}{\numberline {6.1}Defining theories}{42}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
    99
\contentsline {subsection}{*Classes and arities}{44}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   100
\contentsline {section}{\numberline {6.2}Loading a new theory}{44}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   101
\contentsline {section}{\numberline {6.3}Reloading modified theories}{45}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   102
\contentsline {subsection}{Important note for Poly/ML users}{45}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   103
\contentsline {subsection}{*Pseudo theories}{46}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   104
\contentsline {section}{\numberline {6.4}Basic operations on theories}{47}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   105
\contentsline {subsection}{Extracting an axiom from a theory}{47}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   106
\contentsline {subsection}{Building a theory}{47}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   107
\contentsline {subsection}{Inspecting a theory}{47}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   108
\contentsline {section}{\numberline {6.5}Terms}{48}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   109
\contentsline {section}{\numberline {6.6}Variable binding}{49}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   110
\contentsline {section}{\numberline {6.7}Certified terms}{50}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   111
\contentsline {subsection}{Printing terms}{50}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   112
\contentsline {subsection}{Making and inspecting certified terms}{50}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   113
\contentsline {section}{\numberline {6.8}Types}{50}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   114
\contentsline {section}{\numberline {6.9}Certified types}{51}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   115
\contentsline {subsection}{Printing types}{51}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   116
\contentsline {subsection}{Making and inspecting certified types}{51}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   117
\contentsline {chapter}{\numberline {7}Defining Logics}{52}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   118
\contentsline {section}{\numberline {7.1}Priority grammars}{52}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   119
\contentsline {section}{\numberline {7.2}The Pure syntax}{53}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   120
\contentsline {subsection}{Logical types and default syntax}{55}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   121
\contentsline {subsection}{Lexical matters}{55}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   122
\contentsline {subsection}{*Inspecting the syntax}{56}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   123
\contentsline {section}{\numberline {7.3}Mixfix declarations}{58}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   124
\contentsline {subsection}{Grammar productions}{58}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   125
\contentsline {subsection}{The general mixfix form}{59}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   126
\contentsline {subsection}{Example: arithmetic expressions}{60}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   127
\contentsline {subsection}{The mixfix template}{61}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   128
\contentsline {subsection}{Infixes}{61}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   129
\contentsline {subsection}{Binders}{62}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   130
\contentsline {section}{\numberline {7.4}Example: some minimal logics}{62}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   131
\contentsline {chapter}{\numberline {8}Syntax Transformations}{66}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   132
\contentsline {section}{\numberline {8.1}Abstract syntax trees}{66}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   133
\contentsline {section}{\numberline {8.2}Transforming parse trees to {\psc ast}{}s}{67}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   134
\contentsline {section}{\numberline {8.3}Transforming {\psc ast}{}s to terms}{69}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   135
\contentsline {section}{\numberline {8.4}Printing of terms}{69}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   136
\contentsline {section}{\numberline {8.5}Macros: Syntactic rewriting}{71}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   137
\contentsline {subsection}{Specifying macros}{72}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   138
\contentsline {subsection}{Applying rules}{73}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   139
\contentsline {subsection}{Example: the syntax of finite sets}{75}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   140
\contentsline {subsection}{Example: a parse macro for dependent types}{76}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   141
\contentsline {section}{\numberline {8.6}Translation functions}{76}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   142
\contentsline {subsection}{Declaring translation functions}{77}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   143
\contentsline {subsection}{The translation strategy}{77}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   144
\contentsline {subsection}{Example: a print translation for dependent types}{78}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   145
\contentsline {chapter}{\numberline {9}Substitution Tactics}{80}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   146
\contentsline {section}{\numberline {9.1}Substitution rules}{80}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   147
\contentsline {section}{\numberline {9.2}Substitution in the hypotheses}{81}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   148
\contentsline {section}{\numberline {9.3}Setting up {\ptt hyp_subst_tac}}{82}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   149
\contentsline {chapter}{\numberline {10}Simplification}{84}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   150
\contentsline {section}{\numberline {10.1}Simplification sets}{84}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   151
\contentsline {subsection}{Rewrite rules}{84}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   152
\contentsline {subsection}{*Congruence rules}{85}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   153
\contentsline {subsection}{*The subgoaler}{85}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   154
\contentsline {subsection}{*The solver}{86}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   155
\contentsline {subsection}{*The looper}{86}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   156
\contentsline {section}{\numberline {10.2}The simplification tactics}{87}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   157
\contentsline {section}{\numberline {10.3}Examples using the simplifier}{88}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   158
\contentsline {subsection}{A trivial example}{88}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   159
\contentsline {subsection}{An example of tracing}{89}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   160
\contentsline {subsection}{Free variables and simplification}{90}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   161
\contentsline {section}{\numberline {10.4}Permutative rewrite rules}{90}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   162
\contentsline {subsection}{Example: sums of integers}{91}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   163
\contentsline {subsection}{Re-orienting equalities}{93}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   164
\contentsline {section}{\numberline {10.5}*Setting up the simplifier}{93}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   165
\contentsline {subsection}{A collection of standard rewrite rules}{94}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   166
\contentsline {subsection}{Functions for preprocessing the rewrite rules}{94}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   167
\contentsline {subsection}{Making the initial simpset}{96}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   168
\contentsline {subsection}{Case splitting}{97}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   169
\contentsline {chapter}{\numberline {11}The Classical Reasoner}{98}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   170
\contentsline {section}{\numberline {11.1}The sequent calculus}{98}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   171
\contentsline {section}{\numberline {11.2}Simulating sequents by natural deduction}{99}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   172
\contentsline {section}{\numberline {11.3}Extra rules for the sequent calculus}{100}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   173
\contentsline {section}{\numberline {11.4}Classical rule sets}{101}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   174
\contentsline {section}{\numberline {11.5}The classical tactics}{103}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   175
\contentsline {subsection}{The automatic tactics}{103}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   176
\contentsline {subsection}{Single-step tactics}{103}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   177
\contentsline {subsection}{Other useful tactics}{104}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   178
\contentsline {subsection}{Creating swapped rules}{104}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   179
\contentsline {section}{\numberline {11.6}Setting up the classical reasoner}{104}
b5a2e9503a7a final Springer version
lcp
parents: 152
diff changeset
   180
\contentsline {chapter}{\numberline {A}Syntax of Isabelle Theories}{107}