doc-src/Ref/ref.toc
author clasohm
Thu, 25 Nov 1993 14:32:54 +0100
changeset 150 919a03a587eb
parent 141 a133921366cb
child 152 37025f8608a6
permissions -rw-r--r--
changed beginning of "Reading a new theory", added index "automatic loading"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
\contentsline {chapter}{\numberline {1}Introduction}{1}
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}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
\contentsline {section}{\numberline {1.3}Reading files of proofs and theories}{2}
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
     5
\contentsline {section}{\numberline {1.4}Printing of terms and theorems}{3}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
\contentsline {subsection}{Printing limits}{3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
\contentsline {subsection}{Printing of meta-level hypotheses}{3}
141
a133921366cb added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents: 138
diff changeset
     8
\contentsline {subsection}{Printing of types and sorts}{3}
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
     9
\contentsline {subsection}{$\eta $-contraction before printing}{4}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
\contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{4}
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
    11
\contentsline {section}{\numberline {1.6}Shell scripts}{5}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
\contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{6}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
\contentsline {section}{\numberline {2.1}Basic commands}{6}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
\contentsline {subsection}{Starting a backward proof}{6}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
\contentsline {subsection}{Applying a tactic}{7}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
\contentsline {subsection}{Extracting the proved theorem}{8}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
\contentsline {subsection}{Undoing and backtracking}{8}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
\contentsline {subsection}{Printing the proof state}{9}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
\contentsline {subsection}{Timing}{9}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
\contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{9}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
\contentsline {subsection}{Refining a given subgoal}{9}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
\contentsline {subsubsection}{Resolution with a list of theorems}{9}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
\contentsline {subsection}{Scanning shortcuts}{10}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
\contentsline {subsubsection}{Proof by assumption and resolution}{10}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
\contentsline {subsubsection}{Resolution with a list of theorems}{10}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
\contentsline {subsection}{Other shortcuts}{10}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
\contentsline {section}{\numberline {2.3}Advanced features}{11}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
\contentsline {subsection}{Executing batch proofs}{11}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
\contentsline {subsection}{Managing multiple proofs}{11}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
\contentsline {subsubsection}{The stack of proof states}{12}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
\contentsline {subsubsection}{Saving and restoring proof states}{12}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
\contentsline {subsection}{Debugging and inspecting}{12}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
\contentsline {subsubsection}{Reading and printing terms}{13}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
\contentsline {subsubsection}{Inspecting the proof state}{13}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
\contentsline {subsubsection}{Filtering lists of rules}{13}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
\contentsline {chapter}{\numberline {3}Tactics}{14}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
\contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{14}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
\contentsline {subsection}{Resolution tactics}{14}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
\contentsline {subsection}{Assumption tactics}{15}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
\contentsline {subsection}{Matching tactics}{15}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
\contentsline {subsection}{Resolution with instantiation}{15}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
\contentsline {section}{\numberline {3.2}Other basic tactics}{16}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
\contentsline {subsection}{Definitions and meta-level rewriting}{16}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
\contentsline {subsection}{Tactic shortcuts}{17}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
\contentsline {subsection}{Inserting premises and facts}{17}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
\contentsline {subsection}{Theorems useful with tactics}{18}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
\contentsline {section}{\numberline {3.3}Obscure tactics}{18}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
\contentsline {subsection}{Tidying the proof state}{18}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
\contentsline {subsection}{Renaming parameters in a goal}{18}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
\contentsline {subsection}{Composition: resolution without lifting}{19}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
\contentsline {section}{\numberline {3.4}Managing lots of rules}{19}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
\contentsline {subsection}{Combined resolution and elim-resolution}{20}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
\contentsline {subsection}{Discrimination nets for fast resolution}{20}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
\contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{21}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
\contentsline {subsection}{Operations on type {\ptt tactic}}{22}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
\contentsline {subsection}{Tracing}{22}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
\contentsline {subsection}{Sequences}{23}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
\contentsline {subsubsection}{Basic operations on sequences}{23}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
\contentsline {subsubsection}{Converting between sequences and lists}{23}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
\contentsline {subsubsection}{Combining sequences}{23}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
\contentsline {chapter}{\numberline {4}Tacticals}{25}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
\contentsline {section}{\numberline {4.1}The basic tacticals}{25}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
\contentsline {subsection}{Joining two tactics}{25}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
\contentsline {subsection}{Joining a list of tactics}{25}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
\contentsline {subsection}{Repetition tacticals}{26}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
\contentsline {subsection}{Identities for tacticals}{26}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
\contentsline {section}{\numberline {4.2}Control and search tacticals}{27}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
\contentsline {subsection}{Filtering a tactic's results}{27}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
\contentsline {subsection}{Depth-first search}{28}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
\contentsline {subsection}{Other search strategies}{28}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
\contentsline {subsection}{Auxiliary tacticals for searching}{29}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
\contentsline {subsection}{Predicates and functions useful for searching}{29}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
\contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{29}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
\contentsline {subsection}{Restricting a tactic to one subgoal}{30}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
\contentsline {subsection}{Scanning for a subgoal by number}{31}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
\contentsline {subsection}{Joining tactic functions}{32}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
\contentsline {subsection}{Applying a list of tactics to 1}{32}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
\contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{33}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
\contentsline {section}{\numberline {5.1}Basic operations on theorems}{33}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
\contentsline {subsection}{Pretty-printing a theorem}{33}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
\contentsline {subsubsection}{Top-level commands}{33}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
\contentsline {subsubsection}{Operations for programming}{34}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
\contentsline {subsection}{Forwards proof: joining rules by resolution}{34}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
\contentsline {subsection}{Expanding definitions in theorems}{35}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
\contentsline {subsection}{Instantiating a theorem}{35}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
\contentsline {subsection}{Miscellaneous forward rules}{35}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
\contentsline {subsection}{Taking a theorem apart}{36}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
\contentsline {subsection}{Tracing flags for unification}{36}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
\contentsline {section}{\numberline {5.2}Primitive meta-level inference rules}{37}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
\contentsline {subsection}{Propositional rules}{38}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
\contentsline {subsubsection}{Assumption}{38}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
\contentsline {subsubsection}{Implication}{38}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
\contentsline {subsubsection}{Logical equivalence (equality)}{39}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
\contentsline {subsection}{Equality rules}{39}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
\contentsline {subsection}{The $\lambda $-conversion rules}{39}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
\contentsline {subsection}{Universal quantifier rules}{40}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
\contentsline {subsubsection}{Forall introduction}{40}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
\contentsline {subsubsection}{Forall elimination}{40}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
\contentsline {subsubsection}{Instantiation of unknowns}{41}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
\contentsline {subsection}{Freezing/thawing type variables}{41}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
\contentsline {section}{\numberline {5.3}Derived rules for goal-directed proof}{41}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
\contentsline {subsection}{Proof by assumption}{41}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
\contentsline {subsection}{Resolution}{41}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
\contentsline {subsection}{Composition: resolution without lifting}{42}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
\contentsline {subsection}{Other meta-rules}{42}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\contentsline {chapter}{\numberline {6}Theories, Terms and Types}{44}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
\contentsline {section}{\numberline {6.1}Defining Theories}{44}
150
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   108
\contentsline {subsection}{Classes and types}{47}
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   109
\contentsline {section}{\numberline {6.2}Loading Theories}{47}
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   110
\contentsline {subsection}{Reading a new theory}{47}
150
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   111
\contentsline {subsection}{Filenames and paths}{48}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   112
\contentsline {subsection}{Reloading a theory}{48}
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   113
\contentsline {subsection}{Pseudo theories}{48}
150
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   114
\contentsline {subsection}{Removing a theory}{49}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   115
\contentsline {subsection}{Using Poly/{\psc ml}}{49}
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   116
\contentsline {section}{\numberline {6.3}Basic operations on theories}{49}
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   117
\contentsline {subsection}{Extracting an axiom from a theory}{49}
150
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   118
\contentsline {subsection}{Building a theory}{50}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   119
\contentsline {subsection}{Inspecting a theory}{51}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   120
\contentsline {section}{\numberline {6.4}Terms}{52}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   121
\contentsline {section}{\numberline {6.5}Certified terms}{53}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   122
\contentsline {subsection}{Printing terms}{53}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   123
\contentsline {subsection}{Making and inspecting certified terms}{53}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   124
\contentsline {section}{\numberline {6.6}Types}{54}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   125
\contentsline {section}{\numberline {6.7}Certified types}{54}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   126
\contentsline {subsection}{Printing types}{54}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   127
\contentsline {subsection}{Making and inspecting certified types}{54}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   128
\contentsline {chapter}{\numberline {7}Substitution Tactics}{56}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   129
\contentsline {section}{\numberline {7.1}Simple substitution}{56}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   130
\contentsline {section}{\numberline {7.2}Substitution in the hypotheses}{57}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   131
\contentsline {section}{\numberline {7.3}Setting up {\ptt hyp_subst_tac}}{57}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   132
\contentsline {chapter}{\numberline {8}Simplification}{60}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   133
\contentsline {section}{\numberline {8.1}Simplification sets}{60}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   134
\contentsline {subsection}{Rewrite rules}{60}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   135
\contentsline {subsection}{Congruence rules}{61}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   136
\contentsline {subsection}{The subgoaler}{61}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   137
\contentsline {subsection}{The solver}{62}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   138
\contentsline {subsection}{The looper}{62}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   139
\contentsline {section}{\numberline {8.2}The simplification tactics}{63}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   140
\contentsline {section}{\numberline {8.3}Example: using the simplifier}{64}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   141
\contentsline {chapter}{\numberline {9}The classical theorem prover}{67}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   142
\contentsline {section}{\numberline {9.1}The sequent calculus}{67}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   143
\contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{68}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   144
\contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{69}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   145
\contentsline {section}{\numberline {9.4}Classical rule sets}{70}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   146
\contentsline {section}{\numberline {9.5}The classical tactics}{71}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   147
\contentsline {subsection}{Single-step tactics}{72}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   148
\contentsline {subsection}{The automatic tactics}{72}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   149
\contentsline {subsection}{Other useful tactics}{72}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   150
\contentsline {subsection}{Creating swapped rules}{73}
919a03a587eb changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents: 141
diff changeset
   151
\contentsline {section}{\numberline {9.6}Setting up the classical prover}{73}